Stronger version of allocation rule for cancelable invariants.

theories/base_logic/lib/cancelable_invariants.v

@@ -61,12 +61,19 @@ Section proofs.
     - iIntros "?". iApply "HP'". iApply "HP''". done.
   Qed.
 
-  Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1.
+  Lemma cinv_alloc_strong (G : gset gname) E N :
+    (|={E}=> ∃ γ, ⌜ γ ∉ G ⌝ ∧ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I.
   Proof.
-    iIntros "HP".
-    iMod (own_alloc 1%Qp) as (γ) "H1"; first done.
+    iMod (own_alloc_strong 1%Qp G) as (γ) "[Hfresh Hγ]"; first done.
+    iExists γ; iIntros "!> {$Hγ $Hfresh}" (P) "HP".
     iMod (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); first by eauto.
-    iExists _. iFrame. iExists _. iFrame. iIntros "!> !# !>". iSplit; by iIntros "?".
+    iIntros "!>". iExists P. iSplit; last done. iIntros "!# !>"; iSplit; auto.
+  Qed.
+
+  Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1.
+  Proof.
+    iIntros "HP". iMod (cinv_alloc_strong ∅ E N) as (γ _) "[Hγ Halloc]".
+    iExists γ. iFrame "Hγ". by iApply "Halloc".
   Qed.
 
   Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.