Restore side-condition of `iMod` tactic and `ElimModal` TC.

This supports Iris 2 like update modalities, as used in e.g. by @jtassaro.

This commit fixes issue #154.

theories/bi/counter_examples.v

@@ -29,7 +29,7 @@ Module savedprop. Section savedprop.
 
   Instance bupd_mono' : Proper ((⊢) ==> (⊢)) bupd.
   Proof. intros P Q ?. by apply bupd_mono. Qed.
-  Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
+  Instance elim_modal_bupd P Q : ElimModal True (|==> P) P (|==> Q) (|==> Q).
   Proof. by rewrite /ElimModal bupd_frame_r bi.wand_elim_r bupd_trans. Qed.
 
   (** A bad recursive reference: "Assertion with name [i] does not hold" *)
@@ -127,10 +127,10 @@ Module inv. Section inv.
   Lemma fupd_frame_r E P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q).
   Proof. by rewrite comm fupd_frame_l comm. Qed.
 
-  Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
+  Global Instance elim_fupd_fupd E P Q : ElimModal True (fupd E P) P (fupd E Q) (fupd E Q).
   Proof. by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_fupd. Qed.
 
-  Global Instance elim_fupd0_fupd1 P Q : ElimModal (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
+  Global Instance elim_fupd0_fupd1 P Q : ElimModal True (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
   Proof.
     by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
   Qed.

theories/program_logic/total_weakestpre.v

@@ -382,16 +382,16 @@ Section proofmode_classes.
   Proof. by rewrite /IsExcept0 -{2}fupd_twp -except_0_fupd -fupd_intro. Qed.
 
   Global Instance elim_modal_bupd_twp s E e P Φ :
-    ElimModal (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+    ElimModal True (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
   Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_twp. Qed.
 
   Global Instance elim_modal_fupd_twp s E e P Φ :
-    ElimModal (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+    ElimModal True (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_twp. Qed.
 
   Global Instance elim_modal_fupd_twp_atomic s E1 E2 e P Φ :
     Atomic (stuckness_to_atomicity s) e →
-    ElimModal (|={E1,E2}=> P) P
+    ElimModal True (|={E1,E2}=> P) P
             (WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r twp_atomic. Qed.
 

theories/program_logic/weakestpre.v

@@ -376,16 +376,16 @@ Section proofmode_classes.
   Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
 
   Global Instance elim_modal_bupd_wp s E e P Φ :
-    ElimModal (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
+    ElimModal True (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
 
   Global Instance elim_modal_fupd_wp s E e P Φ :
-    ElimModal (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
+    ElimModal True (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
   Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
     Atomic (stuckness_to_atomicity s) e →
-    ElimModal (|={E1,E2}=> P) P
+    ElimModal True (|={E1,E2}=> P) P
             (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
 

theories/proofmode/class_instances.v

@@ -801,19 +801,19 @@ Global Instance from_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PR
 Proof. by rewrite /FromForall -bi_embed_forall => <-. Qed.
 
 (* ElimModal *)
-Global Instance elim_modal_wand P P' Q Q' R :
-  ElimModal P P' Q Q' → ElimModal P P' (R -∗ Q) (R -∗ Q').
+Global Instance elim_modal_wand φ P P' Q Q' R :
+  ElimModal φ P P' Q Q' → ElimModal φ P P' (R -∗ Q) (R -∗ Q').
 Proof.
-  rewrite /ElimModal=> H. apply wand_intro_r.
-  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
+  rewrite /ElimModal=> H Hφ. apply wand_intro_r.
+  rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l; auto.
 Qed.
-Global Instance elim_modal_forall {A} P P' (Φ Ψ : A → PROP) :
-  (∀ x, ElimModal P P' (Φ x) (Ψ x)) → ElimModal P P' (∀ x, Φ x) (∀ x, Ψ x).
+Global Instance elim_modal_forall {A} φ P P' (Φ Ψ : A → PROP) :
+  (∀ x, ElimModal φ P P' (Φ x) (Ψ x)) → ElimModal φ P P' (∀ x, Φ x) (∀ x, Ψ x).
 Proof.
-  rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
+  rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
 Qed.
 Global Instance elim_modal_absorbingly_here P Q :
-  Absorbing Q → ElimModal (bi_absorbingly P) P Q Q.
+  Absorbing Q → ElimModal True (bi_absorbingly P) P Q Q.
 Proof.
   rewrite /ElimModal=> H.
   by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
@@ -1067,13 +1067,13 @@ Proof. apply bupd_intro. Qed.
 
 (* ElimModal *)
 Global Instance elim_modal_bupd `{BUpdFacts PROP} P Q :
-  ElimModal (|==> P) P (|==> Q) (|==> Q).
+  ElimModal True (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
 Global Instance elim_modal_bupd_plain_goal `{BUpdFacts PROP} P Q :
-  Plain Q → ElimModal (|==> P) P Q Q.
+  Plain Q → ElimModal True (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
 Global Instance elim_modal_bupd_plain `{BUpdFacts PROP} P Q :
-  Plain P → ElimModal (|==> P) P Q Q.
+  Plain P → ElimModal True (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
 
 (* AsValid *)
@@ -1415,18 +1415,18 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite sbi_embed_except_0. Qed.
 
 (* ElimModal *)
 Global Instance elim_modal_timeless P Q :
-  IntoExcept0 P P' → IsExcept0 Q → ElimModal P P' Q Q.
+  IntoExcept0 P P' → IsExcept0 Q → ElimModal True P P' Q Q.
 Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I).
   by rewrite (into_except_0 P) -except_0_sep wand_elim_r.
 Qed.
 Global Instance elim_modal_bupd_fupd `{FUpdFacts PROP} E1 E2 P Q :
-  ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
+  ElimModal True (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
 Proof.
   by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
 Qed.
 Global Instance elim_modal_fupd_fupd `{FUpdFacts PROP} E1 E2 E3 P Q :
-  ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+  ElimModal True (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
 Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 
 (* AddModal *)

theories/proofmode/classes.v

@@ -321,11 +321,11 @@ Arguments FromModal {_} _%I _%I : simpl never.
 Arguments from_modal {_} _%I _%I {_}.
 Hint Mode FromModal + ! - : typeclass_instances.
 
-Class ElimModal {PROP : bi} (P P' : PROP) (Q Q' : PROP) :=
-  elim_modal : P ∗ (P' -∗ Q') ⊢ Q.
-Arguments ElimModal {_} _%I _%I _%I _%I : simpl never.
-Arguments elim_modal {_} _%I _%I _%I _%I {_}.
-Hint Mode ElimModal + ! - ! - : typeclass_instances.
+Class ElimModal {PROP : bi} (φ : Prop) (P P' : PROP) (Q Q' : PROP) :=
+  elim_modal : φ → P ∗ (P' -∗ Q') ⊢ Q.
+Arguments ElimModal {_} _ _%I _%I _%I _%I : simpl never.
+Arguments elim_modal {_} _ _%I _%I _%I _%I {_}.
+Hint Mode ElimModal + - ! - ! - : typeclass_instances.
 
 (* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
 add a modality to the goal corresponding to a premise/asserted proposition. *)
@@ -473,5 +473,5 @@ Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
 Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
   FromModal P Q → FromModal (tc_opaque P) Q := id.
-Instance elim_modal_tc_opaque {PROP : bi} (P P' Q Q' : PROP) :
-  ElimModal P P' Q Q' → ElimModal (tc_opaque P) P' Q Q' := id.
+Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
+  ElimModal φ P P' Q Q' → ElimModal φ (tc_opaque P) P' Q Q' := id.

theories/proofmode/coq_tactics.v

@@ -1138,14 +1138,15 @@ Lemma tac_modal_intro Δ P Q :
   FromModal P Q → envs_entails Δ Q → envs_entails Δ P.
 Proof. by rewrite /envs_entails /FromModal=> <- ->. Qed.
 
-Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
+Lemma tac_modal_elim Δ Δ' i p φ P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
-  ElimModal P P' Q Q' →
+  ElimModal φ P P' Q Q' →
+  φ →
   envs_replace i p false (Esnoc Enil i P') Δ = Some Δ' →
   envs_entails Δ' Q' → envs_entails Δ Q.
 Proof.
-  rewrite /envs_entails => ??? HΔ. rewrite envs_replace_singleton_sound //=.
-  rewrite HΔ affinely_persistently_if_elim. by apply elim_modal.
+  rewrite /envs_entails => ???? HΔ. rewrite envs_replace_singleton_sound //=.
+  rewrite HΔ affinely_persistently_if_elim. by eapply elim_modal.
 Qed.
 End bi_tactics.
 

theories/proofmode/monpred.v

@@ -369,29 +369,29 @@ 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' ⎡|==> 𝓠⎤ ⎡|==> 𝓠'⎤.
+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'.
+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).
+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_at_bupd. Qed.
-Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} P 𝓟' 𝓠 𝓠' i:
-  ElimModal (|==> P i) 𝓟' 𝓠 𝓠' →
-  ElimModal ((|==> P) i) 𝓟' 𝓠 𝓠'.
+Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} φ P 𝓟' 𝓠 𝓠' i:
+  ElimModal φ (|==> P i) 𝓟' 𝓠 𝓠' →
+  ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
 Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
 
-Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} 𝓟 𝓟' Q i :
+Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q i :
   AddModal 𝓟 𝓟' (|==> Q i)%I → AddModal 𝓟 𝓟' ((|==> Q) i).
 Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
 End bi.
@@ -470,26 +470,26 @@ Proof.
   by rewrite monPred_at_later.
 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}=> 𝓠'⎤.
+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'.
+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).
+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_at_fupd. Qed.
-Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} E1 E2 P 𝓟' 𝓠 𝓠' i :
-  ElimModal (|={E1,E2}=> P i) 𝓟' 𝓠 𝓠' →
-  ElimModal ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
+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_at_fupd. Qed.
 
 Global Instance add_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 𝓟 𝓟' Q i :

theories/proofmode/tactics.v

@@ -944,12 +944,13 @@ Tactic Notation "iModIntro" :=
      fail "iModIntro:" P "not a modality"|].
 
 Tactic Notation "iModCore" constr(H) :=
-  eapply tac_modal_elim with _ H _ _ _ _;
+  eapply tac_modal_elim with _ H _ _ _ _ _;
     [env_reflexivity || fail "iMod:" H "not found"
     |apply _ ||
      let P := match goal with |- ElimModal ?P _ _ _ => P end in
      let Q := match goal with |- ElimModal _ _ ?Q _ => Q end in
      fail "iMod: cannot eliminate modality " P "in" Q
+    |try fast_done (* optional side-condition *)
     |env_reflexivity|].
 
 (** * Basic destruct tactic *)