Coq Tactics Quick Reference

1. General goal management

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

4. Induction

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