From 4b43fcc26d005c3cde83a0a1fbd407cd268d0f2d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Feb 2018 17:21:09 +0100
Subject: [PATCH] make BUpdFacts depend on SBI

---
 theories/base_logic/upred.v          |   2 +-
 theories/bi/monpred.v                |  76 ++++++++---------
 theories/bi/updates.v                |  12 +--
 theories/proofmode/class_instances.v | 123 ++++++++++++++-------------
 theories/proofmode/monpred.v         |  57 +++++++------
 5 files changed, 136 insertions(+), 134 deletions(-)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index e89357f1e..d551bfb72 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -677,7 +677,7 @@ Lemma ofe_fun_validI `{Finite A} {B : A → ucmraT} (g : ofe_fun B) :
 Proof. by uPred.unseal. Qed.
 
 (* Basic update modality *)
-Global Instance bupd_facts : BUpdFacts (uPredI M).
+Global Instance bupd_facts : BUpdFacts (uPredSI M).
 Proof.
   split.
   - intros n P Q HPQ.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 69b2d365f..ec18ef8dd 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -252,11 +252,11 @@ Ltac unseal :=
   unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
          monPred_absolutely, monPred_relatively, monPred_upclosed, bi_and, bi_or,
          bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand,
-         bi_persistently, bi_affinely, sbi_later;
+         bi_persistently, bi_affinely, bi_plainly, 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_persistently, sbi_plainly,
-         bi_plainly; simpl;
+         sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently, sbi_plainly;
+  simpl;
   unfold monPred_pure, monPred_emp, monPred_internal_eq, monPred_plainly; simpl;
   rewrite !unseal_eqs /=.
 End MonPred.
@@ -472,22 +472,6 @@ Proof.
     by apply bi.forall_intro. by rewrite bi.forall_elim.
 Qed.
 
-Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredI.
-Proof.
-  split; unseal; unfold monPred_bupd_def, monPred_upclosed.
-  - intros n P Q HPQ. split=>/= i. by repeat f_equiv.
-  - intros P. split=>/= i. apply bi.forall_intro=>?. rewrite bi.pure_impl_forall.
-    apply bi.forall_intro=><-. apply bupd_intro.
-  - intros P Q HPQ. split=>/= i. by repeat f_equiv.
-  - intros P. split=>/= i. do 3 f_equiv. rewrite -(bupd_trans (P _))
-      bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
-  - intros P Q. split=> /= i. apply bi.forall_intro=>?.
-    rewrite bi.pure_impl_forall. apply bi.forall_intro=><-.
-    rewrite -bupd_frame_r bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
-  - intros P. split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall
-      bi.forall_elim // -bi.plainly_forall bupd_plainly bi.forall_elim //.
-Qed.
-
 Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP).
 Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
 Global Instance monPred_absolutely_proper : Proper ((≡) ==> (≡)) (@monPred_absolutely I PROP).
@@ -564,12 +548,6 @@ Lemma monPred_at_absolutely i P : (∀ᵢ P) i ⊣⊢ ∀ j, P j.
 Proof. by unseal. Qed.
 Lemma monPred_at_ex i P : (∃ᵢ P) i ⊣⊢ ∃ j, P j.
 Proof. by unseal. Qed.
-Lemma monPred_at_bupd `{BUpdFacts PROP} i P : (|==> P) i ⊣⊢ |==> P i.
-Proof.
-  unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
-  - rewrite !bi.forall_elim //.
-  - do 2 apply bi.forall_intro=>?. by do 2 f_equiv.
-Qed.
 Lemma monPred_at_persistently_if i p P :
   bi_persistently_if p P i ⊣⊢ bi_persistently_if p (P i).
 Proof. destruct p=>//=. apply monPred_at_persistently. Qed.
@@ -709,10 +687,6 @@ Global Instance persistently_absolute P `{!Absolute P} :
   Absolute (bi_persistently P).
 Proof. intros ??. unseal. by rewrite absolute_at. Qed.
 
-Global Instance bupd_absolute `{BUpdFacts PROP} P `{!Absolute P} :
-  Absolute (|==> P)%I.
-Proof. intros ??. by rewrite !monPred_at_bupd absolute_at. Qed.
-
 Global Instance affinely_absolute P `{!Absolute P} : Absolute (bi_affinely P).
 Proof. rewrite /bi_affinely. apply _. Qed.
 Global Instance absorbingly_absolute P `{!Absolute P} :
@@ -740,15 +714,6 @@ Proof.
   eapply bi.pure_elim; [apply bi.and_elim_l|]=>?. rewrite bi.and_elim_r. by f_equiv.
 Qed.
 
-(** bupd *)
-Lemma monPred_bupd_embed `{BUpdFacts PROP} (P : PROP) :
-  ⎡|==> P⎤ ⊣⊢ bupd (PROP:=monPredI) ⎡P⎤.
-Proof.
-  unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
-  - by do 2 apply bi.forall_intro=>?.
-  - rewrite !bi.forall_elim //.
-Qed.
-
 (** Big op *)
 Global Instance monPred_at_monoid_and_homomorphism i :
   MonoidHomomorphism bi_and bi_and (≡) (flip monPred_at i).
