Commit f7af5b3f authored by Robbert Krebbers's avatar Robbert Krebbers

Remove non-fork versions of pure lifting lemmas.

parent ebf06f91
......@@ -162,17 +162,17 @@ Implicit Types σ : state.
Lemma wp_fork s E e Φ :
WP e @ s; {{ _, True }} - Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
Proof.
iIntros "He HΦ".
iApply wp_lift_pure_det_head_step; [done|auto|intros; inv_head_step; eauto|].
iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed.
Lemma twp_fork s E e Φ :
WP e @ s; [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
Proof.
iIntros "He HΦ".
iApply twp_lift_pure_det_head_step; [done|auto|intros; inv_head_step; eauto|].
iIntros "!> /= {$He}". by iApply twp_value.
iIntros "He HΦ". iApply twp_lift_atomic_head_step; [done|].
iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto.
iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed.
(** Heap *)
......
......@@ -54,20 +54,6 @@ Proof.
iIntros (σ κs n) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
Qed.
Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
state_interp_fork_indep
( σ1, head_reducible e1 σ1)
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2)
(|={E,E'}=> κ e2 efs σ, head_step e1 σ κ e2 σ efs
WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
iIntros (???) "H". iApply wp_lift_pure_step; [done| |by eauto|].
{ by destruct s; auto. }
iApply (step_fupd_wand with "H"); iIntros "H".
iIntros (?????). iApply "H"; eauto.
Qed.
Lemma wp_lift_pure_head_stuck E Φ e :
to_val e = None
sub_redexes_are_values e
......@@ -140,18 +126,6 @@ Proof.
iMod ("H" $! v2 σ2 efs with "[//]") as "(-> & ? & ?) /=". by iFrame.
Qed.
Lemma wp_lift_pure_det_head_step {s E E' Φ} e1 e2 efs :
state_interp_fork_indep
( σ1, head_reducible e1 σ1)
( σ1 κ e2' σ2 efs',
head_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' efs = efs')
(|={E,E'}=> WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
intros. rewrite -(wp_lift_pure_det_step e1 e2 efs); eauto.
destruct s; by auto.
Qed.
Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
to_val e1 = None
( σ1, head_reducible e1 σ1)
......
......@@ -53,26 +53,6 @@ Proof.
iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !> !>". by iApply "H".
Qed.
Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
state_interp_fork_indep
( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2)
(|={E,E'}=> κ e2 efs σ, prim_step e1 σ κ e2 σ efs
WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (Hfork Hsafe Hstep) "H". iApply wp_lift_step.
{ specialize (Hsafe inhabitant). destruct s; last done.
by eapply reducible_not_val. }
iIntros (σ1 κ κs n) "Hσ". iMod "H".
iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
{ iPureIntro. destruct s; done. }
iNext. iIntros (e2 σ2 efs Hstep').
destruct (Hstep κ σ1 e2 σ2 efs); auto; subst; clear Hstep.
iMod "Hclose" as "_". iMod "H". iModIntro.
rewrite (Hfork _ _ _ n). iFrame "Hσ". iApply "H"; auto.
Qed.
Lemma wp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E E' Φ e1 :
( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2 efs = [])
......@@ -140,20 +120,6 @@ Proof.
by iApply "H".
Qed.
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
state_interp_fork_indep
( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'
κ = [] σ1 = σ2 e2 = e2' efs = efs')
(|={E,E'}=> WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?? Hpuredet) "H". iApply (wp_lift_pure_step s E E'); try done.
{ by naive_solver. }
iApply (step_fupd_wand with "H"); iIntros "H".
by iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
Qed.
Lemma wp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E E' Φ} e1 e2 :
( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'
......
......@@ -189,22 +189,12 @@ Section lifting.
iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2". iApply "Hs'". iFrame.
Qed.
Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' efs = efs')
(WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
naive_solver. by iNext; iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
Qed.
Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' [] = efs')
( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' efs' = [])
WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) // ?big_sepL_nil ?right_id; eauto.
intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2) //; eauto.
Qed.
End lifting.
......@@ -289,22 +279,12 @@ Section ectx_lifting.
by destruct s; eauto using reducible_not_val.
Qed.
Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
( σ1, head_reducible e1 σ1)
( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' efs = efs')
(WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
iIntros (??) "H"; iApply wp_lift_pure_det_step; try by eauto.
by destruct s; eauto using reducible_not_val.
Qed.
Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
( σ1, head_reducible e1 σ1)
( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' [] = efs')
( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' efs' = [])
WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
iIntros (??) "H"; iApply wp_lift_pure_det_step_no_fork; try by eauto.
by destruct s; eauto using reducible_not_val.
Qed.
End ectx_lifting.
......@@ -31,18 +31,6 @@ Proof.
iApply "H". by eauto.
Qed.
Lemma twp_lift_pure_head_step {s E Φ} e1 :
state_interp_fork_indep
( σ1, head_reducible_no_obs e1 σ1)
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2)
(|={E}=> κ e2 efs σ, head_step e1 σ κ e2 σ efs
WP e2 @ s; E [{ Φ }] [ list] ef efs, WP ef @ s; [{ _, fork_post }])
WP e1 @ s; E [{ Φ }].
Proof using Hinh.
iIntros (???) ">H". iApply twp_lift_pure_step; eauto.
iIntros "!>" (?????). iApply "H"; eauto.
Qed.
Lemma twp_lift_pure_head_step_no_fork {s E Φ} e1 :
( σ1, head_reducible_no_obs e1 σ1)
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2 efs = [])
......@@ -83,15 +71,6 @@ Proof.
iMod ("H" with "[# //]") as "(-> & -> & ? & $) /=". by iFrame.
Qed.
Lemma twp_lift_pure_det_head_step {s E Φ} e1 e2 efs :
state_interp_fork_indep
( σ1, head_reducible_no_obs e1 σ1)
( σ1 κ e2' σ2 efs',
head_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' efs = efs')
(|={E}=> WP e2 @ s; E [{ Φ }] [ list] ef efs, WP ef @ s; [{ _, fork_post }])
WP e1 @ s; E [{ Φ }].
Proof using Hinh. eauto 20 using twp_lift_pure_det_step. Qed.
Lemma twp_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
to_val e1 = None
( σ1, head_reducible_no_obs e1 σ1)
......
......@@ -25,26 +25,7 @@ Lemma twp_lift_step s E Φ e1 :
WP e1 @ s; E [{ Φ }].
Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
(** Derived lifting lemmas. *)
Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
state_interp_fork_indep
( σ1, reducible_no_obs e1 σ1)
( σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2)
(|={E}=> κ e2 efs σ, prim_step e1 σ κ e2 σ efs
WP e2 @ s; E [{ Φ }] [ list] ef efs, WP ef @ s; [{ _, fork_post }])
WP e1 @ s; E [{ Φ }].
Proof.
iIntros (Hfork Hsafe Hstep) "H". iApply twp_lift_step.
{ eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
iIntros (σ1 κs n) "Hσ". iMod "H".
iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
iSplit; [by destruct s|]. iIntros (κ e2 σ2 efs Hstep').
destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
iMod "Hclose" as "_". iModIntro. iSplit; first done. rewrite (Hfork _ _ _ n).
iFrame "Hσ". iApply "H"; auto.
Qed.
Lemma twp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E Φ e1 :
( σ1, reducible_no_obs e1 σ1)
( σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2 efs = [])
......@@ -84,19 +65,6 @@ Proof.
iApply twp_value; last done. by apply of_to_val.
Qed.
Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
state_interp_fork_indep
( σ1, reducible_no_obs e1 σ1)
( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'
κ = [] σ1 = σ2 e2 = e2' efs = efs')
(|={E}=> WP e2 @ s; E [{ Φ }] [ list] ef efs, WP ef @ s; [{ _, fork_post }])
WP e1 @ s; E [{ Φ }].
Proof.
iIntros (?? Hpuredet) ">H". iApply (twp_lift_pure_step _ E); try done.
{ by naive_solver. }
by iIntros "!>" (κ e' efs' σ (->&_&->&->)%Hpuredet).
Qed.
Lemma twp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
( σ1, reducible_no_obs e1 σ1)
( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'
......
......@@ -13,9 +13,6 @@ Class irisG' (Λstate Λobservation : Type) (Σ : gFunctors) := IrisG {
Notation irisG Λ Σ := (irisG' (state Λ) (observation Λ) Σ).
Global Opaque iris_invG.
Definition state_interp_fork_indep `{irisG Λ Σ} :=
σ κs n n', state_interp σ κs n = state_interp σ κs n'.
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
......
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