From e15ec18b34407093cc0c56256cea6b58e72f209d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 3 Dec 2020 17:08:30 +0100
Subject: [PATCH] More powerful from_modal_step_fupdN instance.

---
 iris/proofmode/class_instances_updates.v | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 46f271344..fc0116733 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -159,9 +159,14 @@ Proof. by rewrite /FromModal /= -bupd_intro. Qed.
 Global Instance from_modal_fupd E P `{!BiFUpd PROP} :
   FromModal modality_id (|={E}=> P) (|={E}=> P) P.
 Proof. by rewrite /FromModal /= -fupd_intro. Qed.
-Global Instance from_modal_step_fupdN E n P `{!BiFUpd PROP} :
-  FromModal (modality_laterN n) (|={E}â–·=>^n P) (|={E}â–·=>^n P) P.
-Proof. by rewrite /FromModal /= -step_fupdN_laterN. Qed.
+Global Instance from_modal_step_fupdN Ei Eo n P `{!BiFUpd PROP} :
+  (* Some cases in which [Ei ⊆ Eo] holds *)
+  TCOr (TCEq Ei Eo) (TCOr (TCEq Eo ⊤) (TCEq Ei ∅)) →
+  FromModal (modality_laterN n) (|={Eo}[Ei]â–·=>^n P) (|={Eo}[Ei]â–·=>^n P) P.
+Proof.
+  intros HE. rewrite /FromModal /= -step_fupdN_laterN //.
+  destruct HE as [->|[->| ->]]; set_solver+.
+Qed.
 
 Global Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
   ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
-- 
GitLab