@@ -847,6 +812,41 @@ Local Notation monPredSI := (monPredSI I PROP).
 Implicit Types i : I.
 Implicit Types P Q : monPred.
 
+(** bupd *)
+Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredSI.
+Proof.
+  split; unseal; unfold monPred_bupd_def, monPred_upclosed.
+  - intros n P Q HPQ. split=>/= i. by repeat f_equiv.
+  - intros P. split=>/= i. apply bi.forall_intro=>?. rewrite bi.pure_impl_forall.
+    apply bi.forall_intro=><-. apply bupd_intro.
+  - intros P Q HPQ. split=>/= i. by repeat f_equiv.
+  - intros P. split=>/= i. do 3 f_equiv. rewrite -(bupd_trans (P _))
+      bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
+  - intros P Q. split=> /= i. apply bi.forall_intro=>?.
+    rewrite bi.pure_impl_forall. apply bi.forall_intro=><-.
+    rewrite -bupd_frame_r bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
+  - intros P. split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall
+      bi.forall_elim // -bi.plainly_forall bupd_plainly bi.forall_elim //.
+Qed.
+
+Lemma monPred_at_bupd `{BUpdFacts PROP} i P : (|==> P) i ⊣⊢ |==> P i.
+Proof.
+  unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
+  - rewrite !bi.forall_elim //.
+  - do 2 apply bi.forall_intro=>?. by do 2 f_equiv.
+Qed.
+Global Instance bupd_absolute `{BUpdFacts PROP} P `{!Absolute P} :
+  Absolute (|==> P)%I.
+Proof. intros ??. by rewrite !monPred_at_bupd absolute_at. Qed.
+
+Lemma monPred_bupd_embed `{BUpdFacts PROP} (P : PROP) :
+  ⎡|==> P⎤ ⊣⊢ bupd (PROP:=monPredSI) ⎡P⎤.
+Proof.
+  unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
+  - by do 2 apply bi.forall_intro=>?.
+  - rewrite !bi.forall_elim //.
+Qed.
+
 Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
 Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
 Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 3592d4f96..e84991291 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -51,13 +51,13 @@ Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I
 
 (** BUpd facts  *)
 
-Class BUpdFacts (PROP : bi) `{BUpd PROP} : Prop :=
+Class BUpdFacts (PROP : sbi) `{BUpd PROP} : Prop :=
   { bupd_ne :> NonExpansive bupd;
-    bupd_intro P : P ==∗ P;
-    bupd_mono P Q : (P ⊢ Q) → (|==> P) ==∗ Q;
-    bupd_trans P : (|==> |==> P) ==∗ P;
-    bupd_frame_r P R : (|==> P) ∗ R ==∗ P ∗ R;
-    bupd_plainly P : (|==> bi_plainly P) -∗ P }.
+    bupd_intro (P : PROP) : P ==∗ P;
+    bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q;
+    bupd_trans (P : PROP) : (|==> |==> P) ==∗ P;
+    bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R;
+    bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P }.
 Hint Mode BUpdFacts ! - : typeclass_instances.
 
 Section bupd_derived.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 1a346de18..d5bc2467b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -123,10 +123,6 @@ Global Instance from_assumption_forall {A} p (Φ : A → PROP) Q x :
   FromAssumption p (Φ x) Q → FromAssumption p (∀ x, Φ x) Q.
 Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
 
