tactics.v

Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
    "forall" "(" ident(x1) ")" constr(Hs) :=
  iRevertIntros(x1) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
    "forall" "(" ident(x1) ident(x2) ")" constr(Hs) :=
  iRevertIntros(x1 x2) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
    "forall" "(" ident(x1) ident(x2) ident(x3) ")" constr(Hs) :=
  iRevertIntros(x1 x2 x3) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" constr(Hs) :=
  iRevertIntros(x1 x2 x3 x4) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ")"
    constr(Hs) :=
  iRevertIntros(x1 x2 x3 x4 x5) Hs with (iInductionCore x as aat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ")"
    constr(Hs) :=
  iRevertIntros(x1 x2 x3 x4 x5 x6) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
    ident(x7) ")" constr(Hs) :=
  iRevertIntros(x1 x2 x3 x4 x5 x6 x7) Hs with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
    ident(x7) ident(x8) ")" constr(Hs) :=
  iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) Hs with (iInductionCore x as pat IH).

(** * Löb Induction *)
Tactic Notation "iLöbCore" "as" constr (IH) :=
  eapply tac_löb with _ IH;
    [reflexivity || fail "iLöb: persistent context not empty"
    |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|].

Tactic Notation "iLöb" "as" constr (IH) :=
  iRevertIntros "∗" with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ")" :=
  iRevertIntros(x1) "∗" with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ")" :=
  iRevertIntros(x1 x2) "∗" with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ")" :=
  iRevertIntros(x1 x2 x3) "∗" with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ")" :=
  iRevertIntros(x1 x2 x3 x4) "∗" with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ident(x5) ")" :=
  iRevertIntros(x1 x2 x3 x4 x5) "∗" with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ident(x5) ident(x6) ")" :=
  iRevertIntros(x1 x2 x3 x4 x5 x6) "∗" with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ")" :=
  iRevertIntros(x1 x2 x3 x4 x5 x6 x7) "∗" with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ")" :=
  iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "∗" with (iLöbCore as IH).

Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) :=
  let Hs := constr:(Hs +:+ "∗") in
  iRevertIntros Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ")" constr(Hs) :=
  let Hs := constr:(Hs +:+ "∗") in
  iRevertIntros(x1) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ")"
    constr(Hs) :=
  let Hs := constr:(Hs +:+ "∗") in
  iRevertIntros(x1 x2) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ")" constr(Hs) :=
  let Hs := constr:(Hs +:+ "∗") in
  iRevertIntros(x1 x2 x3) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ")" constr(Hs) :=
  let Hs := constr:(Hs +:+ "∗") in
  iRevertIntros(x1 x2 x3 x4) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ident(x5) ")" constr(Hs) :=
  let Hs := constr:(Hs +:+ "∗") in
  iRevertIntros(x1 x2 x3 x4 x5) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ident(x5) ident(x6) ")" constr(Hs) :=
  let Hs := constr:(Hs +:+ "∗") in
  iRevertIntros(x1 x2 x3 x4 x5 x6) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ")" constr(Hs) :=
  let Hs := constr:(Hs +:+ "∗") in
  iRevertIntros(x1 x2 x3 x4 x5 x6 x7) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
    ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) :=
  let Hs := constr:(Hs +:+ "∗") in
  iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) Hs with (iLöbCore as IH).

(** * Assert *)
Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac) :=
  let H := iFresh in
  let Hs := spec_pat.parse Hs in
  lazymatch Hs with
  | [SGoalPersistent] =>
     eapply tac_assert_persistent with _ H Q;
       [env_cbv; reflexivity
       |(*goal*)
       |apply _ || fail "iAssert:" Q "not persistent"
       |tac H]
  | [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] =>
     let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
     eapply tac_assert with _ _ _ lr Hs' H Q _;
       [match m with
        | false => apply elim_modal_dummy
        | true => apply _ || fail "iAssert: goal not a modality"
        end
       |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
       |env_cbv; reflexivity
       |iFrame Hs_frame (*goal*)
       |tac H]
  | ?pat => fail "iAssert: invalid pattern" pat
  end.

Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
  iAssertCore Q with Hs as (fun H => iDestructHyp H as pat).
Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
  iAssert Q with "[]" as pat.

Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs)
    "as" "%" simple_intropattern(pat) :=
  iAssertCore Q with Hs as (fun H => iPure H as pat).
Tactic Notation "iAssert" open_constr(Q) "as" "%" simple_intropattern(pat) :=
  iAssert Q with "[]" as %pat.

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

Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
  iPoseProofCore lem as true (fun Heq =>
    eapply (tac_rewrite _ Heq _ _ lr);
      [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
      |let P := match goal with |- ?P ⊢ _ => P end in
       (* use ssreflect apply: which is better at dealing with unification
       involving canonical structures. This is useful for the COFE canonical
       structure in uPred_eq that it may have to infer. *)
       apply: reflexivity || fail "iRewrite:" P "not an equality"
      |iRewriteFindPred
      |intros ??? ->; reflexivity|lazy beta; iClear Heq]).

Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore false lem.
Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore true lem.

Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
  iPoseProofCore lem as true (fun Heq =>
    eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
      [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
      |env_cbv; reflexivity || fail "iRewrite:" H "not found"
      |let P := match goal with |- ?P ⊢ _ => P end in
       apply: reflexivity || fail "iRewrite:" P "not an equality"
      |iRewriteFindPred
      |intros ??? ->; reflexivity
      |env_cbv; reflexivity|lazy beta; iClear Heq]).

Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
  iRewriteCore false lem in H.
Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) :=
  iRewriteCore true lem in H.

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

(** * Update modality *)
Tactic Notation "iMod" open_constr(lem) :=
  iDestructCore lem as false (fun H => iModCore H).
Tactic Notation "iMod" open_constr(lem) "as" constr(pat) :=
  iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as pat).
Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
    constr(pat) :=
  iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as ( x1 ) pat).
Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) ")" constr(pat) :=
  iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as ( x1 x2 ) pat).
Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
  iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as ( x1 x2 x3 ) pat).
Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
    constr(pat) :=
  iDestructCore lem as false (fun H =>
    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) ")" constr(pat) :=
  iDestructCore lem as false (fun H =>
    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
  iDestructCore lem as false (fun H =>
    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
    constr(pat) :=
  iDestructCore lem as false (fun H =>
    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
    simple_intropattern(x8) ")" constr(pat) :=
  iDestructCore lem as false (fun H =>
    iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).

Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
  iDestructCore lem as false (fun H => iModCore H; iPure H as pat).

(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
Hint Extern 0 (of_envs _ ⊢ _) => progress iIntros.
Hint Resolve uPred.internal_eq_refl'. (* Maybe make an [iReflexivity] tactic *)

(* We should be able to write [Hint Extern 1 (of_envs _ ⊢ (_ ∗ _)%I) => ...],
but then [eauto] mysteriously fails. See bug 4762 *)
Hint Extern 1 (of_envs _ ⊢ _) =>
  match goal with
  | |- _ ⊢ _ ∧ _ => iSplit
  | |- _ ⊢ _ ∗ _ => iSplit
  | |- _ ⊢ ▷ _ => iNext
  | |- _ ⊢ □ _ => iClear "*"; iAlways
  | |- _ ⊢ ∃ _, _ => iExists _
  | |- _ ⊢ |==> _ => iModIntro
  end.
Hint Extern 1 (of_envs _ ⊢ _) =>
  match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end.
Hint Extern 1 (of_envs _ ⊢ _) =>
  match goal with |- _ ⊢ (_ ∨ _)%I => iRight end.