(* iris/proofmode/ltac_tactics.v *)
From stdpp Require Import namespaces hlist pretty
From iris.bi Require Export bi telescopes
From iris.proofmode Require Import base intro_patterns spec_patterns
From iris.proofmode Require Export classes notation
From iris.prelude Require Import options

Ltac iSolveSideCondition:=
  lazymatch goal with
  | |- pm_error ?err => fail "" err
  | _ => split_and?; try solve [ fast_done | solve_ndisj | tc_solve ]
  end.

Ltac pretty_identH :=
  lazymatch H with
  | INamed ?H => H
  | ?H => H
  end.

Ltac iGetCtx:=
  lazymatch goal with
  | |- envs_entails ?Δ _ => Δ
  | |- context[ envs_split _ _ ?Δ ] => Δ
  end.

Ltac iMissingHypsCoreΔ Hs :=
  let Hhyps := pm_eval (envs_dom Δ) in
  eval vm_compute in (list_difference Hs Hhyps).

Ltac iMissingHypsHs :=
  let Δ := iGetCtx in
  iMissingHypsCore Δ Hs.

Ltac iTypeOfH :=
  let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
  pm_eval (envs_lookup H Δ).

Ltac iBiOfGoal:=
  match goal with |- @envs_entails ?PROP _ _ => PROP end.
Tactic Notation "iMatchHyp" tactic1(tac) :=
  match goal with
  | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
  end.
Tactic Notation "iSelect" open_constr(pat) tactic1(tac) :=
  lazymatch goal with
  | |- context[ environments.Esnoc _ ?x pat ] =>

Ltac iFresh:=

Inductive esel_pat:=
  | ESelPure
  | ESelIdent :  bool → ident → esel_pat.

Local LtaciElaborateSelPat_go pat Δ Hs :=
  lazymatch pat with
  | [] => eval cbv in Hs
  | SelPure :: ?pat =>  iElaborateSelPat_go pat Δ (ESelPure :: Hs)
  | SelIntuitionistic :: ?pat =>
    let Hs' := pm_eval (env_dom (env_intuitionistic Δ)) in
    let Δ' := pm_eval (envs_clear_intuitionistic Δ) in
    iElaborateSelPat_go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
  | SelSpatial :: ?pat =>
    let Hs' := pm_eval (env_dom (env_spatial Δ)) in
    let Δ' := pm_eval (envs_clear_spatial Δ) in
    iElaborateSelPat_go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
  | SelIdent ?H :: ?pat =>
    lazymatch pm_eval (envs_lookup_delete false H Δ) with
    | Some (?p,_,?Δ') =>  iElaborateSelPat_go pat Δ' (ESelIdent p H :: Hs)
    | None =>
      let H := pretty_ident H in
      fail "iElaborateSelPat:" H "not found"
    end
  end.

Ltac iElaborateSelPatpat :=
  lazymatch goal with
  | |- envs_entails ?Δ _ =>
    let pat := sel_pat.parse pat in iElaborateSelPat_go pat Δ (@nil esel_pat)
  end.

Ltac _iClearHypH :=
  eapply tac_clear with 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].

Local LtaciClear_go Hs :=
  lazymatch Hs with
  | [] => idtac
  | ESelPure :: ?Hs => clear; iClear_go Hs
  | ESelIdent _ ?H :: ?Hs => _iClearHyp H; iClear_go Hs
  end.
Tactic Notation "iClear" constr(Hs) :=
  iStartProof; let Hs := iElaborateSelPat Hs in iClear_go Hs.
Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
  iClear Hs; clear xs.
Tactic Notation "iClear" "select" open_constr(pat) :=
  iSelect pat ltac:(fun H => iClear H).

Local LtaciEval_go t Hs :=
  lazymatch Hs with
  | [] => idtac
  | ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
  | ESelIdent _ ?H :: ?Hs =>
    eapply tac_eval_in with 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.
Tactic Notation "iEval" tactic3(t) "in" constr(Hs) :=
  iStartProof; let Hs := iElaborateSelPat Hs in iEval_go t Hs.
Tactic Notation "iSimpl" := iEval (simpl).
Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.