-Global Instance from_assumption_bupd `{BUpdFacts PROP} p P Q :
-  FromAssumption p P Q → FromAssumption p P (|==> Q).
-Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
-
 (* IntoPure *)
 Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
 Proof. by rewrite /IntoPure. Qed.
@@ -249,10 +245,6 @@ Global Instance from_pure_embed `{BiEmbedding PROP PROP'} a P φ :
   FromPure a P φ → FromPure a ⎡P⎤ φ.
 Proof. rewrite /FromPure=> <-. by rewrite bi_embed_affinely_if bi_embed_pure. Qed.
 
-Global Instance from_pure_bupd `{BUpdFacts PROP} a P φ :
-  FromPure a P φ → FromPure a (|==> P) φ.
-Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
-
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
   IntoPersistent true P Q → IntoPersistent p (bi_persistently P) Q | 0.
@@ -416,27 +408,6 @@ Proof.
           -bi_embed_wand => -> //.
 Qed.
 
-Global Instance into_wand_bupd `{BUpdFacts PROP} p q R P Q :
-  IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
-Proof.
-  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
-  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
-Qed.
-
-Global Instance into_wand_bupd_persistent `{BUpdFacts PROP} p q R P Q :
-  IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q).
-Proof.
-  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
-  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
-Qed.
-
-Global Instance into_wand_bupd_args `{BUpdFacts PROP} p q R P Q :
-  IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q).
-Proof.
-  rewrite /IntoWand' /IntoWand /= => ->.
-  apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
-Qed.
-
 (* FromWand *)
 Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
 Proof. by rewrite /FromWand. Qed.
@@ -543,10 +514,6 @@ Global Instance from_sep_big_sepL_app {A} (Φ : nat → A → PROP) l1 l2 :
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. by rewrite /FromSep big_opL_app. Qed.
 
-Global Instance from_sep_bupd `{BUpdFacts PROP} P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
-Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
-
 (* IntoAnd *)
 Global Instance into_and_and p P Q : IntoAnd p (P ∧ Q) P Q | 10.
 Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
@@ -688,12 +655,6 @@ Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
 Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
 Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
-Global Instance from_or_bupd `{BUpdFacts PROP} P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
-Proof.
-  rewrite /FromOr=><-.
-  apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
-Qed.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
@@ -738,11 +699,6 @@ Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
 Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
 Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed.
-Global Instance from_exist_bupd `{BUpdFacts PROP} {A} P (Φ : A → PROP) :
-  FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
-Proof.
-  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-Qed.
 
 (* IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
@@ -866,8 +822,6 @@ Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
 Proof.
   rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
-Global Instance add_modal_bupd `{BUpdFacts PROP} P Q : AddModal (|==> P) P (|==> Q).
-Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
 
 (* Frame *)
 Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
