From 827f464cf1e8040bca403afc2f2b4537fb5c1f7d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 7 Jun 2020 10:59:33 +0200
Subject: [PATCH] linear counterexample: we do not actually need cinv_alloc to
 be that powerful

---
 theories/bi/lib/counterexamples.v | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index bf560efa5..a2a1cc7a6 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -271,9 +271,8 @@ End linear1. End linear1.
 
 (** This proves that if we have linear impredicative invariants, we can still
 drop arbitrary resources (i.e., we can "defeat" linearity).
-Variant 2: maybe the strong invariant creation lemma (variant 1 above) is a bit
-too obvious, so here we just assume that the invariant can depend on the chosen
-[γ].  Moreover, we also have an accessor that gives back the invariant token
+We assume [cinv_alloc] without any bells or whistles.
+Moreover, we also have an accessor that gives back the invariant token
 immediately, not just after the invariant got closed again.
 
 The assumptions here match the proof rules in Iron, save for the side-condition
@@ -306,8 +305,8 @@ Module linear2. Section linear2.
   [cinv_own] but we do not need that. They would also have a name matching
   the [mask] type, but we do not need that either.) *)
   Context (gname : Type) (cinv : gname → PROP → PROP) (cinv_own : gname → PROP).
-  Hypothesis cinv_alloc : ∀ E,
-    ⊢ fupd E E (∃ γ, ∀ P, ▷ P -∗ fupd E E (cinv γ P ∗ cinv_own γ)).
+  Hypothesis cinv_alloc : ∀ E P,
+    ▷ P -∗ fupd E E (∃ γ, cinv γ P ∗ cinv_own γ).
   Hypothesis cinv_acc : ∀ P γ,
     cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 (▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)).
 
@@ -333,8 +332,7 @@ Module linear2. Section linear2.
   Lemma leak P : P -∗ fupd M1 M1 emp.
   Proof.
     iIntros "HP".
-    iMod cinv_alloc as (γ) "Hmkinv".
-    iMod ("Hmkinv" $! True%I with "[//]") as "[Hinv Htok]".
+    iMod ((cinv_alloc _ True%I) with "[//]") as (γ) "[Hinv Htok]".
     iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
     iApply "Hclose". done.
   Qed.
-- 
GitLab