From 98318d33ed1306e70e71e9f0f4cd267c865bb99c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 2 Feb 2016 21:15:11 +0100
Subject: [PATCH] extend derived lifting lemmas to deal with fork (puts them
 on-par with the hoare lifting lemmas)

---
 barrier/lifting.v    | 42 ++++++++++++++++++-------------------
 iris/hoare_lifting.v |  4 ++++
 iris/lifting.v       | 49 +++++++++++++++++++++++++-------------------
 3 files changed, 53 insertions(+), 42 deletions(-)

diff --git a/barrier/lifting.v b/barrier/lifting.v
index e5e821312..dd463d2d0 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -23,21 +23,22 @@ Lemma wp_alloc_pst E σ e v Q :
 Proof.
   (* TODO RJ: Without the set, ssreflect rewrite doesn't work. Figure out why or
      reprot a bug. *)
-  intros. set (φ v' σ' := ∃ l, v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
+  intros. set (φ v' σ' ef := ∃ l, ef = @None expr ∧ v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
   rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
     last by intros; inv_step; eauto 8.
   apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
+  apply wand_intro_l.
   rewrite always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[l [-> [-> ?]]].
-  by rewrite (forall_elim l) const_equiv // left_id wand_elim_r.
+  apply const_elim_l=>-[l [-> [-> [-> ?]]]].
+  by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
 Qed.
 
 Lemma wp_load_pst E σ l v Q :
   σ !! l = Some v →
   (ownP σ ★ ▷ (ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
 Proof.
-  intros; rewrite -(wp_lift_atomic_det_step σ v σ) //;
+  intros; rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
     last (by intros; inv_step; eauto).
 Qed.
 
@@ -46,7 +47,7 @@ Lemma wp_store_pst E σ l e v v' Q :
   (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
 Proof.
   intros.
-  rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ)) //;
+  rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ) None) ?right_id //;
     last by intros; inv_step; eauto.
 Qed.
 
@@ -54,7 +55,7 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
   (ownP σ ★ ▷ (ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
-  intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ) //;
+  intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ None) ?right_id //;
     last by intros; inv_step; eauto.
 Qed.
 
@@ -63,7 +64,7 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
   (ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
   intros.
-  rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ)) //;
+  rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ) None) ?right_id //;
     last by intros; inv_step; eauto.
 Qed.
 
@@ -71,26 +72,25 @@ Qed.
 Lemma wp_fork E e :
   ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
 Proof.
-  rewrite -(wp_lift_pure_step E (λ e' ef, e' = LitUnit ∧ ef = Some e)) //=;
+  rewrite -(wp_lift_pure_det_step (Fork e) LitUnit (Some e)) //=;
     last by intros; inv_step; eauto.
-  apply later_mono, forall_intro=>e2; apply forall_intro=>ef.
-  apply impl_intro_l, const_elim_l=>-[-> ->] /=.
-  apply sep_intro_True_l; last done.
-  by rewrite -wp_value' //; apply const_intro.
+  apply later_mono, sep_intro_True_l; last done.
+  by rewrite -(wp_value' _ _ LitUnit) //; apply const_intro.
 Qed.
 
 Lemma wp_rec E ef e v Q :
   to_val e = Some v →
   ▷ wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_det_step (App _ _) ef.[Rec ef, e /]) //=;
+  intros; rewrite -(wp_lift_pure_det_step (App _ _) ef.[Rec ef, e /] None)
+                     ?right_id //=;
     last by intros; inv_step; eauto.
 Qed.
 
 Lemma wp_plus E n1 n2 Q :
   ▷ Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
-  rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2))) //=;
+  rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2)) None) ?right_id //;
     last by intros; inv_step; eauto.
   by rewrite -wp_value'.
 Qed.
@@ -99,7 +99,7 @@ Lemma wp_le_true E n1 n2 Q :
   n1 ≤ n2 →
   ▷ Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //;
     last by intros; inv_step; eauto with lia.
   by rewrite -wp_value'.
 Qed.
@@ -108,7 +108,7 @@ Lemma wp_le_false E n1 n2 Q :
   n1 > n2 →
   ▷ Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //;
     last by intros; inv_step; eauto with lia.
   by rewrite -wp_value'.
 Qed.
@@ -117,7 +117,7 @@ Lemma wp_fst E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Fst _) e1) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
     last by intros; inv_step; eauto.
   by rewrite -wp_value'.
 Qed.
@@ -126,7 +126,7 @@ Lemma wp_snd E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷ Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Snd _) e2) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
     last by intros; inv_step; eauto.
   by rewrite -wp_value'.
 Qed.
@@ -135,7 +135,7 @@ Lemma wp_case_inl E e0 v0 e1 e2 Q :
   to_val e0 = Some v0 →
   ▷ wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/]) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/] None) ?right_id //;
     last by intros; inv_step; eauto.
 Qed.
 
@@ -143,7 +143,7 @@ Lemma wp_case_inr E e0 v0 e1 e2 Q :
   to_val e0 = Some v0 →
   ▷ wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
 Proof.
-  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/]) //=;
+  intros; rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/] None) ?right_id //;
     last by intros; inv_step; eauto.
 Qed.
 
diff --git a/iris/hoare_lifting.v b/iris/hoare_lifting.v
index 471502d81..172ce73bc 100644
--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -44,6 +44,7 @@ Proof.
   rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
   by apply const_intro.
 Qed.
+
 Lemma ht_lift_atomic_step
     E (φ : expr Λ → state Λ → option (expr Λ) → Prop) P e1 σ1 :
   atomic e1 →
@@ -70,6 +71,7 @@ Proof.
     rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
     by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro.
 Qed.
+
 Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
@@ -95,6 +97,7 @@ Proof.
   rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
   by apply const_intro.
 Qed.
