Merge branch 'robbert/super_iModIntro' into 'gen_proofmode'

Super `iModIntro` tactic that generalizes `iAlways`, `iNext`, `iModIntro`, and more

See merge request FP/iris-coq!121

ProofMode.md

@@ -114,35 +114,26 @@ Separating logic specific tactics
 Modalities
 ----------
 
-- `iModIntro` : introduction of a modality that is an instance of the
-  `FromModal` type class. Instances include: later, except 0, basic update and
-  fancy update.
+- `iModIntro` : introduction of a modality. The type class `FromModal` is used
+  to specify which modalities this tactic should introduce. Instances of that
+  type class include: later, except 0, basic update and fancy update,
+  persistently, affinely, plainly, absorbingly, absolutely, and relatively.
+- `iAlways` : a deprecated alias of `iModIntro`.
+- `iNext n` : introduce `n` laters by stripping that number of laters from all
+  hypotheses. If the argument `n` is not given, it strips one later if the
+  leftmost conjunct is of the shape `▷ P`, or `n` laters if the leftmost
+  conjunct is of the shape `▷^n P`.
 - `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
   an instance of the `ElimModal` type class. Instances include: later, except 0,
   basic update and fancy update.
 
-The persistence and plainness modalities
-----------------------------------------
-
-- `iAlways` : introduce a persistence or plainness modality and the spatial
-  context. In case of a plainness modality, the tactic will prune all persistent
-  hypotheses that are not plain.
-
-The later modality
-------------------
+Induction
+---------
 
-- `iNext n` : introduce `n` laters by stripping that number of laters from all
-  hypotheses. If the argument `n` is not given, it strips one later if the
-  leftmost conjunct is of the shape `▷ P`, or `n` laters if the leftmost
-  conjunct is of the shape `▷^n P`.
 - `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
   generating a hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq
   level variables `x1 ... xn`, the hypotheses given by the selection pattern
   `selpat`, and the spatial context.
-
-Induction
----------
-
 - `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on
   the Coq term `x`. The Coq introduction pattern is used to name the introduced
   variables. The induction hypotheses are inserted into the persistent context
@@ -229,8 +220,8 @@ appear at the top level:
   Items of the selection pattern can be prefixed with `$`, which cause them to
   be framed instead of cleared.
 - `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an persistence or plainness modality (by calling `iAlways`).
-- `!>` : introduce a modality (by calling `iModIntro`).
+- `!>` : introduce a modality by calling `iModIntro`.
+- `!#` : introduce a modality by calling `iModIntro` (deprecated).
 - `/=` : perform `simpl`.
 - `//` : perform `try done` on all goals.
 - `//=` : syntactic sugar for `/= //`

_CoqProject

@@ -101,6 +101,8 @@ theories/proofmode/notation.v
 theories/proofmode/classes.v
 theories/proofmode/class_instances.v
 theories/proofmode/monpred.v
+theories/proofmode/modalities.v
+theories/proofmode/modality_instances.v
 theories/tests/heap_lang.v
 theories/tests/one_shot.v
 theories/tests/proofmode.v

theories/proofmode/class_instances.v

 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Export classes.
+From iris.proofmode Require Export modality_instances classes.
 Set Default Proof Using "Type".
 Import bi.
 
-Section always_modalities.
+Section bi_modalities.
   Context {PROP : bi}.
-  Lemma always_modality_persistently_mixin :
-    always_modality_mixin (@bi_persistently PROP) AIEnvId AIEnvClear.
+
+  Lemma modality_persistently_mixin :
+    modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
   Proof.
-    split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
-      persistently_and, persistently_sep_2 with typeclass_instances.
+    split; simpl; eauto using equiv_entails_sym, persistently_intro,
+      persistently_mono, persistently_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_persistently :=
-    AlwaysModality _ always_modality_persistently_mixin.
+  Definition modality_persistently :=
+    Modality _ modality_persistently_mixin.
 
-  Lemma always_modality_affinely_mixin :
-    always_modality_mixin (@bi_affinely PROP) AIEnvId (AIEnvForall Affine).
+  Lemma modality_affinely_mixin :
+    modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
   Proof.
