Overview of the tactics from LibTactics

Arthur Charguéraud

Notation

E: stands for an expression
H: stands for an existing hypothesis
X: stands for a fresh identifier
I: stands for an introduction pattern 
R: stands for a definition (a "reference") 
__: is a special notation for "wildcard" 

Manipulation of hypotheses

introv I1 I2 .. IN   (introduction that inputs only the name of hypotheses, not variables)
intros_all           (introduces all arguments, unfolding all definitions on the way)
gen H1 H2 .. HN      (generalizes and clears hypotheses and their dependencies)
clears H1 ... HN     (clears hypotheses and their dependencies)
sets X: E            (defines X as a local definition for E, and replaces occurences of E with X)
sets_eq X: E         (introduces a name X and an equality X = E, and replaces occurences of E with X)

Proof structure

false             (replaces the goal by "False", and try to solve it with contradiction and discriminate)
false E           (proves any goal by contradiction, using an absurd term E)
tryfalse          (proves a goal by contradiction or discriminate, or do nothing)
asserts I: E      (asserts statement E as first subgoal, destruct E as I in the second goal)
cuts I: E         (asserts statement E as second subgoal, destruct E as I in the first goal)
put X: E          (define X to be a name for E, synonymous of pose)
lets I: E         (adds an hypothesis I whose type is the type of E)
lets I1 .. IN: E  (a shortand for "lets [I1[..IN]]: E", useful to decompose conjunctions)

N-ary constructions

splits           (splits an N-ary conjunction into N goals)
splits N         (same as above, but unfolds if necessary to obtain N branches)
destructs E      (destructs an N-ary conjunction E into N hypotheses)
branch N         (selects the N-th branch of a M-ary disjunction)
branch N of M    (same as above, but unfolds if necessary to obtain M branches)
branches E       (case analysis on an N-ary disjunction E)
exists E1 .. EN  (to provide witnesses to an N-ary existential goal, wildcards are supported)

Inversion and induction

inverts H             (inversion followed with substitution of freshly introduced variables)
inverts keep H        (same as above, but H is not cleared)
invert H as I1..IN    (same as inverts H, but allows to name produced hypotheses)
inversions H          (faster implementation of inverts H, but might substitute too many variables)
inductions_wf X: E H  (applies the well-founded induction principle for a particular well-founded relation)

Working with equalities

substs            (improved implementation of subst – does not fail on circular equalities)
fequals           (improved implementation of f_equal – calls congruence, and better on tuples)
decides_equality  (improved implementation of decide equality – ability to unfold definitions)
rewrite_all E     (rewrites E as many time as possible)
asserts_rewrite E (rewrites with E and generates E as first subgoal)
cuts_rewrite E    (rewrites with E and generates E as second subgoal)

Simplification and unfolding

simpls        (simpl everywhere in hypotheses and conclusion)
unsimpl E     (replace the simplification of E with E)
unfolds R     (unfolds the definition of R in hypotheses and conclusion)
unfolds       (unfolds the head definition of the goal)
unfolds in H  (unfolds the head definition of the hypothesis H)
folds R       (folds R in hypotheses and conclusion)
renames H1 to H1', .., HN to HN'  (multiple renaming)

Development

skip             (admits the current goal - works even if it contains existential variables)
skip I: E        (adds an hypothesis I of type E to the context, and assume it is true)
skip_cuts E      (replaces the current goal with an arbitrary new goal E)
skip_rewrite E   (rewrites with the equality E, admitting the statement E)
sort             (reorders hypotheses to get all the propositions at the bottom of the goal)

Automation

- any tactic name followed with the symbol "~" will call [auto] on all subgoals
- any tactic name followed with the symbol "*" will call [induction eauto] on all subgoals
- these default bindings may be customized locally in a development

Advanced instantiation mode

lets I: H E1 ... EN                    (instantiates a lemma and names it)
lets I: (>> H E1 ... EN)     

applys H E1 ... EN                     (instantiates a lemma and applies it)
applys (>> H E1 ... EN)     

specializes H E1 ... EN                (instantiates an hypothesis H in-place)
specializes H (>> E1 ... EN)

forwards I: H                          (instantiates a lemma, then "forwards" it)
forwards I: (>> H E1 ... EN) 

Note: "forwards I: H" is equivalent to "lets I: (>> H __ __ .. __)",
which can also be abbreviated as "lets I: (>> H ___)", with a triple-underscore.

Note: any subterm can be of the form rm X, which indicates that the variable X should be cleared after the operation is complete.