proofmode: make it possible for class_instances to use the proofmode

_CoqProject

@@ -95,6 +95,7 @@ theories/heap_lang/lib/increment.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
+theories/proofmode/ltac_tactics.v
 theories/proofmode/environments.v
 theories/proofmode/intro_patterns.v
 theories/proofmode/spec_patterns.v

theories/proofmode/ltac_tactics.v

+From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
+From iris.bi Require Export bi.
+From stdpp Require Import namespaces.
+From iris.proofmode Require Export classes notation.
+From stdpp Require Import hlist pretty.
+Set Default Proof Using "Type".
+Export ident.
+
+Declare Reduction env_cbv := cbv [
+  option_bind
+  beq ascii_beq string_beq positive_beq Pos.succ ident_beq
+  env_lookup env_lookup_delete env_delete env_app env_replace env_dom
+  env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
+  envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
+    envs_simple_replace envs_replace envs_split
+    envs_clear_spatial envs_clear_persistent envs_incr_counter
+    envs_split_go envs_split prop_of_env].
+Ltac env_cbv :=
+  match goal with |- ?u => let v := eval env_cbv in u in change v end.
+Ltac env_reflexivity := env_cbv; exact eq_refl.
+
+(** For most of the tactics, we want to have tight control over the order and
+way in which type class inference is performed. To that end, many tactics make
+use of [notypeclasses refine] and the [iSolveTC] tactic to manually invoke type
+class inference.
+
+The tactic [iSolveTC] does not use [apply _], as that often leads to issues
+because it will try to solve all evars whose type is a typeclass, in
+dependency order (according to Matthieu). If one fails, it aborts. However, we
+generally rely on progress on the main goal to be solved to make progress
+elsewhere. With [typeclasses eauto], that seems to work better.
+
+A drawback of [typeclasses eauto] is that it is multi-success, i.e. whenever
+subsequent tactics fail, it will backtrack to [typeclasses eauto] to try the
+next type class instance. This is almost always undesired and leads to poor
+performance and horrible error messages, so we wrap it in a [once]. *)
+Ltac iSolveTC :=
+  solve [once (typeclasses eauto)].
+
+(** * Misc *)
+
+Ltac iMissingHyps Hs :=
+  let Δ :=
+    lazymatch goal with
+    | |- envs_entails ?Δ _ => Δ
+    | |- context[ envs_split _ _ ?Δ ] => Δ
+    end in
+  let Hhyps := eval env_cbv in (envs_dom Δ) in
+  eval vm_compute in (list_difference Hs Hhyps).
+
+Ltac iTypeOf H :=
+  let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
+  eval env_cbv in (envs_lookup H Δ).
+
+Tactic Notation "iMatchHyp" tactic1(tac) :=
+  match goal with
+  | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
+  end.
+
+(** * Start a proof *)
+Tactic Notation "iStartProof" :=
+  lazymatch goal with
+  | |- envs_entails _ _ => idtac
+  | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
+               [apply _ || fail "iStartProof: not a Bi entailment"
+               |apply tac_adequate]
+  end.
+
+(* Same as above, with 2 differences :
+   - We can specify a BI in which we want the proof to be done
+   - If the goal starts with a let or a ∀, they are automatically
+     introduced. *)
+Tactic Notation "iStartProof" uconstr(PROP) :=
+  lazymatch goal with
+  | |- @envs_entails ?PROP' _ _ =>
+    (* This cannot be shared with the other [iStartProof], because
+    type_term has a non-negligeable performance impact. *)
+    let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
+
+  (* We eta-expand [as_emp_valid_2], in order to make sure that
+     [iStartProof PROP] works even if [PROP] is the carrier type. In
+     this case, typing this expression will end up unifying PROP with
+     [bi_car _], and hence trigger the canonical structures mechanism
+     to find the corresponding bi. *)
+  | |- ?φ => notypeclasses refine ((λ P : PROP, @as_emp_valid_2 φ _ P) _ _ _);
+               [apply _ || fail "iStartProof: not a Bi entailment"
+               |apply tac_adequate]
+  end.
+
+(** * Generate a fresh identifier *)
+(* Tactic Notation tactics cannot return terms *)
+Ltac iFresh :=
+  (* We need to increment the environment counter using [tac_fresh].
+     But because [iFresh] returns a value, we have to let bind
+     [tac_fresh] wrapped under a match to force evaluation of this
+     side-effect. See https://stackoverflow.com/a/46178884 *)
+  let do_incr :=
+      lazymatch goal with
+      | _ => iStartProof; eapply tac_fresh; first by (env_reflexivity)
+      end in
+  lazymatch goal with
+  |- envs_entails ?Δ _ =>
+    let n := eval env_cbv in (env_counter Δ) in
+    constr:(IAnon n)
+  end.
+
+(** * Simplification *)
+Tactic Notation "iEval" tactic(t) :=
+  iStartProof;
+  eapply tac_eval;
+    [let x := fresh in intros x; t; unfold x; reflexivity
+    |].
+
+Tactic Notation "iEval" tactic(t) "in" constr(H) :=
+  iStartProof;
+  eapply tac_eval_in with _ H _ _ _;
+    [env_reflexivity || fail "iEval:" H "not found"
+    |let x := fresh in intros x; t; unfold x; reflexivity
+    |env_reflexivity
+    |].
+
+Tactic Notation "iSimpl" := iEval simpl.
+Tactic Notation "iSimpl" "in" constr(H) := iEval simpl in H.
+
+(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
+pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
+
+  https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html
+
+PMP told me (= Robbert) in person that this is not possible today, but may be
+possible in Ltac2. *)
+
+(** * Context manipulation *)
+Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
+  eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
+    [env_reflexivity || fail "iRename:" H1 "not found"
+    |env_reflexivity || fail "iRename:" H2 "not fresh"|].
+
+Local Inductive esel_pat :=
+  | ESelPure
+  | ESelIdent : bool → ident → esel_pat.
+
+Ltac iElaborateSelPat pat :=
+  let rec go pat Δ Hs :=
+    lazymatch pat with
+    | [] => eval cbv in Hs
+    | SelPure :: ?pat => go pat Δ (ESelPure :: Hs)
+    | SelPersistent :: ?pat =>
+       let Hs' := eval env_cbv in (env_dom (env_intuitionistic Δ)) in
+       let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
+       go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
+    | SelSpatial :: ?pat =>
+       let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
+       let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
+       go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
+    | SelIdent ?H :: ?pat =>
+       lazymatch eval env_cbv in (envs_lookup_delete false H Δ) with
+       | Some (?p,_,?Δ') => go pat Δ' (ESelIdent p H :: Hs)
+       | None => fail "iElaborateSelPat:" H "not found"
+       end
+    end in
+  lazymatch goal with
+  | |- envs_entails ?Δ _ =>
+    let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
+  end.
+
+Local Ltac iClearHyp H :=
+  eapply tac_clear with _ H _ _; (* (i:=H) *)
+    [env_reflexivity || fail "iClear:" H "not found"
+    |env_cbv; apply _ ||
+     let P := match goal with |- TCOr (Affine ?P) _ => P end in
+     fail "iClear:" H ":" P "not affine and the goal not absorbing"
+    |].
+
+Tactic Notation "iClear" constr(Hs) :=
+  let rec go Hs :=
+    lazymatch Hs with
+    | [] => idtac
+    | ESelPure :: ?Hs => clear; go Hs
+    | ESelIdent _ ?H :: ?Hs => iClearHyp H; go Hs
+    end in
+  let Hs := iElaborateSelPat Hs in iStartProof; go Hs.
+
+Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
+  iClear Hs; clear xs.
+
+(** * Assumptions *)
+Tactic Notation "iExact" constr(H) :=
+  eapply tac_assumption with _ H _ _; (* (i:=H) *)
+    [env_reflexivity || fail "iExact:" H "not found"
+    |apply _ ||
+     let P := match goal with |- FromAssumption _ ?P _ => P end in
+     fail "iExact:" H ":" P "does not match goal"
+    |env_cbv; apply _ ||
+     fail "iExact:" H "not absorbing and the remaining hypotheses not affine"].
+
+Tactic Notation "iAssumptionCore" :=
+  let rec find Γ i P :=
+    lazymatch Γ with
+    | Esnoc ?Γ ?j ?Q => first [unify P Q; unify i j|find Γ i P]
+    end in
+  match goal with
+  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
+     first [is_evar i; fail 1 | env_reflexivity]
+  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
+     is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
+     first [is_evar i; fail 1 | env_reflexivity]
+  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
+     is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
+  end.
+
+Tactic Notation "iAssumption" :=
+  let Hass := fresh in
+  let rec find p Γ Q :=
+    lazymatch Γ with
+    | Esnoc ?Γ ?j ?P => first
+       [pose proof (_ : FromAssumption p P Q) as Hass;
+        eapply (tac_assumption _ _ j p P);
+          [env_reflexivity
+          |apply Hass
+          |env_cbv; apply _ ||
+           fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
+       |assert (P = False%I) as Hass by reflexivity;
+        apply (tac_false_destruct _ j p P);
+          [env_reflexivity
+          |exact Hass]
+       |find p Γ Q]
+    end in
+  lazymatch goal with
+  | |- envs_entails (Envs ?Γp ?Γs _) ?Q =>
+     first [find true Γp Q | find false Γs Q
+           |fail "iAssumption:" Q "not found"]
+  end.
+
+(** * False *)
+Tactic Notation "iExFalso" := apply tac_ex_falso.
+
+(** * Making hypotheses persistent or pure *)
+Local Tactic Notation "iPersistent" constr(H) :=
+  eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
+    [env_reflexivity || fail "iPersistent:" H "not found"
+    |apply _ ||
+     let P := match goal with |- IntoPersistent _ ?P _ => P end in
+     fail "iPersistent:" P "not persistent"
+    |env_cbv; apply _ ||
+     let P := match goal with |- TCOr (Affine ?P) _ => P end in
+     fail "iPersistent:" P "not affine and the goal not absorbing"
+    |env_reflexivity|].
+
+Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
+  eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
+    [env_reflexivity || fail "iPure:" H "not found"
+    |apply _ ||
+     let P := match goal with |- IntoPure ?P _ => P end in
+     fail "iPure:" P "not pure"
+    |env_cbv; apply _ ||
+     let P := match goal with |- TCOr (Affine ?P) _ => P end in
+     fail "iPure:" P "not affine and the goal not absorbing"
+    |intros pat].
+
+Tactic Notation "iEmpIntro" :=
+  iStartProof;
+  eapply tac_emp_intro;
+    [env_cbv; apply _ ||
+     fail "iEmpIntro: spatial context contains non-affine hypotheses"].
+
+Tactic Notation "iPureIntro" :=
+  iStartProof;
+  eapply tac_pure_intro;
+    [env_reflexivity
+    |apply _ ||
+     let P := match goal with |- FromPure _ ?P _ => P end in
+     fail "iPureIntro:" P "not pure"
+    |].
+
+(** Framing *)
+Local Ltac iFrameFinish :=
+  lazy iota beta;
+  try match goal with
+  | |- envs_entails _ True => by iPureIntro
+  | |- envs_entails _ emp => iEmpIntro
+  end.
+
+Local Ltac iFramePure t :=
+  iStartProof;
+  let φ := type of t in
+  eapply (tac_frame_pure _ _ _ _ t);
+    [apply _ || fail "iFrame: cannot frame" φ
+    |iFrameFinish].
+
+Local Ltac iFrameHyp H :=
+  iStartProof;
+  eapply tac_frame with _ H _ _ _;
+    [env_reflexivity || fail "iFrame:" H "not found"
+    |apply _ ||
+     let R := match goal with |- Frame _ ?R _ _ => R end in
+     fail "iFrame: cannot frame" R
+    |iFrameFinish].
+
+Local Ltac iFrameAnyPure :=
+  repeat match goal with H : _ |- _ => iFramePure H end.
+
+Local Ltac iFrameAnyPersistent :=
+  iStartProof;
+  let rec go Hs :=
+    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
+  match goal with
+  | |- envs_entails ?Δ _ =>
+     let Hs := eval cbv in (env_dom (env_intuitionistic Δ)) in go Hs
+  end.
+
+Local Ltac iFrameAnySpatial :=
+  iStartProof;
+  let rec go Hs :=
+    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
+  match goal with
+  | |- envs_entails ?Δ _ =>
+     let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
+  end.
+
+Tactic Notation "iFrame" := iFrameAnySpatial.
+
+Tactic Notation "iFrame" "(" constr(t1) ")" :=
+  iFramePure t1.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" :=
+  iFramePure t1; iFrame ( t2 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" :=
+  iFramePure t1; iFrame ( t2 t3 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) ")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) ")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) constr(t7) ")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ).
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) constr(t7) constr(t8)")" :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ).
+
+Tactic Notation "iFrame" constr(Hs) :=
+  let rec go Hs :=
+    lazymatch Hs with
+    | [] => idtac
+    | SelPure :: ?Hs => iFrameAnyPure; go Hs
+    | SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
+    | SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
+    | SelIdent ?H :: ?Hs => iFrameHyp H; go Hs
+    end
+  in let Hs := sel_pat.parse Hs in go Hs.
+Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
+  iFramePure t1; iFrame Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")"
+    constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) constr(t7) ")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ) Hs.
+Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
+    constr(t5) constr(t6) constr(t7) constr(t8)")" constr(Hs) :=
+  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ) Hs.
+
+(** * Basic introduction tactics *)
+Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
+  (* In the case the goal starts with an [let x := _ in _], we do not
+     want to unfold x and start the proof mode. Instead, we want to
+     use intros. So [iStartProof] has to be called only if [intros]
+     fails *)
+  intros x ||
+    (iStartProof;
+     lazymatch goal with
+     | |- envs_entails _ _ =>
+       eapply tac_forall_intro;
+       [apply _ ||
+              let P := match goal with |- FromForall ?P _ => P end in
+              fail "iIntro: cannot turn" P "into a universal quantifier"
+       |lazy beta; intros x]
+     end).
+
+Local Tactic Notation "iIntro" constr(H) :=
+  iStartProof;
+  first
+  [ (* (?Q → _) *)
+    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"
+      |env_reflexivity || fail 1 "iIntro:" H "not fresh"
+      |apply _
+      |]
+  | (* (_ -∗ _) *)
+    eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
+      [apply _
+      | env_reflexivity || fail 1 "iIntro:" H "not fresh"
+      |]
+  | fail "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntro" "#" constr(H) :=
+  iStartProof;
+  first
+  [ (* (?P → _) *)
+    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 _
+      | apply _ ||
+       let P := match goal with |- IntoPersistent _ ?P _ => P end in
+       fail 1 "iIntro:" P "not persistent"
+      |apply _ ||
+       let P := match goal with |- TCOr (Affine ?P) _ => P end in
+       fail 1 "iIntro:" P "not affine and the goal not absorbing"
+      |env_reflexivity || fail 1 "iIntro:" H "not fresh"
+      |]
+  | fail "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntro" "_" :=
+  first
+  [ (* (?Q → _) *)
+    iStartProof; eapply tac_impl_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"
+      |]
+  | (* (∀ _, _) *) iIntro (_)
+  | fail 1 "iIntro: nothing to introduce" ].
+
+Local Tactic Notation "iIntroForall" :=
+  lazymatch goal with
+  | |- ∀ _, ?P => fail (* actually an →, this is handled by iIntro below *)
+  | |- ∀ _, _ => intro
+  | |- let _ := _ in _ => intro
+  | |- _ =>
+    iStartProof;
+    lazymatch goal with
+    | |- envs_entails _ (∀ x : _, _) => let x' := fresh x in iIntro (x')
+    end
+  end.
+Local Tactic Notation "iIntro" :=
+  lazymatch goal with
+  | |- _ → ?P => intro
+  | |- _ =>
+    iStartProof;
+    lazymatch goal with
+    | |- envs_entails _ (_ -∗ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+    | |- envs_entails _ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+    end
+  end.
+
+(** * Specialize *)
+Record iTrm {X As S} :=
+  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : S }.
+Arguments ITrm {_ _ _} _ _ _.
+
+Notation "( H $! x1 .. xn )" :=
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
+Notation "( H $! x1 .. xn 'with' pat )" :=
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
+Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
+
+(** There is some hacky stuff going on here: because of Coq bug #6583, unresolved
+type classes in the arguments `xs` are resolved at arbitrary moments. Tactics
+like `apply`, `split` and `eexists` wrongly trigger type class search to resolve
+these holes. To avoid TC being triggered too eagerly, this tactic uses `refine`
+at most places instead of `apply`. *)
+Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
+  let rec go xs :=
+    lazymatch xs with
+    | hnil => idtac
+    | hcons ?x ?xs =>
+       notypeclasses refine (tac_forall_specialize _ _ H _ _ _ _ _ _ _);
+         [env_reflexivity || fail "iSpecialize:" H "not found"
+         |iSolveTC ||
+          let P := match goal with |- IntoForall ?P _ => P end in
+          fail "iSpecialize: cannot instantiate" P "with" x
+         |lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
+          | |- ∃ _ : ?A, _ =>
+            notypeclasses refine (@ex_intro A _ x (conj _ _))
+          end; [shelve..|env_reflexivity|go xs]]
+    end in
+  go xs.
+
+Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
+  let solve_to_wand H1 :=
+    iSolveTC ||
+    let P := match goal with |- IntoWand _ _ ?P _ _ => P end in
+    fail "iSpecialize:" P "not an implication/wand" in
+  let solve_done d :=
+    lazymatch d with
+    | true =>
+       done ||
+       let Q := match goal with |- envs_entails _ ?Q => Q end in
+       fail "iSpecialize: cannot solve" Q "using done"
+    | false => idtac
+    end in
+  let rec go H1 pats :=
+    lazymatch pats with
+    | [] => idtac
+    | SForall :: ?pats =>
+       idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
+       go H1 pats
+    | SIdent ?H2 :: ?pats =>
+       notypeclasses refine (tac_specialize _ _ _ H2 _ H1 _ _ _ _ _ _ _ _ _ _);
+         [env_reflexivity || fail "iSpecialize:" H2 "not found"
+         |env_reflexivity || fail "iSpecialize:" H1 "not found"
+         |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
+         |env_reflexivity|go H1 pats]
+    | SPureGoal ?d :: ?pats =>
+       notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
+         [env_reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |iSolveTC ||
+          let Q := match goal with |- FromPure _ ?Q _ => Q end in
+          fail "iSpecialize:" Q "not pure"
+         |env_reflexivity
+         |solve_done d (*goal*)
+         |go H1 pats]
+    | SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
+       notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
+         [env_reflexivity || 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
+         |env_reflexivity
+         |iFrame Hs_frame; solve_done d (*goal*)
+         |go H1 pats]
+    | SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
+       fail "iSpecialize: cannot select hypotheses for persistent 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' _ _ _ _ _ _ _ _ _ _ _);
+         [env_reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |lazymatch m with