-    split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
-      affinely_and, affinely_sep_2 with typeclass_instances.
+    split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
+      affinely_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_affinely :=
-    AlwaysModality _ always_modality_affinely_mixin.
+  Definition modality_affinely :=
+    Modality _ modality_affinely_mixin.
 
-  Lemma always_modality_affinely_persistently_mixin :
-    always_modality_mixin (λ P : PROP, □ P)%I AIEnvId AIEnvIsEmpty.
+  Lemma modality_affinely_persistently_mixin :
+    modality_mixin (λ P : PROP, □ P)%I MIEnvId MIEnvIsEmpty.
   Proof.
-    split; eauto using equiv_entails_sym, affinely_persistently_emp,
+    split; simpl; eauto using equiv_entails_sym, affinely_persistently_emp,
       affinely_mono, persistently_mono, affinely_persistently_idemp,
-      affinely_persistently_and, affinely_persistently_sep_2 with typeclass_instances.
+      affinely_persistently_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_affinely_persistently :=
-    AlwaysModality _ always_modality_affinely_persistently_mixin.
+  Definition modality_affinely_persistently :=
+    Modality _ modality_affinely_persistently_mixin.
 
-  Lemma always_modality_plainly_mixin :
-    always_modality_mixin (@bi_plainly PROP) (AIEnvForall Plain) AIEnvClear.
+  Lemma modality_plainly_mixin :
+    modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
   Proof.
-    split; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
-      plainly_and, plainly_sep_2 with typeclass_instances.
+    split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro,
+      plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_plainly :=
-    AlwaysModality _ always_modality_plainly_mixin.
+  Definition modality_plainly :=
+    Modality _ modality_plainly_mixin.
 
-  Lemma always_modality_affinely_plainly_mixin :
-    always_modality_mixin (λ P : PROP, ■ P)%I (AIEnvForall Plain) AIEnvIsEmpty.
+  Lemma modality_affinely_plainly_mixin :
+    modality_mixin (λ P : PROP, ■ P)%I (MIEnvForall Plain) MIEnvIsEmpty.
   Proof.
-    split; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
+    split; simpl; split_and?; eauto using equiv_entails_sym,
+      affinely_plainly_emp, affinely_intro,
       plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
       affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_affinely_plainly :=
