From 31b357ffc42ff007a22971f348d1ba19e8b97b8b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 15 Jan 2018 06:07:21 +0100
Subject: [PATCH] Add instances for eliminating modalities under monPred_at or
 an embedding.

---
 theories/proofmode/monpred.v | 53 ++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 4b534ce07..9c6a17d63 100644
--- a/theories/proofmode/monpred.v
+++ b/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.
-- 
GitLab