From 15946faa8022874824a7442db277efa266c7e11f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 25 May 2021 16:33:11 +0200
Subject: [PATCH] add pure precondition to FromModal

---
 iris/proofmode/class_instances.v             | 10 ++--
 iris/proofmode/class_instances_embedding.v   | 52 +++++++++----------
 iris/proofmode/class_instances_internal_eq.v |  4 +-
 iris/proofmode/class_instances_later.v       |  7 +--
 iris/proofmode/class_instances_plainly.v     |  2 +-
 iris/proofmode/class_instances_updates.v     |  4 +-
 iris/proofmode/classes.v                     | 19 +++----
 iris/proofmode/coq_tactics.v                 | 19 +++----
 iris/proofmode/ltac_tactics.v                |  3 +-
 iris/proofmode/monpred.v                     | 53 +++++++++++---------
 10 files changed, 92 insertions(+), 81 deletions(-)

diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index b72fc6889..75a702635 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -315,23 +315,23 @@ Proof. intros. by rewrite /IntoPersistent. Qed.
 
 (** FromModal *)
 Global Instance from_modal_affinely P :
-  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
+  FromModal True modality_affinely (<affine> P) (<affine> P) P | 2.
 Proof. by rewrite /FromModal. Qed.
 
 Global Instance from_modal_persistently P :
-  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
+  FromModal True modality_persistently (<pers> P) (<pers> P) P | 2.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_intuitionistically P :
-  FromModal modality_intuitionistically (â–¡ P) (â–¡ P) P | 1.
+  FromModal True modality_intuitionistically (â–¡ P) (â–¡ P) P | 1.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_intuitionistically_affine_bi P :
-  BiAffine PROP → FromModal modality_persistently (□ P) (□ P) P | 0.
+  BiAffine PROP → FromModal True modality_persistently (□ P) (□ P) P | 0.
 Proof.
   intros. by rewrite /FromModal /= intuitionistically_into_persistently.
 Qed.
 
 Global Instance from_modal_absorbingly P :
-  FromModal modality_id (<absorb> P) (<absorb> P) P.
+  FromModal True modality_id (<absorb> P) (<absorb> P) P.
 Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
 
 (** IntoWand *)
diff --git a/iris/proofmode/class_instances_embedding.v b/iris/proofmode/class_instances_embedding.v
index 44a3e0645..67a609f54 100644
--- a/iris/proofmode/class_instances_embedding.v
+++ b/iris/proofmode/class_instances_embedding.v
@@ -33,26 +33,26 @@ Qed.
 (* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
 the embedding over the modality. *)
 Global Instance from_modal_embed P :
