Use plainly modality instead of typeclass in BiFUpdPlainly interface.

theories/base_logic/lib/fancy_updates.v

@@ -41,12 +41,12 @@ Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed
 Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
 Proof.
   split.
-  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q ?) "HQP HQ [Hw HE]".
-    iAssert (◇ P)%I as "#>$".
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q) "HQP HQ [Hw HE]".
+    iAssert (◇ ■ P)%I as "#>HP'".
     { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
     by iFrame.
-  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (p E1 E2 P ?) "HP [Hw HE]".
-    iAssert (▷?p ◇ P)%I with "[-]" as "#$"; last by iFrame.
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (p E1 E2 P) "HP [Hw HE]".
+    iAssert (▷?p ◇ ■ P)%I with "[-]" as "#HP'"; last by (rewrite plainly_elim; iFrame).
     iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
 Qed.
 

theories/bi/monpred.v

@@ -957,10 +957,10 @@ Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Q
 Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredSI.
 Proof.
   split; rewrite monPred_fupd_eq; unseal.
-  - intros E P Q ?. split=>/= i. do 3 f_equiv.
-    apply fupd_plain_weak; apply _.
-  - intros p E1 E2 P ?. split=>/= i. specialize (later_fupd_plain p) => HFP.
-    destruct p; simpl; [ unseal | ]; apply HFP, _.
+  - intros E P Q. split=>/= i. do 3 f_equiv.
+    rewrite monPred_at_plainly (bi.forall_elim _) fupd_plainly_weak //=.
+  - intros p E1 E2 P; split=>/= i; specialize (later_fupd_plainly p) => HFP.
+    destruct p; simpl; [ unseal | ]; rewrite monPred_at_plainly (bi.forall_elim _); apply HFP.
 Qed.
 
 Global Instance plainly_objective `{BiPlainly PROP} P : Objective (■ P).

theories/bi/updates.v

@@ -78,10 +78,10 @@ Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
 Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
 
 Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
-  fupd_plain_weak E (P Q : PROP) `{!Plain P} :
-    (Q ={E}=∗ P) -∗ Q ={E}=∗ Q ∗ P;
-  later_fupd_plain p E1 E2 (P : PROP) `{!Plain P} :
-    (▷?p |={E1, E2}=> P) ={E1}=∗ ▷?p ◇ P;
+  fupd_plainly_weak E (P Q : PROP) :
+    (Q ={E}=∗ ■ P) -∗ Q ={E}=∗ Q ∗ P;
+  later_fupd_plainly p E1 E2 (P : PROP) :
+    (▷?p |={E1, E2}=> ■ P) ={E1}=∗ ▷?p ◇ P;
 }.
 Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
@@ -272,6 +272,14 @@ Section fupd_derived.
     intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
   Qed.
 
+  Lemma fupd_plain_weak `{BiPlainly PROP, !BiFUpdPlainly PROP} E P Q `{!Plain P}:
+    (Q ={E}=∗ P) -∗ Q ={E}=∗ Q ∗ P.
+  Proof. by rewrite {1}(plain P) fupd_plainly_weak. Qed.
+
+  Lemma later_fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} p E1 E2 P `{!Plain P} :
+    (▷?p |={E1, E2}=> P) ={E1}=∗ ▷?p ◇ P.
+  Proof. by rewrite {1}(plain P) later_fupd_plainly. Qed.
+
   Lemma fupd_plain_strong `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 P `{!Plain P} :
     (|={E1, E2}=> P) ={E1}=∗ ◇ P.
   Proof. by apply (later_fupd_plain false). Qed.