Support `bi_embed` in `iModIntro'. This fixes #147.

theories/proofmode/class_instances.v

@@ -62,6 +62,19 @@ Section bi_modalities.
   Qed.
   Definition modality_absorbingly :=
     Modality _ modality_absorbingly_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.
@@ -1126,11 +1139,16 @@ Qed.
 Global Instance from_modal_absorbingly P :
   FromModal modality_absorbingly (bi_absorbingly P) P.
 Proof. by rewrite /FromModal. Qed.
-(* FIXME
-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_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.

theories/proofmode/classes.v

@@ -563,6 +563,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

theories/tests/proofmode_monpred.v

@@ -7,6 +7,7 @@ Section tests.
   Local Notation monPredI := (monPredI I PROP).
   Local Notation monPredSI := (monPredSI I PROP).
   Implicit Types P Q R : monPred.
+  Implicit Types 𝓟 𝓠 𝓡 : PROP.
   Implicit Types i j : I.
 
   Lemma test0 P : P -∗ P.
@@ -79,6 +80,10 @@ Section tests.
     ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
 
+  Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 :
+    □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ 𝓟 ∗ 𝓠 ⎤.
+  Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. 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