- 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

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