-    AlwaysModality _ always_modality_affinely_plainly_mixin.
-End always_modalities.
+  Definition modality_affinely_plainly :=
+    Modality _ modality_affinely_plainly_mixin.
+
+  Lemma modality_embed_mixin `{BiEmbedding PROP PROP'} :
+    modality_mixin (@bi_embed PROP PROP' _)
+      (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
+  Proof.
+    split; simpl; split_and?;
+      eauto using equiv_entails_sym, bi_embed_emp, bi_embed_sep, bi_embed_and.
+    - intros P Q. rewrite /IntoEmbed=> ->.
+      by rewrite bi_embed_affinely bi_embed_persistently.
+    - by intros P Q ->.
+  Qed.
+  Definition modality_embed `{BiEmbedding PROP PROP'} :=
+    Modality _ modality_embed_mixin.
+End bi_modalities.
+
+Section sbi_modalities.
+  Context {PROP : sbi}.
+
+  Lemma modality_laterN_mixin n :
+    modality_mixin (@sbi_laterN PROP n)
+      (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
+  Proof.
+    split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
+      laterN_mono, laterN_and, laterN_sep with typeclass_instances.
+    rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_affinely_persistently_2.
+  Qed.
+  Definition modality_laterN n :=
+    Modality _ (modality_laterN_mixin n).
+End sbi_modalities.
 
 Section bi_instances.
 Context {PROP : bi}.
@@ -267,54 +297,54 @@ Global Instance into_persistent_persistent P :
   Persistent P → IntoPersistent false P P | 100.
 Proof. intros. by rewrite /IntoPersistent. Qed.
 
-(* FromAlways *)
-Global Instance from_always_affinely P :
-  FromAlways always_modality_affinely (bi_affinely P) P | 2.
-Proof. by rewrite /FromAlways. Qed.
-
-Global Instance from_always_persistently P :
-  FromAlways always_modality_persistently (bi_persistently P) P | 2.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_persistently P :
-  FromAlways always_modality_affinely_persistently (□ P) P | 1.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_persistently_affine_bi P :
-  BiAffine PROP → FromAlways always_modality_persistently (□ P) P | 0.
-Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
-
-Global Instance from_always_plainly P :
-  FromAlways always_modality_plainly (bi_plainly P) P | 2.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_plainly P :
-  FromAlways always_modality_affinely_plainly (■ P) P | 1.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_plainly_affine_bi P :
-  BiAffine PROP → FromAlways always_modality_plainly (■ P) P | 0.
-Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
-
-Global Instance from_always_affinely_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_affinely P Q →
-  FromAlways always_modality_affinely ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely. Qed.
-Global Instance from_always_persistently_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_persistently P Q →
-  FromAlways always_modality_persistently ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_persistently. Qed.
-Global Instance from_always_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_affinely_persistently P Q →
-  FromAlways always_modality_affinely_persistently ⎡P⎤ ⎡Q⎤.
-Proof.
-  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
-Qed.
-Global Instance from_always_plainly_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_plainly P Q →
-  FromAlways always_modality_plainly ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_plainly. Qed.
-Global Instance from_always_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_affinely_plainly P Q →
-  FromAlways always_modality_affinely_plainly ⎡P⎤ ⎡Q⎤.
-Proof.
-  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
+(* FromModal *)
+Global Instance from_modal_affinely P :
+  FromModal modality_affinely (bi_affinely P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+
+Global Instance from_modal_persistently P :
+  FromModal modality_persistently (bi_persistently P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_persistently P :
+  FromModal modality_affinely_persistently (□ 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.
+Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
+
+Global Instance from_modal_plainly P :
+  FromModal modality_plainly (bi_plainly P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_plainly P :
+  FromModal modality_affinely_plainly (■ 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.
+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⎤.
+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⎤.
+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⎤.
+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⎤.
+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⎤.
+Proof.
+  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
 Qed.
 
 (* IntoWand *)
@@ -1077,11 +1107,19 @@ Proof.
 Qed.
 
 (* FromModal *)
-Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
-Proof. apply absorbingly_intro. Qed.
-Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
-  FromModal P Q → FromModal ⎡P⎤ ⎡Q⎤.
-Proof. by rewrite /FromModal=> ->. Qed.
+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 *)
+Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
+  IntoEmbed ⎡P⎤ P.
+Proof. by rewrite /IntoEmbed. Qed.
 
 (* AsValid *)
 Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
@@ -1410,15 +1448,20 @@ Global Instance is_except_0_fupd `{FUpdFacts PROP} E1 E2 P :
 Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 
 (* FromModal *)
-Global Instance from_modal_later P : FromModal (▷ P) P.
-Proof. apply later_intro. Qed.
-Global Instance from_modal_except_0 P : FromModal (◇ P) P.
-Proof. apply except_0_intro. Qed.
-
-Global Instance from_modal_bupd `{BUpdFacts PROP} P : FromModal (|==> P) P.
-Proof. apply bupd_intro. Qed.
-Global Instance from_modal_fupd E P `{FUpdFacts PROP} : FromModal (|={E}=> P) P.
-Proof. rewrite /FromModal. apply fupd_intro. 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.
+Proof. rewrite /FromLaterN /FromModal. by intros [?] [_ []|?]. Qed.
+Global Instance from_modal_except_0 P : FromModal modality_id (◇ P) P.
+Proof. by rewrite /FromModal /= -except_0_intro. Qed.
+
+Global Instance from_modal_bupd `{BUpdFacts PROP} P :
+  FromModal modality_id (|==> P) P.
+Proof. by rewrite /FromModal /= -bupd_intro. Qed.
+Global Instance from_modal_fupd E P `{FUpdFacts PROP} :
+  FromModal modality_id (|={E}=> P) P.
+Proof. by rewrite /FromModal /= -fupd_intro. Qed.
 
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :

theories/proofmode/classes.v

 From iris.bi Require Export bi.
+From iris.proofmode Require Export modalities.
 From stdpp Require Import namespaces.
 Set Default Proof Using "Type".
 Import bi.
@@ -83,138 +84,22 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
-(* The `iAlways` tactic is not tied to `persistently` and `affinely`, but can be
-instantiated with a variety of comonadic (always-style) modalities.
-
-In order to plug in an always-style modality, one has to decide for both the
-persistent and spatial what action should be performed upon introducing the
-modality:
-
-- Introduction is only allowed when the context is empty.
-- Introduction is only allowed when all hypotheses satisfy some predicate
-  `C : PROP → Prop` (where `C` should be a type class).
-- Introduction will only keep the hypotheses that satisfy some predicate
-  `C : PROP → Prop` (where `C` should be a type class).
-- Introduction will clear the context.
-- Introduction will keep the context as-if.
-
-Formally, these actions correspond to the following inductive type: *)
-Inductive always_intro_spec (PROP : bi) :=
-  | AIEnvIsEmpty
-  | AIEnvForall (C : PROP → Prop)
-  | AIEnvFilter (C : PROP → Prop)
-  | AIEnvClear
-  | AIEnvId.
-Arguments AIEnvIsEmpty {_}.
-Arguments AIEnvForall {_} _.
-Arguments AIEnvFilter {_} _.
-Arguments AIEnvClear {_}.
-Arguments AIEnvId {_}.
-
-(* An always-style modality is then a record packing together the modality with
-the laws it should satisfy to justify the given actions for both contexts: *)
-Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
-    (pspec sspec : always_intro_spec PROP) := {
-  always_modality_mixin_persistent :
-    match pspec with
-    | AIEnvIsEmpty => True
-    | AIEnvForall C | AIEnvFilter C => ∀ P, C P → □ P ⊢ M (□ P)
-    | AIEnvClear => True
-    | AIEnvId => ∀ P, □ P ⊢ M (□ P)
-    end;
-  always_modality_mixin_spatial :
-    match sspec with
-    | AIEnvIsEmpty => True
-    | AIEnvForall C => ∀ P, C P → P ⊢ M P
-    | AIEnvFilter C => (∀ P, C P → P ⊢ M P) ∧ (∀ P, Absorbing (M P))
-    | AIEnvClear => ∀ P, Absorbing (M P)
-    | AIEnvId => False
-    end;
-  always_modality_mixin_emp : emp ⊢ M emp;
-  always_modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
-  always_modality_mixin_and P Q : M P ∧ M Q ⊢ M (P ∧ Q);
-  always_modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
-}.
-
-Record always_modality (PROP : bi) := AlwaysModality {
-  always_modality_car :> PROP → PROP;
-  always_modality_persistent_spec : always_intro_spec PROP;
-  always_modality_spatial_spec : always_intro_spec PROP;
-  always_modality_mixin_of : always_modality_mixin
-    always_modality_car
-    always_modality_persistent_spec always_modality_spatial_spec
-}.
-Arguments AlwaysModality {_} _ {_ _} _.
-Arguments always_modality_persistent_spec {_} _.
-Arguments always_modality_spatial_spec {_} _.
-
-Section always_modality.
-  Context {PROP} (M : always_modality PROP).
-
-  Lemma always_modality_persistent_forall C P :
-    always_modality_persistent_spec M = AIEnvForall C → C P → □ P ⊢ M (□ P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_persistent_filter C P :
-    always_modality_persistent_spec M = AIEnvFilter C → C P → □ P ⊢ M (□ P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_persistent_id P :
-    always_modality_persistent_spec M = AIEnvId → □ P ⊢ M (□ P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_forall C P :
-    always_modality_spatial_spec M = AIEnvForall C → C P → P ⊢ M P.
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_filter C P :
-    always_modality_spatial_spec M = AIEnvFilter C → C P → P ⊢ M P.
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_filter_absorbing C P :
-    always_modality_spatial_spec M = AIEnvFilter C → Absorbing (M P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_clear P :
-    always_modality_spatial_spec M = AIEnvClear → Absorbing (M P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_id :
-    always_modality_spatial_spec M ≠ AIEnvId.
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-
-  Lemma always_modality_emp : emp ⊢ M emp.
-  Proof. eapply always_modality_mixin_emp, always_modality_mixin_of. Qed.
-  Lemma always_modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
-  Proof. eapply always_modality_mixin_mono, always_modality_mixin_of. Qed.
-  Lemma always_modality_and P Q : M P ∧ M Q ⊢ M (P ∧ Q).
-  Proof. eapply always_modality_mixin_and, always_modality_mixin_of. Qed.
-  Lemma always_modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
-  Proof. eapply always_modality_mixin_sep, always_modality_mixin_of. Qed.
-  Global Instance always_modality_mono' : Proper ((⊢) ==> (⊢)) M.
-  Proof. intros P Q. apply always_modality_mono. Qed.
-  Global Instance always_modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
-  Proof. intros P Q. apply always_modality_mono. Qed.
-  Global Instance always_modality_proper : Proper ((≡) ==> (≡)) M.
-  Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using always_modality_mono. Qed.
-
-  Lemma always_modality_persistent_forall_big_and C Ps :
-    always_modality_persistent_spec M = AIEnvForall C →
-    Forall C Ps → □ [∧] Ps ⊢ M (□ [∧] Ps).
-  Proof.
-    induction 2 as [|P Ps ? _ IH]; simpl.
-    - by rewrite persistently_pure affinely_True_emp affinely_emp -always_modality_emp.
-    - rewrite affinely_persistently_and -always_modality_and -IH.
-      by rewrite {1}(always_modality_persistent_forall _ P).
-  Qed.
-  Lemma always_modality_spatial_forall_big_sep C Ps :
-    always_modality_spatial_spec M = AIEnvForall C →
-    Forall C Ps → [∗] Ps ⊢ M ([∗] Ps).
-  Proof.
-    induction 2 as [|P Ps ? _ IH]; simpl.
-    - by rewrite -always_modality_emp.
-    - by rewrite -always_modality_sep -IH {1}(always_modality_spatial_forall _ P).
-  Qed.
-End always_modality.
-
-Class FromAlways {PROP : bi} (M : always_modality PROP) (P Q : PROP) :=
-  from_always : M Q ⊢ P.
-Arguments FromAlways {_} _ _%I _%I : simpl never.
-Arguments from_always {_} _ _%I _%I {_}.
-Hint Mode FromAlways + - ! - : 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].
+
+For modalities [M] that do not need to augment the proof mode environment, one
+can define an instance [FromModal modality_id (M P) P]. Defining such an
+only imposes the proof obligation [P ⊢ M P]. Examples of modalities that have
+such an instance are [bupd], [fupd], [except_0], [monPred_relatively] and
+[bi_absorbingly]. *)
+Class FromModal {PROP1 PROP2 : bi}
+    (M : modality PROP1 PROP2) (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.
 
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : bi_affinely Q ⊢ P.
@@ -332,11 +217,6 @@ Arguments IsExcept0 {_} _%I : simpl never.
 Arguments is_except_0 {_} _%I {_}.
 Hint Mode IsExcept0 + ! : typeclass_instances.
 
-Class FromModal {PROP : bi} (P Q : PROP) := from_modal : Q ⊢ P.
-Arguments FromModal {_} _%I _%I : simpl never.
-Arguments from_modal {_} _%I _%I {_}.
-Hint Mode FromModal + ! - : 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.
@@ -553,6 +433,16 @@ Arguments FromLaterN {_} _%nat_scope _%I _%I.
 Arguments from_laterN {_} _%nat_scope _%I _%I {_}.
 Hint Mode FromLaterN + - ! - : typeclass_instances.
 
+(** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
+embeddings using [iModIntro].
+
+Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤] *)
+Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
+  into_embed : P ⊢ ⎡Q⎤.
+Arguments IntoEmbed {_ _ _} _%I _%I.
+Arguments into_embed {_ _ _} _%I _%I {_}.
+Hint Mode IntoEmbed + + + ! -  : typeclass_instances.
+
 (* We use two type classes for [AsValid], in order to avoid loops in
    typeclass search. Indeed, the [as_valid_embed] instance would try
    to add an arbitrary number of embeddings. To avoid this, the
@@ -644,8 +534,8 @@ 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} (P Q : PROP) :
-  FromModal P Q → FromModal (tc_opaque P) Q := id.
+Instance from_modal_tc_opaque {PROP : bi} M (P Q : PROP) :
+  FromModal M P Q → FromModal M (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

 From iris.bi Require Export bi.
 From iris.bi Require Import tactics.
-From iris.proofmode Require Export base environments classes.
+From iris.proofmode Require Export base environments classes modality_instances.
 Set Default Proof Using "Type".
 Import bi.