Ltac _iUnfoldr := iEval (unfold r).
Tactic Notation "iUnfold" ne_reference_list_sep(ids,",") :=
  ltac1_list_iter _iUnfold ids.

Ltac _iUnfold_inr H := iEval (unfold r) in H.
Tactic Notation "iUnfold" ne_reference_list_sep(ids,",") "in" constr(H) :=
  ltac1_list_iter ltac:(fun r => _iUnfold_in r H) ids.

Ltac _iIntuitionisticH H' :=
  eapply tac_intuitionistic with H 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
     end].

Ltac _iSpatialH H' :=
  eapply tac_spatial with 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
     end].
Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
  eapply tac_pure with H _ _ _;
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iPure:" H "not found"
    |tc_solve ||
     let P := match goal with |- IntoPure ?P _ => P end in
     fail "iPure:" P "not pure"
    |pm_reduce; tc_solve ||
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iPure:" P "not affine and the goal not absorbing"
    |pm_reduce; intros pat].
Tactic Notation "iEmpIntro" :=
  iStartProof;
  eapply tac_emp_intro;
    [pm_reduce; tc_solve ||
     fail "iEmpIntro: spatial context contains non-affine hypotheses"].
Tactic Notation "iPureIntro" :=
  iStartProof;
  eapply tac_pure_intro;
    [tc_solve ||
     let P := match goal with |- FromPure _ ?P _ => P end in
     fail "iPureIntro:" P "not pure"
    |pm_reduce; tc_solve ||

Ltac _iFrameFinish:=
  pm_prettify;
  try match goal with
  | |- envs_entails _ True => by iPureIntro
  | |- envs_entails _ emp => iEmpIntro
  end.

Ltac _iFramePuret :=
  iStartProof;
  let φ := type of t in
  eapply (tac_frame_pure _ _ _ _ t);
    [tc_solve || fail "iFrame: cannot frame" φ
    |].

Ltac _iFrameHypH :=
  iStartProof;
  eapply tac_frame with 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].

Ltac _iFrameAnyPure:=
  repeat match goal with H : _ |- _ => _iFramePure H end.

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 ?Δ _ =>

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 ?Δ _ =>

Ltac _iFrame_goHs :=
  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.

Ltac _iFrame0Hs :=
  let Hs := sel_pat.parse Hs in

Ltac _iFramets Hs :=
  ltac1_list_iter _iFramePure ts;
  _iFrame0 Hs.
Tactic Notation "iFrame" :=
  _iFrameAnySpatial; _iFrameFinish.
Tactic Notation "iFrame" "(" ne_constr_list(ts) ")" := _iFrame ts "".
Tactic Notation "iFrame" constr(Hs) := _iFrame0 Hs.
Tactic Notation "iFrame" "(" ne_constr_list(ts) ")" constr(Hs) := _iFrame ts Hs.
Tactic Notation "iFrame" "select" open_constr(pat) :=
  iSelect pat ltac:(fun H => iFrame H).

Ltac _iIntroSpatialH :=
  iStartProof;
  first
  [
    eapply tac_impl_intro with 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
        end]
  |
    eapply tac_wand_intro with H _ _;
      [tc_solve
      | pm_reduce;
        lazymatch goal with
        | |- False =>
          let H := pretty_ident H in
          fail 1 "iIntro:" H "not fresh"
        | _ => idtac
        end]
  | let H := pretty_ident H in
    fail 1 "iIntro: could not introduce" H ", goal is not a wand or implication" ].

Ltac _iIntroPersistentH :=
  iStartProof;
  first
  [
   eapply tac_impl_intro_intuitionistic with 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
      end]
  |
   eapply tac_wand_intro_intuitionistic with 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
      end]
  |fail 1 "iIntro: nothing to introduce"].

Ltac _iIntroMaybePersistentH p :=
  lazymatch p with
  | true => _iIntroPersistent H
  | _ =>  _iIntroSpatial H
  end.

Ltac _iIntroDrop:=
  iStartProof;
  first
  [
   eapply tac_impl_intro_drop;
     [tc_solve
     |]
  |
   eapply 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"
     |]
  |
   _iIntro (_)

