Support to specify the modality to introduce in `iModIntro`.

See the discussion in #163.

theories/proofmode/class_instances.v

@@ -219,50 +219,65 @@ Proof. intros. by rewrite /IntoPersistent. Qed.
 
 (* FromModal *)
 Global Instance from_modal_affinely P :
-  FromModal modality_affinely (bi_affinely P) P | 2.
+  FromModal modality_affinely (bi_affinely P) (bi_affinely P) P | 2.
 Proof. by rewrite /FromModal. Qed.
 
 Global Instance from_modal_persistently P :
-  FromModal modality_persistently (bi_persistently P) P | 2.
+  FromModal modality_persistently (bi_persistently P) (bi_persistently P) P | 2.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_affinely_persistently P :
-  FromModal modality_affinely_persistently (□ P) P | 1.
+  FromModal modality_affinely_persistently (□ P) (□ P) P | 1.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_affinely_persistently_affine_bi P :
-  BiAffine PROP → FromModal modality_persistently (□ P) P | 0.
+  BiAffine PROP → FromModal modality_persistently (□ P) (□ P) P | 0.
 Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
 
 Global Instance from_modal_plainly P :
-  FromModal modality_plainly (bi_plainly P) P | 2.
+  FromModal modality_plainly (bi_plainly P) (bi_plainly P) P | 2.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_affinely_plainly P :
-  FromModal modality_affinely_plainly (■ P) P | 1.
+  FromModal modality_affinely_plainly (■ P) (■ P) P | 1.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_affinely_plainly_affine_bi P :
-  BiAffine PROP → FromModal modality_plainly (■ P) P | 0.
+  BiAffine PROP → FromModal modality_plainly (■ P) (■ P) P | 0.
 Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
 
-Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} P Q :
-  FromModal modality_affinely P Q →
-  FromModal modality_affinely ⎡P⎤ ⎡Q⎤.
+Global Instance from_modal_absorbingly P :
+  FromModal modality_id (bi_absorbingly P) (bi_absorbingly P) P.
+Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
+
+(* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
+the modality over the embedding. *)
+Global Instance from_modal_embed `{BiEmbedding PROP PROP'} (P : PROP) :
+  FromModal (@modality_embed PROP PROP' _ _) ⎡P⎤ ⎡P⎤ P | 100.
+Proof. by rewrite /FromModal. Qed.
+
+Global Instance from_modal_id_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+  FromModal modality_id sel P Q →
+  FromModal modality_id sel ⎡P⎤ ⎡Q⎤.
+Proof. by rewrite /FromModal /= =><-. Qed.
+
+Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+  FromModal modality_affinely sel P Q →
+  FromModal modality_affinely sel ⎡P⎤ ⎡Q⎤.
 Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely. Qed.
-Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} P Q :
-  FromModal modality_persistently P Q →
-  FromModal modality_persistently ⎡P⎤ ⎡Q⎤.
+Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+  FromModal modality_persistently sel P Q →
+  FromModal modality_persistently sel ⎡P⎤ ⎡Q⎤.
 Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed.
-Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
-  FromModal modality_affinely_persistently P Q →
-  FromModal modality_affinely_persistently ⎡P⎤ ⎡Q⎤.
+Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+  FromModal modality_affinely_persistently sel P Q →
+  FromModal modality_affinely_persistently sel ⎡P⎤ ⎡Q⎤.
 Proof.
   rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
 Qed.
-Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} P Q :
-  FromModal modality_plainly P Q →
-  FromModal modality_plainly ⎡P⎤ ⎡Q⎤.
+Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+  FromModal modality_plainly sel P Q →
+  FromModal modality_plainly sel ⎡P⎤ ⎡Q⎤.
 Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed.
-Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
-  FromModal modality_affinely_plainly P Q →
-  FromModal modality_affinely_plainly ⎡P⎤ ⎡Q⎤.
+Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+  FromModal modality_affinely_plainly sel P Q →
+  FromModal modality_affinely_plainly sel ⎡P⎤ ⎡Q⎤.
 Proof.
   rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
 Qed.
@@ -1030,14 +1045,6 @@ Proof.
   rewrite persistently_elim impl_elim_r //.
 Qed.
 
-(* FromModal *)
-Global Instance from_modal_absorbingly P :
-  FromModal modality_id (bi_absorbingly P) P.
-Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
-Global Instance from_modal_embed `{BiEmbedding PROP PROP'} (P : PROP) :
-  FromModal (@modality_embed PROP PROP' _ _) ⎡P⎤ P.
-Proof. by rewrite /FromModal. Qed.
-
 (* ElimModal *)
 
 (* IntoEmbed *)
@@ -1375,18 +1382,24 @@ Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 Global Instance from_modal_later n P Q :
   NoBackTrack (FromLaterN n P Q) →
   TCIf (TCEq n 0) False TCTrue →
-  FromModal (modality_laterN n) P Q | 100.
+  FromModal (modality_laterN n) (▷^n P) P Q | 99.
+  (* below [from_modal_embed] to prefer introducing a later *)
 Proof. rewrite /FromLaterN /FromModal. by intros [?] [_ []|?]. Qed.
-Global Instance from_modal_except_0 P : FromModal modality_id (◇ P) P.
+Global Instance from_modal_except_0 P : FromModal modality_id (◇ P) (◇ P) P.
 Proof. by rewrite /FromModal /= -except_0_intro. Qed.
 
 Global Instance from_modal_bupd `{BUpdFacts PROP} P :
-  FromModal modality_id (|==> P) P.
+  FromModal modality_id (|==> P) (|==> P) P.
 Proof. by rewrite /FromModal /= -bupd_intro. Qed.
 Global Instance from_modal_fupd E P `{FUpdFacts PROP} :
-  FromModal modality_id (|={E}=> P) P.
+  FromModal modality_id (|={E}=> P) (|={E}=> P) P.
 Proof. by rewrite /FromModal /= -fupd_intro. Qed.
 
+Global Instance from_modal_later_embed `{SbiEmbedding 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 sbi_embed_laterN. Qed.
+
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
   @IntoInternalEq PROP A (x ≡ y) x y.

theories/proofmode/classes.v

@@ -87,19 +87,25 @@ Hint Mode IntoPersistent + + ! - : typeclass_instances.
 (** The [FromModal M P Q] class is used by the [iModIntro] tactic to transform
 a goal [P] into a modality [M] and proposition [Q].
 
-The input is [P] and the outputs are [M] and [Q].
+The inputs are [P] and [sel] and the outputs are [M] and [Q].
+
+The input [sel] can be used to specify which modality to introduce in case there
+are multiple choices to turn [P] into a modality. For example, given [⎡|==> R⎤],
+[sel] can be either [|==> ?e] or [⎡ ?e ⎤], which turn it into an update modality
+or embedding, respectively. In case there is no need to specify the modality to
+introduce, [sel] should be an evar.
 
 For modalities [N] that do not need to augment the proof mode environment, one
 can define an instance [FromModal modality_id (N P) P]. Defining such an
 instance only imposes the proof obligation [P ⊢ N P]. Examples of such
 modalities [N] are [bupd], [fupd], [except_0], [monPred_relatively] and
 [bi_absorbingly]. *)
-Class FromModal {PROP1 PROP2 : bi}
-    (M : modality PROP1 PROP2) (P : PROP2) (Q : PROP1) :=
+Class FromModal {PROP1 PROP2 : bi} {A}
+    (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
   from_modal : M Q ⊢ P.
-Arguments FromModal {_ _} _ _%I _%I : simpl never.
-Arguments from_modal {_ _} _ _%I _%I {_}.
-Hint Mode FromModal - + - ! - : typeclass_instances.
+Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
+Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
+Hint Mode FromModal - + - - - ! - : typeclass_instances.
 
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : bi_affinely Q ⊢ P.
@@ -534,8 +540,9 @@ Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (tc_opaque P) Φ := id.
 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} M (P Q : PROP) :
-  FromModal M P Q → FromModal M (tc_opaque P) Q := id.
+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.
 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 into_inv_tc_opaque {PROP : bi} (P : PROP) N :

theories/proofmode/coq_tactics.v

@@ -1239,8 +1239,8 @@ Section tac_modal_intro.
   Qed.
 
   (** The actual introduction tactic *)
-  Lemma tac_modal_intro Γp Γs Γp' Γs' Q Q' fi :
-    FromModal M Q' Q →
+  Lemma tac_modal_intro {A} (sel : A) Γp Γs Γp' Γs' Q Q' fi :
+    FromModal M sel Q' Q →
     IntoModalPersistentEnv M Γp Γp' (modality_persistent_spec M) →
     IntoModalSpatialEnv M Γs Γs' (modality_spatial_spec M) fi →
     (if fi then Absorbing Q' else TCTrue) →

theories/proofmode/monpred.v

@@ -41,12 +41,36 @@ Implicit Types φ : Prop.
 Implicit Types i j : I.
 
 Global Instance from_modal_absolutely P :
-  FromModal modality_absolutely (∀ᵢ P) P | 1.
+  FromModal modality_absolutely (∀ᵢ P) (∀ᵢ P) P | 1.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_relatively P :
-  FromModal modality_id (∃ᵢ P) P | 1.
+  FromModal modality_id (∃ᵢ P) (∃ᵢ P) P | 1.
 Proof. by rewrite /FromModal /= -monPred_relatively_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.
+Proof.
+  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite 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.
+Proof.
+  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
+Qed.
+Global Instance from_modal_affinely_persistently_monPred_at `(sel : A) P Q 𝓠 i :
+  FromModal modality_affinely_persistently sel P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal modality_affinely_persistently sel (P i) 𝓠 | 0.
+Proof.
+  rewrite /FromModal /MakeMonPredAt /==> <- <-.
+  by rewrite 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 make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
 Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
 Global Instance make_monPred_at_emp i : MakeMonPredAt i emp emp.
@@ -158,26 +182,6 @@ Proof.
   by rewrite -monPred_at_persistently -monPred_at_persistently_if.
 Qed.
 
-Global Instance from_modal_affinely_monPred_at P Q 𝓠 i :
-  FromModal modality_affinely P Q → MakeMonPredAt i Q 𝓠 →
-  FromModal modality_affinely (P i) 𝓠 | 0.
-Proof.
-  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
-Qed.
-Global Instance from_modal_persistently_monPred_at P Q 𝓠 i :
-  FromModal modality_persistently P Q → MakeMonPredAt i Q 𝓠 →
-  FromModal modality_persistently (P i) 𝓠 | 0.
-Proof.
-  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
-Qed.
-Global Instance from_modal_affinely_persistently_monPred_at P Q 𝓠 i :
-  FromModal modality_affinely_persistently P Q → MakeMonPredAt i Q 𝓠 →
-  FromModal modality_affinely_persistently (P i) 𝓠 | 0.
-Proof.
-  rewrite /FromModal /MakeMonPredAt /==> <- <-.
-  by rewrite monPred_at_affinely monPred_at_persistently.
-Qed.
-
 Lemma into_wand_monPred_at_unknown_unknown p q R P 𝓟 Q 𝓠 i :
   IntoWand p q R P Q →  MakeMonPredAt i P 𝓟 → MakeMonPredAt i Q 𝓠 →
   IntoWand p q (R i) 𝓟 𝓠.
@@ -352,9 +356,6 @@ Proof.
                          ?monPred_at_persistently monPred_at_embed.
 Qed.
 
-Global Instance from_modal_monPred_at i P Q 𝓠 :
-  FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 → FromModal modality_id (P i) 𝓠.
-Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
 Global Instance into_embed_absolute P :
   Absolute P → IntoEmbed P (∀ i, P i).
 Proof. rewrite /IntoEmbed=> ?. by rewrite {1}(absolute_absolutely P). Qed.

theories/proofmode/tactics.v

@@ -962,9 +962,9 @@ Local Tactic Notation "iExistDestruct" constr(H)
     |revert y; intros x].
 
 (** * Modality introduction *)
-Tactic Notation "iModIntro" open_constr(M) :=
+Tactic Notation "iModIntro" uconstr(sel) :=
   iStartProof;
-  notypeclasses refine (tac_modal_intro M _ _ _ _ _ _ _ _ _ _ _ _);
+  notypeclasses refine (tac_modal_intro _ sel _ _ _ _ _ _ _ _ _ _ _ _);
     [apply _  ||
      fail "iModIntro: the goal is not a modality"
     |apply _ ||
@@ -986,8 +986,8 @@ Tactic Notation "iModIntro" := iModIntro _.
 Tactic Notation "iAlways" := iModIntro.
 
 (** * Later *)
-Tactic Notation "iNext" open_constr(n) := iModIntro (modality_laterN n).
-Tactic Notation "iNext" := iModIntro (modality_laterN _).
+Tactic Notation "iNext" open_constr(n) := iModIntro (▷^n _)%I.
+Tactic Notation "iNext" := iModIntro (▷^_ _)%I.
 
 (** * Update modality *)
 Tactic Notation "iModCore" constr(H) :=

theories/tests/proofmode_monpred.v

@@ -88,6 +88,10 @@ Section tests.
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
   Proof. iIntros "#H1 H2 H3 H4". iAlways. iFrame. Qed.
 
+  Lemma test_iModIntro_embed_nested P 𝓟 𝓠 :
+    □ P -∗ ⎡◇ 𝓟⎤ -∗ ⎡◇ 𝓠⎤ -∗ ⎡ ◇ (𝓟 ∗ 𝓠) ⎤.
+  Proof. iIntros "#H1 H2 H3". iModIntro ⎡ _ ⎤%I. by iSplitL "H2". Qed.
+
   (* This is a hack to avoid avoid coq bug #5735: sections variables
      ignore hint modes. So we assume the instances in a way that
      cannot be used by type class resolution, and then declare the