phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/ltac_tactics.v *)
(* Converts a selection pattern (given as a string) to a list of
elaborated selection patterns. *)
Ltac iElaborateSelPat pat
:=
  lazymatch goal with
  | |- envs_entails ?Δ _ =>
    let pat := sel_pat.parse pat in iElaborateSelPat_go pat Δ (@nil esel_pat)
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iClearHyp H
:=
  notypeclasses refine (tac_clear _ H _ _ _ _ _ _); (* (i:=H) *)
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iClear:" H "not found"
    |pm_reduce; tc_solve ||
     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"
    |pm_reduce].
(* iris/proofmode/ltac_tactics.v *)
Ltac iClear_go Hs
:=
  lazymatch Hs with
  | [] => idtac
  | ESelPure :: ?Hs => clear; iClear_go Hs
  | ESelIdent _ ?H :: ?Hs => _iClearHyp H; iClear_go Hs
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac iEval_go t Hs
:=
  lazymatch Hs with
  | [] => idtac
  | ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
  | ESelIdent _ ?H :: ?Hs =>
    notypeclasses refine (tac_eval_in _ H _ _ _ _ _ _ _);
      [pm_reflexivity || let H := pretty_ident H in fail "iEval:" H "not found"
      |let x := fresh in intros x; t; unfold x; reflexivity
      |pm_reduce; iEval_go t Hs]
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iUnfold r
:= iEval (unfold r).
(* iris/proofmode/ltac_tactics.v *)
Ltac _iUnfold_in r H
:= iEval (unfold r) in H.
(* iris/proofmode/ltac_tactics.v *)
(* * Making hypotheses intuitionistic or pure *)
Ltac _iIntuitionistic H H'
:=
  notypeclasses refine (tac_intuitionistic _ H H' _ _ _ _ _ _ _ _); (* (i:=H) (j:=H') *)
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iIntuitionistic:" H "not found"
    |tc_solve ||
     let P := match goal with |- IntoPersistent _ ?P _ => P end in
     fail "iIntuitionistic:" P "not persistent"
    |pm_reduce; tc_solve ||
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iIntuitionistic:" P "not affine and the goal not absorbing"
    |pm_reduce;
     lazymatch goal with
     | |- False =>
       let H' := pretty_ident H' in
       fail "iIntuitionistic:" H' "not fresh"
     | _ => idtac (* subgoal *)
     end].
(* iris/proofmode/ltac_tactics.v *)
Ltac _iSpatial H H'
:=
  notypeclasses refine (tac_spatial _ H H' _ _ _ _ _ _ _);
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iSpatial:" H "not found"
    |pm_reduce; tc_solve
    |pm_reduce;
     lazymatch goal with
     | |- False =>
       let H' := pretty_ident H' in
       fail "iSpatial:" H' "not fresh"
     | _ => idtac (* subgoal *)
     end].
(* iris/proofmode/ltac_tactics.v *)
(* The [iFrame] tactic either finishes the goal (if it becomes [True] or
[emp]) or makes progress and gives a new goal.

The (internal) tactic [_iFrameFinish] closes the goal if it is [True] or [emp].
We have to be careful when to call this tactic. We should only call it when
no more hypotheses to frame are left. For instance, given [H1 : P, H2 : Q] and
goal [P] a call to [iFrame "H1 H2"] should fail because [H2] has not been
framed.

This means we should call [_iFrameFinish] only at the very end. Hence, all
internal helping tactics do not call [_iFrameFinish]. This job is left for the
top-level tactics [_iFrame0] and [_iFrame] tactics (which underpin the final
[iFrame] tactic). *)
Ltac _iFrameFinish
:=
  pm_prettify;
  try match goal with
  | |- envs_entails _ True => by iPureIntro
  | |- envs_entails _ emp => iEmpIntro
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iFramePure t
:=
  iStartProof;
  let φ := type of t in
  notypeclasses refine (tac_frame_pure _ _ _ _ t _ _);
    [tc_solve || fail "iFrame: cannot frame" φ
    |].
(* iris/proofmode/ltac_tactics.v *)
Ltac _iFrameHyp H
:=
  iStartProof;
  notypeclasses refine (tac_frame _ H _ _ _ _ _ _ _);
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iFrame:" H "not found"
    |tc_solve ||
     let R := match goal with |- Frame _ ?R _ _ => R end in
     fail "iFrame: cannot frame" R
    |pm_reduce].
