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" with
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 that reports an import is
required to use it. Importing Coq.Program.Equality will shadow this notation
with the actual dependent induction tactic.
Tactic Notation "dependent" "induction" ident(H) :=
fail "To use dependent induction, 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.