Coq Tactics Quick Reference

1. General goal management

auto - try a collection of tactics
auto with arith - specifically request arithmetic reasoning
tauto - intuitionistic propositional tautologies
intuition - intuitionistic first-order tautologies, breaks the goal. Very useful.
- intuition eauto - a variant that also calls eauto.
assert t, assert (H : t) - adds a new hypothesis, and a separate subgoal for proving it
assumption - proves the goal if it is computationally equal to a hypothesis
clear H - removes a hypothesis from the context
cut - like assert
simpl [in H] - simplify using computation
compute [in H] - use computation, more powerful than simpl and may produce larger terms
unfold id [in H] - unfolds the definition of an indentifier
fold id - folds back the definition of an identifier. Useful when you unfolded a recursive function into a fix.
set id := e in * - give a name "id" to the expression e
clearbody id - clears the body of id (e.g., introduced with set)

Connective	Introduction tactics	Elimination tactics
/\ (conjunction)	split (variant of constructor)	elim (variant of induction)
\/ (disjunction)	left, right	elim (variant of induction)
=> (implication)	intro [a], intros [a b H], intros until a	apply t, apply t with (a := t)
False		absurd
True	constructor [n], constructor n with (a := t)
Exists	exists t	elim (variant of induction)
Forall	intro [a], intros [a b H], intros until a	apply t, apply t with (a := t)
=	reflexivity, symmetry, transitivity t, congruence	rewrite [<-] t, rewrite [<-] t in H, subst, replace
~ (disequality)	elim (variant of induction)	intro

omega - Presburger arithmetic (propositional formulas, with equalities, inequalities, for nat and Z)
auto with arith -
ring - associative commutative rewriting
field - equalities in commutative fields (like ring, but with division)
fourier - linear inequations with propositional structure, on real numbers

Introduction (prove inductive facts)
- apply - treat each constructor as a lemma
- constructor [n] - name the constructor, or let Coq try them all
Elimination (use inductive assumptions
- induction t - applies the induction principle for the type of t, generates subgoals as many as there are constructors, and adds the inductive hypotheses in the contexts. If t is an identifier, then it does "intros until t" before.
- destruct t - performs case analysis without recursion (like induction but no induction hypotheses).
- elim t - like induction but does not deal with the hypotheses, and does not add the induction hypotheses in the context.
- case t - like destruct but does not deal with the hypotheses
- discriminate [H] - proves any goal from a hypothesis H that asserts the equality of two terms build using different constructors
- injection H - if H states an equality of two terms using the same constructor, then injection adds to the context the equalities implied by the fact that the constructors are injective functions
- inversion H - This is like induction, but pays attention to the particular form of the type of H, and will only consider the cases that could have been used (e.g., a hypothesis of this form could have been proved only with these cases, with these bindings). This has the advantage that it discards quickly some cases.

Functional induction is a useful tactic for proofs by induction on the evaluation of a function