From d02b774e94995188f6f4f7b99a19e01e8fdc0bf7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 16 Jan 2020 20:51:35 +0100
Subject: [PATCH] show that cancellable invariants can also be created open

---
 theories/base_logic/lib/cancelable_invariants.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index c03416e0d..d38a8816c 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -99,6 +99,14 @@ Section proofs.
     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γ".
-- 
GitLab