A type class for plainly.

Based on an earlier MR by @jung.

_CoqProject

@@ -28,6 +28,7 @@ theories/algebra/proofmode_classes.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
 theories/bi/derived_laws.v
+theories/bi/plainly.v
 theories/bi/big_op.v
 theories/bi/updates.v
 theories/bi/bi.v

theories/base_logic/derived.v

@@ -30,11 +30,8 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
 Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
-Lemma affinely_plainly_cmra_valid {A : cmraT} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
-Proof.
-  rewrite affine_affinely.
-  apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _.
-Qed.
+Lemma plainly_cmra_valid {A : cmraT} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
+Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
 Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
   rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.

theories/base_logic/lib/fancy_updates.v

@@ -30,6 +30,16 @@ Proof.
     iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
     iIntros "!> !>". by iApply "HP".
   - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
+Qed.
+Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
+  {| bi_fupd_mixin := uPred_fupd_mixin |}.
+
+Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
+Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
+
+Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
+Proof.
+  split.
   - iIntros (E1 E2 E2' P Q ? (E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
     rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
     iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
@@ -39,9 +49,4 @@ Proof.
   - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P ?) "HP [Hw HE]".
     iAssert (▷ ◇ P)%I with "[-]" as "#$"; last by iFrame.
     iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
-Qed.
-Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
-  {| bi_fupd_mixin := uPred_fupd_mixin |}.
-
-Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
-Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
+Qed.
\ No newline at end of file

theories/base_logic/upred.v

 From iris.algebra Require Export cmra updates.
-From iris.bi Require Export derived_connectives updates.
+From iris.bi Require Export derived_connectives updates plainly.
 From stdpp Require Import finite.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
@@ -278,13 +278,13 @@ Definition uPred_wand_eq :
 (* Equivalently, this could be `∀ y, P n y`.  That's closer to the intuition
    of "embedding the step-indexed logic in Iris", but the two are equivalent
    because Iris is afine.  The following is easier to work with. *)
-Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
+Program Definition uPred_plainly_def {M} : Plainly (uPred M) := λ P,
   {| uPred_holds n x := P n ε |}.
 Solve Obligations with naive_solver eauto using uPred_mono, 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 :
-  @uPred_plainly = @uPred_plainly_def := seal_eq uPred_plainly_aux.
+Definition uPred_plainly_aux {M} : seal (@uPred_plainly_def M). by eexists. Qed.
+Definition uPred_plainly {M} := unseal (@uPred_plainly_aux M).
+Definition uPred_plainly_eq M :
+  @plainly _ uPred_plainly = @uPred_plainly_def M := seal_eq uPred_plainly_aux.
 
 Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
@@ -347,11 +347,11 @@ Definition unseal_eqs :=
   uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
   uPred_cmra_valid_eq, @uPred_bupd_eq).
 Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
-  unfold bi_emp; simpl;
+  unfold bi_emp; simpl; unfold sbi_emp; simpl;
   unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
-  bi_sep, bi_wand, bi_plainly, bi_persistently, sbi_internal_eq, sbi_later; simpl;
+  bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
   unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
-  sbi_internal_eq, sbi_sep, sbi_wand, sbi_plainly, sbi_persistently; simpl;
+  sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl;
   rewrite !unseal_eqs /=.
 End uPred_unseal.
 Import uPred_unseal.
@@ -361,7 +361,7 @@ Local Arguments uPred_holds {_} !_ _ _ /.
 Lemma uPred_bi_mixin (M : ucmraT) :
   BiMixin
     uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
-    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand uPred_plainly
+    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
     uPred_persistently.
 Proof.
   split.
@@ -398,9 +398,6 @@ Proof.
     intros n P P' HP Q Q' HQ; split=> n' x ??.
     unseal; split; intros HPQ x' n'' ???;
       apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
-  - (* NonExpansive uPred_plainly *)
-    intros n P1 P2 HP.
-    unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
   - (* NonExpansive uPred_persistently *)
     intros n P1 P2 HP.
     unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
@@ -460,32 +457,12 @@ Proof.
   - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
     intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
     eapply HPQR; eauto using cmra_validN_op_l.
