From 56e966fd3ccc2bda415518eb8f6fffbf5095ca8f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 7 Jun 2020 11:00:12 +0200
Subject: [PATCH] remove the weaker counterexample (now that the other one only
 requires a boring cinv_alloc)

---
 theories/bi/lib/counterexamples.v | 57 ++-----------------------------
 1 file changed, 2 insertions(+), 55 deletions(-)

diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index a2a1cc7a6..5f91cfe4f 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -216,59 +216,6 @@ Module inv. Section inv.
   Qed.
 End inv. End inv.
 
-(** This proves that if we have linear impredicative invariants, we can still
-drop arbitrary resources (i.e., we can "defeat" linearity).
-Variant 1: we assume a strong invariant creation lemma that lets us create
-invariants in the "open" state. *)
-Module linear1. Section linear1.
-  Context {PROP: bi}.
-  Implicit Types P : PROP.
-
-  (** Assumptions. *)
-  (** We have the mask-changing update modality (two classes: empty/full mask) *)
-  Inductive mask := M0 | M1.
-  Context (fupd : mask → mask → PROP → PROP).
-  Arguments fupd _ _ _%I.
-  Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E E P.
-  Hypothesis fupd_mono : ∀ E1 E2 P Q, (P ⊢ Q) → fupd E1 E2 P ⊢ fupd E1 E2 Q.
-  Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P.
-  Hypothesis fupd_frame_l : ∀ E1 E2 P Q, P ∗ fupd E1 E2 Q ⊢ fupd E1 E2 (P ∗ Q).
-
-  (** We have cancelable invariants. (Really they would have fractions at
-  [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_open :  ∀ P,
-    ⊢ fupd M1 M0 (∃ γ, cinv γ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)).
-
-  (** Some general lemmas and proof mode compatibility. *)
-  Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
-  Proof. intros P Q ?. by apply fupd_mono. Qed.
-  Instance fupd_proper E1 E2 : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E1 E2).
-  Proof.
-    intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
-  Qed.
-
-  Lemma fupd_frame_r E1 E2 P Q : fupd E1 E2 P ∗ Q ⊢ fupd E1 E2 (P ∗ Q).
-  Proof. by rewrite comm fupd_frame_l comm. Qed.
-
-  Global Instance elim_fupd_fupd p E1 E2 E3 P Q :
-    ElimModal True p false (fupd E1 E2 P) P (fupd E1 E3 Q) (fupd E2 E3 Q).
-  Proof.
-    by rewrite /ElimModal bi.intuitionistically_if_elim
-      fupd_frame_r bi.wand_elim_r fupd_fupd.
-  Qed.
-
-  (** Counterexample: now we can make any resource disappear. *)
-  Lemma leak P : P -∗ fupd M1 M1 emp.
-  Proof.
-    iIntros "HP".
-    set (INV := (∃ γ Q, cinv γ Q ∗ cinv_own γ ∗ P)%I).
-    iMod (cinv_alloc_open INV) as (γ) "(Hinv & Htok & Hclose)".
-    iApply "Hclose". iNext. iExists γ, _. iFrame.
-  Qed.
-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).
 We assume [cinv_alloc] without any bells or whistles.
@@ -287,7 +234,7 @@ There, the stronger variant of the "unlock" rule (see Aquinas Hobor's PhD thesis
 "Oracle Semantics", §4.7, p. 88) also permits putting the token of a lock
 entirely into that lock.
 *)
-Module linear2. Section linear2.
+Module linear. Section linear.
   Context {PROP: bi}.
   Implicit Types P : PROP.
 
@@ -336,4 +283,4 @@ Module linear2. Section linear2.
     iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
     iApply "Hclose". done.
   Qed.
-End linear2. End linear2.
+End linear. End linear.
-- 
GitLab