Merge branch 'naught' into 'master'

The plainness modality

See merge request FP/iris-coq!71

ProofMode.md

@@ -31,7 +31,7 @@ Context management
 - `iRevert (x1 ... xn) "selpat"` : revert the hypotheses given by the selection
   pattern `selpat` into wands, and the Coq level hypotheses/variables
   `x1 ... xn` into universal quantifiers. Persistent hypotheses are wrapped into
-  the always modality.
+  the persistence modality.
 - `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
 - `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
   implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
@@ -162,8 +162,8 @@ Miscellaneous
   introduces pure connectives.
 - The proof mode adds hints to the core `eauto` database so that `eauto`
   automatically introduces: conjunctions and disjunctions, universal and
-  existential quantifiers, implications and wand, always, later and update
-  modalities, and pure connectives.
+  existential quantifiers, implications and wand, plainness, persistence, later
+  and update modalities, and pure connectives.
 
 Selection patterns
 ==================
@@ -207,7 +207,9 @@ appear at the top level:
   Items of the selection pattern can be prefixed with `$`, which cause them to
   be framed instead of cleared.
 - `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an always modality and clear the spatial context.
+- `!#` : introduce an persistence or plainness modality and clear the spatial
+  context. In case of a plainness modality, it will prune all persistent
+  hypotheses that are not plain.
 - `!>` : introduce a modality.
 - `/=` : perform `simpl`.
 - `//` : perform `try done` on all goals.

theories/base_logic/big_op.v

@@ -149,6 +149,14 @@ Section list.
     by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   Qed.
 