Ltac _iIntroForall:=
  lazymatch goal with
  | |- ∀ _, ?P => fail
  | |- ∀ _, _ => intro
  | |- let _ := _ in _ => intro
  | |- _ =>
    iStartProof;
    lazymatch goal with
    | |- envs_entails _ (∀ x : _, _) => let x' := fresh x in _iIntro (x')
    end
  end.

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.

Ltac iForallRevertx :=
  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
       [eapply tac_pure_revert;
         [tc_solve
         |]
       |err x]
  | _ =>
    revert x; first
      [apply tac_forall_revert;

Ltac _iRevert_goHs :=
  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.

Ltac _iRevert0Hs :=
  iStartProof;
  let Hs := iElaborateSelPat Hs in
  _iRevert_go Hs.

Ltac _iRevertxs Hs :=
  _iRevert0 Hs;
  ltac1_list_rev_iter iForallRevert xs.
Tactic Notation "iRevert" constr(Hs) := _iRevert0 Hs.
Tactic Notation "iRevert" "(" ne_ident_list(xs) ")" := _iRevert xs "".
Tactic Notation "iRevert" "(" ne_ident_list(xs) ")" constr(Hs) := _iRevert xs Hs.
Tactic Notation "iRevert" "select" open_constr(pat) :=
  iSelect pat ltac:(fun H => iRevertHyp H).

Record iTrm{X As S} :=
  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : S }.

Global ArgumentsITrm {_ _ _} _ _ _.

Ltac iIntoEmpValid_go:=
  lazymatch goal with
  | |- IntoEmpValid (let _ := _ in _) _ =>

Ltac iIntoEmpValid:=

Local LtaciSpecializeArgs_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, _ =>
          notypeclasses refine (@ex_intro A _ x _)
        end; [shelve..|pm_reduce; iSpecializeArgs_go H xs]]
  end.

Local TacticNotation "iSpecializeArgs" constr(H) open_constr(xs) :=
  iSpecializeArgs_go H xs.

Ltac iSpecializePat_goH1 pats :=
  let solve_to_wand H1 :=
    tc_solve ||
    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 =>
       first [ done
             | let Q := match goal with |- envs_entails _ ?Q => Q end in
               fail 1 "iSpecialize: cannot solve" Q "using done"
             | let Q := match goal with |- ?Q => Q end in
               fail 1 "iSpecialize: cannot solve" Q "using done" ]
    | false => idtac
    end in
  let Δ := iGetCtx in
  lazymatch pats with
    | [] => idtac
    | SIdent ?H2 [] :: ?pats =>

Local TacticNotation "iSpecializePat" open_constr(H) constr(pat) :=
  let pats := spec_pat.parse pat in iSpecializePat_go H pats.

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
     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
     end
  end.

Local LtaciApplyHypExact H :=
  eapply tac_assumption with H _ _;
    [pm_reflexivity
    |tc_solve
    |pm_reduce; tc_solve ||
     fail 1 "iApply: remaining hypotheses not affine and the goal not absorbing"].

Local LtaciApplyHypLoop H :=
  first
    [eapply tac_apply with H _ _ _;
      [pm_reflexivity
      |tc_solve
      |pm_reduce]
    |iSpecializePat H "[]"; last iApplyHypLoop H].
Tactic Notation "iApplyHyp" constr(H) :=
  first
    [iApplyHypExact H
    |iApplyHypLoop H
    |lazymatch iTypeOf H with
     | Some (_,?Q) => fail 1 "iApply: cannot apply" Q
     end].
Tactic Notation "iApply" open_constr(lem) :=
  iPoseProofCore lem as false (fun H => iApplyHyp H);
  pm_prettify.

Ltac _iAndDestructH H1 H2 :=
  eapply tac_and_destruct with H _ H1 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
     end].

Ltac _iAndDestructChoiceH d H' :=
  eapply tac_and_destruct_choice with 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
     end].

