state the lifting lemmas slightly differently

barrier/lifting.v

@@ -45,10 +45,10 @@ Qed.
 
 (* TODO RJ: Figure out some better way to make the
    postcondition a predicate over a *location* *)
-Lemma wp_alloc_pst E σ e v:
+Lemma wp_alloc_pst E σ e v Q :
   e2v e = Some v →
-  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc e)
-       (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)).
+  (ownP (Σ:=Σ) σ ★ ▷(∀ l, ■(σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ) -★ Q (LocV l)))
+       ⊑ wp (Σ:=Σ) E (Alloc e) Q.
 Proof.
   (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *)
   intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
@@ -62,21 +62,19 @@ Proof.
     apply (not_elem_of_dom (D := gset loc)). apply is_fresh.
   - reflexivity.
   - reflexivity.
-  - (* RJ FIXME I am sure there is a better way to invoke right_id, but I could not find it. *)
-    rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
-    apply sep_mono; first done. rewrite -later_intro.
+  - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono.
     apply forall_intro=>e2. apply forall_intro=>σ2.
-    apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
+    apply wand_intro_l. rewrite -pvs_intro.
+    rewrite always_and_sep_l' -associative -always_and_sep_l'.
     apply const_elim_l. intros [l [-> [-> Hl]]].
-    rewrite -wp_value'; last reflexivity.
-    erewrite <-exist_intro with (a := l). apply and_intro.
-    + by apply const_intro.
-    + done.
+    rewrite (forall_elim _ l). eapply const_intro_l; first eexact Hl.
+    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
+    rewrite -wp_value'; done.
 Qed.
 
-Lemma wp_load_pst E σ l v:
+Lemma wp_load_pst E σ l v Q :
   σ !! l = Some v →
-  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Load (Loc l)) (λ v', ■(v' = v) ∧ ownP (Σ:=Σ) σ).
+  (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q v)) ⊑ wp (Σ:=Σ) E (Load (Loc l)) Q.
 Proof.
   intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first.
@@ -85,21 +83,19 @@ Proof.
   - do 3 eexists. econstructor; eassumption.
   - reflexivity.
   - reflexivity.
-  - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
-    apply sep_mono; first done. rewrite -later_intro.
+  - rewrite -pvs_intro.
+    apply sep_mono; first done. apply later_mono.
     apply forall_intro=>e2. apply forall_intro=>σ2.
-    apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
+    apply wand_intro_l. rewrite -pvs_intro.
+    rewrite always_and_sep_l' -associative -always_and_sep_l'.
     apply const_elim_l. intros [-> ->].
-    rewrite -wp_value. apply and_intro.
-    + by apply const_intro.
-    + done.
+    by rewrite wand_elim_r -wp_value.
 Qed.
 
-Lemma wp_store_pst E σ l e v v':
+Lemma wp_store_pst E σ l e v v' Q :
   e2v e = Some v →
   σ !! l = Some v' →
-  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) e)
-       (λ v', ■(v' = LitUnitV) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)).
+  (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp (Σ:=Σ) E (Store (Loc l) e) Q.
 Proof.
   intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first.
@@ -108,21 +104,19 @@ Proof.
   - do 3 eexists. eapply StoreS; last (eexists; eassumption). eassumption.
   - reflexivity.
   - reflexivity.
-  - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
-    apply sep_mono; first done. rewrite -later_intro.
+  - rewrite -pvs_intro.
+    apply sep_mono; first done. apply later_mono.
     apply forall_intro=>e2. apply forall_intro=>σ2.
-    apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
+    apply wand_intro_l. rewrite -pvs_intro.
+    rewrite always_and_sep_l' -associative -always_and_sep_l'.
     apply const_elim_l. intros [-> ->].
-    rewrite -wp_value'; last reflexivity. apply and_intro.
-    + by apply const_intro.
-    + done.
+    by rewrite wand_elim_r -wp_value'.
 Qed.
 
-Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' :
+Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
   e2v e1 = Some v1 → e2v e2 = Some v2 →
   σ !! l = Some v' → v' <> v1 →
-  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2)
-       (λ v', ■(v' = LitFalseV) ∧ ownP (Σ:=Σ) σ).
+  (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q LitFalseV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q.
 Proof.
   intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', e' = LitFalse ∧ σ' = σ); last first.
@@ -133,21 +127,19 @@ Proof.
   - do 3 eexists. eapply CasFailS; eassumption.
   - reflexivity.
   - reflexivity.
-  - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
-    apply sep_mono; first done. rewrite -later_intro.
+  - rewrite -pvs_intro.
+    apply sep_mono; first done. apply later_mono.
     apply forall_intro=>e2'. apply forall_intro=>σ2'.
-    apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
+    apply wand_intro_l. rewrite -pvs_intro.
+    rewrite always_and_sep_l' -associative -always_and_sep_l'.
     apply const_elim_l. intros [-> ->].
-    rewrite -wp_value'; last reflexivity. apply and_intro.
-    + by apply const_intro.
-    + done.
+    by rewrite wand_elim_r -wp_value'.
 Qed.
 
-Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 :
+Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
   e2v e1 = Some v1 → e2v e2 = Some v2 →
   σ !! l = Some v1 →
-  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2)
-       (λ v', ■(v' = LitTrueV) ∧ ownP (Σ:=Σ) (<[l:=v2]>σ)).
+  (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q.
 Proof.
   intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ); last first.