+  Global Instance big_sepL_nil_plain Φ : Plain ([∗ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL_plain Φ l :
+    (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x).
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Global Instance big_sepL_plain_id Ps : TCForall Plain Ps → Plain ([∗] Ps).
+  Proof. induction 1; simpl; apply _. Qed.
+
   Global Instance big_sepL_nil_persistent Φ :
     Persistent ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
@@ -342,12 +350,19 @@ Section gmap.
     by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   Qed.
 
+  Global Instance big_sepM_empty_plain Φ : Plain ([∗ map] k↦x ∈ ∅, Φ k x).
+  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
+  Global Instance big_sepM_plain Φ m :
+    (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x ∈ m, Φ k x).
+  Proof. intros. apply big_sepL_plain=> _ [??]; apply _. Qed.
+
   Global Instance big_sepM_empty_persistent Φ :
     Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
   Global Instance big_sepM_persistent Φ m :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
+
   Global Instance big_sepM_nil_timeless Φ :
     Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
@@ -490,11 +505,18 @@ Section gset.
     by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   Qed.
 
+  Global Instance big_sepS_empty_plain Φ : Plain ([∗ set] x ∈ ∅, Φ x).
+  Proof. rewrite /big_opS elements_empty. apply _. Qed.
+  Global Instance big_sepS_plain Φ X :
+    (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
+  Proof. rewrite /big_opS. apply _. Qed.
+
   Global Instance big_sepS_empty_persistent Φ : Persistent ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
   Global Instance big_sepS_persistent Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
+
   Global Instance big_sepS_nil_timeless Φ : Timeless ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
   Global Instance big_sepS_timeless Φ X :
@@ -578,11 +600,18 @@ Section gmultiset.
     □?q ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □?q Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
+  Global Instance big_sepMS_empty_plain Φ : Plain ([∗ mset] x ∈ ∅, Φ x).
+  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
+  Global Instance big_sepMS_plain Φ X :
+    (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
+  Proof. rewrite /big_opMS. apply _. Qed.
+
   Global Instance big_sepMS_empty_persistent Φ : Persistent ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
   Global Instance big_sepMS_persistent Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
+
   Global Instance big_sepMS_nil_timeless Φ : Timeless ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
   Global Instance big_sepMS_timeless Φ X :

theories/base_logic/derived.v

@@ -39,6 +39,11 @@ Arguments persistent {_} _ {_}.
 Hint Mode Persistent + ! : typeclass_instances.
 Instance: Params (@Persistent) 1.
 
+Class Plain {M} (P : uPred M) := plain : P ⊢ ■ P.
+Arguments plain {_} _ {_}.
+Hint Mode Plain + ! : typeclass_instances.
+Instance: Params (@Plain) 1.
+
 Module uPred.
 Section derived.
 Context {M : ucmraT}.
@@ -471,6 +476,104 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q.
 Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 
+(* Plainness modality *)
+Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@uPred_plainly M).
+Proof. intros P Q; apply plainly_mono. Qed.
+Global Instance naugth_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@uPred_plainly M).
+Proof. intros P Q; apply plainly_mono. Qed.
+
+Lemma plainly_elim P : ■ P ⊢ P.
+Proof. by rewrite plainly_elim' persistently_elim. Qed.
+Hint Resolve plainly_mono plainly_elim.
+Lemma plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
+Proof. intros <-. apply plainly_idemp. Qed.
+Lemma plainly_idemp P : ■ ■ P ⊣⊢ ■ P.
+Proof. apply (anti_symm _); auto using plainly_idemp. Qed.
+
+Lemma persistently_plainly P : □ ■ P ⊣⊢ ■ P.
+Proof.
+  apply (anti_symm _); auto using persistently_elim.
+  by rewrite -plainly_elim' plainly_idemp.
+Qed.
+Lemma plainly_persistently P : ■ □ P ⊣⊢ ■ P.
+Proof.
+  apply (anti_symm _); auto using plainly_mono, persistently_elim.
+  by rewrite -plainly_elim' plainly_idemp.
+Qed.
+
+Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Proof.
+  apply (anti_symm _); auto.
+  apply pure_elim'=> Hφ.
+  trans (∀ x : False, ■ True : uPred M)%I; [by apply forall_intro|].
+  rewrite plainly_forall_2. auto using plainly_mono, pure_intro.
+Qed.
+Lemma plainly_forall {A} (Ψ : A → uPred M) : (■ ∀ a, Ψ a) ⊣⊢ (∀ a, ■ Ψ a).
+Proof.
+  apply (anti_symm _); auto using plainly_forall_2.
+  apply forall_intro=> x. by rewrite (forall_elim x).
+Qed.
+Lemma plainly_exist {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊣⊢ (∃ a, ■ Ψ a).
+Proof.
+  apply (anti_symm _); auto using plainly_exist_1.
+  apply exist_elim=> x. by rewrite (exist_intro x).
+Qed.
+Lemma plainly_and P Q : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q.
+Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
+Lemma plainly_or P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q.
+Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
+Lemma plainly_impl P Q : ■ (P → Q) ⊢ ■ P → ■ Q.
+Proof.
+  apply impl_intro_l; rewrite -plainly_and.
+  apply plainly_mono, impl_elim with P; auto.
+Qed.
+Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+  apply (anti_symm (⊢)); auto using persistently_elim.
+  apply (internal_eq_rewrite a b (λ b, ■ (a ≡ b))%I); auto.
+  { intros n; solve_proper. }
+  rewrite -(internal_eq_refl a) plainly_pure; auto.
+Qed.
+
+Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
+Proof. by rewrite -persistently_plainly persistently_and_sep_l_1. Qed.
+Lemma plainly_and_sep_l' P Q : ■ P ∧ Q ⊣⊢ ■ P ∗ Q.
+Proof. apply (anti_symm (⊢)); auto using plainly_and_sep_l_1. Qed.
+Lemma plainly_and_sep_r' P Q : P ∧ ■ Q ⊣⊢ P ∗ ■ Q.
+Proof. by rewrite !(comm _ P) plainly_and_sep_l'. Qed.
+Lemma plainly_sep_dup' P : ■ P ⊣⊢ ■ P ∗ ■ P.
+Proof. by rewrite -plainly_and_sep_l' idemp. Qed.
+
+Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊣⊢ ■ (P ∗ Q).
+Proof.
+  apply (anti_symm (⊢)); auto.
+  rewrite -{1}plainly_idemp plainly_and plainly_and_sep_l'; auto.
+Qed.
+Lemma plainly_sep P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Proof. by rewrite -plainly_and_sep -plainly_and_sep_l' plainly_and. Qed.
+
+Lemma plainly_wand P Q : ■ (P -∗ Q) ⊢ ■ P -∗ ■ Q.
+Proof. by apply wand_intro_r; rewrite -plainly_sep wand_elim_l. Qed.
+Lemma plainly_impl_wand P Q : ■ (P → Q) ⊣⊢ ■ (P -∗ Q).
+Proof.
+  apply (anti_symm (⊢)); [by rewrite -impl_wand_1|].
+  apply plainly_intro', impl_intro_r.
+  by rewrite plainly_and_sep_l' plainly_elim wand_elim_l.
+Qed.
+Lemma wand_impl_plainly P Q : (■ P -∗ Q) ⊣⊢ (■ P → Q).
+Proof.
+  apply (anti_symm (⊢)); [|by rewrite -impl_wand_1].
+  apply impl_intro_l. by rewrite plainly_and_sep_l' wand_elim_r.
+Qed.
+Lemma plainly_entails_l' P Q : (P ⊢ ■ Q) → P ⊢ ■ Q ∗ P.
+Proof. intros; rewrite -plainly_and_sep_l'; auto. Qed.
+Lemma plainly_entails_r' P Q : (P ⊢ ■ Q) → P ⊢ P ∗ ■ Q.
+Proof. intros; rewrite -plainly_and_sep_r'; auto. Qed.
+
+Lemma plainly_laterN n P : ■ ▷^n P ⊣⊢ ▷^n ■ P.
+Proof. induction n as [|n IH]; simpl; auto. by rewrite plainly_later IH. Qed.
+
 (* Always derived *)
 Hint Resolve persistently_mono persistently_elim.
 Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@uPred_persistently M).
@@ -485,12 +588,7 @@ Lemma persistently_idemp P : □ □ P ⊣⊢ □ P.
 Proof. apply (anti_symm _); auto using persistently_idemp_2. Qed.
 
 Lemma persistently_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof.
-  apply (anti_symm _); auto.
-  apply pure_elim'=> Hφ.
-  trans (∀ x : False, □ True : uPred M)%I; [by apply forall_intro|].
-  rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
-Qed.
+Proof. by rewrite -plainly_pure persistently_plainly. Qed.
 Lemma persistently_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
 Proof.
   apply (anti_symm _); auto using persistently_forall_2.
@@ -511,12 +609,7 @@ Proof.
   apply persistently_mono, impl_elim with P; auto.
 Qed.
 Lemma persistently_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
-  apply (anti_symm (⊢)); auto using persistently_elim.
-  apply (internal_eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
-  { intros n; solve_proper. }
-  rewrite -(internal_eq_refl a) persistently_pure; auto.
-Qed.
+Proof. by rewrite -plainly_internal_eq persistently_plainly. Qed.
 
 Lemma persistently_and_sep_l P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
 Proof. apply (anti_symm (⊢)); auto using persistently_and_sep_l_1. Qed.
@@ -616,7 +709,6 @@ Proof. apply wand_intro_r; rewrite -later_sep; eauto using wand_elim_l. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
-
 (* Iterated later modality *)
 Global Instance laterN_ne m : NonExpansive (@uPred_laterN M m).
 Proof. induction m; simpl. by intros ???. solve_proper. Qed.
@@ -747,6 +839,8 @@ Lemma except_0_persistently P : ◇ □ P ⊣⊢ □ ◇ P.
 Proof. by rewrite /uPred_except_0 persistently_or persistently_later persistently_pure. Qed.
 Lemma except_0_persistently_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
 Proof. destruct p; simpl; auto using except_0_persistently. Qed.
+Lemma except_0_plainly P : ◇ ■ P ⊣⊢ ■ ◇ P.
+Proof. by rewrite /uPred_except_0 plainly_or plainly_later plainly_pure. Qed.
 Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
 Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
@@ -764,11 +858,10 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by auto. apply ownM_unit. Qed.
+Lemma plainly_cmra_valid {A : cmraT} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
+Proof. apply (anti_symm _); auto using plainly_elim, plainly_cmra_valid_1. Qed.
 Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-Proof.
-  intros; apply (anti_symm _); first by apply:persistently_elim.
-  apply:persistently_cmra_valid_1.
-Qed.
+Proof. by rewrite -plainly_cmra_valid persistently_plainly. Qed.
 
 (** * Derived rules *)
 Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M).
@@ -860,6 +953,25 @@ Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A)
   (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
+(* Derived lemmas for plainness *)
+Global Instance Plain_proper : Proper ((≡) ==> iff) (@Plain M).
+Proof. solve_proper. Qed.
+Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
+  NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
+Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
+
+(* Not an instance, see the bottom of this file *)
+Lemma plain_persistent P : Plain P → Persistent P.
+Proof. rewrite /Plain /Persistent=> HP. by rewrite {1}HP plainly_elim'. Qed.
+
+Lemma plainly_plainly P `{!Plain P} : ■ P ⊣⊢ P.
+Proof. apply (anti_symm (⊢)); eauto. Qed.
+Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ ■ Q.
+Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
+
+Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
+Proof. by rewrite -{1}(plainly_plainly P) bupd_plainly. Qed.
+
 (* Derived lemmas for persistence *)
 Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent M).
 Proof. solve_proper. Qed.
@@ -889,20 +1001,71 @@ Proof.
   apply impl_intro_l. by rewrite and_sep_l wand_elim_r.
 Qed.
 
+(* Plain *)
+Global Instance pure_plain φ : Plain (⌜φ⌝ : uPred M)%I.
+Proof. by rewrite /Plain plainly_pure. Qed.
+Global Instance impl_plain P Q : Plain P → Plain Q → Plain (P → Q).
+Proof.
+  rewrite /Plain=> HP HQ.
+  by rewrite {2}HP -plainly_impl_plainly -HQ plainly_elim.
+Qed.
+Global Instance wand_plain P Q : Plain P → Plain Q → Plain (P -∗ Q)%I.
+Proof.
+  rewrite /Plain=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -plainly_impl_plainly -HQ.
+Qed.
+Global Instance plainly_plain P : Plain (■ P).
+Proof. by intros; apply plainly_intro'. Qed.
+Global Instance persistently_plain P : Plain P → Plain (□ P).
+Proof. rewrite /Plain=> HP. by rewrite {1}HP persistently_plainly plainly_persistently. Qed.
+Global Instance and_plain P Q :
+  Plain P → Plain Q → Plain (P ∧ Q).
+Proof. by intros; rewrite /Plain plainly_and; apply and_mono. Qed.
+Global Instance or_plain P Q :
+  Plain P → Plain Q → Plain (P ∨ Q).
+Proof. by intros; rewrite /Plain plainly_or; apply or_mono. Qed.
+Global Instance sep_plain P Q :
+  Plain P → Plain Q → Plain (P ∗ Q).
+Proof. by intros; rewrite /Plain plainly_sep; apply sep_mono. Qed.
+Global Instance forall_plain {A} (Ψ : A → uPred M) :
+  (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x).
+Proof. by intros; rewrite /Plain plainly_forall; apply forall_mono. Qed.
+Global Instance exist_palin {A} (Ψ : A → uPred M) :
+  (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x).
+Proof. by intros; rewrite /Plain plainly_exist; apply exist_mono. Qed.
+Global Instance internal_eq_plain {A : ofeT} (a b : A) :
+  Plain (a ≡ b : uPred M)%I.
+Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
+Global Instance cmra_valid_plain {A : cmraT} (a : A) :
+  Plain (✓ a : uPred M)%I.
+Proof. by intros; rewrite /Plain; apply plainly_cmra_valid_1. Qed.
+Global Instance later_plain P : Plain P → Plain (▷ P).
+Proof. by intros; rewrite /Plain plainly_later; apply later_mono. Qed.
+Global Instance except_0_plain P : Plain P → Plain (◇ P).
+Proof. by intros; rewrite /Plain -except_0_plainly; apply except_0_mono. Qed.
+Global Instance laterN_plain n P : Plain P → Plain (▷^n P).
+Proof. induction n; apply _. Qed.
+Global Instance from_option_palin {A} P (Ψ : A → uPred M) (mx : option A) :
+  (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
+Proof. destruct mx; apply _. Qed.
+
 (* Persistence *)
 Global Instance pure_persistent φ : Persistent (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /Persistent persistently_pure. Qed.
-Global Instance pure_impl_persistent φ Q :
-  Persistent Q → Persistent (⌜φ⌝ → Q)%I.
+Global Instance impl_persistent P Q :
+  Plain P → Persistent Q → Persistent (P → Q).
 Proof.
-  rewrite /Persistent pure_impl_forall persistently_forall. auto using forall_mono.
+  rewrite /Plain /Persistent=> HP HQ.
+  rewrite {2}HP -persistently_impl_plainly. by rewrite -HQ plainly_elim.
 Qed.
-Global Instance pure_wand_persistent φ Q :
-  Persistent Q → Persistent (⌜φ⌝ -∗ Q)%I.
+Global Instance wand_persistent P Q :
+  Plain P → Persistent Q → Persistent (P -∗ Q)%I.
 Proof.
-  rewrite /Persistent -impl_wand pure_impl_forall persistently_forall.
-  auto using forall_mono.
+  rewrite /Plain /Persistent=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -persistently_impl_plainly -HQ.
 Qed.
+Global Instance plainly_persistent P : Persistent (■ P).
+Proof. by rewrite /Persistent persistently_plainly. Qed.
 Global Instance persistently_persistent P : Persistent (□ P).
 Proof. by intros; apply persistently_intro'. Qed.
 Global Instance and_persistent P Q :
@@ -930,6 +1093,8 @@ Global Instance later_persistent P : Persistent P → Persistent (▷ P).
 Proof. by intros; rewrite /Persistent persistently_later; apply later_mono. Qed.
 Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
 Proof. induction n; apply _. Qed.
+Global Instance except_0_persistent P : Persistent P → Persistent (◇ P).
+Proof. by intros; rewrite /Persistent -except_0_persistently; apply except_0_mono. Qed.
 Global Instance ownM_persistent : CoreId a → Persistent (@uPred_ownM M a).
 Proof. intros. by rewrite /Persistent persistently_ownM. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
@@ -947,6 +1112,9 @@ Global Instance uPred_sep_monoid : Monoid (@uPred_sep M) :=
 Global Instance uPred_persistently_and_homomorphism :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_persistently M).
 Proof. split; [split; try apply _|]. apply persistently_and. apply persistently_pure. Qed.
+Global Instance uPred_plainly_and_homomorphism :
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_plainly M).
+Proof. split; [split; try apply _|]. apply plainly_and. apply plainly_pure. Qed.
 Global Instance uPred_persistently_if_and_homomorphism b :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_persistently_if M b).
 Proof. split; [split; try apply _|]. apply persistently_if_and. apply persistently_if_pure. Qed.
@@ -963,6 +1131,9 @@ Proof. split; [split; try apply _|]. apply except_0_and. apply except_0_True. Qe
 Global Instance uPred_persistently_or_homomorphism :
   MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_persistently M).
 Proof. split; [split; try apply _|]. apply persistently_or. apply persistently_pure. Qed.
+Global Instance uPred_plainly_or_homomorphism :
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_plainly M).
+Proof. split; [split; try apply _|]. apply plainly_or. apply plainly_pure. Qed.
 Global Instance uPred_persistently_if_or_homomorphism b :
   MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_persistently_if M b).
 Proof. split; [split; try apply _|]. apply persistently_if_or. apply persistently_if_pure. Qed.
@@ -974,11 +1145,14 @@ Global Instance uPred_laterN_or_homomorphism n :
 Proof. split; try apply _. apply laterN_or. Qed.
 Global Instance uPred_except_0_or_homomorphism :
   WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_except_0 M).
-Proof. split; try apply _. apply except_0_or. Qed. 
+Proof. split; try apply _. apply except_0_or. Qed.
 
 Global Instance uPred_persistently_sep_homomorphism :
   MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_persistently M).
 Proof. split; [split; try apply _|]. apply persistently_sep. apply persistently_pure. Qed.
+Global Instance uPred_plainly_sep_homomorphism :
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_plainly M).
+Proof. split; [split; try apply _|]. apply plainly_sep. apply plainly_pure. Qed.
 Global Instance uPred_persistently_if_sep_homomorphism b :
   MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_persistently_if M b).
 Proof. split; [split; try apply _|]. apply persistently_if_sep. apply persistently_if_pure. Qed.
@@ -996,3 +1170,12 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 End derived.
 End uPred.
+
+(* When declared as an actual instance, [plain_persistent] will give cause
+failing proof searches to take exponential time, as Coq will try to apply it
+the instance at any node in the proof search tree.
+
+To avoid that, we declare it using a [Hint Immediate], so that it will only be
+used at the leaves of the proof search tree, i.e. when the premise of the hint
+can be derived from just the current context. *)
+Hint Immediate uPred.plain_persistent : typeclass_instances.

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 :=
-  (∀ `(!Persistent Q), ⌜P ⊢ Q⌝ → Q)%I.
+  (∀ Q, ■ (Q → □ Q) → ■ (P → Q) → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -24,25 +14,31 @@ Section core.
   Implicit Types P Q : uPred M.
 
   Lemma coreP_intro P : P -∗ coreP P.
-  Proof. rewrite /coreP. iIntros "HP". by iIntros (Q HQ ->). Qed.
+  Proof. rewrite /coreP. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ". Qed.
 
   Global Instance coreP_persistent P : Persistent (coreP P).
-  Proof. rewrite /coreP. apply _. 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 /Persistent. iIntros "HC" (Q).
+    iApply persistently_impl_plainly. iIntros "#HQ".
+    iApply persistently_impl_plainly. iIntros "#HPQ".
+    iApply "HQ". by iApply "HC".
   Qed.
 
+  Global Instance coreP_ne : NonExpansive (@coreP M).
+  Proof. solve_proper. Qed.
   Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
-  Proof. intros P Q. rewrite !equiv_spec=>-[??]. by split; apply coreP_mono. Qed.
+  Proof. solve_proper. Qed.
+
+  Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
+  Proof.
+    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 : Persistent 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".

theories/base_logic/lib/counter_examples.v

@@ -40,13 +40,11 @@ Module savedprop. Section savedprop.
 
   Lemma contradiction : False.
   Proof using All.
-    apply (@soundness M False 1); simpl.
+    apply (@consistency M); simpl.
     iIntros "". iMod A_alloc as (i) "#H".
     iPoseProof (saved_NA with "H") as "HN".
-    iModIntro. iNext.
-    iApply "HN". iApply saved_A. done.
+    iApply "HN". by iApply saved_A.
   Qed.
-
 End savedprop. End savedprop.
 
 (** This proves that we need the ▷ when opening invariants. *)

theories/base_logic/primitive.v

@@ -97,6 +97,14 @@ Definition uPred_wand {M} := unseal uPred_wand_aux M.
 Definition uPred_wand_eq :
   @uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux.
 
+Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
+  {| uPred_holds n x := P n ε |}.
+Solve Obligations with naive_solver eauto using uPred_closed, ucmra_unit_validN.
+Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed.
+Definition uPred_plainly {M} := unseal uPred_plainly_aux M.
+Definition uPred_plainly_eq :