core: don't use the turnstile inside the logic

theories/base_logic/lib/core.v

@@ -5,7 +5,7 @@ Import uPred.
 
 (** 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.
+  (∀ Q, ☃ (Q → □ Q) → ☃ (P → Q) → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -14,10 +14,16 @@ Section core.
   Implicit Types P Q : uPred M.
 
   Lemma coreP_intro P : P -∗ coreP P.
-  Proof. iIntros "HP". iIntros (Q HQ) "HPQ". by iApply "HPQ". Qed.
+  Proof. iIntros "HP". iIntros (Q) "_ HPQ". by iApply "HPQ". Qed.
 
   Global Instance coreP_persistent P : PersistentP (coreP P).
-  Proof. rewrite /coreP. apply _. Qed.
+  Proof.
+    rewrite /coreP /PersistentP. iIntros "HC".
+    iApply always_forall. iIntros (Q). (* FIXME: iIntros should apply always_forall automatically. *)
+    iApply always_impl_plainly. iIntros "#HQ".
+    iApply always_impl_plainly. iIntros "#HPQ".
+    iApply "HQ". iApply "HC"; done.
+  Qed.
 
   Global Instance coreP_ne : NonExpansive (@coreP M).
   Proof. solve_proper. Qed.
@@ -26,8 +32,8 @@ Section core.
 
   Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
   Proof.
-    rewrite /coreP. iIntros (P P' HP) "H"; iIntros (Q ?) "#HPQ".
-    iApply ("H" $! Q with "[]"). by rewrite HP.
+    rewrite /coreP. iIntros (P P' HP) "H"; iIntros (Q) "#HQ #HPQ".
+    iApply ("H" $! Q with "[]"); first done. by rewrite HP.
   Qed.
 
   Lemma coreP_elim P : PersistentP P → coreP P -∗ P.