# 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)

## 2. Propositional and equality reasoning

 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

## 3. Arithmetic

• 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

## 4. Induction

• 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

• works better for recursive functions than for definitions.
• Must make sure that the goal contains "f x1 x2 ..." where xi are variables.