Implement JH's idea of a "core of an assertion"

_CoqProject

@@ -84,6 +84,7 @@ theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/counter_examples.v
 theories/base_logic/lib/fractional.v
 theories/base_logic/lib/gen_heap.v
+theories/base_logic/lib/core.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v

theories/base_logic/lib/core.v

+From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import tactics.
+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. *)
+
+Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
+  (∀ (Q : uPred M) `(!PersistentP Q, !P -∗ Q), Q)%I.
+
+Section core.
+  Context {M : ucmraT}.
+  Implicit Types P Q : uPred M.
+
+  Lemma coreP_intro P :
+    P -∗ coreP P.
+  Proof.
+    iIntros "HP". iIntros (Q HQ HPQ). by iApply HPQ.
+  Qed.
+
+  Global Instance coreP_persistent P :
+    PersistentP (coreP P).
+  Proof.
+    iIntros "HCP". iApply always_forall. iIntros (Q).
+    iApply always_forall. iIntros (HQ). iApply always_forall.
+    iIntros (HPQ). iApply HQ. unshelve iApply ("HCP" $! Q). done.
+  Qed.
+
+  Lemma corP_elim P :
+    PersistentP P → coreP P -∗ P.
+  Proof.
+    iIntros (?) "HCP". unshelve iApply ("HCP" $! P).
+    iIntros "P". done.
+  Qed.
+End core.
+
+
+