Commit 54c37314 authored by Dan Frumin's avatar Dan Frumin Committed by Robbert Krebbers

Get rid of the `pure.v` file

parent 1fb1b2c7
......@@ -55,7 +55,6 @@ theories/base_logic/lib/core.v
theories/base_logic/lib/fancy_updates_from_vs.v
theories/program_logic/adequacy.v
theories/program_logic/lifting.v
theories/program_logic/pure.v
theories/program_logic/weakestpre.v
theories/program_logic/hoare.v
theories/program_logic/language.v
......
From iris.base_logic Require Export gen_heap.
From iris.program_logic Require Export weakestpre pure.
From iris.program_logic Require Export weakestpre lifting.
From iris.program_logic Require Import ectx_lifting.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics.
......@@ -195,7 +195,7 @@ Qed.
Lemma wp_seq E e1 e2 Φ :
is_Some (to_val e1) Closed [] e2
WP e2 @ E {{ Φ }} WP Seq e1 e2 @ E {{ Φ }}.
Proof. iIntros ([? ?] ?). rewrite -wp_pure'; by eauto. Qed.
Proof. iIntros ([? ?] ?). rewrite -wp_pure_step_later; by eauto. Qed.
Lemma wp_skip E Φ : Φ (LitV LitUnit) WP Skip @ E {{ Φ }}.
Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
......@@ -203,11 +203,11 @@ Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
is_Some (to_val e0) Closed (x1 :b: []) e1
WP subst' x1 e0 e1 @ E {{ Φ }} WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure'; by eauto. Qed.
Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
is_Some (to_val e0) Closed (x2 :b: []) e2
WP subst' x2 e0 e2 @ E {{ Φ }} WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure'; by eauto. Qed.
Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
End lifting.
......@@ -47,7 +47,7 @@ Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
(Δ WP fill K e1 @ E {{ Φ }}).
Proof.
intros ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite -lifting.wp_bind HΔ' -wp_pure' //.
rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
by rewrite -ectx_lifting.wp_ectx_bind_inv.
Qed.
......
......@@ -150,6 +150,18 @@ Section ectx_language.
exists (fill K' e2''); rewrite -fill_comp; split; auto.
econstructor; eauto.
Qed.
Lemma det_head_step_pureexec e1 e2 :
( σ, head_reducible e1 σ)
( σ1 e2' σ2 efs, head_step e1 σ1 e2' σ2 efs σ1 = σ2 e2=e2' efs = [])
PureExec True e1 e2.
Proof.
intros Hp1 Hp2. split.
- intros σ _. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
eexists e2', σ2, efs.
eapply (Ectx_step _ _ _ _ _ empty_ectx); eauto using fill_empty.
- intros σ1 e2' σ2 efs _ ?%head_reducible_prim_step; eauto.
Qed.
End ectx_language.
Arguments ectx_lang _ {_ _ _ _}.
......@@ -93,4 +93,16 @@ Section language.
exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
by rewrite -!Permutation_middle !assoc_L Ht.
Qed.
Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
pure_exec_safe σ :
P reducible e1 σ;
pure_exec_puredet σ1 e2' σ2 efs :
P prim_step e1 σ1 e2' σ2 efs σ1 = σ2 e2 = e2' efs = [];
}.
Lemma hoist_pred_pureexec (P : Prop) (e1 e2 : expr Λ) :
(P PureExec True e1 e2)
PureExec P e1 e2.
Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
End language.
......@@ -68,4 +68,22 @@ Proof.
iApply (step_fupd_wand with "H"); iIntros "H".
by iIntros (e' efs' σ (_&->&->)%Hpuredet).
Qed.
Lemma wp_pure_step_fupd `{Inhabited (state Λ)} E E' e1 e2 φ Φ :
PureExec φ e1 e2
φ
(|={E,E'}=> WP e2 @ E {{ Φ }}) WP e1 @ E {{ Φ }}.
Proof.
iIntros ([??] Hφ) "HWP".
iApply (wp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|].
rewrite big_sepL_nil right_id //.
Qed.
Lemma wp_pure_step_later `{Inhabited (state Λ)} E e1 e2 φ Φ :
PureExec φ e1 e2
φ
WP e2 @ E {{ Φ }} WP e1 @ E {{ Φ }}.
Proof.
intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //.
Qed.
End lifting.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import lifting language ectx_language.
Set Default Proof Using "Type".
Section pure_language.
Context `{irisG Λ Σ}.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types φ : Prop.
Implicit Types e : expr Λ.
Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
pure_exec_safe :
P -> σ, language.reducible e1 σ;
pure_exec_puredet :
P -> σ1 e2' σ2 efs, language.prim_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs;
}.
Lemma wp_pure `{Inhabited (state Λ)} E E' e1 e2 φ Φ :
PureExec φ e1 e2
φ
(|={E,E'}=> WP e2 @ E {{ Φ }}) WP e1 @ E {{ Φ }}.
Proof.
iIntros (? Hφ) "HWP".
iApply (wp_lift_pure_det_step with "[HWP]").
{ apply (pure_exec_safe Hφ). }
{ apply (pure_exec_puredet Hφ). }
rewrite big_sepL_nil right_id //.
Qed.
Lemma wp_pure' `{Inhabited (state Λ)} E e1 e2 φ Φ :
PureExec φ e1 e2
φ
( WP e2 @ E {{ Φ }}) WP e1 @ E {{ Φ }}.
Proof.
intros ? ?.
rewrite -wp_pure //.
rewrite -step_fupd_intro //.
Qed.
Lemma hoist_pred_pureexec (P : Prop) (e1 e2 : expr Λ) :
(P PureExec True e1 e2)
PureExec P e1 e2.
Proof.
intros HPE.
split; intros HP; destruct (HPE HP); eauto.
Qed.
End pure_language.
Section pure_ectx_language.
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
Lemma det_head_step_pureexec (e1 e2 : expr) :
( σ, head_reducible e1 σ)
( σ1 e2' σ2 efs, head_step e1 σ1 e2' σ2 efs -> σ1=σ2 /\ e2=e2' /\ [] = efs)
PureExec True e1 e2.
Proof.
intros Hp1 Hp2.
split; intros _.
- intros σ. destruct (Hp1 σ) as (? & ? & ? & ?).
do 3 eexists. simpl.
eapply (Ectx_step _ _ _ _ _ empty_ectx); eauto using fill_empty.
- move => σ1 e2' σ2 efs /=.
intros ?%head_reducible_prim_step; eauto.
Qed.
End pure_ectx_language.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment