Convert tactics that use lookup_delete.

tests/proofmode.ref

@@ -494,9 +494,24 @@ In nested Ltac calls to "iSpecialize (open_constr)",
 "iSpecializeCore (open_constr) as (constr)",
 "iSpecializeCore (open_constr) as (constr)",
 "iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
-Tactic failure: iSpecialize: "H" not found.
+"iSpecializePat (open_constr) (constr)", "iSpecializePat_go" and
+"notypeclasses refine (uconstr)", last call failed.
+Illegal application (Non-functional construction): 
+The expression
+ "coq_tactics.tac_specialize false
+    {|
+    environments.env_intuitionistic := ;
+    environments.env_spatial := "HW" : P -∗ Q
+    "HP" : P
+    ;
+    environments.env_counter := 1%positive |} "H" "HW" 
+    ?q ?P2 ?R ?Q ?f" of type
+ ""HW" : P -∗ Q
+ "HP" : P
+ --------------------------------------∗
+ ?Q
+ " cannot be applied to the term
+ "?y" : "?T"
 "iExact_fail"
      : string
 The command has indeed failed with message:

theories/proofmode/coq_tactics.v

@@ -61,15 +61,18 @@ Proof. intros H. induction H; simpl; apply _. Qed.
 Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.
 Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
 
-(* TODO: convert to not take Δ' *)
-Lemma tac_assumption Δ Δ' i p P Q :
-  envs_lookup_delete true i Δ = Some (p,P,Δ') →
-  FromAssumption p P Q →
-  (if env_spatial_is_nil Δ' then TCTrue
-   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
+Lemma tac_assumption Δ i Q :
+  match envs_lookup_delete true i Δ with
+  | None => False
+  | Some (p,P,Δ') =>
+    FromAssumption p P Q ∧
+    (if env_spatial_is_nil Δ' then TCTrue
+     else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ')))
+  end →
   envs_entails Δ Q.
 Proof.
-  intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
+  destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+  intros (?&H). rewrite envs_entails_eq envs_lookup_delete_sound //.
   destruct (env_spatial_is_nil Δ') eqn:?.
   - by rewrite (env_spatial_is_nil_intuitionistically Δ') // sep_elim_l.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
@@ -88,14 +91,17 @@ Proof.
   by rewrite wand_elim_r.
 Qed.
 
-(* TODO: convert to not take Δ' *)
-Lemma tac_clear Δ Δ' i p P Q :
-  envs_lookup_delete true i Δ = Some (p,P,Δ') →
-  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
-  envs_entails Δ' Q →
+Lemma tac_clear Δ i Q :
+  match envs_lookup_delete true i Δ with
+  | None => False
+  | Some (p,P,Δ') =>
+    (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) ∧
+    envs_entails Δ' Q
+  end →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_delete_sound //.
+  destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+  rewrite envs_entails_eq. intros(?&HQ). rewrite envs_lookup_delete_sound //.
   by destruct p; rewrite /= HQ sep_elim_r.
 Qed.
 
@@ -124,14 +130,18 @@ Proof.
   - by apply pure_intro.
 Qed.
 
-(* TODO: convert to not take Δ' *)
-Lemma tac_pure Δ Δ' i p P φ Q :
-  envs_lookup_delete true i Δ = Some (p, P, Δ') →
-  IntoPure P φ →
-  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
-  (φ → envs_entails Δ' Q) → envs_entails Δ Q.
+Lemma tac_pure Δ i φ Q :
+  match envs_lookup_delete true i Δ with
+  | None => False
+  | Some (p, P, Δ') =>
+    IntoPure P φ ∧
+    (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) ∧
+    (φ → envs_entails Δ' Q)
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> ?? HPQ HQ.
+  destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+  rewrite envs_entails_eq. intros (?&HPQ&HQ).
   rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
   - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
     by apply pure_elim_l.
@@ -253,18 +263,23 @@ Qed.
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
 (* TODO: convert to not take Δ' *)
-Lemma tac_specialize remove_intuitionistic Δ Δ' i p j q P1 P2 R Q :
-  envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ') →
-  envs_lookup j Δ' = Some (q, R) →
-  IntoWand q p R P1 P2 →
-  match envs_replace j q (p && q) (Esnoc Enil j P2) Δ' with
-  | Some Δ'' => envs_entails Δ'' Q
-  | None => False
-  end → envs_entails Δ Q.
+Lemma tac_specialize remove_intuitionistic Δ i j q P2 R Q :
+  match envs_lookup_delete remove_intuitionistic i Δ with
+  | None => False → envs_entails Δ Q
+  | Some (p, P1, Δ') =>
+    envs_lookup j Δ' = Some (q, R) →
+    IntoWand q p R P1 P2 →
+    match envs_replace j q (p && q) (Esnoc Enil j P2) Δ' with
+    | None => False
+    | Some Δ'' => envs_entails Δ'' Q
+    end → envs_entails Δ Q
+  end.
 Proof.
+  destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
   rewrite envs_entails_eq /IntoWand.
-  intros [? ->]%envs_lookup_delete_Some ? HR ?.
-  destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
+  apply envs_lookup_delete_Some in Hlookup as (?&->).
+  destruct (envs_replace) as [Δ''|] eqn:Hrep; last by (intros; exfalso; intuition).
+  intros ? HR <-.
   rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
   rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
   - rewrite -{1}intuitionistically_idemp -{1}intuitionistically_if_idemp.
@@ -273,17 +288,29 @@ Proof.
   - by rewrite HR assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
-  envs_lookup_delete true j Δ = Some (q, R, Δ') →
-  IntoWand q false R P1 P2 → AddModal P1' P1 Q →
-  (''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
-    Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
-    Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
-  envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q.
+Lemma tac_specialize_assert Δ j neg js P1 P2 P1' Q :
+  match envs_lookup_delete true j Δ with
+  | None => False → envs_entails Δ Q
+  | Some (q, R, Δ') =>
+    IntoWand q false R P1 P2 →
+    AddModal P1' P1 Q →
+    match
+      (''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
+       Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
+       Some (Δ1,Δ2')) (* does not preserve position of [j] *)
+    with
+    | None => False → envs_entails Δ Q
+    | Some (Δ1,Δ2') =>
+      envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q
+    end
+  end.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
-  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
-    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
+  destruct envs_lookup_delete as [((q&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+  rewrite envs_entails_eq. apply envs_lookup_delete_Some in Hlookup as (?&->).
+  intros ? ?.
+  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:Heq_split; simplify_eq/=; last by (intros; exfalso).
+  destruct (envs_app _ _ _) eqn:Heq_app; simplify_eq/=; last by (intros; exfalso).
+  intros HP1 HQ.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_singleton_sound Δ2) //; simpl.
   rewrite HP1 (into_wand q false) /= -(add_modal P1' P1 Q). cancel [P1'].
@@ -297,15 +324,21 @@ Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
 Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
 Proof. by unlock. Qed.
 
-Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
-  envs_lookup_delete true j Δ = Some (q, R, Δ') →
-  IntoWand q false R P1 P2 →
-  AddModal P1' P1 Q →
-  envs_entails Δ' (P1' ∗ locked Q') →
-  Q' = (P2 -∗ Q)%I →
-  envs_entails Δ Q.
+Lemma tac_specialize_frame Δ j P1 P2 P1' Q Q' :
+  match envs_lookup_delete true j Δ with
+  | None => False → envs_entails Δ Q
+  | Some (q, R, Δ') =>
+    IntoWand q false R P1 P2 →
+    AddModal P1' P1 Q →
+    envs_entails Δ' (P1' ∗ locked Q') →
+    Q' = (P2 -∗ Q)%I →
+    envs_entails Δ Q
+  end.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
+  destruct envs_lookup_delete as [((q&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+  rewrite envs_entails_eq.
+  apply envs_lookup_delete_Some in Hlookup as (?&->).
+  intros ? ? HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
   rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
@@ -330,20 +363,27 @@ Proof.
   by rewrite intuitionistically_emp left_id wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert_intuitionistic Δ Δ' j q P1 P1' P2 R Q :
-  envs_lookup_delete true j Δ = Some (q, R, Δ') →
-  IntoWand q true R P1 P2 →
-  Persistent P1 →
-  IntoAbsorbingly P1' P1 →
-  envs_entails Δ' P1' →
-  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
-  | Some Δ'' => envs_entails Δ'' Q
-  | None => False
-  end → envs_entails Δ Q.
+Lemma tac_specialize_assert_intuitionistic Δ j P1 P1' P2 Q :
+  match envs_lookup_delete true j Δ with
+  | None => False → envs_entails Δ Q
+  | Some (q, R, Δ') =>
+    IntoWand q true R P1 P2 →
+    Persistent P1 →
+    IntoAbsorbingly P1' P1 →
+    envs_entails Δ' P1' →
+    match envs_simple_replace j q (Esnoc Enil j P2) Δ with
+    | None => False → envs_entails Δ Q
+    | Some Δ'' =>
+      envs_entails Δ'' Q → envs_entails Δ Q
+    end
+  end.
 Proof.
-  rewrite envs_entails_eq => /envs_lookup_delete_Some [? ->] ??? HP1 HQ.
-  destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
-  rewrite -HQ envs_lookup_sound //.
+  destruct envs_lookup_delete as [((q&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+  apply envs_lookup_delete_Some in Hlookup as (?&->).
+  rewrite envs_entails_eq.
+  destruct (envs_simple_replace) as [Δ''|] eqn:Hrep; last by (intros; exfalso; intuition).
+  intros ? ? ? HP1 <- .
+  rewrite envs_lookup_sound //.
   rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
   rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
   rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
@@ -464,12 +504,17 @@ Proof.
   by rewrite wand_elim_r.
 Qed.
 
-Lemma tac_apply Δ Δ' i p R P1 P2 :
-  envs_lookup_delete true i Δ = Some (p, R, Δ') →
-  IntoWand p false R P1 P2 →
-  envs_entails Δ' P1 → envs_entails Δ P2.
+Lemma tac_apply Δ i P1 P2 :
+  match envs_lookup_delete true i Δ with
+  | None => False
+  | Some (p, R, Δ') =>
+    IntoWand p false R P1 P2 ∧
+    envs_entails Δ' P1
+  end →
+  envs_entails Δ P2.
 Proof.
-  rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_delete_sound //.
+  destruct envs_lookup_delete as [((p&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+  rewrite envs_entails_eq. intros (?&HP1). rewrite envs_lookup_delete_sound //.
   by rewrite (into_wand p false) /= HP1 wand_elim_l.
 Qed.
 
@@ -570,13 +615,19 @@ Proof.
   auto using and_intro, pure_intro.
 Qed.
 
-Lemma tac_frame Δ Δ' i p R P Q :
-  envs_lookup_delete false i Δ = Some (p, R, Δ') →
-  Frame p R P Q →
-  envs_entails Δ' Q → envs_entails Δ P.
+Lemma tac_frame Δ i P Q :
+  match envs_lookup_delete false i Δ with
+  | None => False
+  | Some (p, R, Δ') =>
+    Frame p R P Q ∧
+    envs_entails Δ' Q
+  end →
+  envs_entails Δ P.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hframe HQ.
-  rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
+  destruct envs_lookup_delete as [((p&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+  rewrite envs_entails_eq. intros (Hframe&Heq).
+  apply envs_lookup_delete_Some in Hlookup as (?&->).
+  rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe Heq.
 Qed.
 
 (** * Disjunction *)

theories/proofmode/ltac_tactics.v

@@ -172,15 +172,20 @@ Ltac iElaborateSelPat pat :=
   end.
 
 Local Ltac iClearHyp H :=
-  eapply tac_clear with _ H _ _; (* (i:=H) *)
-    [pm_reflexivity ||
-     let H := pretty_ident H in
-     fail "iClear:" H "not found"
-    |pm_reduce; iSolveTC ||
-     let H := pretty_ident H in
-     let P := match goal with |- TCOr (Affine ?P) _ => P end in
-     fail "iClear:" H ":" P "not affine and the goal not absorbing"
-    |].
+  eapply tac_clear with H; (* (i:=H) *)
+    pm_reduce;
+    lazymatch goal with
+    | |- False =>
+      let H := pretty_ident H in
+      fail "iClear:" H "not found"
+    | _ =>
+      esplit;
+      [pm_reduce; iSolveTC ||
+       let H := pretty_ident H in
+       let P := match goal with |- TCOr (Affine ?P) _ => P end in
+       fail "iClear:" H ":" P "not affine and the goal not absorbing"
+      |]
+    end.
 
 Local Ltac iClear_go Hs :=
   lazymatch Hs with
@@ -228,17 +233,22 @@ Ltac, but it may be possible in Ltac2. *)
 
 (** * Assumptions *)
 Tactic Notation "iExact" constr(H) :=
-  eapply tac_assumption with _ H _ _; (* (i:=H) *)
-    [pm_reflexivity ||
-     let H := pretty_ident H in
-     fail "iExact:" H "not found"
-    |iSolveTC ||
-     let H := pretty_ident H in
-     let P := match goal with |- FromAssumption _ ?P _ => P end in
-     fail "iExact:" H ":" P "does not match goal"
-    |pm_reduce; iSolveTC ||
-     let H := pretty_ident H in
-     fail "iExact:" H "not absorbing and the remaining hypotheses not affine"].
+  eapply tac_assumption with H; (* (i:=H) *)
+    pm_reduce;
+    lazymatch goal with
+    |- False =>
+       let H := pretty_ident H in
+       fail "iExact:" H "not found"
+    | _ =>
+       split;
+       [iSolveTC ||
+        let H := pretty_ident H in
+        let P := match goal with |- FromAssumption _ ?P _ => P end in
+        fail "iExact:" H ":" P "does not match goal"
+       |pm_reduce; iSolveTC ||
+        let H := pretty_ident H in
+        fail "iExact:" H "not absorbing and the remaining hypotheses not affine"]
+    end.
 
 Tactic Notation "iAssumptionCore" :=
   let rec find Γ i P :=
@@ -262,11 +272,16 @@ Tactic Notation "iAssumption" :=
     lazymatch Γ with
     | Esnoc ?Γ ?j ?P => first
        [pose proof (_ : FromAssumption p P Q) as Hass;
-        eapply (tac_assumption _ _ j p P);
-          [pm_reflexivity
-          |apply Hass
-          |pm_reduce; iSolveTC ||
-           fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
+        eapply (tac_assumption _ j);
+          pm_reduce;
+          lazymatch goal with
+          |- False => fail 1
+          | _ =>
+            split;
+           [apply Hass
+            |pm_reduce; iSolveTC ||
+            fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
+          end
        |assert (P = False%I) as Hass by reflexivity;
         apply (tac_false_destruct _ j p P);
           [pm_reflexivity
@@ -297,17 +312,22 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
     |pm_reduce].
 
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
-  eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
-    [pm_reflexivity ||
-     let H := pretty_ident H in
-     fail "iPure:" H "not found"
-    |iSolveTC ||
-     let P := match goal with |- IntoPure ?P _ => P end in
-     fail "iPure:" P "not pure"
-    |pm_reduce; iSolveTC ||
-     let P := match goal with |- TCOr (Affine ?P) _ => P end in
-     fail "iPure:" P "not affine and the goal not absorbing"
-    |intros pat].
+  eapply tac_pure with H _; (* (i:=H1) *)
+    pm_reduce;
+    lazymatch goal with
+    | |- False =>
+      let H := pretty_ident H in
+      fail "iPure:" H "not found"
+    | _ =>
+      split_and!;
+      [iSolveTC ||
+       let P := match goal with |- IntoPure ?P _ => P end in
+       fail "iPure:" P "not pure"
+       |pm_reduce; iSolveTC ||
+       let P := match goal with |- TCOr (Affine ?P) _ => P end in
+       fail "iPure:" P "not affine and the goal not absorbing"
+       |intros pat]
+    end.
 
 Tactic Notation "iEmpIntro" :=
   iStartProof;
@@ -342,14 +362,19 @@ Local Ltac iFramePure t :=
 
 Local Ltac iFrameHyp H :=
   iStartProof;
-  eapply tac_frame with _ H _ _ _;
-    [pm_reflexivity ||
-     let H := pretty_ident H in
-     fail "iFrame:" H "not found"
-    |iSolveTC ||
-     let R := match goal with |- Frame _ ?R _ _ => R end in
-     fail "iFrame: cannot frame" R
-    |iFrameFinish].
+  eapply tac_frame with H _;
+    [pm_reduce;
+     lazymatch goal with
+     |- False =>
+       let H := pretty_ident H in
+       fail "iFrame:" H "not found"
+     | _ =>
+       split;
+       [iSolveTC ||
+       let R := match goal with |- Frame _ ?R _ _ => R end in
+       fail "iFrame: cannot frame" R
+       |iFrameFinish]
+     end].
 
 Local Ltac iFrameAnyPure :=
   repeat match goal with H : _ |- _ => iFramePure H end.
@@ -784,18 +809,28 @@ Ltac iSpecializePat_go H1 pats :=
     | SIdent ?H2 [] :: ?pats =>
        (* If we not need to specialize [H2] we can avoid a lot of unncessary
        context manipulation. *)
-       notypeclasses refine (tac_specialize false _ _ H2 _ H1 _ _ _ _ _ _ _ _ _);
-         [pm_reflexivity ||
-          let H2 := pretty_ident H2 in
-          fail "iSpecialize:" H2 "not found"
-         |pm_reflexivity ||
+         match goal with
+         | |- envs_entails ?Δ _ =>
+       notypeclasses refine (tac_specialize false Δ H2 H1 _ _ _ _ _ _ _);
+       [ lazymatch goal with
+       | |- False =>
+         let H2 := pretty_ident H2 in
+         fail "iSpecialize:" H2 "not found"
+       | _ =>
+         pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
+         end
          |iSolveTC ||
           let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
           let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
           fail "iSpecialize: cannot instantiate" P "with" Q
-         |pm_reduce; iSpecializePat_go H1 pats]
+         |pm_reduce;
+          lazymatch goal with
+            | |- False => fail
+            | _ => iSpecializePat_go H1 pats
+          end]
+       end
     | SIdent ?H2 ?pats1 :: ?pats =>
        (* If [H2] is in the intuitionistic context, we copy it into a new
        hypothesis [Htmp], so that it can be used multiple times. *)
@@ -811,18 +846,29 @@ Ltac iSpecializePat_go H1 pats :=
          Ltac backtraces (which would otherwise include the whole closure). *)
          [.. (* side-conditions of [iSpecialize] *)
          |(* Use [remove_intuitionistic = true] to remove the copy [Htmp]. *)
-          notypeclasses refine (tac_specialize true _ _ H2tmp _ H1 _ _ _ _ _ _ _ _ _);
-            [pm_reflexivity ||
-             let H2tmp := pretty_ident H2tmp in
-             fail "iSpecialize:" H2tmp "not found"
-            |pm_reflexivity ||
+         match goal with
+         | |- envs_entails ?Δ _ =>
+           (* TODO: the error handling here does not seem correct now *)
+          notypeclasses refine (tac_specialize true Δ H2tmp H1 _ _ _ _ _ _ _);
+          [ lazymatch goal with
+          | |- False =>
+            let H2tmp := pretty_ident H2tmp in
+            fail "iSpecialize:" H2tmp "not found"
+          | _ =>
+            pm_reflexivity ||
              let H1 := pretty_ident H1 in
              fail "iSpecialize:" H1 "not found"
+            end
             |iSolveTC ||
              let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
              let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
              fail "iSpecialize: cannot instantiate" P "with" Q
-            |pm_reduce; iSpecializePat_go H1 pats]]
+            |pm_reduce;
+             lazymatch goal with
+               | |- False => fail
+               | _ => iSpecializePat_go H1 pats
+             end]
+         end]
     | SPureGoal ?d :: ?pats =>
        notypeclasses refine (tac_specialize_assert_pure _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
@@ -836,62 +882,92 @@ Ltac iSpecializePat_go H1 pats :=
          |pm_reduce;
           iSpecializePat_go H1 pats]
     | SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
-       notypeclasses refine (tac_specialize_assert_intuitionistic _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
-         [pm_reflexivity ||
-          let H1 := pretty_ident H1 in
-          fail "iSpecialize:" H1 "not found"
-         |solve_to_wand H1
-         |iSolveTC ||
-          let Q := match goal with |- Persistent ?Q => Q end in
-          fail "iSpecialize:" Q "not persistent"
-         |iSolveTC
-         |iFrame Hs_frame; solve_done d (*goal*)
-         |pm_reduce; iSpecializePat_go H1 pats]
+       match goal with
+       | |- envs_entails ?Δ _ =>
+         notypeclasses refine (tac_specialize_assert_intuitionistic Δ H1 _ _ _ _ _ _ _ _ _);
+         [ lazymatch goal with
+           | |- False =>
+             let H1 := pretty_ident H1 in
+             fail "iSpecialize:" H1 "not found"
+           | _ =>
+           solve_to_wand H1
+           end
+           |iSolveTC ||
+            let Q := match goal with |- Persistent ?Q => Q end in
+            fail "iSpecialize:" Q "not persistent"
+           |iSolveTC
+           |iFrame Hs_frame; solve_done d (*goal*)
+           | pm_reduce; iSpecializePat_go H1 pats]
+       end
     | SGoal (SpecGoal GIntuitionistic _ _ _ _) :: ?pats =>
        fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
     | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
        let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
-       notypeclasses refine (tac_specialize_assert _ _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _);
-         [pm_reflexivity ||
-          let H1 := pretty_ident H1 in
-          fail "iSpecialize:" H1 "not found"
-         |solve_to_wand H1
-         |lazymatch m with
-          | GSpatial => class_apply add_modal_id
-          | GModal => iSolveTC || fail "iSpecialize: goal not a modality"