+
 Lemma ht_lift_pure_det_step
     E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 e2 ef :
   to_val e1 = None →
@@ -114,4 +117,5 @@ Proof.
     rewrite -always_and_sep_l' -associative; apply const_elim_l=>-[??]; subst.
     by rewrite /= /ht always_elim impl_elim_r.
 Qed.
+
 End lifting.
diff --git a/iris/lifting.v b/iris/lifting.v
index 62e1fcc4c..94093941b 100644
--- a/iris/lifting.v
+++ b/iris/lifting.v
@@ -56,53 +56,60 @@ Qed.
 Opaque uPred_holds.
 Import uPred.
 
-Lemma wp_lift_atomic_step {E Q} e1 (φ : val Λ → state Λ → Prop) σ1 :
+Lemma wp_lift_atomic_step {E Q} e1 (φ : val Λ → state Λ → option (expr Λ) → Prop) σ1 :
   to_val e1 = None →
   reducible e1 σ1 →
-  (∀ e' σ' ef, prim_step e1 σ1 e' σ' ef → ∃ v', ef = None ∧ to_val e' = Some v' ∧ φ v' σ') →
-  (ownP σ1 ★ ▷ ∀ v2 σ2, (■ φ v2 σ2 ∧ ownP σ2 -★ Q v2)) ⊑ wp E e1 Q.
+  (∀ e' σ' ef, prim_step e1 σ1 e' σ' ef → ∃ v', to_val e' = Some v' ∧ φ v' σ' ef) →
+  (ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ v2 σ2 ef ∧ ownP σ2 -★
+     Q v2 ★ default True ef (flip (wp coPset_all) (λ _, True)))
+    ⊑ wp E e1 Q.
 Proof.
   intros He Hsafe Hstep.
   rewrite -(wp_lift_step E E
-    (λ e' σ' ef, ∃ v', ef = None ∧ to_val e' = Some v' ∧ φ v' σ') _ e1 σ1) //; [].
+    (λ e' σ' ef, ∃ v', to_val e' = Some v' ∧ φ v' σ' ef) _ e1 σ1) //; [].
   rewrite -pvs_intro. apply sep_mono, later_mono; first done.
   apply forall_intro=>e2'; apply forall_intro=>σ2'.
   apply forall_intro=>ef; apply wand_intro_l.
   rewrite always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[v2' [-> [Hv ?]]] /=.
-  rewrite -pvs_intro right_id -wp_value'; last by eassumption.
-  rewrite (forall_elim v2') (forall_elim σ2') const_equiv //.
-  by rewrite left_id wand_elim_r.
+  apply const_elim_l=>-[v2' [Hv ?]] /=.
+  rewrite -pvs_intro.
+  rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
+  rewrite left_id wand_elim_r. apply sep_mono; last done.
+  (* FIXME RJ why can't I do this rewrite before doing sep_mono? *)
+  by rewrite -(wp_value' _ _ e2').
 Qed.
 
-Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 :
+Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :
   to_val e1 = None →
   reducible e1 σ1 →
-  (∀ e' σ' ef, prim_step e1 σ1 e' σ' ef → ef = None ∧ e' = of_val v2 ∧ σ' = σ2) →
-  (ownP σ1 ★ ▷ (ownP σ2 -★ Q v2)) ⊑ wp E e1 Q.
+  (∀ e' σ' ef', prim_step e1 σ1 e' σ' ef' → ef' = ef ∧ e' = of_val v2 ∧ σ' = σ2) →
+  (ownP σ1 ★ ▷ (ownP σ2 -★ Q v2 ★
+                       default True ef (flip (wp coPset_all) (λ _, True))))
+    ⊑ wp E e1 Q.
 Proof.
   intros He Hsafe Hstep.
-  rewrite -(wp_lift_atomic_step _ (λ v' σ', v' = v2 ∧ σ' = σ2) σ1) //; last first.
+  rewrite -(wp_lift_atomic_step _ (λ v' σ' ef', v' = v2 ∧ σ' = σ2 ∧ ef' = ef) σ1) //;
+    last first.
   { intros. exists v2. apply Hstep in H. destruct_conjs; subst.
     eauto using to_of_val. }
   apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2'; apply forall_intro=>σ2'.
+  apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'.
   apply wand_intro_l.
   rewrite always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[-> ->] /=.
+  apply const_elim_l=>-[-> [-> ->]] /=.
   by rewrite wand_elim_r.
 Qed.
 
-Lemma wp_lift_pure_det_step {E Q} e1 e2 :
+Lemma wp_lift_pure_det_step {E Q} e1 e2 ef :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
-  (∀ σ1 e' σ' ef, prim_step e1 σ1 e' σ' ef → σ1 = σ' ∧ ef = None ∧ e' = e2) →
-  (▷ wp E e2 Q) ⊑ wp E e1 Q.
+  (∀ σ1 e' σ' ef', prim_step e1 σ1 e' σ' ef' → σ1 = σ' ∧ ef' = ef ∧ e' = e2) →
+  ▷ (wp E e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True))) ⊑ wp E e1 Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_step E (λ e' ef, ef = None ∧ e' = e2) _ e1) //=.
-  apply later_mono, forall_intro=>e'; apply forall_intro=>ef.
-  apply impl_intro_l, const_elim_l=>-[-> ->] /=.
-  by rewrite right_id.
+  intros. rewrite -(wp_lift_pure_step E (λ e' ef', ef' = ef ∧ e' = e2) _ e1) //=.
+  apply later_mono, forall_intro=>e'; apply forall_intro=>ef'.
+  apply impl_intro_l, const_elim_l=>-[-> ->] /=; done.
 Qed.
 
 End lifting.
+
-- 
GitLab