Commit 2a806d70 authored by Robbert Krebbers's avatar Robbert Krebbers

Consistently state equalities in pure lifting lemmas with "post-state" on the LHS.

parent ba89c977
......@@ -217,7 +217,7 @@ Section ectx_language.
Record pure_head_step (e1 e2 : expr Λ) := {
pure_head_step_safe σ1 : head_reducible_no_obs e1 σ1;
pure_head_step_det σ1 κ e2' σ2 efs :
head_step e1 σ1 κ e2' σ2 efs κ = [] σ1 = σ2 e2 = e2' efs = []
head_step e1 σ1 κ e2' σ2 efs κ = [] σ2 = σ1 e2' = e2 efs = []
}.
Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2 pure_step e1 e2.
......
......@@ -130,7 +130,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
to_val e1 = None
( σ1, head_reducible e1 σ1)
( σ1 κ e2' σ2 efs',
head_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' efs' = [])
head_step e1 σ1 κ e2' σ2 efs' κ = [] σ2 = σ1 e2' = e2 efs' = [])
(|={E,E'}=> WP e2 @ s; E {{ Φ }}) WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2); eauto.
......@@ -141,7 +141,7 @@ Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
to_val e1 = None
( σ1, head_reducible e1 σ1)
( σ1 κ e2' σ2 efs',
head_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' efs' = [])
head_step e1 σ1 κ e2' σ2 efs' κ = [] σ2 = σ1 e2' = e2 efs' = [])
WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
......
......@@ -177,7 +177,7 @@ Section language.
Record pure_step (e1 e2 : expr Λ) := {
pure_step_safe σ1 : reducible_no_obs e1 σ1;
pure_step_det σ1 κ e2' σ2 efs :
prim_step e1 σ1 κ e2' σ2 efs κ = [] σ1 = σ2 e2 = e2' efs = []
prim_step e1 σ1 κ e2' σ2 efs κ = [] σ2 = σ1 e2' = e2 efs = []
}.
(* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
......
......@@ -55,7 +55,7 @@ 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 = [])
( κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs κ = [] σ2 = σ1 efs = [])
(|={E,E'}=> κ e2 efs σ, prim_step e1 σ κ e2 σ efs WP e2 @ s; E {{ Φ }})
WP e1 @ s; E {{ Φ }}.
Proof.
......@@ -123,7 +123,7 @@ 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'
κ = [] σ1 = σ2 e2 = e2' efs' = [])
κ = [] σ2 = σ1 e2' = e2 efs' = [])
(|={E,E'}=> WP e2 @ s; E {{ Φ }}) WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step_no_fork s E E'); try done.
......
......@@ -132,7 +132,7 @@ Section lifting.
Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s 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)
( σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs κ = [] σ2 = σ1)
( κ e2 efs σ, prim_step e1 σ κ e2 σ efs
WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
......@@ -167,21 +167,21 @@ Section lifting.
Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :
(if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs'
σ2 = σ2' to_val e2' = Some v2 efs = efs')
σ2' = σ2 to_val e2' = Some v2 efs' = efs)
(ownP σ1) (ownP σ2 -
Φ v2 [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (? Hdet) "[Hσ1 Hσ2]"; iApply ownP_lift_atomic_step; try done.
iFrame; iNext; iIntros (κ' e2' σ2' efs' ?) "Hσ2'".
edestruct (Hdet κ') as (->&Hval&->); first done. rewrite Hval.
edestruct (Hdet κ') as (<-&Hval&<-); first done. rewrite Hval.
iApply ("Hσ2" with "Hσ2'").
Qed.
Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
(if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs'
σ2 = σ2' to_val e2' = Some v2 [] = efs')
σ2' = σ2 to_val e2' = Some v2 efs' = [])
{{{ (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
Proof.
intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
......@@ -191,7 +191,7 @@ Section lifting.
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' κ = [] σ2 = σ1 e2' = e2 efs' = [])
WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2) //; eauto.
......@@ -233,7 +233,7 @@ Section ectx_lifting.
Lemma ownP_lift_pure_head_step s E Φ e1 :
( σ1, head_reducible e1 σ1)
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2)
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = [] σ2 = σ1)
( κ e2 efs σ, head_step e1 σ κ e2 σ efs
WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
......@@ -259,7 +259,7 @@ Section ectx_lifting.
Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 v2 σ2 efs :
head_reducible e1 σ1
( κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs'
σ2 = σ2' to_val e2' = Some v2 efs = efs')
σ2' = σ2 to_val e2' = Some v2 efs' = efs)
(ownP σ1) (ownP σ2 -
Φ v2 [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
......@@ -272,7 +272,7 @@ Section ectx_lifting.
Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 κ v2 σ2 :
head_reducible e1 σ1
( κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs'
κ = κ' σ2 = σ2' to_val e2' = Some v2 [] = efs')
κ' = κ σ2' = σ2 to_val e2' = Some v2 efs' = [])
{{{ (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
Proof.
intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
......@@ -281,7 +281,7 @@ Section ectx_lifting.
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' κ = [] σ2 = σ1 e2' = e2 efs' = [])
WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
iIntros (??) "H"; iApply wp_lift_pure_det_step_no_fork; try by eauto.
......
......@@ -33,7 +33,7 @@ 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 = [])
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = [] σ2 = σ1 efs = [])
(|={E}=> κ e2 efs σ, head_step e1 σ κ e2 σ efs WP e2 @ s; E [{ Φ }] )
WP e1 @ s; E [{ Φ }].
Proof using Hinh.
......@@ -75,7 +75,7 @@ Lemma twp_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
to_val e1 = None
( σ1, head_reducible_no_obs e1 σ1)
( σ1 κ e2' σ2 efs',
head_step e1 σ1 κ e2' σ2 efs' κ = [] σ1 = σ2 e2 = e2' efs' = [])
head_step e1 σ1 κ e2' σ2 efs' κ = [] σ2 = σ1 e2' = e2 efs' = [])
WP e2 @ s; E [{ Φ }] WP e1 @ s; E [{ Φ }].
Proof using Hinh.
intros. rewrite -(twp_lift_pure_det_step_no_fork e1 e2); eauto.
......
......@@ -28,7 +28,7 @@ Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
(** Derived lifting lemmas. *)
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 = [])
( σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs κ = [] σ2 = σ1 efs = [])
(|={E}=> κ e2 efs σ, prim_step e1 σ κ e2 σ efs WP e2 @ s; E [{ Φ }])
WP e1 @ s; E [{ Φ }].
Proof.
......@@ -68,7 +68,7 @@ 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'
κ = [] σ1 = σ2 e2 = e2' efs' = [])
κ = [] σ2 = σ1 e2' = e2 efs' = [])
(|={E}=> WP e2 @ s; E [{ Φ }]) WP e1 @ s; E [{ Φ }].
Proof.
iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step_no_fork s E); try done.
......
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