generalize core to all BIs

_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

theories/base_logic/lib/core.v → theories/bi/lib/core.v

-From iris.base_logic Require Import base_logic.
+From iris.bi Require Export bi plainly.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
-Import uPred.
+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 {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ Q, ■ (P → □ Q) → □ Q)%I.
+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 {M : ucmraT}.
-  Implicit Types P Q : uPred M.
+  Context `{!BiPlainly PROP}.
+  Implicit Types P Q : PROP.
 
   Lemma coreP_intro P : P -∗ coreP P.
-  Proof. rewrite /coreP. iIntros "HP" (Q) "HPQ". by iApply "HPQ". Qed.
+  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 "HC". Qed.
+  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 M).
+  Global Instance coreP_ne : NonExpansive (coreP (PROP:=PROP)).
   Proof. solve_proper. Qed.
-  Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
+  Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (coreP (PROP:=PROP)).
   Proof. solve_proper. Qed.
 
-  Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
+  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". iApply ("HCP" $! P with "[]"). auto.
+    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.
 
-  Lemma coreP_wand P Q : (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
+  (* 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".

theories/bi/plainly.v

-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.