Add instances for eliminating modalities under monPred_at or an embedding.

theories/proofmode/monpred.v

@@ -320,6 +320,33 @@ Qed.
 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_bupd_at. Qed.
+Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} P 𝓟' 𝓠 𝓠' i:
+  ElimModal (|==> P i) 𝓟' 𝓠 𝓠' →
+  ElimModal ((|==> P) i) 𝓟' 𝓠 𝓠'.
+Proof. by rewrite /ElimModal monPred_bupd_at. Qed.
+
+Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} 𝓟 𝓟' Q i :
+  AddModal 𝓟 𝓟' (|==> Q i)%I → AddModal 𝓟 𝓟' ((|==> Q) i).
+Proof. by rewrite /AddModal !monPred_bupd_at. Qed.
+
 End bi.
 
 (* When P and/or Q are evars when doing typeclass search on [IntoWand
@@ -384,4 +411,30 @@ Qed.
 Global Instance from_later_monPred_at i n P Q 𝓠 :
   FromLaterN n P Q → MakeMonPredAt i Q 𝓠 → FromLaterN n (P i) 𝓠.
 Proof. rewrite /FromLaterN /MakeMonPredAt=> <- <-. elim n=>//= ? ->. by unseal. 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}=> 𝓠'⎤.
+Proof. by rewrite /ElimModal !monPred_fupd_embed. Qed.
+Global Instance elim_modal_embed_fupd_hyp `{FUpdFacts 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 `{FUpdFacts 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 `{FUpdFacts 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).
+Proof. by rewrite /ElimModal !monPred_fupd_at. Qed.
+Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} E1 E2 P 𝓟' 𝓠 𝓠' i :
+  ElimModal (|={E1,E2}=> P i) 𝓟' 𝓠 𝓠' →
+  ElimModal ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
+Proof. by rewrite /ElimModal monPred_fupd_at. Qed.
+
+Global Instance add_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 𝓟 𝓟' Q i :
+  AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) → AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
+Proof. by rewrite /AddModal !monPred_fupd_at. Qed.
 End sbi.