Ltac _iExistsx :=
  iStartProof;
  eapply tac_exist;
    [tc_solve ||
     let P := match goal with |- FromExist ?P _ => P end in
     fail "iExists:" P "not an existential"
    |pm_prettify; eexists x

Ltac _iExistDestructFailP := first
  [

Ltac _ident_for_patpat :=
  lazymatch pat with
  | IIdent ?x => x
  | _ => let x := iFresh in x
  end.

Ltac _ident_for_pat_defaultpat default :=
  lazymatch pat with
  | IIdent ?x => x
  | _ =>
    lazymatch default with
    | IAnon _ => default
    | _ => let x := iFresh in x
    end
  end.

Ltac _iDestructHypGoHz pat0 pat :=
  lazymatch pat with
  | IFresh =>
     lazymatch Hz with
     | IAnon _ => idtac
     | INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
     end
  | IDrop => _iClearHyp Hz
  | IFrame => iFrame Hz
  | IIdent Hz => idtac
  | IIdent ?y => iRename Hz into y
  | IList [[]] => iExFalso; iExact Hz

Ltac _iDestructHypFindPatHgo pat found pats :=
  lazymatch pats with
  | [] =>
    lazymatch found with
    | true => pm_prettify
    | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
    end
  | ISimpl :: ?pats => simpl; _iDestructHypFindPat Hgo pat found pats
  | IClear ?H :: ?pats => iClear H; _iDestructHypFindPat Hgo pat found pats
  | IClearFrame ?H :: ?pats => iFrame H; _iDestructHypFindPat Hgo pat found pats
  | ?pat1 :: ?pats =>
     lazymatch found with
     | false => _iDestructHypGo Hgo pat pat1; _iDestructHypFindPat Hgo pat true pats
     | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
     end
  end.

Ltac _iDestructHyp0H pat :=
  let pats := intro_pat.parse pat in
  _iDestructHypFindPat H pat false pats.

Ltac _iDestructHypH xs pat :=
  ltac1_list_iter ltac:(fun x => _iExistDestruct H as x H) xs;
  _iDestructHyp0 H pat.
Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
  _iDestructHyp0 H pat.
Tactic Notation "iDestructHyp" constr(H) "as"
  "(" ne_simple_intropattern_list(xs) ")" constr(pat) := _iDestructHyp H xs pat.

Ltac _iIntros_gopats startproof :=
  lazymatch pats with
  | [] =>
    lazymatch startproof with
    | true => iStartProof
    | false => idtac
    end

Ltac _iIntros0pat :=
  let pats := intro_pat.parse pat in

Ltac _iIntrosxs pat :=
  ltac1_list_iter ltac:(fun x => _iIntro (x)) xs;
  _iIntros0 pat.
Tactic Notation "iIntros" := _iIntros0 [IAll].
Tactic Notation "iIntros" constr(pat) := _iIntros0 pat.
Tactic Notation "iIntros" "(" ne_simple_intropattern_list(xs) ")" :=
  _iIntros xs "".
Tactic Notation "iIntros" "(" ne_simple_intropattern_list(xs) ")" constr(pat) :=
  _iIntros xs pat.
Tactic Notation "iIntros" constr(pat) "(" ne_simple_intropattern_list(xs) ")" :=
  _iIntros0 pat; _iIntros xs "".
Tactic Notation "iIntros" constr(pat1)
    "(" ne_simple_intropattern_list(xs) ")" constr(pat2) :=
  _iIntros0 pat1; _iIntros xs pat2.

Ltac _iRevertIntros_goHs tac :=
  lazymatch Hs with
  | [] => tac ()
  | ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
  | ESelIdent ?p ?H :: ?Hs =>
    iRevertHyp H; _iRevertIntros_go Hs tac; _iIntroMaybePersistent H p
  end.

Ltac _iRevertIntros0Hs tac :=
  try iStartProof;
  let Hs := iElaborateSelPat Hs in
  _iRevertIntros_go Hs tac.

Ltac _iRevertIntrosxs Hs tac :=
  _iRevertIntros0 Hs ltac:(fun _ => _iRevert xs ""; tac (); _iIntros xs "").
Tactic Notation "iRevertIntros" constr(Hs) "with" tactic3(tac) :=
  _iRevertIntros0 Hs tac.
Tactic Notation "iRevertIntros" "(" ne_ident_list(xs) ")" constr(Hs) "with" tactic3(tac):=
  _iRevertIntros xs Hs tac.
Tactic Notation "iRevertIntros" "with" tactic3(tac) :=
  _iRevertIntros0 "" tac.
Tactic Notation "iRevertIntros" "(" ne_ident_list(xs) ")" "with" tactic3(tac):=
  _iRevertIntros xs "" tac.

Ltac _iDestruct0lem pat :=
  iDestructCore lem as pat (fun H => iDestructHyp H as pat).

Ltac _iDestructlem xs pat :=
  iDestructCore lem as pat (fun H => _iDestructHyp H xs pat).
Tactic Notation "iDestruct" open_constr(lem) "as" constr(pat) :=
  _iDestruct0 lem pat.
Tactic Notation "iDestruct" open_constr(lem) "as" "(" ne_simple_intropattern_list(xs) ")"
    constr(pat) :=
  _iDestruct lem xs pat.
Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
  iDestructCore lem as true (fun H => iPure H as pat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" constr(ipat) :=
  iSelect pat ltac:(fun H => _iDestruct0 H ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
    ne_simple_intropattern_list(xs) ")" constr(ipat) :=
  iSelect pat ltac:(fun H => _iDestruct H xs ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "%" simple_intropattern(ipat) :=
  iSelect pat ltac:(fun H => iDestruct H as % ipat).
Tactic Notation "iPoseProof" open_constr(lem) "as" constr(pat) :=
  iPoseProofCore lem as pat (fun H => iDestructHyp H as pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" "(" ne_simple_intropattern_list(xs) ")"
    constr(pat) :=
  iPoseProofCore lem as pat (fun H => _iDestructHyp H xs pat).

Ltac iHypsContainingx :=
  let rec go Γ x Hs :=
    lazymatch Γ with
    | Enil => constr:(Hs)
    | Esnoc ?Γ ?H ?Q =>
       match Q with
       | context [x] => go Γ x (H :: Hs)
       | _ => go Γ x Hs
       end
     end in
  let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _ _) _ => Γp end in
  let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs _) _ => Γs end in
  let Hs := go Γp x (@nil ident) in go Γs x Hs.

Ltac _iInductionx xs Hs tac IH :=

Ltac _iInduction0x Hs tac IH :=
  with_ltac1_nil ltac:(fun xs => _iInduction x xs Hs tac IH).

Ltac _iLöbxs Hs IH :=

Ltac _iLöb0Hs IH :=
  with_ltac1_nil ltac:(fun xs => _iLöb xs Hs IH).
Tactic Notation "iLöb" "as" constr (IH) :=
  _iLöb0 "" IH.
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ne_ident_list(xs) ")" :=
  _iLöb xs "" IH.
Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) :=
  _iLöb0 Hs IH.
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ne_ident_list(xs) ")" constr(Hs) :=
  _iLöb xs Hs IH.

Local LtaciRewriteFindPred :=
  match goal with
  | |- _ ⊣⊢ ?Φ ?x =>
     generalize x;
     match goal with |- (∀ y, @?Ψ y ⊣⊢ _) => unify Φ Ψ; reflexivity end
  end.

Local TacticNotation "iRewriteCore" constr(lr) open_constr(lem) :=
  iPoseProofCore lem as true (fun Heq =>
    eapply (tac_rewrite _ Heq _ _ lr);
      [pm_reflexivity ||
       let Heq := pretty_ident Heq in
       fail "iRewrite:" Heq "not found"
      |tc_solve ||
       let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
       fail "iRewrite:" P "not an equality"
      |iRewriteFindPred
      |intros ??? ->; reflexivity|pm_prettify; _iClearHyp Heq]).
Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore Right lem.
Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore Left lem.

Local TacticNotation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
  iPoseProofCore lem as true (fun Heq =>
    eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
      [pm_reflexivity ||
       let Heq := pretty_ident Heq in
       fail "iRewrite:" Heq "not found"
      |pm_reflexivity ||
       let H := pretty_ident H in
       fail "iRewrite:" H "not found"
      |tc_solve ||
       let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
       fail "iRewrite:" P "not an equality"
      |iRewriteFindPred
      |intros ??? ->; reflexivity
      |pm_reduce; pm_prettify; _iClearHyp Heq]).
Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
  iRewriteCore Right lem in H.
Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) :=
  iRewriteCore Left lem in H.

Ltac iSimplifyEq:= repeat (
  iMatchHyp (fun H P => match P with ⌜_ = _⌝%I => iDestruct H as %? end)
  || simplify_eq/=).

Ltac _iDestructAccAndHyp0pat x H :=
  lazymatch type of x with
  | unit => destruct x as []; _iDestructHyp0 H pat
  | _ => fail "Missing intro pattern for accessor variable"
  end.

Ltac _iDestructAccAndHypxs pat x H :=
  let go := ltac2:(tac xs |-
    match of_ltac1_list xs with
    | [] =>
      Control.throw_invalid_argument "iDestructAccAndHyp: List should be non-empty"
    | x1 :: xs' =>
      ltac1:(x1 |- intros x1) x1;
      ltac1:(tac xs' |- tac xs') tac (Ltac1.of_list xs')
    end) in
  lazymatch type of x with
  | unit => destruct x as []; _iDestructHyp H xs pat
  | _ => revert x; go ltac:(fun xs' => _iDestructHyp H xs' pat) xs
  end.

Global HintExtern 0 (_ ⊢ _) => iStartProof : core.

Global HintExtern 0 (⊢ _) => iStartProof : core.

Global HintExtern 0 (envs_entails _ _) => iPureIntro; try done : core.

Global HintExtern 0 (envs_entails _ ?Q) =>
  first [is_evar Q; fail 1|iAssumption] : core.

Global HintExtern 0 (envs_entails _ emp) => iEmpIntro : core.

Global HintExtern 0 (envs_entails _ (_ ≡ _)) =>
  rewrite envs_entails_unseal; apply internal_eq_refl : core.

Global HintExtern 0 (envs_entails _ (big_opL _ _ _)) =>
  rewrite envs_entails_unseal; apply (big_sepL_nil' _) : core.

Global HintExtern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
  rewrite envs_entails_unseal; apply (big_sepL2_nil' _) : core.

Global HintExtern 0 (envs_entails _ (big_opM _ _ _)) =>
  rewrite envs_entails_unseal; apply (big_sepM_empty' _) : core.

Global HintExtern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
  rewrite envs_entails_unseal; apply (big_sepM2_empty' _) : core.

Global HintExtern 0 (envs_entails _ (big_opS _ _ _)) =>
  rewrite envs_entails_unseal; apply (big_sepS_empty' _) : core.

Global HintExtern 0 (envs_entails _ (big_opMS _ _ _)) =>
  rewrite envs_entails_unseal; apply (big_sepMS_empty' _) : core.

Global HintExtern 0 (envs_entails _ (∀ _, _)) => iIntros : core.

Global HintExtern 0 (envs_entails _ (_ → _)) => iIntros : core.

Global HintExtern 0 (envs_entails _ (_ -∗ _)) => iIntros : core.

Global HintExtern 0 (envs_entails _ (∀.. _, _)) => iIntros (?) : core.

Global HintExtern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.

Global HintExtern 1 (envs_entails _ (_ ∗ _)) => iSplit : core.

Global HintExtern 1 (envs_entails _ (_ ↔ _)) => iSplit : core.

Global HintExtern 1 (envs_entails _ (_ ∗-∗ _)) => iSplit : core.

Global HintExtern 1 (envs_entails _ (▷ _)) => iNext : core.

Global HintExtern 1 (envs_entails _ (■ _)) => iModIntro : core.

Global HintExtern 1 (envs_entails _ (<pers> _)) => iModIntro : core.

Global HintExtern 1 (envs_entails _ (<affine> _)) => iModIntro : core.

Global HintExtern 1 (envs_entails _ (□ _)) => iModIntro : core.

Global HintExtern 1 (envs_entails _ (∃ _, _)) => iExists _ : core.

Global HintExtern 1 (envs_entails _ (∃.. _, _)) => iExists _ : core.

Global HintExtern 1 (envs_entails _ (◇ _)) => iModIntro : core.

Global HintExtern 1 (envs_entails _ (_ ∨ _)) => iLeft : core.

Global HintExtern 1 (envs_entails _ (_ ∨ _)) => iRight : core.

Global HintExtern 1 (envs_entails _ (|==> _)) => iModIntro : core.

Global HintExtern 1 (envs_entails _ (<absorb> _)) => iModIntro : core.

Global HintExtern 2 (envs_entails _ (|={_}=> _)) => iModIntro : core.

Global HintExtern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.