@@ -1087,29 +1041,14 @@ Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
   (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 
-Global Instance frame_bupd `{BUpdFacts PROP} p R P Q :
-  Frame p R P Q → Frame p R (|==> P) (|==> Q).
-Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
-
 (* FromModal *)
 Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
 Proof. apply absorbingly_intro. Qed.
 Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
   FromModal P Q → FromModal ⎡P⎤ ⎡Q⎤.
 Proof. by rewrite /FromModal=> ->. Qed.
-Global Instance from_modal_bupd `{BUpdFacts PROP} P : FromModal (|==> P) P.
-Proof. apply bupd_intro. Qed.
 
 (* ElimModal *)
-Global Instance elim_modal_bupd `{BUpdFacts PROP} P Q :
-  ElimModal True (|==> P) P (|==> Q) (|==> Q).
-Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
-Global Instance elim_modal_bupd_plain_goal `{BUpdFacts PROP} P Q :
-  Plain Q → ElimModal True (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
-Global Instance elim_modal_bupd_plain `{BUpdFacts PROP} P Q :
-  Plain P → ElimModal True (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
 
 (* AsValid *)
 Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
@@ -1146,6 +1085,10 @@ Proof. rewrite /FromAssumption=>->. apply laterN_intro. Qed.
 Global Instance from_assumption_except_0 p P Q :
   FromAssumption p P Q → FromAssumption p P (◇ Q)%I.
 Proof. rewrite /FromAssumption=>->. apply except_0_intro. Qed.
+
+Global Instance from_assumption_bupd `{BUpdFacts PROP} p P Q :
+  FromAssumption p P Q → FromAssumption p P (|==> Q).
+Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
 Global Instance from_assumption_fupd `{FUpdFacts PROP} E p P Q :
   FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
@@ -1160,6 +1103,10 @@ Global Instance from_pure_laterN a n P φ : FromPure a P φ → FromPure a (▷^
 Proof. rewrite /FromPure=> ->. apply laterN_intro. Qed.
 Global Instance from_pure_except_0 a P φ : FromPure a P φ → FromPure a (◇ P) φ.
 Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
+
+Global Instance from_pure_bupd `{BUpdFacts PROP} a P φ :
+  FromPure a P φ → FromPure a (|==> P) φ.
+Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
 Global Instance from_pure_fupd `{FUpdFacts PROP} a E P φ :
   FromPure a P φ → FromPure a (|={E}=> P) φ.
 Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
@@ -1200,6 +1147,25 @@ Proof.
              (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
 Qed.
 
+Global Instance into_wand_bupd `{BUpdFacts PROP} p q R P Q :
+  IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
+Proof.
+  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
+  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
+Qed.
+Global Instance into_wand_bupd_persistent `{BUpdFacts PROP} p q R P Q :
+  IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q).
+Proof.
+  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
+  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
+Qed.
+Global Instance into_wand_bupd_args `{BUpdFacts PROP} p q R P Q :
+  IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q).
+Proof.
+  rewrite /IntoWand' /IntoWand /= => ->.
+  apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
+Qed.
+
 Global Instance into_wand_fupd `{FUpdFacts PROP} E p q R P Q :
   IntoWand false false R P Q →
   IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
@@ -1241,6 +1207,10 @@ Proof. rewrite /FromSep=> <-. by rewrite laterN_sep. Qed.
 Global Instance from_sep_except_0 P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /FromSep=><-. by rewrite except_0_sep. Qed.
+
+Global Instance from_sep_bupd `{BUpdFacts PROP} P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
+Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
 Global Instance from_sep_fupd `{FUpdFacts PROP} E P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
 Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.
@@ -1301,6 +1271,13 @@ Proof. rewrite /FromOr=><-. by rewrite laterN_or. Qed.
 Global Instance from_or_except_0 P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /FromOr=><-. by rewrite except_0_or. Qed.
+
+Global Instance from_or_bupd `{BUpdFacts PROP} P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
+Proof.
+  rewrite /FromOr=><-.
+  apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
+Qed.
 Global Instance from_or_fupd `{FUpdFacts PROP} E1 E2 P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
 Proof.
@@ -1333,6 +1310,12 @@ Qed.
 Global Instance from_exist_except_0 {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (◇ P) (λ a, ◇ (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite except_0_exist_2. Qed.
+
+Global Instance from_exist_bupd `{BUpdFacts PROP} {A} P (Φ : A → PROP) :
+  FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
+Proof.
+  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
+Qed.
 Global Instance from_exist_fupd `{FUpdFacts PROP} {A} E1 E2 P (Φ : A → PROP) :
   FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
 Proof.
@@ -1401,6 +1384,9 @@ Global Instance from_modal_later P : FromModal (â–· P) P.
 Proof. apply later_intro. Qed.
 Global Instance from_modal_except_0 P : FromModal (â—‡ P) P.
 Proof. apply except_0_intro. Qed.
+
+Global Instance from_modal_bupd `{BUpdFacts PROP} P : FromModal (|==> P) P.
+Proof. apply bupd_intro. Qed.
 Global Instance from_modal_fupd E P `{FUpdFacts PROP} : FromModal (|={E}=> P) P.
 Proof. rewrite /FromModal. apply fupd_intro. Qed.
 
@@ -1456,6 +1442,15 @@ Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I).
   by rewrite (into_except_0 P) -except_0_sep wand_elim_r.
 Qed.
+Global Instance elim_modal_bupd `{BUpdFacts PROP} P Q :
+  ElimModal True (|==> P) P (|==> Q) (|==> Q).
+Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
+Global Instance elim_modal_bupd_plain_goal `{BUpdFacts PROP} P Q :
+  Plain Q → ElimModal True (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
+Global Instance elim_modal_bupd_plain `{BUpdFacts PROP} P Q :
+  Plain P → ElimModal True (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
 Global Instance elim_modal_bupd_fupd `{FUpdFacts PROP} E1 E2 P Q :
   ElimModal True (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
 Proof.
@@ -1489,6 +1484,9 @@ Proof.
   intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I).
   by rewrite -except_0_sep wand_elim_r except_0_later.
 Qed.
+
+Global Instance add_modal_bupd `{BUpdFacts PROP} P Q : AddModal (|==> P) P (|==> Q).
+Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
 Global Instance add_modal_fupd `{FUpdFacts PROP} E1 E2 P Q :
   AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
 Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
@@ -1514,6 +1512,9 @@ Proof.
   by rewrite later_affinely_persistently_if_2 later_sep.
 Qed.
 
+Global Instance frame_bupd `{BUpdFacts PROP} p R P Q :
+  Frame p R P Q → Frame p R (|==> P) (|==> Q).
+Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
 Global Instance frame_fupd `{FUpdFacts PROP} p E1 E2 R P Q :
   Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
 Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 0735be61a..790f15a0f 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -102,9 +102,6 @@ Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) ⌜i ⊑
 Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
 Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
 Proof. by rewrite /MakeMonPredAt. Qed.
-Global Instance make_monPred_at_bupd `{BUpdFacts PROP} i P 𝓟 :
-  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
-Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
 
 Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
   MakeMonPredAt i P 𝓟 → IsBiIndexRel j i → FromAssumption p (P j) 𝓟.
@@ -369,31 +366,6 @@ Global Instance from_modal_monPred_at i P Q 𝓠 :
   FromModal P Q → MakeMonPredAt i Q 𝓠 → FromModal (P i) 𝓠.
 Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
 
-Global Instance elim_modal_embed_bupd_goal `{BUpdFacts PROP} φ P P' 𝓠 𝓠' :
-  ElimModal φ P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠'⎤)%I →
-  ElimModal φ P P' ⎡|==> 𝓠⎤ ⎡|==> 𝓠'⎤.
-Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed.
-Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} φ 𝓟 P' Q Q' :
-  ElimModal φ (|==> ⎡𝓟⎤)%I P' Q Q' →
-  ElimModal φ ⎡|==> 𝓟⎤ P' Q Q'.
-Proof. by rewrite /ElimModal monPred_bupd_embed. Qed.
-
-Global Instance add_modal_embed_bupd_goal `{BUpdFacts PROP} P P' 𝓠 :
-  AddModal P P' (|==> ⎡𝓠⎤)%I → AddModal P P' ⎡|==> 𝓠⎤.
-Proof. by rewrite /AddModal !monPred_bupd_embed. Qed.
-
-Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q Q' i :
-  ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i) →
-  ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
-Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
-Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} φ P 𝓟' 𝓠 𝓠' i:
-  ElimModal φ (|==> P i) 𝓟' 𝓠 𝓠' →
-  ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
-Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
-
-Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q i :
-  AddModal 𝓟 𝓟' (|==> Q i)%I → AddModal 𝓟 𝓟' ((|==> Q) i).
-Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
 End bi.
 
 (* When P and/or Q are evars when doing typeclass search on [IntoWand
@@ -442,6 +414,9 @@ Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
 Global Instance make_monPred_at_laterN i n P 𝓠 :
   MakeMonPredAt i P 𝓠 → MakeMonPredAt i (▷^n P)%I (▷^n 𝓠)%I.
 Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
+Global Instance make_monPred_at_bupd `{BUpdFacts PROP} i P 𝓟 :
+  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
+Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
 Global Instance make_monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P 𝓟 :
   MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> 𝓟)%I.
 Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
@@ -470,6 +445,32 @@ Proof.
   by rewrite monPred_at_later.
 Qed.
 
+Global Instance elim_modal_embed_bupd_goal `{BUpdFacts PROP} φ P P' 𝓠 𝓠' :
+  ElimModal φ P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠'⎤)%I →
+  ElimModal φ P P' ⎡|==> 𝓠⎤ ⎡|==> 𝓠'⎤.
+Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed.
+Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} φ 𝓟 P' Q Q' :
+  ElimModal φ (|==> ⎡𝓟⎤)%I P' Q Q' →
+  ElimModal φ ⎡|==> 𝓟⎤ P' Q Q'.
+Proof. by rewrite /ElimModal monPred_bupd_embed. Qed.
+
+Global Instance add_modal_embed_bupd_goal `{BUpdFacts PROP} P P' 𝓠 :
+  AddModal P P' (|==> ⎡𝓠⎤)%I → AddModal P P' ⎡|==> 𝓠⎤.
+Proof. by rewrite /AddModal !monPred_bupd_embed. Qed.
+
+Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q Q' i :
+  ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i) →
+  ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
+Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
+Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} φ P 𝓟' 𝓠 𝓠' i:
+  ElimModal φ (|==> P i) 𝓟' 𝓠 𝓠' →
+  ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
+Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
+
+Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q i :
+  AddModal 𝓟 𝓟' (|==> Q i)%I → AddModal 𝓟 𝓟' ((|==> Q) i).
+Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
+
 Global Instance elim_modal_embed_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 P P' 𝓠 𝓠' :
   ElimModal φ P P' (|={E1,E3}=> ⎡𝓠⎤)%I (|={E2,E3}=> ⎡𝓠'⎤)%I →
   ElimModal φ P P' ⎡|={E1,E3}=> 𝓠⎤ ⎡|={E2,E3}=> 𝓠'⎤.
-- 
GitLab