From c654549ec831dc5af51648a1d7a0404b6b6641ee Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 5 Mar 2016 13:00:51 +0100
Subject: [PATCH] fix compilation *oops*; make inv_alloc more flexible

---
 barrier/client.v           |  4 +---
 barrier/proof.v            |  2 +-
 heap_lang/heap.v           |  4 ++--
 heap_lang/tests.v          | 10 +++++-----
 program_logic/auth.v       |  8 ++++----
 program_logic/invariants.v |  7 +++++--
 program_logic/sts.v        |  7 +++----
 7 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/barrier/client.v b/barrier/client.v
index c22706cf6..01c882963 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -76,9 +76,7 @@ Section ClosedProofs.
 
   Lemma client_safe_closed Ïƒ : {{ ownP Ïƒ : iProp }} client {{ Î» v, True }}.
   Proof.
-    apply ht_alt. rewrite (heap_alloc âŠ¤ (nroot .@ "Barrier")); last first.
-    { (* FIXME Really?? set_solver takes forever on "âŠ† âŠ¤"?!? *)
-      by move=>? _. }
+    apply ht_alt. rewrite (heap_alloc (nroot .@ "Barrier")); last done.
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
     rewrite -(client_safe (nroot .@ "Barrier") (nroot .@ "Heap")) //.
     (* This, too, should be automated. *)
diff --git a/barrier/proof.v b/barrier/proof.v
index db13c6cd9..5c340160d 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -2,8 +2,8 @@ From prelude Require Import functions.
 From algebra Require Import upred_big_op upred_tactics.
 From program_logic Require Import sts saved_prop.
 From heap_lang Require Export heap wp_tactics.
-From barrier Require Import protocol.
 From barrier Require Export barrier.
+From barrier Require Import protocol.
 Import uPred.
 
 (** The monoids we need. *)
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 50bcfc955..eb0ed8990 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -90,13 +90,13 @@ Section heap.
   Hint Resolve heap_store_valid.
 
   (** Allocation *)
-  Lemma heap_alloc E N Ïƒ :
+  Lemma heap_alloc N E Ïƒ :
     authG heap_lang Î£ heapR â†’ nclose N âŠ† E â†’
     ownP Ïƒ âŠ‘ (|={E}=> âˆƒ _ : heapG Î£, heap_ctx N âˆ§ Î â˜…{map Ïƒ} (Î» l v, l â†¦ v)).
   Proof.
     intros. rewrite -{1}(from_to_heap Ïƒ). etrans.
     { rewrite [ownP _]later_intro.
-      apply (auth_alloc (ownP âˆ˜ of_heap) E N (to_heap Ïƒ)); last done.
+      apply (auth_alloc (ownP âˆ˜ of_heap) N E (to_heap Ïƒ)); last done.
       apply to_heap_valid. }
     apply pvs_mono, exist_elim=> Î³.
     rewrite -(exist_intro (HeapG _ _ Î³)); apply and_mono_r.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 6aa456571..87e3f05e1 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -24,7 +24,7 @@ Section LiftingTests.
   Definition heap_e  : expr [] :=
     let: "x" := ref #1 in '"x" <- !'"x" + #1 ;; !'"x".
   Lemma heap_e_spec E N :