-  - (* (P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q *)
-    intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
-  - (* bi_plainly P ⊢ bi_persistently P *)
-    unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
-  - (* bi_plainly P ⊢ bi_plainly (bi_plainly P) *)
-    unseal; split=> n x ?? //.
-  - (* (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a) *)
-    by unseal.
-  - (* (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q) *)
-    unseal; split=> /= n x ? HPQ n' x' ????.
-    eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
-    apply (HPQ n' x); eauto using cmra_validN_le.
-  - (* (bi_plainly P → bi_plainly Q) ⊢ bi_plainly (bi_plainly P → Q) *)
-    unseal; split=> /= n x ? HPQ n' x' ????.
-    eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
-    apply (HPQ n' x); eauto using cmra_validN_le.
-  - (* P ⊢ bi_plainly emp (ADMISSIBLE) *)
-    by unseal.
-  - (* bi_plainly P ∗ Q ⊢ bi_plainly P *)
-    intros P Q. move: (uPred_persistently P)=> P'.
-    unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
-      eauto using uPred_mono, cmra_includedN_l.
   - (* (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
   - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
     intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
+  - (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
+    by unseal.
   - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
     by unseal.
   - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
@@ -499,10 +476,10 @@ Proof.
     exists (core x), x; rewrite ?cmra_core_l; auto.
 Qed.
 
-Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin uPred_ofe_mixin
-  uPred_entails uPred_pure uPred_and uPred_or uPred_impl
-  (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
-  uPred_plainly uPred_persistently (@uPred_internal_eq M) uPred_later.
+Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
+  uPred_entails uPred_pure uPred_or uPred_impl
+  (@uPred_forall M) (@uPred_exist M) uPred_sep
+  uPred_persistently (@uPred_internal_eq M) uPred_later.
 Proof.
   split.
   - (* Contractive sbi_later *)
@@ -523,10 +500,6 @@ Proof.
     by unseal.
   - (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝ *)
     intros A a b ?. unseal; split=> n x ?; by apply (discrete_iff n).
-  - (* bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
-    unseal; split=> n x ? /= HPQ. split=> n' x' ??.
-    move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
-    move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
   - (* Next x ≡ Next y ⊢ ▷ (x ≡ y) *)
     by unseal.
   - (* ▷ (x ≡ y) ⊢ Next x ≡ Next y *)
@@ -550,10 +523,6 @@ Proof.
   - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
     intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
     exists x1, x2; eauto using dist_S.
-  - (* ▷ bi_plainly P ⊢ bi_plainly (▷ P) *)
-    by unseal.
-  - (* bi_plainly (▷ P) ⊢ ▷ bi_plainly P *)
-    by unseal.
   - (* ▷ bi_persistently P ⊢ bi_persistently (▷ P) *)
     by unseal.
   - (* bi_persistently (▷ P) ⊢ ▷ bi_persistently P *)
@@ -575,6 +544,46 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid.
 (* Latest notation *)
 Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
 
+Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
+Proof.
+  split.
+  - (* NonExpansive uPred_plainly *)
+    intros n P1 P2 HP.
+    unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
+  - (* (P ⊢ Q) → ■ P ⊢ ■ Q *)
+    intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
+  - (* ■ P ⊢ bi_persistently P *)
+    unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
+  - (* ■ P ⊢ ■ ■ P *)
+    unseal; split=> n x ?? //.
+  - (* (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a) *)
+    by unseal.
+  - (* (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q) *)
+    unseal; split=> /= n x ? HPQ n' x' ????.
+    eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
+    apply (HPQ n' x); eauto using cmra_validN_le.
+  - (* (■ P → ■ Q) ⊢ ■ (■ P → Q) *)
+    unseal; split=> /= n x ? HPQ n' x' ????.
+    eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
+    apply (HPQ n' x); eauto using cmra_validN_le.
+  - (* P ⊢ ■ emp (ADMISSIBLE) *)
+    by unseal.
+  - (* ■ P ∗ Q ⊢ ■ P *)
+    intros P Q. move: (uPred_persistently P)=> P'.
+    unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
+      eauto using uPred_mono, cmra_includedN_l.
+  - (* ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
+    unseal; split=> n x ? /= HPQ. split=> n' x' ??.
+    move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?.
+    move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver.
+  - (* ▷ ■ P ⊢ ■ ▷ P *)
+    by unseal.
+  - (* ■ ▷ P ⊢ ▷ ■ P *)
+    by unseal.
+Qed.
+Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
+  {| bi_plainly_mixin := uPred_plainly_mixin M |}.
+
 Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
 Proof.
   split.
@@ -593,12 +602,16 @@ Proof.
     { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
     exists (x' ⋅ x2); split; first by rewrite -assoc.
     exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
-  - unseal; split => n x Hnx /= Hng.
-    destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
-    eapply uPred_mono; eauto using ucmra_unit_leastN.
 Qed.
 Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
 
+Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
+Proof.
+  rewrite /BiBUpdPlainly. unseal; split => n x Hnx /= Hng.
+  destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
+  eapply uPred_mono; eauto using ucmra_unit_leastN.
+Qed.
+
 Module uPred.
 Include uPred_unseal.
 Section uPred.
@@ -630,7 +643,7 @@ Global Instance cmra_valid_proper {A : cmraT} :
 Global Instance uPred_affine : BiAffine (uPredI M) | 0.
 Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
 
-Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredI M).
+Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
 Proof. unfold BiPlainlyExist. by unseal. Qed.
 
 (** Limits *)
@@ -684,7 +697,7 @@ Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ (False : u
 Proof.
   intros Ha. unseal. split=> n x ??; apply Ha, cmra_validN_le with n; auto.
 Qed.
-Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ bi_plainly (✓ a : uPred M).
+Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ (✓ a : uPred M).
 Proof. by unseal. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ (✓ a : uPred M).
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.

theories/bi/bi.v

-From iris.bi Require Export derived_laws big_op updates embedding.
+From iris.bi Require Export derived_laws big_op updates plainly embedding.
 Set Default Proof Using "Type".
 
 Module Import bi.
@@ -16,4 +16,4 @@ Hint Resolve sep_elim_l sep_elim_r sep_mono : BI.
 Hint Immediate True_intro False_elim : BI.
 (*
 Hint Immediate iff_refl internal_eq_refl' : BI.
-*)
\ No newline at end of file
+*)

theories/bi/big_op.v

 From iris.algebra Require Export big_op.
 From iris.bi Require Export derived_laws.
+From iris.bi Require Import plainly.
 From stdpp Require Import countable fin_collections functions.
 Set Default Proof Using "Type".
 
@@ -125,10 +126,6 @@ Section sep_list.
     ⊢ ([∗ list] k↦x ∈ l, Φ k x) ∧ ([∗ list] k↦x ∈ l, Ψ k x).
   Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepL_plainly `{BiAffine PROP} Φ l :
-    bi_plainly ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, bi_plainly (Φ k x).
-  Proof. apply (big_opL_commute _). Qed.
-
   Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
     bi_persistently ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢
     [∗ list] k↦x ∈ l, bi_persistently (Φ k x).
@@ -163,16 +160,6 @@ Section sep_list.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   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.
@@ -278,10 +265,6 @@ Section and_list.
     ⊢ ([∧ list] k↦x ∈ l, Φ k x) ∧ ([∧ list] k↦x ∈ l, Ψ k x).
   Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_andL_plainly Φ l :
-    bi_plainly ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, bi_plainly (Φ k x).
-  Proof. apply (big_opL_commute _). Qed.
-
   Lemma big_andL_persistently Φ l :
     bi_persistently ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢
     [∧ list] k↦x ∈ l, bi_persistently (Φ k x).
@@ -299,19 +282,13 @@ Section and_list.
     - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
   Qed.
 
-  Global Instance big_andL_nil_plain Φ :
-    Plain ([∧ list] k↦x ∈ [], Φ k x).
-  Proof. simpl; apply _. Qed.
-  Global Instance big_andL_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_andL_nil_persistent Φ :
     Persistent ([∧ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
   Global Instance big_andL_persistent Φ l :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∧ list] k↦x ∈ l, Φ k x).
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
 End and_list.
 
 (** ** Big ops over finite maps *)
@@ -420,10 +397,6 @@ Section gmap.
     ⊢ ([∗ map] k↦x ∈ m, Φ k x) ∧ ([∗ map] k↦x ∈ m, Ψ k x).
   Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepM_plainly `{BiAffine PROP} Φ m :
-    bi_plainly ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, bi_plainly (Φ k x).
-  Proof. apply (big_opM_commute _). Qed.
-
   Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
     (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
       ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
@@ -464,12 +437,6 @@ Section gmap.
       by rewrite pure_True // True_impl.
   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.
@@ -596,10 +563,6 @@ Section gset.
     ([∗ set] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ set] y ∈ X, Φ y) ∧ ([∗ set] y ∈ X, Ψ y).
   Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepS_plainly `{BiAffine PROP} Φ X :
-    bi_plainly ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_plainly (Φ y).
-  Proof. apply (big_opS_commute _). Qed.
-
   Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
     bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_persistently (Φ y).
   Proof. apply (big_opS_commute _). Qed.
@@ -633,12 +596,6 @@ Section gset.
       by rewrite pure_True ?True_impl; last set_solver.
   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.
@@ -714,21 +671,11 @@ Section gmultiset.
     ([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y).
   Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
 
-  Lemma big_sepMS_plainly `{BiAffine PROP} Φ X :
-    bi_plainly ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, bi_plainly (Φ y).
-  Proof. apply (big_opMS_commute _). Qed.
-
   Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
     bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
       [∗ mset] y ∈ X, bi_persistently (Φ 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.
@@ -773,6 +720,34 @@ Section list.
   Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
     TCForall Timeless Ps → Timeless ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepL_plainly `{!BiAffine PROP} Φ l :
+      ■ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, ■ (Φ k x).
+    Proof. apply (big_opL_commute _). Qed.
+
+    Global Instance big_sepL_nil_plain `{!BiAffine PROP} Φ :
+      Plain ([∗ list] k↦x ∈ [], Φ k x).
+    Proof. simpl; apply _. Qed.
+
+    Global Instance big_sepL_plain `{!BiAffine PROP} Φ l :
+      (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x).
+    Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
+    Lemma big_andL_plainly Φ l :
+      ■ ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, ■ (Φ k x).
+    Proof. apply (big_opL_commute _). Qed.
+
+    Global Instance big_andL_nil_plain Φ :
+      Plain ([∧ list] k↦x ∈ [], Φ k x).
+    Proof. simpl; apply _. Qed.
+
+    Global Instance big_andL_plain Φ l :
+      (∀ k x, Plain (Φ k x)) → Plain ([∧ list] k↦x ∈ l, Φ k x).
+    Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  End plainly.
 End list.
 
 (** ** Big ops over finite maps *)
@@ -795,6 +770,21 @@ Section gmap.
   Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
     (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepM_plainly `{BiAffine PROP} Φ m :
+      ■ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, ■ (Φ k x).
+    Proof. apply (big_opM_commute _). Qed.
+
+    Global Instance big_sepM_empty_plain `{BiAffine PROP} Φ :
+      Plain ([∗ map] k↦x ∈ ∅, Φ k x).
+    Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
+    Global Instance big_sepM_plain `{BiAffine PROP} Φ m :
+      (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x  ∈ m, Φ k x).
+    Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed.
+  End plainly.
 End gmap.
 
 (** ** Big ops over finite sets *)
@@ -817,6 +807,20 @@ Section gset.
   Global Instance big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
     (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepS_plainly `{BiAffine PROP} Φ X :
+      ■ ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, ■ (Φ y).
+    Proof. apply (big_opS_commute _). Qed.
+
+    Global Instance big_sepS_empty_plain `{BiAffine PROP} Φ : Plain ([∗ set] x ∈ ∅, Φ x).
+    Proof. rewrite /big_opS elements_empty. apply _. Qed.
+    Global Instance big_sepS_plain `{BiAffine PROP} Φ X :
+      (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x).
+    Proof. rewrite /big_opS. apply _. Qed.
+  End plainly.
 End gset.
 
 (** ** Big ops over finite multisets *)
@@ -839,6 +843,20 @@ Section gmultiset.
   Global Instance big_sepMS_timeless `{!Timeless (emp%I : PROP)} Φ X :
     (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepMS_plainly `{BiAffine PROP} Φ X :
+      ■ ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, ■ (Φ y).
+    Proof. apply (big_opMS_commute _). Qed.
+
+    Global Instance big_sepMS_empty_plain `{BiAffine PROP} Φ : Plain ([∗ mset] x ∈ ∅, Φ x).
+    Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
+    Global Instance big_sepMS_plain `{BiAffine PROP} Φ X :
+      (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x).
+    Proof. rewrite /big_opMS. apply _. Qed.
+  End plainly.
 End gmultiset.
 End sbi_big_op.
 End bi.

theories/bi/derived_connectives.v

@@ -13,12 +13,6 @@ Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Instance: Params (@bi_wand_iff) 1.
 Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
 
-Class Plain {PROP : bi} (P : PROP) := plain : P ⊢ bi_plainly P.
-Arguments Plain {_} _%I : simpl never.
-Arguments plain {_} _%I {_}.
-Hint Mode Plain + ! : typeclass_instances.
-Instance: Params (@Plain) 1.
-
 Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
 Arguments Persistent {_} _%I : simpl never.
 Arguments persistent {_} _%I {_}.
@@ -31,8 +25,6 @@ Instance: Params (@bi_affinely) 1.
 Typeclasses Opaque bi_affinely.
 Notation "□ P" := (bi_affinely (bi_persistently P))%I
   (at level 20, right associativity) : bi_scope.
-Notation "■ P" := (bi_affinely (bi_plainly P))%I
-  (at level 20, right associativity) : bi_scope.
 
 Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
 Arguments Affine {_} _%I : simpl never.
@@ -45,11 +37,6 @@ Existing Instance absorbing_bi | 0.
 Class BiPositive (PROP : bi) :=
   bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
 
-Class BiPlainlyExist (PROP : bi) :=
-  plainly_exist_1 A (Ψ : A → PROP) :
-    bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a).
-Arguments plainly_exist_1 _ {_ _} _.
-
 Definition