# Library Coq.Init.Tactics

# Useful tactics

Ltac exfalso := elimtype False.

A tactic for proof by contradiction. With contradict H,

- H:~A |- B gives |- A
- H:~A |- ~B gives H: B |- A
- H: A |- B gives |- ~A
- H: A |- ~B gives H: B |- ~A
- H:False leads to a resolved subgoal.

Ltac contradict H :=

let save tac H := let x:=fresh in intro x; tac H; rename x into H

in

let negpos H := case H; clear H

in

let negneg H := save negpos H

in

let pospos H :=

let A := type of H in (exfalso; revert H; try fold (~A))

in

let posneg H := save pospos H

in

let neg H := match goal with

| |- (~_) => negneg H

| |- (_->False) => negneg H

| |- _ => negpos H

end in

let pos H := match goal with

| |- (~_) => posneg H

| |- (_->False) => posneg H

| |- _ => pospos H

end in

match type of H with

| (~_) => neg H

| (_->False) => neg H

| _ => (elim H;fail) || pos H

end.

Ltac absurd_hyp H :=

idtac "absurd_hyp is OBSOLETE: use contradict instead.";

let T := type of H in

absurd T.

Ltac false_hyp H G :=

let T := type of H in absurd T; [ apply G | assumption ].

Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x.

Ltac destr_eq H := discriminate H || (try (injection H as [= H])).

Tactic Notation "destruct_with_eqn" constr(x) :=

destruct x eqn:?.

Tactic Notation "destruct_with_eqn" ident(n) :=

try intros until n; destruct n eqn:?.

Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=

destruct x eqn:H.

Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=

try intros until n; destruct n eqn:H.

Break every hypothesis of a certain type

Ltac destruct_all t :=

match goal with

| x : t |- _ => destruct x; destruct_all t

| _ => idtac

end.

Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.

Tactic Notation "rewrite_all" "<-" constr(eq) := repeat rewrite <- eq in *.

Tactics for applying equivalences.
The following code provides tactics "apply -> t", "apply <- t",
"apply -> t in H" and "apply <- t in H". Here t is a term whose type
consists of nested dependent and nondependent products with an
equivalence A <-> B as the conclusion. The tactics with "->" in their
names apply A -> B while those with "<-" in the name apply B -> A.

Ltac find_equiv H :=

let T := type of H in

lazymatch T with

| ?A -> ?B =>

let H1 := fresh in

let H2 := fresh in

cut A;

[intro H1; pose proof (H H1) as H2; clear H H1;

rename H2 into H; find_equiv H |

clear H]

| forall x : ?t, _ =>

let a := fresh "a" in

let H1 := fresh "H" in

evar (a : t); pose proof (H a) as H1; unfold a in H1;

clear a; clear H; rename H1 into H; find_equiv H

| ?A <-> ?B => idtac

| _ => fail "The given statement does not seem to end with an equivalence."

end.

Ltac bapply lemma todo :=

let H := fresh in

pose proof lemma as H;

find_equiv H; [todo H; clear H | .. ].

Tactic Notation "apply" "->" constr(lemma) :=

bapply lemma ltac:(fun H => destruct H as [H _]; apply H).

Tactic Notation "apply" "<-" constr(lemma) :=

bapply lemma ltac:(fun H => destruct H as [_ H]; apply H).

Tactic Notation "apply" "->" constr(lemma) "in" hyp(J) :=

bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J).

Tactic Notation "apply" "<-" constr(lemma) "in" hyp(J) :=

bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).

An experimental tactic simpler than auto that is useful for ending
proofs "in one step"

Ltac easy :=

let rec use_hyp H :=

match type of H with

| _ /\ _ => exact H || destruct_hyp H

| _ => try solve [inversion H]

end

with do_intro := let H := fresh in intro H; use_hyp H

with destruct_hyp H := case H; clear H; do_intro; do_intro in

let rec use_hyps :=

match goal with

| H : _ /\ _ |- _ => exact H || (destruct_hyp H; use_hyps)

| H : _ |- _ => solve [inversion H]

| _ => idtac

end in

let do_atom :=

solve [ trivial with eq_true | reflexivity | symmetry; trivial | contradiction ] in

let rec do_ccl :=

try do_atom;

repeat (do_intro; try do_atom);

solve [ split; do_ccl ] in

solve [ do_atom | use_hyps; do_ccl ] ||

fail "Cannot solve this goal".

Tactic Notation "now" tactic(t) := t; easy.

Slightly more than easy

Ltac easy' := repeat split; simpl; easy || now destruct 1.

A tactic to document or check what is proved at some point of a script

Ltac now_show c := change c.

Support for rewriting decidability statements

Set Implicit Arguments.

Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}),

C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide.

Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}),

~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide.

Tactic Notation "decide" constr(lemma) "with" constr(H) :=

let try_to_merge_hyps H :=

try (clear H; intro H) ||