-     nclose N âŠ† E â†’ heap_ctx N âŠ‘ || heap_e @ E {{ Î» v, v = #2 }}.
+     nclose N âŠ† E â†’ heap_ctx N âŠ‘ #> heap_e @ E {{ Î» v, v = #2 }}.
   Proof.
     rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
     wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
@@ -44,7 +44,7 @@ Section LiftingTests.
 
   Lemma FindPred_spec n1 n2 E Î¦ :
     n1 < n2 â†’ 
-    Î¦ #(n2 - 1) âŠ‘ || FindPred #n2 #n1 @ E {{ Î¦ }}.
+    Î¦ #(n2 - 1) âŠ‘ #> FindPred #n2 #n1 @ E {{ Î¦ }}.
   Proof.
     revert n1. wp_rec=>n1 Hn.
     wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
@@ -53,7 +53,7 @@ Section LiftingTests.
     - assert (n1 = n2 - 1) as -> by omega; auto with I.
   Qed.
 
-  Lemma Pred_spec n E Î¦ : â–· Î¦ #(n - 1) âŠ‘ || Pred #n @ E {{ Î¦ }}.
+  Lemma Pred_spec n E Î¦ : â–· Î¦ #(n - 1) âŠ‘ #> Pred #n @ E {{ Î¦ }}.
   Proof.
     wp_lam. wp_op=> ?; wp_if.
     - wp_op. wp_op.
@@ -63,7 +63,7 @@ Section LiftingTests.
   Qed.
 
   Lemma Pred_user E :
-    (True : iProp) âŠ‘ || let: "x" := Pred #42 in ^Pred '"x" @ E {{ Î» v, v = #40 }}.
+    (True : iProp) âŠ‘ #> let: "x" := Pred #42 in ^Pred '"x" @ E {{ Î» v, v = #40 }}.
   Proof.
     intros. ewp apply Pred_spec. wp_let. ewp apply Pred_spec. auto with I.
   Qed.
@@ -75,7 +75,7 @@ Section ClosedProofs.
 
   Lemma heap_e_closed Ïƒ : {{ ownP Ïƒ : iProp }} heap_e {{ Î» v, v = #2 }}.
   Proof.
-    apply ht_alt. rewrite (heap_alloc âŠ¤ nroot); last by rewrite nclose_nroot.
+    apply ht_alt. rewrite (heap_alloc nroot âŠ¤); last by rewrite nclose_nroot.
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
     rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
   Qed.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 4e99d933f..337e90d55 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -49,19 +49,19 @@ Section auth.
   Lemma auth_own_valid Î³ a : auth_own Î³ a âŠ‘ âœ“ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 
-  Lemma auth_alloc E N a :
+  Lemma auth_alloc N E a :
     âœ“ a â†’ nclose N âŠ† E â†’
     â–· Ï† a âŠ‘ (|={E}=> âˆƒ Î³, auth_ctx Î³ N Ï† âˆ§ auth_own Î³ a).
   Proof.
     intros Ha HN. eapply sep_elim_True_r.
-    { by eapply (own_alloc (Auth (Excl a) a) N). }
-    rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //. apply pvs_strip_pvs.
+    { by eapply (own_alloc (Auth (Excl a) a) E). }
+    rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>Î³. rewrite -(exist_intro Î³).
     trans (â–· auth_inv Î³ Ï† â˜… auth_own Î³ a)%I.
     { rewrite /auth_inv -(exist_intro a) later_sep.
       ecancel [â–· Ï† _]%I.
       by rewrite -later_intro -own_op auth_both_op. }
-    rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
+    rewrite (inv_alloc N E) // /auth_ctx pvs_frame_r. apply pvs_mono.
     by rewrite always_and_sep_l.
   Qed.
 
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index e22f4a8d2..324e00387 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -68,7 +68,10 @@ Lemma wp_open_close E e N P Î¦ R :
   R âŠ‘ #> e @ E {{ Î¦ }}.
 Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
 
-Lemma inv_alloc N P : â–· P âŠ‘ pvs N N (inv N P).
-Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
+Lemma inv_alloc N E P : nclose N âŠ† E â†’ â–· P âŠ‘ pvs E E (inv N P).
+Proof. 
+  intros. rewrite -(pvs_mask_weaken N) //.
+  by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
+Qed.
 
 End inv.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 814c5ae98..101ff16bf 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -81,16 +81,15 @@ Section sts.
     â–· Ï† s âŠ‘ (|={E}=> âˆƒ Î³, sts_ctx Î³ N Ï† âˆ§ sts_own Î³ s (âŠ¤ âˆ– sts.tok s)).
   Proof.
     intros HN. eapply sep_elim_True_r.
-    { apply (own_alloc (sts_auth s (âŠ¤ âˆ– sts.tok s)) N).
+    { apply (own_alloc (sts_auth s (âŠ¤ âˆ– sts.tok s)) E).
       apply sts_auth_valid; set_solver. }
-    rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //.
-    apply pvs_strip_pvs.
+    rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>Î³. rewrite -(exist_intro Î³).
     trans (â–· sts_inv Î³ Ï† â˜… sts_own Î³ s (âŠ¤ âˆ– sts.tok s))%I.
     { rewrite /sts_inv -(exist_intro s) later_sep.
       ecancel [â–· Ï† _]%I.
       by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
-    rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
+    rewrite (inv_alloc N E) // /sts_ctx pvs_frame_r.
     by rewrite always_and_sep_l.
   Qed.
 
-- 
GitLab