From 0236daec596f4ddfb9cf4ae0f1b573efb5e3527b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 9 Sep 2019 07:28:10 +0200
Subject: [PATCH] elim_modal_at instance.
---
theories/proofmode/monpred.v | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 843c93990..47789deb9 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -440,6 +440,13 @@ Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ p p' P ð“Ÿ ð“Ÿ' ð“
ElimModal φ p p' (|==> ð“Ÿ) ð“Ÿ' ð“ ð“ ' →
ElimModal φ p p' ((|==> P) i) ð“Ÿ' ð“ ð“ '.
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_bupd=><-. Qed.
+Global Instance elim_modal_at φ p p' ð“Ÿ ð“Ÿ' P P' V:
+ ElimModal φ p p' ⎡ð“ŸâŽ¤ ⎡ð“Ÿ'⎤ P P' → ElimModal φ p p' ð“Ÿ ð“Ÿ' (P V) (P' V).
+Proof.
+ rewrite /ElimModal -!embed_intuitionistically_if.
+ iIntros (HH Hφ) "[? HP]". iApply HH; [done|]. iFrame. iIntros (? <-) "?".
+ by iApply "HP".
+Qed.
Global Instance add_modal_at_bupd_goal `{BiBUpd PROP} φ ð“Ÿ ð“Ÿ' Q i :
AddModal ð“Ÿ ð“Ÿ' (|==> Q i)%I → AddModal ð“Ÿ ð“Ÿ' ((|==> Q) i).
--
GitLab