(* iris/proofmode/ltac_tactics.v *)
Ltac _iFrameAnyPure
:=
  repeat match goal with H : _ |- _ => _iFramePure H end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iFrameAnyIntuitionistic
:=
  iStartProof;
  let rec go Hs :=
    match Hs with [] => idtac | ?H :: ?Hs => repeat _iFrameHyp H; go Hs end in
  match goal with
  | |- envs_entails ?Δ _ =>
     (* [lazy] because [Δ] involves user terms *)
     let Hs := eval lazy in (env_dom (env_intuitionistic Δ)) in go Hs
  end.
(* iris/proofmode/ltac_tactics.v *)
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 ?Δ _ =>
     (* [lazy] because [Δ] involves user terms *)
     let Hs := eval lazy in (env_dom (env_spatial Δ)) in go Hs
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iFrame_go Hs
:=
  lazymatch Hs with
  | [] => idtac
  | SelPure :: ?Hs => _iFrameAnyPure; _iFrame_go Hs
  | SelIntuitionistic :: ?Hs => _iFrameAnyIntuitionistic; _iFrame_go Hs
  | SelSpatial :: ?Hs => _iFrameAnySpatial; _iFrame_go Hs
  | SelIdent ?H :: ?Hs => _iFrameHyp H; _iFrame_go Hs
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iFrame0 Hs
:=
  let Hs := sel_pat.parse Hs in
  (** An explicit call to frame nothing (i.e., [iFrame ""]) should not
  accidentally close the goal using [_iFrameFinish]. *)
  lazymatch Hs with
  | [] => idtac
  | _ => _iFrame_go Hs; _iFrameFinish
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iFrame ts Hs
:=
  ltac1_list_iter _iFramePure ts;
  _iFrame0 Hs.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iIntroSpatial H
:=
  iStartProof;
  first
  [(* (?Q → _) *)
    notypeclasses refine (tac_impl_intro _ H _ _ _ _ _ _ _ _); (* (i:=H) *)
      [tc_solve
      |pm_reduce; tc_solve ||
       let P := lazymatch goal with |- Persistent ?P => P end in
       let H := pretty_ident H in
       fail 1 "iIntro: introducing non-persistent" H ":" P
              "into non-empty spatial context"
      |tc_solve
      |pm_reduce;
       let H := pretty_ident H in
        lazymatch goal with
        | |- False =>
          let H := pretty_ident H in
          fail 1 "iIntro:" H "not fresh"
        | _ => idtac (* subgoal *)
        end]
  |(* (_ -∗ _) *)
    notypeclasses refine (tac_wand_intro _ H _ _ _ _ _); (* (i:=H) *)
      [tc_solve
      | pm_reduce;
        lazymatch goal with
        | |- False =>
          let H := pretty_ident H in
          fail 1 "iIntro:" H "not fresh"
        | _ => idtac (* subgoal *)
        end]
  | let H := pretty_ident H in
    fail 1 "iIntro: could not introduce" H ", goal is not a wand or implication" ].
(* iris/proofmode/ltac_tactics.v *)
Ltac _iIntroPersistent H
:=
  iStartProof;
  first
  [(* (?P → _) *)
   notypeclasses refine (tac_impl_intro_intuitionistic _ H _ _ _ _ _ _ _); (* (i:=H) *)
     [tc_solve
     |tc_solve ||
      let P := match goal with |- IntoPersistent _ ?P _ => P end in
      fail 1 "iIntro:" P "not persistent"
     |pm_reduce;
      lazymatch goal with
      | |- False =>
        let H := pretty_ident H in
        fail 1 "iIntro:" H "not fresh"
      | _ => idtac (* subgoal *)
      end]
  |(* (?P -∗ _) *)
   notypeclasses refine (tac_wand_intro_intuitionistic _ H _ _ _ _ _ _ _ _); (* (i:=H) *)
     [tc_solve
     |tc_solve ||
      let P := match goal with |- IntoPersistent _ ?P _ => P end in
      fail 1 "iIntro:" P "not intuitionistic"
     |tc_solve ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail 1 "iIntro:" P "not affine and the goal not absorbing"
     |pm_reduce;
      lazymatch goal with
      | |- False =>
        let H := pretty_ident H in
        fail 1 "iIntro:" H "not fresh"
      | _ => idtac (* subgoal *)
      end]
  |fail 1 "iIntro: nothing to introduce"].