-  FromModal (@modality_embed PROP PROP' _) ⎡P⎤ ⎡P⎤ P.
+  FromModal True (@modality_embed PROP PROP' _) ⎡P⎤ ⎡P⎤ P.
 Proof. by rewrite /FromModal. Qed.
 
-Global Instance from_modal_id_embed `(sel : A) P Q :
-  FromModal modality_id sel P Q →
-  FromModal modality_id sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. by rewrite /FromModal /= =><-. Qed.
-
-Global Instance from_modal_affinely_embed `(sel : A) P Q :
-  FromModal modality_affinely sel P Q →
-  FromModal modality_affinely sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
-Global Instance from_modal_persistently_embed `(sel : A) P Q :
-  FromModal modality_persistently sel P Q →
-  FromModal modality_persistently sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
-Global Instance from_modal_intuitionistically_embed `(sel : A) P Q :
-  FromModal modality_intuitionistically sel P Q →
-  FromModal modality_intuitionistically sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
+Global Instance from_modal_id_embed φ `(sel : A) P Q :
+  FromModal φ modality_id sel P Q →
+  FromModal φ modality_id sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ. Qed.
+
+Global Instance from_modal_affinely_embed φ `(sel : A) P Q :
+  FromModal φ modality_affinely sel P Q →
+  FromModal φ modality_affinely sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_affinely_2. Qed.
+Global Instance from_modal_persistently_embed φ `(sel : A) P Q :
+  FromModal φ modality_persistently sel P Q →
+  FromModal φ modality_persistently sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_persistently. Qed.
+Global Instance from_modal_intuitionistically_embed φ `(sel : A) P Q :
+  FromModal φ modality_intuitionistically sel P Q →
+  FromModal φ modality_intuitionistically sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_intuitionistically_2. Qed.
 
 Global Instance into_wand_embed p q R P Q :
   IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
@@ -139,16 +139,16 @@ Global Instance is_except_0_embed `{!BiEmbedLater PROP PROP'} P :
   IsExcept0 P → IsExcept0 ⎡P⎤.
 Proof. by rewrite /IsExcept0 -embed_except_0=>->. Qed.
 
-Global Instance from_modal_later_embed `{!BiEmbedLater PROP PROP'} `(sel : A) n P Q :
-  FromModal (modality_laterN n) sel P Q →
-  FromModal (modality_laterN n) sel ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_laterN. Qed.
+Global Instance from_modal_later_embed `{!BiEmbedLater PROP PROP'} φ `(sel : A) n P Q :
+  FromModal φ (modality_laterN n) sel P Q →
+  FromModal φ (modality_laterN n) sel ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_laterN. Qed.
 
 Global Instance from_modal_plainly_embed
-    `{!BiPlainly PROP, !BiPlainly PROP', !BiEmbedPlainly PROP PROP'} `(sel : A) P Q :
-  FromModal modality_plainly sel P Q →
-  FromModal (PROP2:=PROP') modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
+    `{!BiPlainly PROP, !BiPlainly PROP', !BiEmbedPlainly PROP PROP'} φ `(sel : A) P Q :
+  FromModal φ modality_plainly sel P Q →
+  FromModal φ (PROP2:=PROP') modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
+Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_plainly. Qed.
 
 Global Instance into_internal_eq_embed
     `{!BiInternalEq PROP, !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
diff --git a/iris/proofmode/class_instances_internal_eq.v b/iris/proofmode/class_instances_internal_eq.v
index 879b65fe3..6bfde426c 100644
--- a/iris/proofmode/class_instances_internal_eq.v
+++ b/iris/proofmode/class_instances_internal_eq.v
@@ -17,7 +17,7 @@ Global Instance into_pure_eq {A : ofe} (a b : A) :
 Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
 
 Global Instance from_modal_Next {A : ofe} (x y : A) :
-  FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
+  FromModal (PROP1:=PROP) (PROP2:=PROP) True (modality_laterN 1)
     (▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
 Proof. by rewrite /FromModal /= later_equivI. Qed.
 
@@ -47,4 +47,4 @@ Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
 Global Instance into_internal_eq_persistently {A : ofe} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
-End class_instances_internal_eq.
\ No newline at end of file
+End class_instances_internal_eq.
diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index 87d1c84a4..e1a37c576 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -205,12 +205,13 @@ Proof. by rewrite /IsExcept0 except_0_later. Qed.
 
 (** FromModal *)
 Global Instance from_modal_later P :
-  FromModal (modality_laterN 1) (â–·^1 P) (â–· P) P.
+  FromModal True (modality_laterN 1) (â–·^1 P) (â–· P) P.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_laterN n P :
-  FromModal (modality_laterN n) (â–·^n P) (â–·^n P) P.
+  FromModal True (modality_laterN n) (â–·^n P) (â–·^n P) P.
 Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_except_0 P : FromModal modality_id (â—‡ P) (â—‡ P) P.
+Global Instance from_modal_except_0 P :
+  FromModal True modality_id (â—‡ P) (â—‡ P) P.
 Proof. by rewrite /FromModal /= -except_0_intro. Qed.
 
 (** IntoExcept0 *)
diff --git a/iris/proofmode/class_instances_plainly.v b/iris/proofmode/class_instances_plainly.v
index 44353c915..efd3aa468 100644
--- a/iris/proofmode/class_instances_plainly.v
+++ b/iris/proofmode/class_instances_plainly.v
@@ -88,7 +88,7 @@ Global Instance from_forall_plainly {A} P (Φ : A → PROP) name :
 Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
 
 Global Instance from_modal_plainly P :
-  FromModal modality_plainly (â–  P) (â–  P) P | 2.
+  FromModal True modality_plainly (â–  P) (â–  P) P | 2.
 Proof. by rewrite /FromModal. Qed.
 
 Global Instance into_except_0_plainly `{!BiPlainlyExist PROP} P Q :
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index e0f110a4f..28147e995 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -124,10 +124,10 @@ Global Instance is_except_0_fupd `{!BiFUpd PROP} E1 E2 P :
 Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 
 Global Instance from_modal_bupd `{!BiBUpd PROP} P :
-  FromModal modality_id (|==> P) (|==> P) P.
+  FromModal True modality_id (|==> P) (|==> P) P.
 Proof. by rewrite /FromModal /= -bupd_intro. Qed.
 Global Instance from_modal_fupd E P `{!BiFUpd PROP} :
-  FromModal modality_id (|={E}=> P) (|={E}=> P) P.
+  FromModal True modality_id (|={E}=> P) (|={E}=> P) P.
 Proof. by rewrite /FromModal /= -fupd_intro. Qed.
 
 Global Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 3b8ce451f..9fa198020 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -96,8 +96,9 @@ Global Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Global Arguments into_persistent {_} _ _%I _%I {_}.
 Global Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
-(** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to transform
-a goal [P] into a modality [M] and proposition [Q].
+(** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to
+transform a goal [P] into a modality [M] and proposition [Q], under additional
+pure assumptions [φ].
 
 The inputs are [P] and [sel] and the outputs are [M] and [Q].
 
@@ -113,11 +114,11 @@ instance only imposes the proof obligation [P ⊢ N P]. Examples of such
 modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
 [bi_absorbingly]. *)
 Class FromModal {PROP1 PROP2 : bi} {A}
-    (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
-  from_modal : M Q ⊢ P.
-Global Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
-Global Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
-Global Hint Mode FromModal - + - - - ! - : typeclass_instances.
+    (φ : Prop) (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
+  from_modal : φ → M Q ⊢ P.
+Global Arguments FromModal {_ _ _} _ _ _%I _%I _%I : simpl never.
+Global Arguments from_modal {_ _ _} _ _ _ _%I _%I {_}.
+Global Hint Mode FromModal - + - - - - ! - : typeclass_instances.
 
 (** The [FromAffinely P Q] class is used to add an [<affine>] modality to the
 proposition [Q].
@@ -645,8 +646,8 @@ Global Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PRO
 Global Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
 Global Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
-    M (sel : A) (P : PROP2) (Q : PROP1) :
-  FromModal M sel P Q → FromModal M sel (tc_opaque P) Q := id.
+    φ M (sel : A) (P : PROP2) (Q : PROP1) :
+  FromModal φ M sel P Q → FromModal φ M sel (tc_opaque P) Q := id.
 Global Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
   ElimModal φ p p' P P' Q Q' → ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
 Global Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index a2c2007f3..ab186a294 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -1029,14 +1029,15 @@ Section tac_modal_intro.
   Qed.
 
   (** The actual introduction tactic *)
-  Lemma tac_modal_intro {A} (sel : A) Γp Γs n Γp' Γs' Q Q' fi :
-    FromModal M sel Q' Q →
+  Lemma tac_modal_intro {A} φ (sel : A) Γp Γs n Γp' Γs' Q Q' fi :
+    FromModal φ M sel Q' Q →
     IntoModalIntuitionisticEnv M Γp Γp' (modality_intuitionistic_action M) →
     IntoModalSpatialEnv M Γs Γs' (modality_spatial_action M) fi →
     (if fi then Absorbing Q' else TCTrue) →
+    φ →
     envs_entails (Envs Γp' Γs' n) Q → envs_entails (Envs Γp Γs n) Q'.
   Proof.
-    rewrite envs_entails_eq /FromModal !of_envs_eq => HQ' HΓp HΓs ? HQ.
+    rewrite envs_entails_eq /FromModal !of_envs_eq => HQ' HΓp HΓs ? Hφ HQ.
     apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs' n)) as Hwf.
     { split; simpl in *.
       - destruct HΓp as [| |????? []| |]; eauto using Enil_wf.
@@ -1060,19 +1061,19 @@ Section tac_modal_intro.
     move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
     remember (modality_spatial_action M).
     destruct HΓs as [? M|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
-    - by rewrite -HQ' /= !right_id.
-    - rewrite -HQ' {1}(modality_spatial_forall_big_sep _ _ Γs) //.
+    - by rewrite -HQ' //= !right_id.
+    - rewrite -HQ' // {1}(modality_spatial_forall_big_sep _ _ Γs) //.
       by rewrite modality_sep.
     - destruct fi.
-      + rewrite -(absorbing Q') /bi_absorbingly -HQ' (comm _ True%I).
+      + rewrite -(absorbing Q') /bi_absorbingly -HQ' // (comm _ True%I).
         rewrite -modality_sep -assoc. apply sep_mono_r.
         eauto using modality_spatial_transform.
-      + rewrite -HQ' -modality_sep. apply sep_mono_r.
+      + rewrite -HQ' // -modality_sep. apply sep_mono_r.
         rewrite -(right_id emp%I bi_sep (M _)).
         eauto using modality_spatial_transform.
-    - rewrite -HQ' /= right_id comm -{2}(modality_spatial_clear M) //.
+    - rewrite -HQ' //= right_id comm -{2}(modality_spatial_clear M) //.
       by rewrite (True_intro ([∗] Γs)).
-    - rewrite -HQ' {1}(modality_spatial_id M ([∗] Γs)) //.
+    - rewrite -HQ' // {1}(modality_spatial_id M ([∗] Γs)) //.
       by rewrite -modality_sep.
   Qed.
 End tac_modal_intro.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 275e549f5..bfd12ae7b 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1385,7 +1385,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Modality introduction *)
 Tactic Notation "iModIntro" uconstr(sel) :=
   iStartProof;
-  notypeclasses refine (tac_modal_intro _ sel _ _ _ _ _ _ _ _ _ _ _ _ _);
+  notypeclasses refine (tac_modal_intro _ _ sel _ _ _ _ _ _ _ _ _ _ _ _ _ _);
     [iSolveTC ||
      fail "iModIntro: the goal is not a modality"
     |iSolveTC ||
@@ -1402,6 +1402,7 @@ Tactic Notation "iModIntro" uconstr(sel) :=
      end
     |pm_reduce; iSolveTC ||
      fail "iModIntro: cannot filter spatial context when goal is not absorbing"
+    |iSolveSideCondition
     |pm_prettify (* reduce redexes created by instantiation *)
      (* subgoal *) ].
 Tactic Notation "iModIntro" := iModIntro _.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 0a7db19c0..7073ed8d2 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -55,35 +55,40 @@ Implicit Types φ : Prop.
 Implicit Types i j : I.
 
 Global Instance from_modal_objectively P :
-  FromModal modality_objectively (<obj> P) (<obj> P) P | 1.
+  FromModal True modality_objectively (<obj> P) (<obj> P) P | 1.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_subjectively P :
-  FromModal modality_id (<subj> P) (<subj> P) P | 1.
+  FromModal True modality_id (<subj> P) (<subj> P) P | 1.
 Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.
 
-Global Instance from_modal_affinely_monPred_at `(sel : A) P Q 𝓠 i :
-  FromModal modality_affinely sel P Q → MakeMonPredAt i Q 𝓠 →
-  FromModal modality_affinely sel (P i) 𝓠 | 0.
+Global Instance from_modal_affinely_monPred_at φ `(sel : A) P Q 𝓠 i :
+  FromModal φ modality_affinely sel P Q →
+  MakeMonPredAt i Q 𝓠 →
+  FromModal φ modality_affinely sel (P i) 𝓠 | 0.
 Proof.
-  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
+  rewrite /FromModal /MakeMonPredAt /==> HPQ <- ?.
+  by rewrite -HPQ // monPred_at_affinely.
 Qed.
-Global Instance from_modal_persistently_monPred_at `(sel : A) P Q 𝓠 i :
-  FromModal modality_persistently sel P Q → MakeMonPredAt i Q 𝓠 →
-  FromModal modality_persistently sel (P i) 𝓠 | 0.
+Global Instance from_modal_persistently_monPred_at φ `(sel : A) P Q 𝓠 i :
+  FromModal φ modality_persistently sel P Q →
+  MakeMonPredAt i Q 𝓠 →
+  FromModal φ modality_persistently sel (P i) 𝓠 | 0.
 Proof.
-  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
+  rewrite /FromModal /MakeMonPredAt /==> HPQ <- ?.
+  by rewrite -HPQ // monPred_at_persistently.
 Qed.
-Global Instance from_modal_intuitionistically_monPred_at `(sel : A) P Q 𝓠 i :
-  FromModal modality_intuitionistically sel P Q → MakeMonPredAt i Q 𝓠 →
-  FromModal modality_intuitionistically sel (P i) 𝓠 | 0.
+Global Instance from_modal_intuitionistically_monPred_at φ `(sel : A) P Q 𝓠 i :
+  FromModal φ modality_intuitionistically sel P Q →
+  MakeMonPredAt i Q 𝓠 →
+  FromModal φ modality_intuitionistically sel (P i) 𝓠 | 0.
 Proof.
-  rewrite /FromModal /MakeMonPredAt /==> <- <-.
-  by rewrite monPred_at_affinely monPred_at_persistently.
+  rewrite /FromModal /MakeMonPredAt /==> HPQ <- ?.
+  by rewrite -HPQ // monPred_at_affinely monPred_at_persistently.
 Qed.
-Global Instance from_modal_id_monPred_at `(sel : A) P Q 𝓠 i :
-  FromModal modality_id sel P Q → MakeMonPredAt i Q 𝓠 →
-  FromModal modality_id sel (P i) 𝓠.
-Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
+Global Instance from_modal_id_monPred_at φ `(sel : A) P Q 𝓠 i :
+  FromModal φ modality_id sel P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal φ modality_id sel (P i) 𝓠.
+Proof. rewrite /FromModal /MakeMonPredAt=> HPQ <- ?. by rewrite -HPQ. Qed.
 
 Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
 Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
@@ -511,11 +516,13 @@ Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
   by rewrite monPred_at_later.
 Qed.
-Global Instance from_later_monPred_at i `(sel : A) n P Q 𝓠 :
-  FromModal (modality_laterN n) sel P Q → MakeMonPredAt i Q 𝓠 →
-  FromModal (modality_laterN n) sel (P i) 𝓠.
+Global Instance from_later_monPred_at i φ `(sel : A) n P Q 𝓠 :
+  FromModal φ (modality_laterN n) sel P Q →
+  MakeMonPredAt i Q 𝓠 →
+  FromModal φ (modality_laterN n) sel (P i) 𝓠.
 Proof.
-  rewrite /FromModal /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
+  rewrite /FromModal /MakeMonPredAt=> HPQ <- ?. rewrite -HPQ //.
+  elim n=>//= ? ->.
   by rewrite monPred_at_later.
 Qed.
 
-- 
GitLab