From 334b689e6c86d711e0d1cce8027bf1666d1b9d50 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Sat, 20 Oct 2018 09:01:42 -0400
Subject: [PATCH] Use plainly modality instead of typeclass in BiFUpdPlainly
 interface.

---
 theories/base_logic/lib/fancy_updates.v |  8 ++++----
 theories/bi/monpred.v                   |  8 ++++----
 theories/bi/updates.v                   | 16 ++++++++++++----
 3 files changed, 20 insertions(+), 12 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 03397a4e2..2d910d657 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/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.
 
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index cd936f5db..5a3be2fc9 100644
--- a/theories/bi/monpred.v
+++ b/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).
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 8df0ab3db..50827b359 100644
--- a/theories/bi/updates.v
+++ b/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.
-- 
GitLab