Commit a5c777d9 authored by Ralf Jung's avatar Ralf Jung

curry lifting lemmas

parent 46f8eed8
...@@ -52,7 +52,7 @@ Lemma wp_alloc_pst E σ v : ...@@ -52,7 +52,7 @@ Lemma wp_alloc_pst E σ v :
Proof. Proof.
iIntros (Φ) "HP HΦ". iIntros (Φ) "HP HΦ".
iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto. iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step. iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
iSplitL; last by iApply big_sepL_nil. iApply "HΦ". by iSplit. iSplitL; last by iApply big_sepL_nil. iApply "HΦ". by iSplit.
Qed. Qed.
......
...@@ -17,14 +17,14 @@ Proof. apply: weakestpre.wp_bind. Qed. ...@@ -17,14 +17,14 @@ Proof. apply: weakestpre.wp_bind. Qed.
Lemma wp_lift_head_step E Φ e1 : Lemma wp_lift_head_step E Φ e1 :
(|={E,}=> σ1, head_reducible e1 σ1 ownP σ1 (|={E,}=> σ1, head_reducible e1 σ1 ownP σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ownP σ2 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs - ownP σ2
={,E}= WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }}) ={,E}= WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof.
iIntros "H". iApply (wp_lift_step E); try done. iIntros "H". iApply (wp_lift_step E); try done.
iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1. iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "[% ?]". iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
iApply "Hwp". by eauto. iApply ("Hwp" with "* []"); by eauto.
Qed. Qed.
Lemma wp_lift_pure_head_step E Φ e1 : Lemma wp_lift_pure_head_step E Φ e1 :
...@@ -41,12 +41,12 @@ Qed. ...@@ -41,12 +41,12 @@ Qed.
Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 : Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
head_reducible e1 σ1 head_reducible e1 σ1
ownP σ1 ( e2 σ2 efs, ownP σ1 ( e2 σ2 efs,
head_step e1 σ1 e2 σ2 efs ownP σ2 - head_step e1 σ1 e2 σ2 efs - ownP σ2 -
default False (to_val e2) Φ [ list] ef efs, WP ef {{ _, True }}) default False (to_val e2) Φ [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof.
iIntros (?) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext. iIntros (?) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
iIntros (???) "[% ?]". iApply "H". eauto. iIntros (???) "% ?". iApply ("H" with "* []"); eauto.
Qed. Qed.
Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs : Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
......
...@@ -12,7 +12,7 @@ Implicit Types Φ : val Λ → iProp Σ. ...@@ -12,7 +12,7 @@ Implicit Types Φ : val Λ → iProp Σ.
Lemma wp_lift_step E Φ e1 : Lemma wp_lift_step E Φ e1 :
(|={E,}=> σ1, reducible e1 σ1 ownP σ1 (|={E,}=> σ1, reducible e1 σ1 ownP σ1
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ownP σ2 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2
={,E}= WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }}) ={,E}= WP e2 @ E {{ Φ }} [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof.
...@@ -25,7 +25,7 @@ Proof. ...@@ -25,7 +25,7 @@ Proof.
iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame. iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep). iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
iMod (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame. iMod (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
iApply "H"; eauto. iApply ("H" with "* []"); eauto.
Qed. Qed.
Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 : Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
...@@ -46,15 +46,15 @@ Qed. ...@@ -46,15 +46,15 @@ Qed.
(** Derived lifting lemmas. *) (** Derived lifting lemmas. *)
Lemma wp_lift_atomic_step {E Φ} e1 σ1 : Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
reducible e1 σ1 reducible e1 σ1
( ownP σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ownP σ2 - ( ownP σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2 -
default False (to_val e2) Φ [ list] ef efs, WP ef {{ _, True }}) default False (to_val e2) Φ [ list] ef efs, WP ef {{ _, True }})
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof.
iIntros (?) "[Hσ H]". iApply (wp_lift_step E _ e1). iIntros (?) "[Hσ H]". iApply (wp_lift_step E _ e1).
iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver. iModIntro. iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver. iModIntro.
iExists σ1. iFrame "Hσ"; iSplit; eauto. iExists σ1. iFrame "Hσ"; iSplit; eauto.
iNext; iIntros (e2 σ2 efs) "[% Hσ]". iNext; iIntros (e2 σ2 efs) "% Hσ".
iDestruct ("H" $! e2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto. iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
destruct (to_val e2) eqn:?; last by iExFalso. destruct (to_val e2) eqn:?; last by iExFalso.
iMod "Hclose". iApply wp_value; auto using to_of_val. done. iMod "Hclose". iApply wp_value; auto using to_of_val. done.
Qed. Qed.
...@@ -68,7 +68,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs : ...@@ -68,7 +68,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof.
iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done. iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
iFrame. iNext. iIntros (e2' σ2' efs') "[% Hσ2']". iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2". edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
Qed. Qed.
......
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