From 0d187bae3ab49902eb7823e8b2f24d2e3d10f515 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 2 Feb 2020 18:14:29 +0100
Subject: [PATCH] add strongest variant of cinv_alloc_open

---
 .../base_logic/lib/cancelable_invariants.v    | 69 ++++++++++++-------
 1 file changed, 44 insertions(+), 25 deletions(-)

diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index d38a8816c..248d6dbd5 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -60,22 +60,54 @@ Section proofs.
     iSplit; iIntros "[?|$]"; iLeft; by iApply "HP".
   Qed.
 
+  (*** Allocation rules. *)
+  (** The "strong" variants permit any infinite [I], and choosing [P] is delayed
+  until after [Î³] was chosen. *)
   Lemma cinv_alloc_strong (I : gname â†’ Prop) E N :
     pred_infinite I â†’
-    (|={E}=> âˆƒ Î³, âŒœ I Î³ âŒ âˆ§ cinv_own Î³ 1 âˆ— âˆ€ P, â–· P ={E}=âˆ— cinv N Î³ P)%I.
+    (|={E}=> âˆƒ Î³, âŒœ I Î³ âŒ âˆ— cinv_own Î³ 1 âˆ— âˆ€ P, â–· P ={E}=âˆ— cinv N Î³ P)%I.
   Proof.
     iIntros (?). iMod (own_alloc_strong 1%Qp I) as (Î³) "[Hfresh HÎ³]"; [done|done|].
-    iExists Î³; iIntros "!> {$HÎ³ $Hfresh}" (P) "HP".
+    iExists Î³. iIntros "!> {$HÎ³ $Hfresh}" (P) "HP".
     iMod (inv_alloc N _ (P âˆ¨ cinv_own Î³ 1) with "[HP]"); eauto.
   Qed.
 
+  (** The "open" variants create the invariant in the open state, and delay
+  having to prove [P]. *)
+  Lemma cinv_alloc_strong_open (I : gname â†’ Prop) E N :
+    pred_infinite I â†’
+    â†‘N âŠ† E â†’
+    (|={E}=> âˆƒ Î³, âŒœ I Î³ âŒ âˆ— cinv_own Î³ 1 âˆ— âˆ€ P,
+      |={E,Eâˆ–â†‘N}=> cinv N Î³ P âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True))%I.
+  Proof.
+    iIntros (??). iMod (own_alloc_strong 1%Qp I) as (Î³) "[Hfresh HÎ³]"; [done|done|].
+    iExists Î³. iIntros "!> {$HÎ³ $Hfresh}" (P).
+    iMod (inv_alloc_open N _ (P âˆ¨ cinv_own Î³ 1)) as "[Hinv Hclose]"; first by eauto.
+    iIntros "!>". iFrame. iIntros "HP". iApply "Hclose". iLeft. done.
+  Qed.
+
   Lemma cinv_alloc_cofinite (G : gset gname) E N :
-    (|={E}=> âˆƒ Î³, âŒœ Î³ âˆ‰ G âŒ âˆ§ cinv_own Î³ 1 âˆ— âˆ€ P, â–· P ={E}=âˆ— cinv N Î³ P)%I.
+    (|={E}=> âˆƒ Î³, âŒœ Î³ âˆ‰ G âŒ âˆ— cinv_own Î³ 1 âˆ— âˆ€ P, â–· P ={E}=âˆ— cinv N Î³ P)%I.
   Proof.
     apply cinv_alloc_strong. apply (pred_infinite_set (C:=gset gname))=> E'.
     exists (fresh (G âˆª E')). apply not_elem_of_union, is_fresh.
   Qed.
 
+  Lemma cinv_alloc E N P : â–· P ={E}=âˆ— âˆƒ Î³, cinv N Î³ P âˆ— cinv_own Î³ 1.
+  Proof.
+    iIntros "HP". iMod (cinv_alloc_cofinite âˆ… E N) as (Î³ _) "[HÎ³ Halloc]".
+    iExists Î³. iFrame "HÎ³". by iApply "Halloc".
+  Qed.
+
+  Lemma cinv_alloc_open E N P :
+    â†‘N âŠ† E â†’ (|={E,Eâˆ–â†‘N}=> âˆƒ Î³, cinv N Î³ P âˆ— cinv_own Î³ 1 âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True))%I.
+  Proof.
+    iIntros (?). iMod (cinv_alloc_strong_open (Î» _, True)) as (Î³) "(_ & Htok & Hmake)"; [|done|].
+    { apply pred_infinite_True. }
+    iMod ("Hmake" $! P) as "[Hinv Hclose]". iIntros "!>". iExists Î³. iFrame.
+  Qed.
+
+  (*** Accessors *)
   Lemma cinv_open_strong E N Î³ p P :
     â†‘N âŠ† E â†’
     cinv N Î³ P -âˆ— (cinv_own Î³ p ={E,Eâˆ–â†‘N}=âˆ—
@@ -93,28 +125,6 @@ Section proofs.
     - iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
   Qed.
 
-  Lemma cinv_alloc E N P : â–· P ={E}=âˆ— âˆƒ Î³, cinv N Î³ P âˆ— cinv_own Î³ 1.
-  Proof.
-    iIntros "HP". iMod (cinv_alloc_cofinite âˆ… E N) as (Î³ _) "[HÎ³ Halloc]".
-    iExists Î³. iFrame "HÎ³". by iApply "Halloc".
-  Qed.
-
-  Lemma cinv_alloc_open E N P :
-    â†‘N âŠ† E â†’ (|={E,Eâˆ–â†‘N}=> âˆƒ Î³, cinv N Î³ P âˆ— cinv_own Î³ 1 âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True))%I.
-  Proof.
-    iIntros (?). iMod (own_alloc 1%Qp) as (Î³) "HÎ³"; [done..|].
-    iMod (inv_alloc_open N _ (P âˆ¨ cinv_own Î³ 1)) as "[Hinv Hclose]"; [done..|].
-    iExists Î³; iIntros "!> {$HÎ³ $Hinv} HP". iApply "Hclose". by eauto.
-  Qed.
-
-  Lemma cinv_cancel E N Î³ P : â†‘N âŠ† E â†’ cinv N Î³ P -âˆ— cinv_own Î³ 1 ={E}=âˆ— â–· P.
-  Proof.
-    iIntros (?) "#Hinv HÎ³".
-    iMod (cinv_open_strong with "Hinv HÎ³") as "($ & HÎ³ & H)"; first done.
-    rewrite {2}(union_difference_L (â†‘N) E)=> //.
-    iApply "H". by iRight.
-  Qed.
-
   Lemma cinv_open E N Î³ p P :
     â†‘N âŠ† E â†’
     cinv N Î³ P -âˆ— cinv_own Î³ p ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— cinv_own Î³ p âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True).
@@ -126,6 +136,15 @@ Section proofs.
     iApply "H". by iLeft.
   Qed.
 
+  (*** Other *)
+  Lemma cinv_cancel E N Î³ P : â†‘N âŠ† E â†’ cinv N Î³ P -âˆ— cinv_own Î³ 1 ={E}=âˆ— â–· P.
+  Proof.
+    iIntros (?) "#Hinv HÎ³".
+    iMod (cinv_open_strong with "Hinv HÎ³") as "($ & HÎ³ & H)"; first done.
+    rewrite {2}(union_difference_L (â†‘N) E)=> //.
+    iApply "H". by iRight.
+  Qed.
+
   Global Instance into_inv_cinv N Î³ P : IntoInv (cinv N Î³ P) N := {}.
 
   Global Instance into_acc_cinv E N Î³ P p :
-- 
GitLab