From 2891ccae2087f0341a1ca5200c29a2302e1dabaa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Mar 2017 19:40:56 +0100
Subject: [PATCH] generalize lifting lemmas: better support view shifts that
 take a step

---
 theories/heap_lang/lifting.v          | 20 +++++++++---------
 theories/program_logic/ectx_lifting.v | 30 +++++++++++++++++++--------
 theories/program_logic/lifting.v      | 24 +++++++++++++--------
 3 files changed, 46 insertions(+), 28 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index ec64faebe..9de570086 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -76,7 +76,7 @@ Lemma wp_fork E e Φ :
   ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
+  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
   - intros; inv_head_step; eauto.
 Qed.
 
@@ -86,7 +86,7 @@ Lemma wp_rec E f x erec e1 e2 Φ :
   Closed (f :b: x :b: []) erec →
   ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
 Proof.
-  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _)
+  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step_no_fork' (App _ _)
     (subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
   intros; inv_head_step; eauto.
 Qed.
@@ -96,7 +96,7 @@ Lemma wp_un_op E op e v v' Φ :
   un_op_eval op v = Some v' →
   ▷ Φ v' ⊢ WP UnOp op e @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step_no_fork (UnOp op _) (of_val v'))
+  intros. rewrite -(wp_lift_pure_det_head_step_no_fork' (UnOp op _) (of_val v'))
     -?wp_value'; eauto.
   intros; inv_head_step; eauto.
 Qed.
@@ -106,7 +106,7 @@ Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
   bin_op_eval op v1 v2 = Some v' →
   ▷ (Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val v'))
+  intros. rewrite -(wp_lift_pure_det_head_step_no_fork' (BinOp op _ _) (of_val v'))
     -?wp_value'; eauto.
   intros; inv_head_step; eauto.
 Qed.
@@ -114,14 +114,14 @@ Qed.
 Lemma wp_if_true E e1 e2 Φ :
   ▷ WP e1 @ E {{ Φ }} ⊢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
 Proof.
-  apply wp_lift_pure_det_head_step_no_fork; eauto.
+  apply wp_lift_pure_det_head_step_no_fork'; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_false E e1 e2 Φ :
   ▷ WP e2 @ E {{ Φ }} ⊢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
 Proof.
-  apply wp_lift_pure_det_head_step_no_fork; eauto.
+  apply wp_lift_pure_det_head_step_no_fork'; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -130,7 +130,7 @@ Lemma wp_fst E e1 v1 e2 Φ :
   ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros ? [v2 ?].
-  rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1) -?wp_value; eauto.
+  rewrite -(wp_lift_pure_det_head_step_no_fork' (Fst _) e1) -?wp_value; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -139,7 +139,7 @@ Lemma wp_snd E e1 e2 v2 Φ :
   ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
   intros [v1 ?] ?.
-  rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2) -?wp_value; eauto.
+  rewrite -(wp_lift_pure_det_head_step_no_fork' (Snd _) e2) -?wp_value; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -148,7 +148,7 @@ Lemma wp_case_inl E e0 e1 e2 Φ :
   ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
 Proof.
   intros [v0 ?].
-  rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e1 e0)); eauto.
+  rewrite -(wp_lift_pure_det_head_step_no_fork' (Case _ _ _) (App e1 e0)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -157,7 +157,7 @@ Lemma wp_case_inr E e0 e1 e2 Φ :
   ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
 Proof.
   intros [v0 ?].
-  rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e2 e0)); eauto.
+  rewrite -(wp_lift_pure_det_head_step_no_fork' (Case _ _ _) (App e2 e0)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index e0c0f468b..bac5de8a2 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -12,11 +12,11 @@ Implicit Types v : val.
 Implicit Types e : expr.
 Hint Resolve head_prim_reducible head_reducible_prim_step.
 
-Lemma wp_ectx_bind {E e} K Φ :
+Lemma wp_ectx_bind {E Φ} K e :
   WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
 Proof. apply: weakestpre.wp_bind. Qed.
 
-Lemma wp_lift_head_step E Φ e1 :
+Lemma wp_lift_head_step {E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
@@ -30,14 +30,15 @@ Proof.
   iApply "H". by eauto.
 Qed.
 
-Lemma wp_lift_pure_head_step E Φ e1 :
+Lemma wp_lift_pure_head_step {E E' Φ} e1 :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
-  (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
+  (|={E,E'}▷=> ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
     WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof using Hinh.
-  iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext.
+  iIntros (??) "H". iApply wp_lift_pure_step; eauto.
+  iMod "H" as "H". iModIntro. iNext. iMod "H" as "H". iModIntro.
   iIntros (????). iApply "H". eauto.
 Qed.
 
@@ -70,21 +71,32 @@ Proof.
   by iApply big_sepL_nil.
 Qed.
 
-Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
+Lemma wp_lift_pure_det_head_step {E 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 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  (|={E,E'}▷=> WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
 
-Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork {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') →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
 Qed.
+
+Lemma wp_lift_pure_det_head_step_no_fork' {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') →
+  ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+Proof using Hinh.
+  intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
+  rewrite -step_fupd_intro //.
+Qed.
 End wp.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 1e69da79f..2aebb9a24 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -21,21 +21,24 @@ Lemma wp_lift_step E Φ e1 :
 Proof. by rewrite wp_unfold /wp_pre=> ->. Qed.
 
 (** Derived lifting lemmas. *)
-Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
+Lemma wp_lift_pure_step `{Inhabited (state Λ)} E E' Φ e1 :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
-  (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
+  (|={E,E'}▷=> ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
     WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
   { eapply reducible_not_val, (Hsafe inhabitant). }
-  iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-  iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+  iIntros (σ1) "Hσ". iMod "H" as "H".
+  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
+  iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
-  iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
+  iMod "Hclose" as "_". iFrame "Hσ". iMod "H" as "H". iApply "H"; auto.
 Qed.
 
+(* Atomic steps don't need any mask-changing business here, one can
+   use the generic lemmas here. *)
 Lemma wp_lift_atomic_step {E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
@@ -54,13 +57,16 @@ Proof.
   by iApply wp_value.
 Qed.
 
-Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
+Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E E' Φ} e1 e2 efs :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-  ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  (|={E,E'}▷=> WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
-  by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
+  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done.
+  { by intros; eapply Hpuredet. }
+  (* TODO: Can we make this nicer? iNext for fupd, for example, could help. *)
+  iMod "H" as "H". iModIntro. iNext. iMod "H" as "H". iModIntro.
+  by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 End lifting.
-- 
GitLab