Make it possible to introduce an hypothesis which is behind an embedding.

theories/proofmode/class_instances.v

@@ -359,6 +359,20 @@ Proof.
   apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
 Qed.
 
+(* FromWand *)
+Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
+Proof. by rewrite /FromWand. Qed.
+Global Instance from_wand_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
+  FromWand P Q1 Q2 → FromWand ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromWand -bi_embed_wand => <-. Qed.
+
+(* FromImpl *)
+Global Instance from_impl_impl P1 P2 : FromImpl (P1 → P2) P1 P2.
+Proof. by rewrite /FromImpl. Qed.
+Global Instance from_impl_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
+  FromImpl P Q1 Q2 → FromImpl ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromImpl -bi_embed_impl => <-. Qed.
+
 (* FromAnd *)
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
 Proof. by rewrite /FromAnd. Qed.

theories/proofmode/classes.v

@@ -117,6 +117,16 @@ Instance into_wand_impl' {PROP : bi} p q (P Q P' Q' : PROP) :
   IntoWand' p q (P → Q) P' Q' → IntoWand p q (P → Q) P' Q' | 100.
 Proof. done. Qed.
 
+Class FromWand {PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.
+Arguments FromWand {_} _%I _%I _%I : simpl never.
+Arguments from_wand {_} _%I _%I _%I {_}.
+Hint Mode FromWand + ! - - : typeclass_instances.
+
+Class FromImpl {PROP : bi} (P Q1 Q2 : PROP) := from_impl : (Q1 → Q2) ⊢ P.
+Arguments FromImpl {_} _%I _%I _%I : simpl never.
+Arguments from_impl {_} _%I _%I _%I {_}.
+Hint Mode FromImpl + ! - - : typeclass_instances.
+
 Class FromSep {PROP : bi} (P Q1 Q2 : PROP) := from_sep : Q1 ∗ Q2 ⊢ P.
 Arguments FromSep {_} _%I _%I _%I : simpl never.
 Arguments from_sep {_} _%I _%I _%I {_}.
@@ -315,6 +325,8 @@ Instance from_pure_tc_opaque {PROP : bi} (P : PROP) φ :
   FromPure P φ → FromPure (tc_opaque P) φ := id.
 Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
   FromLaterN n P Q → FromLaterN n (tc_opaque P) Q := id.
+Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
+  FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id.
 Instance into_wand_tc_opaque {PROP : bi} p q (R P Q : PROP) :
   IntoWand p q R P Q → IntoWand p q (tc_opaque R) P Q := id.
 (* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)

theories/proofmode/coq_tactics.v

@@ -634,13 +634,14 @@ Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
   envs_app p (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ∗ □?p Q ⊢ of_envs Δ'.
 Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.
 
-Lemma tac_impl_intro Δ Δ' i P P' Q :
+Lemma tac_impl_intro Δ Δ' i P P' Q R :
+  FromImpl R P Q →
   (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
   envs_app false (Esnoc Enil i P') Δ = Some Δ' →
   FromAffinely P' P →
-  envs_entails Δ' Q → envs_entails Δ (P → Q).
+  envs_entails Δ' Q → envs_entails Δ R.
 Proof.
-  rewrite /envs_entails => ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
+  rewrite /FromImpl /envs_entails => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
   - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
     rewrite envs_app_singleton_sound //; simpl.
     rewrite -(from_affinely P') -affinely_and_lr.
@@ -648,66 +649,63 @@ Proof.
   - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
     by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
 Qed.
-Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
+Lemma tac_impl_intro_persistent Δ Δ' i P P' Q R :
+  FromImpl R P Q →
   IntoPersistent false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ (P → Q).
+  envs_entails Δ' Q → envs_entails Δ R.
 Proof.
-  rewrite /envs_entails => ?? <-.
+  rewrite /FromImpl /envs_entails => <- ?? <-.
   rewrite envs_app_singleton_sound //=. apply impl_intro_l.
   rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
   by rewrite persistently_and_affinely_sep_l wand_elim_r.
 Qed.
-Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
-  (φ → envs_entails Δ ⌜ψ⌝) → envs_entails Δ ⌜φ → ψ⌝.
-Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
-Lemma tac_impl_intro_pure Δ P φ Q :
-  IntoPure P φ → (φ → envs_entails Δ Q) → envs_entails Δ (P → Q).
-Proof.
-  intros. apply impl_intro_l. rewrite (into_pure P). by apply pure_elim_l.
-Qed.
-
-Lemma tac_impl_intro_drop Δ P Q : envs_entails Δ Q → envs_entails Δ (P → Q).
-Proof. rewrite /envs_entails=> ?. apply impl_intro_l. by rewrite and_elim_r. Qed.
+Lemma tac_impl_intro_drop Δ P Q R :
+  FromImpl R P Q → envs_entails Δ Q → envs_entails Δ R.
+Proof. rewrite /FromImpl /envs_entails=> <- ?. apply impl_intro_l. by rewrite and_elim_r. Qed.
 
-Lemma tac_wand_intro Δ Δ' i P Q :
+Lemma tac_wand_intro Δ Δ' i P Q R :
+  FromWand R P Q →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ (P -∗ Q).
+  envs_entails Δ' Q → envs_entails Δ R.
 Proof.
-  rewrite /envs_entails=> ? HQ.
+  rewrite /FromWand /envs_entails=> <- ? HQ.
   rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
-Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
+Lemma tac_wand_intro_persistent Δ Δ' i P P' Q R :
+  FromWand R P Q →
   IntoPersistent false P P' →
   TCOr (Affine P) (Absorbing Q) →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ (P -∗ Q).
+  envs_entails Δ' Q → envs_entails Δ R.
 Proof.
-  rewrite /envs_entails => ? HPQ ? HQ. rewrite envs_app_singleton_sound //=.
-  apply wand_intro_l. destruct HPQ.
+  rewrite /FromWand /envs_entails => <- ? HPQ ? HQ.
+  rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
   - rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
             (into_persistent _ P) wand_elim_r //.
   - rewrite (_ : P = □?false P)%I // (into_persistent _ P).
     by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
                absorbingly_sep_l wand_elim_r HQ.
 Qed.
-Lemma tac_wand_intro_pure Δ P φ Q :
+Lemma tac_wand_intro_pure Δ P φ Q R :
+  FromWand R P Q →
   IntoPure P φ →
   TCOr (Affine P) (Absorbing Q) →
-  (φ → envs_entails Δ Q) → envs_entails Δ (P -∗ Q).
+  (φ → envs_entails Δ Q) → envs_entails Δ R.
 Proof.
-  intros ? HPQ HQ. apply wand_intro_l. destruct HPQ.
+  rewrite /FromWand. intros <- ? HPQ HQ. apply wand_intro_l. destruct HPQ.
   - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
     by apply pure_elim_l.
   - rewrite (into_pure P) (persistent_absorbingly_affinely ⌜ _ ⌝%I) absorbingly_sep_lr.
     rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
-Lemma tac_wand_intro_drop Δ P Q :
+Lemma tac_wand_intro_drop Δ P Q R :
+  FromWand R P Q →
   TCOr (Affine P) (Absorbing Q) →
   envs_entails Δ Q →
-  envs_entails Δ (P -∗ Q).
+  envs_entails Δ R.
 Proof.
-  rewrite /envs_entails => HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
+  rewrite /envs_entails /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
 Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],

theories/proofmode/tactics.v

@@ -355,8 +355,9 @@ Local Tactic Notation "iIntro" constr(H) :=
   iStartProof;
   first
   [ (* (?Q → _) *)
-    eapply tac_impl_intro with _ H _; (* (i:=H) *)
-      [env_cbv; apply _ ||
+    eapply tac_impl_intro with _ H _ _ _; (* (i:=H) *)
+      [apply _
+      |env_cbv; apply _ ||
        let P := lazymatch goal with |- Persistent ?P => P end in
        fail 1 "iIntro: introducing non-persistent" H ":" P
               "into non-empty spatial context"
@@ -364,8 +365,9 @@ Local Tactic Notation "iIntro" constr(H) :=
       |apply _
       |]
   | (* (_ -∗ _) *)
-    eapply tac_wand_intro with _ H; (* (i:=H) *)
-      [env_reflexivity || fail 1 "iIntro:" H "not fresh"
+    eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
+      [apply _
+      | env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
   | fail "iIntro: nothing to introduce" ].
 
@@ -373,15 +375,17 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
   iStartProof;
   first
   [ (* (?P → _) *)
-    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
-      [apply _ ||
+    eapply tac_impl_intro_persistent with _ H _ _ _; (* (i:=H) *)
+      [apply _
+      |apply _ ||
        let P := match goal with |- IntoPersistent _ ?P _ => P end in
        fail 1 "iIntro:" P "not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
   | (* (?P -∗ _) *)
-    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
-      [apply _ ||
+    eapply tac_wand_intro_persistent with _ H _ _ _; (* (i:=H) *)
+      [ apply _
+      | apply _ ||
        let P := match goal with |- IntoPersistent _ ?P _ => P end in
        fail 1 "iIntro:" P "not persistent"
       |apply _ ||
@@ -393,10 +397,13 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
 
 Local Tactic Notation "iIntro" "_" :=
   first
-  [ (* (?Q → _) *) iStartProof; apply tac_impl_intro_drop
+  [ (* (?Q → _) *)
+    iStartProof; eapply tac_impl_intro_drop;
+    [ apply _ | ]
   | (* (_ -∗ _) *)
-    iStartProof; apply tac_wand_intro_drop;
-      [apply _ ||
+    iStartProof; eapply tac_wand_intro_drop;
+      [ apply _
+      | apply _ ||
        let P := match goal with |- TCOr (Affine ?P) _ => P end in
        fail 1 "iIntro:" P "not affine and the goal not absorbing"
       |]