(let H' := fresh H "bis" in intro H'; try clear H') ||

(let H' := fresh in intro H'; try clear H') in

match type of H with

| ~ ?C => apply (decide_right lemma H); try_to_merge_hyps H

| ?C -> False => apply (decide_right lemma H); try_to_merge_hyps H

| _ => apply (decide_left lemma H); try_to_merge_hyps H

end.

Clear an hypothesis and its dependencies

Tactic Notation "clear" "dependent" hyp(h) :=

let rec depclear h :=

clear h ||

match goal with

| H : context [ h ] |- _ => depclear H; depclear h

| H := context [ h ] |- _ => depclear H; depclear h

end ||

fail "hypothesis to clear is used in the conclusion (maybe indirectly)"

in depclear h.

Revert an hypothesis and its dependencies :
this is actually generalize dependent...

Tactic Notation "revert" "dependent" hyp(h) :=

generalize dependent h.

Provide an error message for dependent induction/dependent destruction that
reports an import is required to use it. Importing Coq.Program.Equality will
shadow this notation with the actual tactics.

Tactic Notation "dependent" "induction" ident(H) :=

fail "To use dependent induction, first [Require Import Coq.Program.Equality.]".

Tactic Notation "dependent" "destruction" ident(H) :=

fail "To use dependent destruction, first [Require Import Coq.Program.Equality.]".

### inversion_sigma

The built-in inversion will frequently leave equalities of dependent pairs. When the first type in the pair is an hProp or otherwise simplifies, inversion_sigma is useful; it will replace the equality of pairs with a pair of equalities, one involving a term casted along the other. This might also prove useful for writing a version of inversion / dependent destruction which does not lose information, i.e., does not turn a goal which is provable into one which requires axiom K / UIP.Ltac simpl_proj_exist_in H :=

repeat match type of H with

| context G[proj1_sig (exist _ ?x ?p)]

=> let G' := context G[x] in change G' in H

| context G[proj2_sig (exist _ ?x ?p)]

=> let G' := context G[p] in change G' in H

| context G[projT1 (existT _ ?x ?p)]

=> let G' := context G[x] in change G' in H

| context G[projT2 (existT _ ?x ?p)]

=> let G' := context G[p] in change G' in H

| context G[proj3_sig (exist2 _ _ ?x ?p ?q)]

=> let G' := context G[q] in change G' in H

| context G[projT3 (existT2 _ _ ?x ?p ?q)]

=> let G' := context G[q] in change G' in H

| context G[sig_of_sig2 (@exist2 ?A ?P ?Q ?x ?p ?q)]

=> let G' := context G[@exist A P x p] in change G' in H

| context G[sigT_of_sigT2 (@existT2 ?A ?P ?Q ?x ?p ?q)]

=> let G' := context G[@existT A P x p] in change G' in H

end.

Ltac induction_sigma_in_using H rect :=

let H0 := fresh H in

let H1 := fresh H in

induction H as [H0 H1] using (rect _ _ _ _);

simpl_proj_exist_in H0;

simpl_proj_exist_in H1.

Ltac induction_sigma2_in_using H rect :=

let H0 := fresh H in

let H1 := fresh H in

let H2 := fresh H in

induction H as [H0 H1 H2] using (rect _ _ _ _ _);

simpl_proj_exist_in H0;

simpl_proj_exist_in H1;

simpl_proj_exist_in H2.

Ltac inversion_sigma_step :=

match goal with

| [ H : _ = exist _ _ _ |- _ ]

=> induction_sigma_in_using H @eq_sig_rect

| [ H : _ = existT _ _ _ |- _ ]

=> induction_sigma_in_using H @eq_sigT_rect

| [ H : exist _ _ _ = _ |- _ ]

=> induction_sigma_in_using H @eq_sig_rect

| [ H : existT _ _ _ = _ |- _ ]

=> induction_sigma_in_using H @eq_sigT_rect

| [ H : _ = exist2 _ _ _ _ _ |- _ ]

=> induction_sigma2_in_using H @eq_sig2_rect

| [ H : _ = existT2 _ _ _ _ _ |- _ ]

=> induction_sigma2_in_using H @eq_sigT2_rect

| [ H : exist2 _ _ _ _ _ = _ |- _ ]

=> induction_sigma_in_using H @eq_sig2_rect

| [ H : existT2 _ _ _ _ _ = _ |- _ ]

=> induction_sigma_in_using H @eq_sigT2_rect

end.

Ltac inversion_sigma := repeat inversion_sigma_step.

A version of time that works for constrs

Ltac time_constr tac :=

let eval_early := match goal with _ => restart_timer end in

let ret := tac () in

let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in

ret.

Useful combinators

Ltac assert_fails tac :=

tryif (once tac) then gfail 0 tac "succeeds" else idtac.

Ltac assert_succeeds tac :=

tryif (assert_fails tac) then gfail 0 tac "fails" else idtac.

Tactic Notation "assert_succeeds" tactic3(tac) :=

assert_succeeds tac.

Tactic Notation "assert_fails" tactic3(tac) :=

assert_fails tac.

#[global]

Hint Variables Opaque : rewrite.