(* iris/proofmode/ltac_tactics.v *)
(* Introduce [H] into persistent (if [p] is true) or spatial (if [p] is false)
context *)
Ltac _iIntroMaybePersistent H p
:=
  lazymatch p with
  | true => _iIntroPersistent H
  | _ =>  _iIntroSpatial H
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iIntroDrop
:=
  iStartProof;
  first
  [(* (?Q → _) *)
   notypeclasses refine (tac_impl_intro_drop _ _ _ _ _ _);
     [tc_solve
     |(* subgoal *)]
  |(* (_ -∗ _) *)
   notypeclasses refine (tac_wand_intro_drop _ _ _ _ _ _ _);
     [tc_solve
     |tc_solve ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail 1 "iIntro:" P "not affine and the goal not absorbing"
     |(* subgoal *)]
  |(* (∀ _, _) *)
   _iIntro (_)
   (* subgoal *)
  |fail 1 "iIntro: nothing to introduce"].
(* iris/proofmode/ltac_tactics.v *)
Ltac _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.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iIntro
:=
  lazymatch goal with
  | |- _ → ?P => intro
  | |- _ =>
    iStartProof;
    lazymatch goal with
    | |- envs_entails _ (_ -∗ _) => _iIntro (?) ||
        let H := iFresh in
        _iIntroPersistent H ||
        _iIntroSpatial H
    | |- envs_entails _ (_ → _) => _iIntro (?) ||
         let H := iFresh in
         _iIntroSpatial H ||
         _iIntroSpatial H
    end
  end.
(* iris/proofmode/ltac_tactics.v *)
(* * Revert *)
Ltac iForallRevert x
:=
  let err x :=
    intros x;
    iMatchHyp (fun H P =>
      lazymatch P with
      | context [x] =>
         let H := pretty_ident H in fail 2 "iRevert:" x "is used in hypothesis" H
      end) in
  iStartProof;
  first [let A := type of x in idtac|fail 1 "iRevert:" x "not in scope"];
  let A := type of x in
  lazymatch type of A with
  | Prop =>
     revert x; first
       [notypeclasses refine (tac_pure_revert _ _ _ _ _ _);
         [tc_solve (* [MakeAffinely], should never fail *)
         |]
       |err x]
  | _ =>
    revert x; first
      [notypeclasses refine (tac_forall_revert _ _ _);
       (* Ensure the name [x] is preserved, see [test_iRevert_order_and_names]. *)
       lazymatch goal with
       | |- envs_entails ?Δ (bi_forall ?P) =>
         change (envs_entails Δ (∀ x, P x)); lazy beta
       end
      |err x]
  | _ => revert x; first [notypeclasses refine (tac_forall_revert _ _ _)|err x]
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iRevert_go Hs
:=
  lazymatch Hs with
  | [] => idtac
  | ESelPure :: ?Hs =>
     repeat match goal with x : _ |- _ => revert x end;
     _iRevert_go Hs
  | ESelIdent _ ?H :: ?Hs => iRevertHyp H; _iRevert_go Hs
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iRevert0 Hs
:=
  iStartProof;
  let Hs := iElaborateSelPat Hs in
  _iRevert_go Hs.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iRevert xs Hs
:=
  _iRevert0 Hs;
  ltac1_list_rev_iter iForallRevert xs.
(* iris/proofmode/ltac_tactics.v *)
(* * The specialize and pose proof tactics *)
Record iTrm {X As S}
:=
  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : S }.
(* iris/proofmode/ltac_tactics.v *)
Notation "( H $! x1 .. xn )"
:=
  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
(* iris/proofmode/ltac_tactics.v *)
Notation "( H $! x1 .. xn 'with' pat )"
:=
  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