@@ -160,14 +152,13 @@ Proof.
   - do 3 eexists. eapply CasSucS; eassumption.
   - reflexivity.
   - reflexivity.
-  - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
-    apply sep_mono; first done. rewrite -later_intro.
+  - rewrite -pvs_intro.
+    apply sep_mono; first done. apply later_mono.
     apply forall_intro=>e2'. apply forall_intro=>σ2'.
-    apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
+    apply wand_intro_l. rewrite -pvs_intro.
+    rewrite always_and_sep_l' -associative -always_and_sep_l'.
     apply const_elim_l. intros [-> ->].
-    rewrite -wp_value'; last reflexivity. apply and_intro.
-    + by apply const_intro.
-    + done.
+    by rewrite wand_elim_r -wp_value'.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
@@ -218,7 +209,7 @@ Proof.
     rewrite right_id. done.
 Qed.
 
-Lemma wp_rec' E e v Q :
+Lemma wp_rec E e v Q :
   ▷wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q ⊑ wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q.
 Proof.
   etransitivity; last eapply wp_lift_pure_step with
@@ -233,7 +224,7 @@ Qed.
 Lemma wp_lam E e v Q :
   ▷wp (Σ:=Σ) E (e.[v2e v/]) Q ⊑ wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q.
 Proof.
-  rewrite -wp_rec'.
+  rewrite -wp_rec.
   (* RJ: This pulls in functional extensionality. If that bothers us, we have
      to talk to the Autosubst guys. *)
   by asimpl.

barrier/tests.v

@@ -37,25 +37,27 @@ Module LiftingTests.
   Goal ∀ σ E, (ownP (Σ:=Σ) σ) ⊑ (wp (Σ:=Σ) E e (λ v, ■(v = LitNatV 2))).
   Proof.
     move=> σ E. rewrite /e.
-    rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). rewrite -wp_mono.
-    { eapply wp_alloc_pst; done. }
-    move=>v; apply exist_elim=>l. apply const_elim_l; move=>[-> _] {v}.
+    rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). rewrite -wp_alloc_pst; last done.
+    apply sep_intro_True_r; first done.
+    rewrite -later_intro. apply forall_intro=>l.
+    apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
     rewrite -wp_lam -later_intro. asimpl.
     rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _)
                                    (PlusLCtx EmptyCtx _)) (Load (Loc _)))).
-    rewrite -wp_mono.
-    { eapply wp_load_pst. apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
-    move=>v; apply const_elim_l; move=>-> {v}.
+    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
+    { apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
+    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))).
     rewrite -wp_plus -later_intro.
     rewrite -(wp_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))).
-    rewrite -wp_mono.
-    { eapply wp_store_pst; first reflexivity. apply: lookup_insert. }
-    move=>v; apply const_elim_l; move=>-> {v}.
+    rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
+    { apply: lookup_insert. }
+    { reflexivity. }
+    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     rewrite -wp_lam -later_intro. asimpl.
-    rewrite -wp_mono.
-    { eapply wp_load_pst. apply: lookup_insert. }
-    move=>v; apply const_elim_l; move=>-> {v}.
+    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
+    { apply: lookup_insert. }
+    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     by apply const_intro.
   Qed.
 End LiftingTests.

modures/logic.v

@@ -616,6 +616,16 @@ Proof. intros ->; apply sep_elim_l. Qed.
 Lemma sep_elim_r' P Q R : Q ⊑ R → (P ★ Q) ⊑ R.
 Proof. intros ->; apply sep_elim_r. Qed.
 Hint Resolve sep_elim_l' sep_elim_r'.
+Lemma sep_intro_True_l P Q R : True ⊑ P → R ⊑ Q → R ⊑ (P ★ Q).
+Proof.
+  intros HP HQ. etransitivity; last (eapply sep_mono; eassumption).
+  by rewrite left_id.
+Qed.
+Lemma sep_intro_True_r P Q R : R ⊑ P → True ⊑ Q → R ⊑ (P ★ Q).
+Proof.
+  intros HP HQ. etransitivity; last (eapply sep_mono; eassumption).
+  by rewrite right_id.
+Qed.
 Lemma wand_intro_l P Q R : (Q ★ P) ⊑ R → P ⊑ (Q -★ R).
 Proof. rewrite (commutative _); apply wand_intro_r. Qed.
 Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊑ Q.