From c82cc68ee6f9861691cc1f3ff6747ef87ae7e52d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Mar 2018 16:52:15 +0100
Subject: [PATCH] generalize core to all BIs

---
 _CoqProject                    |  2 +-
 theories/base_logic/lib/core.v | 45 -----------------------
 theories/bi/lib/core.v         | 66 ++++++++++++++++++++++++++++++++++
 theories/bi/plainly.v          |  2 +-
 4 files changed, 68 insertions(+), 47 deletions(-)
 delete mode 100644 theories/base_logic/lib/core.v
 create mode 100644 theories/bi/lib/core.v

diff --git a/_CoqProject b/_CoqProject
index 4ddfcad28..50d473944 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,6 +39,7 @@ theories/bi/monpred.v
 theories/bi/embedding.v
 theories/bi/lib/fractional.v
 theories/bi/lib/atomic.v
+theories/bi/lib/core.v
 theories/base_logic/upred.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v
@@ -58,7 +59,6 @@ theories/base_logic/lib/boxes.v
 theories/base_logic/lib/na_invariants.v
 theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/gen_heap.v
-theories/base_logic/lib/core.v
 theories/base_logic/lib/fancy_updates_from_vs.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
deleted file mode 100644
index f64ad81cf..000000000
--- a/theories/base_logic/lib/core.v
+++ /dev/null
@@ -1,45 +0,0 @@
-From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
-Import uPred.
-
-(** The "core" of an assertion is its maximal persistent part,
-    i.e. the conjunction of all persistent assertions that are weaker
-    than P (as in, implied by P). *)
-Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ Q, ■ (P → □ Q) → □ Q)%I.
-Instance: Params (@coreP) 1.
-Typeclasses Opaque coreP.
-
-Section core.
-  Context {M : ucmraT}.
-  Implicit Types P Q : uPred M.
-
-  Lemma coreP_intro P : P -∗ coreP P.
-  Proof. rewrite /coreP. iIntros "HP" (Q) "HPQ". by iApply "HPQ". Qed.
-
-  Global Instance coreP_persistent P : Persistent (coreP P).
-  Proof. rewrite /coreP /Persistent. iIntros "#HC" (Q) "!#". iApply "HC". 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. solve_proper. Qed.
-
-  Lemma coreP_elim P : Persistent P → coreP P -∗ P.
-  Proof.
-    rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P with "[]"). auto.
-  Qed.
-
-  Lemma coreP_wand P Q : (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
-  Proof.
-    split.
-    - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
-      iAlways. by iApply HP.
-    - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
-      by iDestruct (coreP_elim with "HcQ") as "#HQ".
-  Qed.
-End core.
diff --git a/theories/bi/lib/core.v b/theories/bi/lib/core.v
new file mode 100644
index 000000000..cdd8ee502
--- /dev/null
+++ b/theories/bi/lib/core.v
@@ -0,0 +1,66 @@
+From iris.bi Require Export bi plainly.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import bi.
+
+(** The "core" of an assertion is its maximal persistent part,
+    i.e. the conjunction of all persistent assertions that are weaker
+    than P (as in, implied by P). *)
+Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
+  (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q)%I.
+Instance: Params (@coreP) 1.
+Typeclasses Opaque coreP.
+
+Section core.
+  Context `{!BiPlainly PROP}.
+  Implicit Types P Q : PROP.
+
+  Lemma coreP_intro P : P -∗ coreP P.
+  Proof.
+    rewrite /coreP. iIntros "HP" (Q) "_ HPQ".
+    (* FIXME: Cannot apply HPQ directly. *)
+    iDestruct (affinely_plainly_elim with "HPQ") as "HPQ".
+    by iApply "HPQ".
+  Qed.
+
+  Global Instance coreP_persistent P : Persistent (coreP P).
+  Proof.
+    rewrite /coreP /Persistent. iIntros "HC" (Q).
+    iApply persistently_impl_plainly. iIntros "#HQ".
+    iApply persistently_impl_plainly. iIntros "#HPQ".
+    iApply "HQ".
+    (* FIXME: [iApply "HC"] should work. *)
+    iSpecialize ("HC" with "HQ"). iSpecialize ("HC" with "HPQ"). done.
+  Qed.
+
+  Global Instance coreP_ne : NonExpansive (coreP (PROP:=PROP)).
+  Proof. solve_proper. Qed.
+  Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (coreP (PROP:=PROP)).
+  Proof. solve_proper. Qed.
+
+  Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (coreP (PROP:=PROP)).
+  Proof. solve_proper. Qed.
+
+  Lemma coreP_elim P : Persistent P → coreP P -∗ P.
+  Proof.
+    rewrite /coreP. iIntros (?) "HCP". iSpecialize ("HCP" $! P).
+    (* FIXME: [iApply "HCP"] should work. *)
+    iAssert (■ (P -∗ <pers> P))%I as "#HPpers".
+    { iModIntro. iApply persistent. }
+    iSpecialize ("HCP" with "HPpers").
+    iAssert (■ (P -∗ P))%I as "#HP".
+    { iIntros "!> HP". done. }
+    iSpecialize ("HCP" with "HP").
+    done.
+  Qed.
+
+  (* TODO: Can we generalize this to non-affine BIs? *)
+  Lemma coreP_wand `{!BiAffine PROP} P Q : (coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
+  Proof.
+    split.
+    - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
+      iAlways. by iApply HP.
+    - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
+      by iDestruct (coreP_elim with "HcQ") as "#HQ".
+  Qed.
+End core.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 7f63cc8bf..756364c99 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export derived_laws.
+From iris.bi Require Import derived_laws.
 From iris.algebra Require Import monoid.
 Import interface.bi derived_laws.bi.
 
-- 
GitLab