(* iris/proofmode/ltac_tactics.v *)
Notation "( H 'with' pat )"
:= (ITrm H hnil pat) (at level 0).
(* iris/proofmode/ltac_tactics.v *)
(* The tactic [iIntoEmpValid] tactic "imports a Coq lemma into the proofmode",
i.e., it solves a goal [IntoEmpValid ψ ?Q]. The argument [ψ] must be of the
following shape:

[∀ (x_1 : A_1) .. (x_n : A_n), φ]

for which we have an instance [AsEmpValid DirectionIntoEmpValid φ ?Q].

Examples of such [φ]s are

- [⊢ P], in which case [?Q] is unified with [P].
- [P1 ⊢ P2], in which case [?Q] is unified with [P1 -∗ P2].
- [P1 ⊣⊢ P2], in which case [?Q] is unified with [P1 ↔ P2].

The tactic instantiates each dependent argument [x_i : A_i] with an evar, and
generates a goal [A_i] for each non-dependent argument [x_i : A_i].

For example, if goal is [IntoEmpValid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
[iIntoEmpValid] tactic generates an evar [?x], a subgoal [P ?x], and unifies
[?Q] with [R1 ?x -∗ R2 ?x].

The tactic is implemented so as to provide a "fast path" for the arrow, forall
and tforall cases, gated by syntactic ltac pattern matching on the shape of the
goal. This is an optimization: the behavior of the tactic is equivalent to the
code in the last "wildcard" case, but faster on larger goals, where running
(possibly failing) [notypeclasses refine]s can take a significant amount of
time. *)
Ltac _iIntoEmpValid_go
:=
  lazymatch goal with
  | |- IntoEmpValid (let _ := _ in _) _ =>
    (* Normalize [let] so we don't need to rely on type class search to do so.
    Letting type class search do so is unreliable, see Iris issue #520, and test
    [test_apply_wand_below_let]. *)
    lazy zeta; _iIntoEmpValid_go
  | |- IntoEmpValid (?φ → ?ψ) _ =>
    (* Case [φ → ψ] *)
    (* note: the ltac pattern [_ → _] would not work as it would also match
       [∀ _, _] *)
    notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
      [(*goal for [φ] *)|_iIntoEmpValid_go]
  | |- IntoEmpValid (∀ _ : _, _) _ =>
    (* Case [∀ x : A, φ] *)
    (* Placeholder for the witness, so we can call [try_resolve_ground_tc]. *)
    let x := open_constr:(_) in
    notypeclasses refine (into_emp_valid_forall _ _ x _);
    try_resolve_ground_tc x;
    _iIntoEmpValid_go
  | |- IntoEmpValid (∀.. _ : _, _) _ =>
    (* The witness is a telescope, so it cannot be a type class. Hence no need
    for [try_resolve_ground_tc] in this case. *)
    notypeclasses refine (into_emp_valid_tforall _ _ _ _);
    _iIntoEmpValid_go
  | |- _ =>
    first
      [(* Case [φ → ψ] *)
       notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
         [(*goal for [φ] *)|_iIntoEmpValid_go]
      |(* Case [∀ x : A, φ] *)
       (* The handling of type classes should be exactlty the same as the "fast
       path" for [∀] above. *)
       let x := open_constr:(_) in
       notypeclasses refine (into_emp_valid_forall _ _ x _);
       try_resolve_ground_tc x;
       _iIntoEmpValid_go
      |(* Case [∀.. x : TT, φ] *)
       notypeclasses refine (into_emp_valid_tforall _ _ _ _); _iIntoEmpValid_go
      |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
       notypeclasses refine (into_emp_valid_here _ _ _) ]
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac iIntoEmpValid
:=
  (* Factor out the base case of the loop to avoid needless backtracking *)
  _iIntoEmpValid_go;
    [.. (* goals for premises *)
    |tc_solve ||
     lazymatch goal with |- @AsEmpValid ?PROP _ ?φ _ =>
        fail "iPoseProof:" φ "not a" PROP "assertion" end].
(* iris/proofmode/ltac_tactics.v *)
Ltac _iSpecializeArgs_go H xs
:=
  lazymatch xs with
  | hnil => idtac
  | hcons ?x ?xs =>
     notypeclasses refine (tac_forall_specialize _ H _ _ _ _ _ _ _);
       [pm_reflexivity ||
        let H := pretty_ident H in
        fail "iSpecialize:" H "not found"
       |tc_solve ||
        let P := match goal with |- IntoForall ?P _ => P end in
        fail "iSpecialize: cannot instantiate" P "with" x
       |lazymatch goal with
        | |- ∃ _ : ?A, _ =>
          (* First coerce [x] into the expected type [A]. For instance, we might
          have [x : nat] and [A := Z]. *)
          let x := constr:(x:A) in
          (* Then instantiate the quantifier with the coerced term *)
          notypeclasses refine (ex_intro _ x _);
          (* And resolve ground type classes in the coerced term *)
          try_resolve_ground_tc x
        end; pm_reduce; _iSpecializeArgs_go H xs]
  end.
(* iris/proofmode/ltac_tactics.v *)
(* The tactics [iSpecialize trm as #] and [iSpecializeCore trm as true] allow
one to use the entire spatial context /twice/: the first time for proving the
premises [Q1 .. Qn] of [H : Q1 -* .. -∗ Qn -∗ R], and the second time for
proving the remaining goal. This is possible if all of the following properties
hold:
1. The conclusion [R] of the hypothesis [H] is persistent.
2. The specialization pattern [[> ..]] for wrapping a modality is not used for
   any of the premises [Q1 .. Qn].
3. The BI is either affine, or the hypothesis [H] resides in the intuitionistic
   context.

The copying of the context for proving the premises of [H] and the remaining
goal is implemented using the lemma [tac_specialize_intuitionistic_helper].

Since the tactic [iSpecialize .. as #] is used a helper to implement
[iDestruct .. as "#.."], [iPoseProof .. as "#.."], [iSpecialize .. as "#.."],
and friends, the behavior on violations of these conditions is as follows:

- If condition 1 is violated (i.e. the conclusion [R] of [H] is not persistent),
  the tactic will fail.
- If condition 2 or 3 is violated, the tactic will fall back to consuming the
  hypotheses for proving the premises [Q1 .. Qn]. That is, it will fall back to
  not using [tac_specialize_intuitionistic_helper].

The function [use_tac_specialize_intuitionistic_helper Δ pat] below returns
[true] iff the specialization pattern [pat] consumes any spatial hypotheses,
and does not contain the pattern [[> ..]] (cf. condition 2). If the function
returns [false], then the conclusion can be moved in the intuitionistic context
even if conditions 1 and 3 do not hold. Therefore, in that case, we prefer
putting the conclusion to the intuitionistic context directly and not using
[tac_specialize_intuitionistic_helper], which requires conditions 1 and 3. *)
Fixpoint use_tac_specialize_intuitionistic_helper {M}
    (Δ : envs M) (pats : list spec_pat) : bool
:=
  match pats with
  | [] => false
  | SPureGoal _ :: pats =>
     use_tac_specialize_intuitionistic_helper Δ pats
  | SAutoFrame _ :: _ => true
  | SIdent H _ :: pats =>
     match envs_lookup_delete false H Δ with
     | Some (false, _, Δ) => true
     | Some (true, _, Δ) => use_tac_specialize_intuitionistic_helper Δ pats
     | None => false (* dummy case (invalid pattern, will fail in the tactic anyway) *)
     end
  | SGoal (SpecGoal GModal _ _ _ _) :: _ => false
  | SGoal (SpecGoal GIntuitionistic _ _ _ _) :: pats =>
     use_tac_specialize_intuitionistic_helper Δ pats
  | SGoal (SpecGoal GSpatial neg Hs_frame Hs _) :: pats =>
     match envs_split (if neg is true then Right else Left)
                      (if neg then Hs else pm_app Hs_frame Hs) Δ with
     | Some (Δ1,Δ2) => if env_spatial_is_nil Δ1
                       then use_tac_specialize_intuitionistic_helper Δ2 pats
                       else true
     | None => false (* dummy case (invalid pattern, will fail in the tactic anyway) *)
     end
  end.
(* iris/proofmode/ltac_tactics.v *)
(* The helper [iApplyHypExact] takes care of the [n=0] case. It fails with level
0 if we should proceed to the [n > 0] case, and with level 1 if there is an
actual error. *)
Ltac iApplyHypExact H
:=
  notypeclasses refine (tac_assumption _ H _ _ _ _ _ _); (* (i:=H) *)
    [pm_reflexivity
    |tc_solve
    |pm_reduce; tc_solve ||
     fail 1 "iApply: remaining hypotheses not affine and the goal not absorbing"].
(* iris/proofmode/ltac_tactics.v *)
Ltac iApplyHypLoop H
:=
  first
    [notypeclasses refine (tac_apply _ H _ _ _ _ _ _ _);
      [pm_reflexivity
      |tc_solve
      |pm_reduce]
    |iSpecializePat H "[]"; last iApplyHypLoop H].
(* iris/proofmode/ltac_tactics.v *)
(* iDestruct H as [H1 H2] *)
Ltac _iAndDestruct H H1 H2
:=
  notypeclasses refine (tac_and_destruct _ H _ H1 H2 _ _ _ _ _ _ _);
    (* (i:=H) (j1:=H1) (j2:=H2) *)
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iAndDestruct:" H "not found"
    |pm_reduce; tc_solve ||
     let P :=
       lazymatch goal with
       | |- IntoSep ?P _ _ => P
       | |- IntoAnd _ ?P _ _ => P
       end in
     fail "iAndDestruct: cannot destruct" P
    |pm_reduce;
     lazymatch goal with
       | |- False =>
         let H1 := pretty_ident H1 in
         let H2 := pretty_ident H2 in
         fail "iAndDestruct:" H1 "or" H2 "not fresh"
       | _ => idtac (* subgoal *)
     end].
(* iris/proofmode/ltac_tactics.v *)
(* iDestruct H as (depending on d) [H _] or [_ H] *)
Ltac _iAndDestructChoice H d H'
:=
  notypeclasses refine (tac_and_destruct_choice _ H _ d H' _ _ _ _ _ _ _);
    [pm_reflexivity || fail "iAndDestructChoice:" H "not found"
    |pm_reduce; tc_solve ||
     let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
     fail "iAndDestructChoice: cannot destruct" P
    |pm_reduce;
     lazymatch goal with
     | |- False =>
       let H' := pretty_ident H' in
       fail "iAndDestructChoice:" H' "not fresh"
     | _ => idtac (* subgoal *)
     end].
(* iris/proofmode/ltac_tactics.v *)
(* * Existential *)
Ltac _iExists x
:=
  iStartProof;
  notypeclasses refine (tac_exist _ _ _ _ _);
    [tc_solve ||
     let P := match goal with |- FromExist ?P _ => P end in
     fail "iExists:" P "not an existential"
    |pm_prettify; eexists x
     (* subgoal *) ].
(* iris/proofmode/ltac_tactics.v *)
Ltac _iExistDestructFail P
:= first
  [ (* Give a special error message if one tries to destruct [▷ ∃ x : A. Q]
    without [A] being inhabited, or some variation thereof (e.g., with other
    modalities in between). *)
    (* Search for [IntoExist] with the assumption that any type is inhabited.
    Here, [T] contains the type class query, [t] will be the instance (failure
    happens if no instance is found, in which case the default error is given by
    backtracking to the second branch of [first].
    We then match on the type of the instance [t] to extract the type for which
    no [Inhabited] instance could be found. *)
    let T := open_constr:((∀ B, Inhabited B) → IntoExist P _ _) in
    let t := constr:(_ : T) in
    lazymatch type of t with
    | _ → IntoExist (A:=?A) _ _ _ => fail 1 "iExistDestruct: cannot destruct" P
        "because no `Inhabited` instance for" A "could be found"
    end
  | fail 1 "iExistDestruct: cannot destruct" P ].
(* iris/proofmode/ltac_tactics.v *)
(* Two helper tactics to compute an identifier for the hypothesis corresponding
   to the intro-pattern [pat], when trying to avoid extra renamings. These
   mainly look whether the pattern is a name, and use that name in that case.
   Otherwise, [ident_for_pat] generates a fresh name (a safe option), and
   [ident_for_pat_default] uses the [default] name that it was provided if
   it is an anonymous name. *)
Ltac _ident_for_pat pat
:=
  lazymatch pat with
  | IIdent ?x => x
  | _ => let x := iFresh in x
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _ident_for_pat_default pat default
:=
  lazymatch pat with
  | IIdent ?x => x
  | _ =>
    lazymatch default with
    | IAnon _ => default
    | _ => let x := iFresh in x
    end
  end.