From 8193c66d7f20b6ad21f69f67bb44b19e31713981 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 Oct 2017 00:12:29 +0200
Subject: [PATCH] Port the core to use the plain modality and prove it is
 non-expansive.

---
 theories/base_logic/lib/core.v | 33 ++++++++++++---------------------
 1 file changed, 12 insertions(+), 21 deletions(-)

diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index adf16b59d..d9c5d2434 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -3,19 +3,9 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-(** The "core" of an assertion is its maximal persistent part.
-    It can be defined entirely within the logic... at least
-    in the shallow embedding.
-    WARNING: The function "coreP" is NOT NON-EXPANSIVE.
-    This is because the turnstile is not non-expansive as a function
-    from iProp to (discreteC Prop).
-    To obtain a core that's non-expansive, we would have to add another
-    modality to the logic: a box that removes access to *all* resources,
-    not just restricts access to the core.
-*)
-
+(** The "core" of an assertion is its maximal persistent part. *)
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ `(!PersistentP Q), ⌜P ⊢ Q⌝ → Q)%I.
+  (∀ `(!PersistentP Q), ☃ (P → Q) → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -24,25 +14,26 @@ Section core.
   Implicit Types P Q : uPred M.
 
   Lemma coreP_intro P : P -∗ coreP P.
-  Proof. iIntros "HP". by iIntros (Q HQ ->). Qed.
+  Proof. iIntros "HP". iIntros (Q HQ) "HPQ". by iApply "HPQ". Qed.
 
   Global Instance coreP_persistent P : PersistentP (coreP P).
   Proof. rewrite /coreP. apply _. Qed.
 
+  Global Instance coreP_ne : NonExpansive (@coreP M).
+  Proof. solve_proper. Qed.
+  Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
+  Proof. solve_proper. Qed.
+
   Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
   Proof.
-    rewrite /coreP. iIntros (P P' ?) "H"; iIntros (Q ??).
-    iApply ("H" $! Q with "[%]"). by etrans.
+    rewrite /coreP. iIntros (P P' HP) "H"; iIntros (Q ?) "#HPQ".
+    iApply ("H" $! Q with "[]"). by rewrite HP.
   Qed.
 
-  Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
-  Proof. intros P Q. rewrite !equiv_spec=>-[??]. by split; apply coreP_mono. Qed.
-
   Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
-  Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed.
+  Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P); auto. Qed.
 
-  Lemma coreP_wand P Q :
-    (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
+  Lemma coreP_wand P Q : (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
   Proof.
     split.
     - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
-- 
GitLab