From 256de028b392838a7b92f1f24026605d3a21d549 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Oct 2020 13:46:53 +0200
Subject: [PATCH] =?UTF-8?q?Remove=20=C2=AC=20notation=20in=20counterexampl?=
 =?UTF-8?q?es.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/lib/counterexamples.v | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 3297952f2..a9eaff530 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -9,7 +9,6 @@ Set Default Proof Using "Type*".
 name-dependent allocation. *)
 Module savedprop. Section savedprop.
   Context `{BiAffine PROP}.
-  Notation "¬ P" := (□ (P → False))%I : bi_scope.
   Implicit Types P : PROP.
 
   Context (bupd : PROP → PROP).
@@ -39,15 +38,15 @@ Module savedprop. Section savedprop.
   Qed.
 
   (** A bad recursive reference: "Assertion with name [i] does not hold" *)
-  Definition A (i : ident) : PROP := (∃ P, ¬ P ∗ saved i P)%I.
+  Definition A (i : ident) : PROP := (∃ P, □ ¬ P ∗ saved i P)%I.
 
   Lemma A_alloc : ⊢ |==> ∃ i, saved i (A i).
   Proof. by apply sprop_alloc_dep. Qed.
 
   Lemma saved_NA i : saved i (A i) ⊢ ¬ A i.
   Proof.
-    iIntros "#Hs !> #HA". iPoseProof "HA" as "HA'".
-    iDestruct "HA'" as (P) "[#HNP HsP]". iApply "HNP".
+    iIntros "#Hs #HA". iPoseProof "HA" as "HA'".
+    iDestruct "HA'" as (P) "[HNP HsP]". iApply "HNP".
     iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]".
     { eauto. }
     iApply "HP". done.
@@ -55,8 +54,8 @@ Module savedprop. Section savedprop.
 
   Lemma saved_A i : saved i (A i) ⊢ A i.
   Proof.
-    iIntros "#Hs". iExists (A i). iFrame "#".
-    by iApply saved_NA.
+    iIntros "#Hs". iExists (A i). iFrame "Hs".
+    iIntros "!>". by iApply saved_NA.
   Qed.
 
   Lemma contradiction : False.
@@ -188,14 +187,14 @@ Module inv. Section inv.
   Qed.
 
   (** And now we tie a bad knot. *)
-  Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : bi_scope.
-  Definition A i : PROP := (∃ P, ¬P ∗ saved i P)%I.
+  Notation not_fupd P := (□ (P -∗ fupd M1 False))%I.
+  Definition A i : PROP := (∃ P, not_fupd P ∗ saved i P)%I.
   Global Instance A_persistent i : Persistent (A i) := _.
 
   Lemma A_alloc : ⊢ fupd M1 (∃ i, saved i (A i)).
   Proof. by apply saved_alloc. Qed.
 
-  Lemma saved_NA i : saved i (A i) ⊢ ¬A i.
+  Lemma saved_NA i : saved i (A i) ⊢ not_fupd (A i).
   Proof.
     iIntros "#Hi !> #HA". iPoseProof "HA" as "HA'".
     iDestruct "HA'" as (P) "#[HNP Hi']".
-- 
GitLab