Add classes BiEmbedFUpd and BiEmbedBUpd for the interractions between embeddings and updates.

theories/bi/embedding.v

 From iris.algebra Require Import monoid.
-From iris.bi Require Import interface derived_laws big_op plainly.
+From iris.bi Require Import interface derived_laws big_op plainly updates.
 From stdpp Require Import hlist.
 
 Class Embed (A B : Type) := embed : A → B.
@@ -41,6 +41,20 @@ Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
 Hint Mode SbiEmbed ! - - : typeclass_instances.
 Hint Mode SbiEmbed - ! - : typeclass_instances.
 
+Class BiEmbedBUpd (PROP1 PROP2 : bi)
+      `{BiEmbed PROP1 PROP2, BiBUpd PROP1, BiBUpd PROP2} := {
+  embed_bupd  P : ⎡|==> P⎤ ⊣⊢ bupd (PROP:=PROP2) ⎡P⎤
+}.
+Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
+Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
+
+Class BiEmbedFUpd (PROP1 PROP2 : sbi)
+      `{BiEmbed PROP1 PROP2, BiFUpd PROP1, BiFUpd PROP2} := {
+  embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢ fupd (PROP:=PROP2) E1 E2 ⎡P⎤
+}.
+Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
+Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
+
 Section embed_laws.
   Context `{BiEmbed PROP1 PROP2}.
   Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).

theories/bi/monpred.v

@@ -845,10 +845,11 @@ Global Instance bupd_absolute `{BiBUpd PROP} P `{!Absolute P} :
   Absolute (|==> P)%I.
 Proof. intros ??. by rewrite !monPred_at_bupd absolute_at. Qed.
 
-Lemma monPred_bupd_embed `{BiBUpd PROP} (P : PROP) :
-  ⎡|==> P⎤ ⊣⊢ bupd (PROP:=monPredI) ⎡P⎤.
+Global Instance monPred_bi_embed_bupd `{BiBUpd PROP} :
+  BiEmbedBUpd PROP monPredI.
 Proof.
-  unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
+  split. 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.
@@ -937,6 +938,14 @@ Proof.
     do 2 setoid_rewrite bi.later_forall. do 4 f_equiv. apply later_fupd_plain, _.
 Qed.
 
+Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredSI.
+Proof.
+  split. 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.
+
 (** Unfolding lemmas *)
 Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
 Proof. by unseal. Qed.
@@ -955,14 +964,6 @@ Qed.
 Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
 Proof. by unseal. Qed.
 
-Lemma monPred_fupd_embed `{BiFUpd PROP} E1 E2 (P : PROP) :
-  ⎡|={E1,E2}=> P⎤ ⊣⊢ fupd E1 E2 (PROP:=monPred) ⎡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.
-
 Lemma monPred_equivI {PROP' : sbi} P Q :
   sbi_internal_eq (PROP:=PROP') P Q ⊣⊢ ∀ i, P i ≡ Q i.
 Proof.

theories/proofmode/class_instances.v

@@ -702,6 +702,21 @@ Proof.
   by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
 Qed.
 
+Global Instance elim_modal_bupd `{BiBUpd 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_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
+       φ (P P' : PROP') (Q Q' : PROP) :
+  ElimModal φ P P' (|==> ⎡Q⎤)%I (|==> ⎡Q'⎤)%I →
+  ElimModal φ P P' ⎡|==> Q⎤ ⎡|==> Q'⎤.
+Proof. by rewrite /ElimModal !embed_bupd. Qed.
+Global Instance elim_modal_embed_bupd_hyp `{BiEmbedBUpd PROP PROP'}
+       φ (P : PROP) (P' Q Q' : PROP') :
+  ElimModal φ (|==> ⎡P⎤)%I P' Q Q' →
+  ElimModal φ ⎡|==> P⎤ P' Q Q'.
+Proof. by rewrite /ElimModal !embed_bupd. Qed.
+
 (* AddModal *)
 Global Instance add_modal_wand P P' Q R :
   AddModal P P' Q → AddModal P P' (R -∗ Q).
@@ -714,6 +729,10 @@ 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_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
+       (P P' : PROP') (Q : PROP) :
+  AddModal P P' (|==> ⎡Q⎤)%I → AddModal P P' ⎡|==> Q⎤.
+Proof. by rewrite /AddModal !embed_bupd. Qed.
 
 (* Frame *)
 Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
@@ -1445,9 +1464,7 @@ 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 `{BiBUpd 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 `{BiBUpdPlainly 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.
@@ -1459,10 +1476,22 @@ Global Instance elim_modal_bupd_fupd `{BiBUpdFUpd PROP} E1 E2 P Q :
 Proof.
   by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
 Qed.
+
 Global Instance elim_modal_fupd_fupd `{BiFUpd PROP} E1 E2 E3 P Q :
   ElimModal True (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
 Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 
+Global Instance elim_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
+       φ E1 E2 E3 (P P' : PROP') (Q Q' : PROP) :
+  ElimModal φ P P' (|={E1,E3}=> ⎡Q⎤)%I (|={E2,E3}=> ⎡Q'⎤)%I →
+  ElimModal φ P P' ⎡|={E1,E3}=> Q⎤ ⎡|={E2,E3}=> Q'⎤.
+Proof. by rewrite /ElimModal !embed_fupd. Qed.
+Global Instance elim_modal_embed_fupd_hyp `{BiEmbedFUpd PROP PROP'}
+       φ E1 E2 (P : PROP) (P' Q Q' : PROP') :
+  ElimModal φ (|={E1,E2}=> ⎡P⎤)%I P' Q Q' →
+  ElimModal φ ⎡|={E1,E2}=> P⎤ P' Q Q'.
+Proof. by rewrite /ElimModal embed_fupd. Qed.
+
 (* AddModal *)
 (* High priority to add a ▷ rather than a ◇ when P is timeless. *)
 Global Instance add_modal_later_except_0 P Q :
@@ -1494,6 +1523,11 @@ Global Instance add_modal_fupd `{BiFUpd 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.
 
+Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
+       E1 E2 (P P' : PROP') (Q : PROP) :
+  AddModal P P' (|={E1,E2}=> ⎡Q⎤)%I → AddModal P P' ⎡|={E1,E2}=> Q⎤.
+Proof. by rewrite /AddModal !embed_fupd. Qed.
+
 (* Frame *)
 Global Instance frame_eq_embed `{SbiEmbed PROP PROP'} p P Q (Q' : PROP')
        {A : ofeT} (a b : A) :

theories/proofmode/monpred.v

@@ -353,19 +353,6 @@ Proof.
   by rewrite {1}(absolute_absolutely P) monPred_absolutely_unfold.
 Qed.
 
-Global Instance elim_modal_embed_bupd_goal `{BiBUpd 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 `{BiBUpd 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 `{BiBUpd 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 `{BiBUpd PROP} φ 𝓟 𝓟' Q Q' i :
   ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i) →
   ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
@@ -471,19 +458,6 @@ Proof.
   by rewrite monPred_at_later.
 Qed.
 
-Global Instance elim_modal_embed_fupd_goal `{BiFUpd PROP} φ E1 E2 E3 P P' 𝓠 𝓠' :
-  ElimModal φ P P' (|={E1,E3}=> ⎡𝓠⎤)%I (|={E2,E3}=> ⎡𝓠'⎤)%I →
-  ElimModal φ P P' ⎡|={E1,E3}=> 𝓠⎤ ⎡|={E2,E3}=> 𝓠'⎤.
-Proof. by rewrite /ElimModal !monPred_fupd_embed. Qed.
-Global Instance elim_modal_embed_fupd_hyp `{BiFUpd PROP} φ E1 E2 𝓟 P' Q Q' :
-  ElimModal φ (|={E1,E2}=> ⎡𝓟⎤)%I P' Q Q' →
-  ElimModal φ ⎡|={E1,E2}=> 𝓟⎤ P' Q Q'.
-Proof. by rewrite /ElimModal monPred_fupd_embed. Qed.
-
-Global Instance add_modal_embed_fupd_goal `{BiFUpd PROP} E1 E2 P P' 𝓠 :
-  AddModal P P' (|={E1,E2}=> ⎡𝓠⎤)%I → AddModal P P' ⎡|={E1,E2}=> 𝓠⎤.
-Proof. by rewrite /AddModal !monPred_fupd_embed. Qed.
-
 Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ E1 E2 E3 𝓟 𝓟' Q Q' i :
   ElimModal φ 𝓟 𝓟' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) →
   ElimModal φ 𝓟 𝓟' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).