From b8d083f223bf68a0f49ab8340f0b0a0921c496db Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Feb 2020 14:49:00 +0100
Subject: [PATCH] explain why the open inv-creation does not imply the other
 variants

---
 theories/base_logic/lib/cancelable_invariants.v | 5 +++--
 theories/base_logic/lib/invariants.v            | 1 +
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 248d6dbd5..0aaa353d3 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -62,7 +62,7 @@ Section proofs.
 
   (*** Allocation rules. *)
   (** The "strong" variants permit any infinite [I], and choosing [P] is delayed
-  until after [γ] was chosen. *)
+  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.
@@ -73,7 +73,8 @@ Section proofs.
   Qed.
 
   (** The "open" variants create the invariant in the open state, and delay
-  having to prove [P]. *)
+  having to prove [P].
+  These do not imply the other variants because of the extra assumption [↑N ⊆ E]. *)
   Lemma cinv_alloc_strong_open (I : gname → Prop) E N :
     pred_infinite I →
     ↑N ⊆ E →
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 320f7fc86..e14ca4939 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -56,6 +56,7 @@ Section inv.
     do 2 iModIntro. iExists i. auto.
   Qed.
 
+  (* This does not imply [own_inv_alloc] due to the extra assumption [↑N ⊆ E]. *)
   Lemma own_inv_alloc_open N E P :
     ↑N ⊆ E → (|={E, E∖↑N}=> own_inv N P ∗ (▷P ={E∖↑N, E}=∗ True))%I.
   Proof.
-- 
GitLab