A deduction rule is a link between some (unique) formula, that we call
the conclusion and (several) formulæ that we call the premises. Indeed, a deduction rule can be read in two ways. The first
one has the shape: ``if I know this and this then I can deduce
this''. For instance, if I have a proof of A and a proof of B
then I have a proof of A /\ B. This is forward reasoning from
premises to conclusion. The other way says: ``to prove this I
have to prove this and this''. For instance, to prove A /\ B, I
have to prove A and I have to prove B. This is backward reasoning
which proceeds from conclusion to premises. We say that the conclusion
is the goal to prove and premises are the
subgoals. The tactics implement backward
reasoning. When applied to a goal, a tactic replaces this goal with
the subgoals it generates. We say that a tactic reduces a goal to its
subgoal(s).
Each (sub)goal is denoted with a number. The current goal is numbered
1. By default, a tactic is applied to the current goal, but one can
address a particular goal in the list by writing n:tactic which
means ``apply tactic tactic to goal number n''.
We can show the list of subgoals by typing Show (see
Section 7.3.1).
Since not every rule applies to a given statement, every tactic cannot be
used to reduce any goal. In other words, before applying a tactic to a
given goal, the system checks that some preconditions are
satisfied. If it is not the case, the tactic raises an error message.
Tactics are build from atomic tactics and tactic expressions (which
extends the folklore notion of tactical) to combine those atomic
tactics. This chapter is devoted to atomic tactics. The tactic
language will be described in chapter 9.
There are, at least, three levels of atomic tactics. The simplest one
implements basic rules of the logical framework. The second level is
the one of derived rules which are built by combination of other
tactics. The third one implements heuristics or decision procedures to
build a complete proof of a goal.
8.1 Invocation of tactics
A tactic is applied as an ordinary command. If the tactic does not
address the first subgoal, the command may be preceded by the wished
subgoal number as shown below:
tactic_invocation 
::= 
num : tactic . 

 
tactic . 
8.2 Explicit proof as a term
8.2.1 exact term
This tactic applies to any goal. It gives directly the exact proof
term of the goal. Let T be our goal, let p be a term of type
U then exact p succeeds iff T and U are
convertible (see Section 4.3).
Error messages: 
Not an exact proof
8.2.2 refine term
This tactic allows to give an exact proof but still with some
holes. The holes are noted ``_''.
Error messages: 
invalid argument:
the tactic refine doesn't know what to do
with the term you gave.
 Refine passed illformed term: the term you gave is not
a valid proof (not easy to debug in general).
This message may also occur in higherlevel tactics, which call
refine internally.
 Cannot infer a term for this placeholder
there is a hole in the term you gave
which type cannot be inferred. Put a cast around it.
An example of use is given in section 10.1.
8.3 Basics
Tactics presented in this section implement the basic typing rules of
Cic given in Chapter 4.
8.3.1 assumption
This tactic applies to any goal. It implements the
``Var'' rule given in
Section 4.2. It looks in the local context for an
hypothesis which type is equal to the goal. If it is the case, the
subgoal is proved. Otherwise, it fails.
Error messages: 
No such assumption
8.3.2 clear ident
This tactic erases the hypothesis named ident in the local context
of the current goal. Then ident is no more displayed and no more
usable in the proof development.
Variants:  clear ident_{1} ... ident_{n}.
This is equivalent to clear ident_{1}. ... clear
ident_{n}.
 clearbody ident.
This tactic expects ident to be a local definition then clears
its body. Otherwise said, this tactic turns a definition into an
assumption.
Error messages: 
ident not found
 ident is used in the conclusion
 ident is used in the hypothesis ident'
8.3.3 move ident_{1} after ident_{2}
This moves the hypothesis named ident_{1} in the local context
after the hypothesis named ident_{2}.
If ident_{1} comes before ident_{2} in the order of dependences,
then all hypotheses between ident_{1} and ident_{2} which
(possibly indirectly) depend on ident_{1} are moved also.
If ident_{1} comes after ident_{2} in the order of dependences,
then all hypotheses between ident_{1} and ident_{2} which
(possibly indirectly) occur in ident_{1} are moved also.
Error messages:  ident_{i} not found
 Cannot move ident_{1} after ident_{2}:
it occurs in ident_{2}
 Cannot move ident_{1} after ident_{2}:
it depends on ident_{2}
8.3.4 rename ident_{1} into ident_{2}
This renames hypothesis ident_{1} into ident_{2} in the current
context^{1}
Error messages:  ident_{2} not found
 ident_{2} is already used
This tactic applies to a goal which is either a product or starts with
a let binder. If the goal is a product, the tactic implements the
``Lam'' rule given in
Section 4.2^{2}. If the
goal starts with a let binder then the tactic implements a mix of the
``Let'' and ``Conv''.
If the current goal is a dependent product forall x:T, U (resp let x:=t in U) then intro puts x:T (resp x:=t)
in the local context.
The new subgoal is U.
If the goal is a non dependent product T > U, then it puts
in the local context either Hn:T (if T is of
type Set or Prop) or Xn:T (if the type
of T is Type). The optional index n is such that Hn or Xn is a fresh identifier.
In both cases the new subgoal is U.
If the goal is neither a product nor starting with a let definition,
the tactic intro applies the tactic red until the tactic
intro can be applied or the goal is not reducible.
Error messages: 
No product even after headreduction
 ident is already used
Variants:  intros
Repeats intro until it meets the headconstant. It never reduces
headconstants and it never fails.
 intro ident
Applies intro but forces ident to be the name of the
introduced hypothesis.
Error message: name ident is already used
Remark: If a name used by intro hides the base name of a global
constant then the latter can still be referred to by a qualified name
(see 2.5.2).
 intros ident_{1} ... ident_{n}
Is equivalent to the composed tactic intro ident_{1}; ... ;
intro ident_{n}.
More generally, the intros tactic takes a pattern as
argument in order to introduce names for components of an inductive
definition or to clear introduced hypotheses; This is explained
in 8.7.3.
 intros until ident
Repeats intro until it meets a premise of the goal having form
( ident : term ) and discharges the variable
named ident of the current goal.
Error message: No such hypothesis in current goal
 intros until num
Repeats intro until the numth nondependent premise. For
instance, on the subgoal forall x y:nat, x=y > forall z:nat,z=x>z=y
the
tactic intros until 2 is equivalent to intros x y H
z H0 (assuming x, y, H, z and H0 do not already
occur in context).
Error message: No such hypothesis in current goal
Happens when num is 0 or is greater than the number of nondependent
products of the goal.
 intro after ident
Applies intro but puts the introduced
hypothesis after the hypothesis ident in the hypotheses.
Error messages: 
No product even after headreduction
 No such hypothesis : ident
 intro ident_{1} after ident_{2}
Behaves as previously but ident_{1} is the name of the introduced
hypothesis. It is equivalent to intro ident_{1}; move
ident_{1} after ident_{2}.
Error messages: 
No product even after headreduction
 No such hypothesis : ident
8.3.6 apply term
This tactic applies to any goal. The argument term is a term
wellformed in the local context. The tactic apply tries to
match the current goal against the conclusion of the type of term.
If it succeeds, then the tactic returns as many subgoals as the number
of non dependent premises of the type of term. The tactic apply relies on firstorder patternmatching with dependent
types. See pattern in section 8.5.7 to transform a
secondorder patternmatching problem into a firstorder one.
Error messages: 
Impossible to unify ... with ...
The apply
tactic failed to match the conclusion of term and the current goal.
You can help the apply tactic by transforming your
goal with the change or pattern tactics (see
sections 8.5.7, 8.3.10).
 generated subgoal term' has metavariables in it
This occurs when some instantiations of premises of term are not
deducible from the unification. This is the case, for instance, when
you want to apply a transitivity property. In this case, you have to
use one of the variants below:
Variants:  apply term with term_{1} ... term_{n}
Provides apply with explicit instantiations for all dependent
premises of the type of term which do not occur in the conclusion
and consequently cannot be found by unification. Notice that
term_{1} ... term_{n} must be given according to the order
of these dependent premises of the type of term.
Error message: Not the right number of missing arguments
 apply term with (ref_{1} := term_{1}) ... (ref_{n}
:= term_{n})
This also provides apply with values for instantiating
premises. But variables are referred by names and non dependent
products by order (see syntax in Section 8.3.11).
 eapply term
The tactic eapply behaves as apply but does not fail
when no instantiation are deducible for some variables in the
premises. Rather, it turns these variables into socalled
existential variables which are variables still to instantiate. An
existential variable is identified by a name of the form ?n
where n is a number. The instantiation is intended to be found
later in the proof.
An example of use of eapply is given in
Section 10.2.
 lapply term
This tactic applies to any goal, say G. The argument term
has to be wellformed in the current context, its type being
reducible to a nondependent product A > B with B
possibly containing products. Then it generates two subgoals B>G and A. Applying lapply H (where H has type
A>B and B does not start with a product) does the same
as giving the sequence cut B. 2:apply H. where cut is
described below.
Warning: When term contains more than one non
dependent product the tactic lapply only takes into account the
first product.
8.3.7 set ( ident := term )
Warning: V8 updating to do
This replaces term by ident in the conclusion or in the
hypotheses of the current goal and adds the new definition ident:= term to the local context. The default is to make this
replacement only in the conclusion.
Variants:  set ( ident := term ) in *
This is equivalent to the above form but applies everywhere in the
goal (both in conclusion and hypotheses).
 set ( ident := term ) in * 
This is equivalent to the above form but applies everywhere in the
hypotheses.
 set ( ident := term ) in  *
This is equivalent to the default behaviour of set.
 set ( ident_{0} := term ) in ident_{1}
This behaves the same but substitutes term not in the goal but in
the hypothesis named ident_{1}.
 set ( ident_{0} := term ) in
ident_{1} at num_{1} ... num_{n}
This notation allows to specify which occurrences of the hypothesis
named ident_{1} (or the goal if ident_{1} is the word Goal) should be substituted. The occurrences are numbered from left
to right. A negative occurrence number means an occurrence which
should not be substituted.
 set ( ident_{0} := term ) in
ident_{1} at num_{1}^{1} ... num_{n1}^{1}, ...ident_{m} at num_{1}^{m} ...num_{nm}^{m}
It substitutes term at occurrences num_{1}^{i} ...
num_{ni}^{i} of hypothesis ident_{i}. One of the ident's
may be the word Goal.
 pose ( ident := term )
This adds the local definition ident := term to the current
context without performing any replacement in the goal or in the
hypotheses.
 pose term
This behaves as pose ( ident := term ) but
ident is generated by Coq.
8.3.8 assert ( ident : form )
This tactic applies to any goal. assert (H : U) adds a new
hypothesis of name H asserting U to the current goal
and opens a new subgoal U^{3}. The subgoal U comes first
in the list of subgoals remaining to prove.
Error messages: 
Not a proposition or a type
Arises when the argument form is neither of type Prop, Set nor Type.
Variants:  assert form
This behaves as assert ( ident : form ) but
ident is generated by Coq.
 assert ( ident := term )
This behaves as assert (ident : type);[exact
termidtac] where type is the type of term.
 cut form
This tactic applies to any goal. It implements the non dependent
case of the ``App'' rule given in
Section 4.2. (This is Modus Ponens inference rule.)
cut U transforms the current goal T into the two
following subgoals: U > T and U. The subgoal U
> T comes first in the list of remaining subgoal to prove.
8.3.9 generalize term
This tactic applies to any goal. It generalizes the conclusion w.r.t.
one subterm of it. For example:
Coq < Show.
1 subgoal
x : nat
y : nat
============================
0 <= x + y + y
Coq < generalize (x + y + y).
1 subgoal
x : nat
y : nat
============================
forall n : nat, 0 <= n
If the goal is G and t is a subterm of type T in the goal, then
generalize t replaces the goal by forall (x:T), G'
where G' is obtained from G by replacing all occurrences of t by
x. The name of the variable (here n) is chosen accordingly
to T.
Variants: 
generalize term_{1} ... term_{n}
Is equivalent to generalize term_{n}; ... ; generalize
term_{1}. Note that the sequence of term_{i}'s are processed
from n to 1.
 generalize dependent term
This generalizes term but also all hypotheses which depend
on term. It clears the generalized hypotheses.
This tactic applies to any goal. It implements the rule
``Conv'' given in section 4.3. change U replaces the current goal T with U providing that
U is wellformed and that T and U are convertible.
Error messages: 
Not convertible
Variants: 
change term_{1} with term_{2}
This replaces the occurrences of term_{1} by term_{2} in the
current goal. The terms term_{1} and term_{2} must be
convertible.
 change term_{1} at num_{1} ... num_{i} with term_{2}
This replaces the occurrences numbered num_{1} ... num_{i} of
term_{1} by term_{2} in the current goal.
The terms term_{1} and term_{2} must be convertible.
Error message: Too few occurrences
 change term in ident
 change term_{1} with term_{2} in ident
 change term_{1} at num_{1} ... num_{i} with term_{2} in
ident
This applies the change tactic not to the goal but to the
hypothesis ident.
See also: 8.5
8.3.11 Bindings list
A bindings list is generally used after the keyword with in
tactics. The general shape of a bindings list is (ref_{1} :=
term_{1}) ... (ref_{n} := term_{n}) where ref is either an
ident or a num. It is used to provide a tactic with a list of
values (term_{1}, ..., term_{n}) that have to be substituted
respectively to ref_{1}, ..., ref_{n}. For all i in [1...
n], if ref_{i} is ident_{i} then it references the dependent
product ident_{i}:T (for some type T); if ref_{i} is
num_{i} then it references the num_{i}th non dependent premise.
A bindings list can also be a simple list of terms term_{1}
term_{2} ...term_{n}. In that case the references to which
these terms correspond are determined by the tactic. In case of elim (see section 4) the terms should correspond to
all the dependent products in the type of term while in the case of
apply only the dependent products which are not bound in
the conclusion of the type are given.
8.4 Negation and contradiction
8.4.1 absurd term
This tactic applies to any goal. The argument term is any
proposition P of type Prop. This tactic applies False elimination, that is it deduces the current goal from False, and generates as subgoals ~P and P. It is
very useful in proofs by cases, where some cases are impossible. In
most cases, P or ~P is one of the hypotheses of
the local context.
8.4.2 contradiction
This tactic applies to any goal. The contradiction tactic
attempts to find in the current context (after all intros) one
which is equivalent to False. It permits to prune irrelevant
cases. This tactic is a macro for the tactics sequence intros;
elimtype False; assumption.
Error messages: 
No such assumption
8.5 Conversion tactics
This set of tactics implements different specialized usages of the
tactic change.
All conversion tactics (including change) can be
parameterised by the parts of the goal where the conversion can
occur. The specification of such parts are called clauses. It
can be either the conclusion, or an hypothesis. In the case of a
defined hypothesis it is possible to specify if the conversion should
occur on the type part, the body part or both (default).
Clauses are written after a conversion tactic (tactic
set 8.3.7 also uses clasues) and are introduced by
the keyword in. If no clause is provided, the default is to
perform the conversion only in the conclusion.
The syntax and description of the various clauses follows:

in H_{1} ... H_{n} 
 only in hypotheses H_{1}
...H_{n}
 in H_{1} ... H_{n}  *
 in hypotheses H_{1} ...
H_{n} and in the conclusion
 in * 
 in every hypothesis
 in *
 (equivalent to in *  *) everywhere
 in (type of H_{1}) (value of H_{2}) ... 
 in
type part of H_{1}, in the value part of H_{2}, etc.
For backward compatibility, the notation in H_{1}... H_{n}
performs the conversion in hypotheses H_{1}... H_{n}.
8.5.1 cbv flag_{1} ... flag_{n}, lazy flag_{1}
... flag_{n} and compute
These parameterized reduction tactics apply to any goal and perform
the normalization of the goal according to the specified flags. Since
the reduction considered in Coq include beta (reduction of
functional application), delta (unfolding of transparent constants,
see 6.2.5), iota (reduction of Cases, Fix
and CoFix expressions) and zeta (removal of local
definitions), every flag is one of beta, delta, iota, zeta, [qualid_{1}...qualid_{k}] and [qualid_{1}...qualid_{k}]. The last two flags give the list
of constants to unfold, or the list of constants not to unfold. These
two flags can occur only after the delta flag.
If alone (i.e. not
followed by [qualid_{1}...qualid_{k}] or [qualid_{1}...qualid_{k}]), the delta flag means that all constants must be unfolded.
However, the delta flag does not apply to variables bound by a
letin construction whose unfolding is controlled by the zeta flag only. In addition, there is a flag Evar to perform
instantiation of existential variables (``?'') when an instantiation
actually exists.
The goal may be normalized with two strategies: lazy (lazy
tactic), or callbyvalue (cbv tactic). The lazy strategy
is a callbyneed strategy, with sharing of reductions: the arguments of a
function call are partially evaluated only when necessary, but if an
argument is used several times, it is computed only once. This
reduction is efficient for reducing expressions with dead code. For
instance, the proofs of a proposition there exists_{T} x. P(x) reduce to a
pair of a witness t, and a proof that t verifies the predicate
P. Most of the time, t may be computed without computing the proof
of P(t), thanks to the lazy strategy.
The callbyvalue strategy is the one used in ML languages: the
arguments of a function call are evaluated first, using a weak
reduction (no reduction under the lambdaabstractions). Despite the
lazy strategy always performs fewer reductions than the callbyvalue
strategy, the latter should be preferred for evaluating purely
computational expressions (i.e. with few dead code).
Variants: 
compute
This tactic is an alias for cbv beta delta evar iota zeta.
Error messages: 
Delta must be specified before
A list of constants appeared before the delta flag.
This tactic applies to a goal which has the form forall (x:T1)...(xk:Tk), c t1 ... tn where c is a constant. If
c is transparent then it replaces c with its definition
(say t) and then reduces (t t1 ... tn) according to
betaiotareduction rules.
Error messages: 
Not reducible
This tactic applies to any goal. It replaces the current goal with its
head normal form according to the betadeltaiotareduction rules.
hnf does not produce a real head normal form but either a
product or an applicative term in head normal form or a variable.
Example: The term forall n:nat, (plus (S n) (S n))
is not reduced by hnf.
Remark: The delta rule only applies to transparent constants
(see section 6.2.4 on transparency and opacity).
This tactic applies to any goal. The tactic simpl first applies
betaiotareduction rule. Then it expands transparent constants
and tries to reduce T' according, once more, to betaiota
rules. But when the iota rule is not applicable then possible
deltareductions are not applied. For instance trying to use simpl on (plus n O)=n does change nothing.
Variants: 
simpl term
This applies simpl only to the occurrences of term in the
current goal.
 simpl term at num_{1} ... num_{i}
This applies simpl only to the num_{1}, ..., num_{i}
occurrences of term in the current goal.
Error message: Too few occurrences
 simpl ident
This applies simpl only to the applicative subterms whose head
occurrence is ident.
 simpl ident at num_{1} ... num_{i}
This applies simpl only to the num_{1}, ..., num_{i}
applicative subterms whose head occurrence is ident.
8.5.5 unfold qualid
This tactic applies to any goal. The argument qualid must denote a
defined transparent constant or local definition (see Sections 1.3.2 and 6.2.5). The tactic unfold applies the delta rule to each occurrence of the constant
to which qualid refers in the current goal and then replaces it
with its betaiotanormal form.
Error messages: 
qualid does not denote an evaluable constant
Variants: 
unfold qualid_{1}, ..., qualid_{n}
Replaces simultaneously qualid_{1}, ..., qualid_{n}
with their definitions and replaces the current goal with its
betaiota normal form.
 unfold qualid_{1} at num_{1}^{1}, ..., num_{i}^{1},
..., qualid_{n} at num_{1}^{n} ... num_{j}^{n}
The lists num_{1}^{1}, ..., num_{i}^{1} and num_{1}^{n}, ...,
num_{j}^{n} specify the occurrences of qualid_{1}, ...,
qualid_{n} to be unfolded. Occurrences are located from left to
right.
Error message: bad occurrence number of qualid_{i}
Error message: qualid_{i} does not occur
This tactic applies to any goal. The term term is reduced using the red
tactic. Every occurrence of the resulting term in the goal is then
substituted for term.
Variants: 
fold term_{1} ... term_{n}
Equivalent to fold term_{1};...; fold term_{n}.
8.5.7 pattern term
This command applies to any goal. The argument term must be a free
subterm of the current goal. The command pattern performs
betaexpansion (the inverse of betareduction) of the current goal
(say T) by

replacing all occurrences of term in T with a fresh variable
 abstracting this variable
 applying the abstracted goal to term
For instance, if the current goal T is expressible has phi(t)
where the notation captures all the instances of t in phi(t),
then pattern t transforms it into (fun x:A => phi(x)) t. This command can be used, for instance, when the tactic
apply fails on matching.
Variants: 
pattern term at num_{1} ... num_{n}
Only the occurrences num_{1} ... num_{n} of term will be
considered for betaexpansion. Occurrences are located from left
to right.
 pattern term_{1}, ..., term_{m}
Starting from a goal phi(t_{1} ... t_{m}), the tactic
pattern t_{1}, ..., t_{m} generates the equivalent goal (fun (x_{1}:A_{1}) ... (x_{m}:A_{m}) => phi(x_{1}...
x_{m})) t_{1} ... t_{m}.
If t_{i} occurs in one of the
generated types A_{j} these occurrences will also be considered and
possibly abstracted.
 pattern term_{1} at num_{1}^{1} ... num_{n1}^{1}, ...,
term_{m} at num_{1}^{m} ... num_{nm}^{m}
This behaves as above but processing only the occurrences num_{1}^{1},
..., num_{i}^{1} of term_{1}, ..., num_{1}^{m}, ..., num_{j}^{m}
of term_{m} starting from term_{m}.
8.5.8 Conversion tactics applied to hypotheses
conv_tactic in ident_{1} ... ident_{n}
Applies the conversion tactic conv_tactic to the
hypotheses ident_{1}, ..., ident_{n}. The tactic conv_tactic is
any of the conversion tactics listed in this section.
If ident_{i} is a local definition, then ident_{i} can be replaced
by (Type of ident_{i}) to address not the body but the type of the
local definition. Example: unfold not in (Type of H1) (Type of H3).
Error messages: 
No such hypothesis : ident.
8.6 Introductions
Introduction tactics address goals which are inductive constants.
They are used when one guesses that the goal can be obtained with one
of its constructors' type.
8.6.1 constructor num
This tactic applies to a goal such that the head of its conclusion is
an inductive constant (say I). The argument num must be less
or equal to the numbers of constructor(s) of I. Let ci be
the ith constructor of I, then constructor i is
equivalent to intros; apply ci.
Error messages: 
Not an inductive product
 Not enough constructors
Variants: 
constructor
This tries constructor 1 then constructor 2,
... , then constructor n where n if
the number of constructors of the head of the goal.
 constructor num with bindings_list
Let ci be the ith constructor of I, then constructor i with bindings_list is equivalent to intros;
apply ci with bindings_list.
Warning: the terms in the bindings_list are checked
in the context where constructor is executed and not in the
context where apply is executed (the introductions are not
taken into account).
 split
Applies if I has only one constructor, typically in the case
of conjunction A/\ B. Then, it is equivalent to constructor 1.
 exists bindings_list
Applies if I has only one constructor, for instance in the
case of existential quantification there exists x· P(x).
Then, it is equivalent to intros; constructor 1 with bindings_list.
 left, right
Apply if I has two constructors, for instance in the case of
disjunction A\/ B. Then, they are respectively equivalent to constructor 1 and constructor 2.
 left bindings_list, right bindings_list, split
bindings_list
As soon as the inductive type has the right number of constructors,
these expressions are equivalent to the corresponding constructor i with bindings_list.
8.7 Eliminations (Induction and Case Analysis)
Elimination tactics are useful to prove statements by induction or
case analysis. Indeed, they make use of the elimination (or
induction) principles generated with inductive definitions (see
Section 4.5).
8.7.1 induction term
This tactic applies to any goal. The type of the argument term must
be an inductive constant. Then, the tactic induction
generates subgoals, one for each possible form of term, i.e. one
for each constructor of the inductive type.
The tactic induction automatically replaces every occurrences
of term in the conclusion and the hypotheses of the goal. It
automatically adds induction hypotheses (using names of the form IHn1) to the local context. If some hypothesis must not be taken
into account in the induction hypothesis, then it needs to be removed
first (you can also use the tactics elim or simple induction,
see below).
There are particular cases:
 If term is an identifier ident denoting a quantified
variable of the conclusion of the goal, then induction ident
behaves as intros until ident; induction ident
 If term is a num, then induction num behaves as
intros until num followed by induction applied to the
last introduced hypothesis.
Remark: For simple induction on a numeral, use syntax induction
(num) (not very interesting anyway).
Example:
Coq < Lemma induction_test : forall n:nat, n = n > n <= n.
1 subgoal
============================
forall n : nat, n = n > n <= n
Coq < intros n H.
1 subgoal
n : nat
H : n = n
============================
n <= n
Coq < induction n.
2 subgoals
H : 0 = 0
============================
0 <= 0
subgoal 2 is:
S n <= S n
Error messages: 
Not an inductive product
 Cannot refine to conclusions with metavariables
As induction uses apply, see Section 8.3.6 and
the variant elim ... with ... below.
Variants: 
induction term as intro_pattern
This behaves as induction term but uses the names in
intro_pattern to names the variables introduced in the context.
The intro_pattern must have the form [ p_{11} ...p_{1n1}  ...  p_{m1} ...p_{mnm} ] with m being the number of constructors of the type of
term. Each variable introduced by induction in the context
of the i^{th} goal gets its name from the list p_{i1} ...p_{ini} in order. If there are not enough names, induction
invents names for the remaining variables to introduce. More
generally, the p's can be any introduction patterns (see
Section 8.7.3). This provides a concise notation for
nested induction.
Remark: for an inductive type with one constructeur, the pattern notation
(p_{1},...,p_{n}) can be used instead of
[ p_{1} ...p_{n} ].
 induction term using qualid
This behaves as induction term but using the induction
scheme of name qualid. It does not expect that the type of
term is inductive.
 induction term using qualid as intro_pattern
This combines induction term using qualid
and induction term as intro_pattern.
 elim term
This is a more basic induction tactic. Again, the type of the
argument term must be an inductive constant. Then according to
the type of the goal, the tactic elim chooses the right
destructor and applies it (as in the case of the apply
tactic). For instance, assume that our proof context contains n:nat, assume that our current goal is T of type Prop, then elim n is equivalent to apply nat_ind with
(n:=n). The tactic elim does not affect the hypotheses of
the goal, neither introduces the induction loading into the context
of hypotheses.
 elim term
also works when the type of term starts with products and the
head symbol is an inductive definition. In that case the tactic
tries both to find an object in the inductive definition and to use
this inductive definition for elimination. In case of nondependent
products in the type, subgoals are generated corresponding to the
hypotheses. In the case of dependent products, the tactic will try
to find an instance for which the elimination lemma applies.
 elim term with term_{1} ... term_{n}
Allows the user to give explicitly the values for dependent
premises of the elimination schema. All arguments must be given.
Error message: Not the right number of dependent arguments
 elim term with ref_{1} := term_{1} ... ref_{n}
:= term_{n}
Provides also elim with values for instantiating premises by
associating explicitly variables (or non dependent products) with
their intended instance.
 elim term_{1} using term_{2}
Allows the user to give explicitly an elimination predicate
term_{2} which is not the standard one for the underlying inductive
type of term_{1}. Each of the term_{1} and term_{2} is either
a simple term or a term with a bindings list (see 8.3.11).
 elimtype form
The argument form must be inductively defined. elimtype I
is equivalent to cut I. intro Hn; elim Hn;
clear Hn. Therefore the hypothesis Hn will
not appear in the context(s) of the subgoal(s). Conversely, if t is a term of (inductive) type I and which does not occur
in the goal then elim t is equivalent to elimtype I; 2:
exact t.
Error message: Impossible to unify ... with ...
Arises when form needs to be applied to parameters.
 simple induction ident
This tactic behaves as intros until
ident; elim ident when ident is a quantified
variable of the goal.
 simple induction num
This tactic behaves as intros until
num; elim ident where ident is the name given by
intros until num to the numth nondependent premise of
the goal.
8.7.2 destruct term
The tactic destruct is used to perform case analysis without
recursion. Its behavior is similar to induction except
that no induction hypothesis is generated. It applies to any goal and
the type of term must be inductively defined. There are particular cases:
 If term is an identifier ident denoting a quantified
variable of the conclusion of the goal, then destruct ident
behaves as intros until ident; destruct ident
 If term is a num, then destruct num behaves as
intros until num followed by destruct applied to the
last introduced hypothesis.
Remark: For destruction of a numeral, use syntax destruct
(num) (not very interesting anyway).
Variants: 
destruct term as intro_pattern
This behaves as destruct term but uses the names in
intro_pattern to names the variables introduced in the context.
The intro_pattern must have the form [ p_{11} ...p_{1n1}  ...  p_{m1} ...p_{mnm} ] with m being the number of constructors of the type of
term. Each variable introduced by destruct in the context
of the i^{th} goal gets its name from the list p_{i1} ...p_{ini} in order. If there are not enough names, destruct
invents names for the remaining variables to introduce. More
generally, the p's can be any introduction patterns (see
Section 8.7.3). This provides a concise notation for
nested destruction.
Remark: for an inductive type with one constructeur, the pattern notation
(p_{1},...,p_{n}) can be used instead of
[ p_{1} ...p_{n} ].
 destruct term using qualid
This is a synonym of induction term using qualid.
 destruct term as intro_pattern using qualid
This is a synonym of induction term using qualid as
intro_pattern.
 case term
The tactic case is a more basic tactic to perform case
analysis without recursion. It behaves as elim term but using
a caseanalysis elimination principle and not a recursive one.
 case term with term_{1} ... term_{n}
Analogous to elim ... with above.
 simple destruct ident
This tactic behaves as intros until
ident; case ident when ident is a quantified
variable of the goal.
 simple destruct num
This tactic behaves as intros until
num; case ident where ident is the name given by
intros until num to the numth nondependent premise of
the goal.
8.7.3 intros intro_pattern ... intro_pattern
The tactic intros applied to introduction patterns performs both
introduction of variables and case analysis in order to give names to
components of an hypothesis.
An introduction pattern is either:

the wildcard: _
 a variable
 a disjunction of lists of patterns:
[p_{11} ... p_{1m1}  ...  p_{11} ... p_{nmn}]
 a conjunction of patterns: ( p_{1} , ... , p_{n} )
The behavior of intros is defined inductively over the
structure of the pattern given as argument:

introduction on the wildcard do the introduction and then
immediately clear (cf 8.3.2) the corresponding hypothesis;
 introduction on a variable behaves like described in 8.3.5;
 introduction over a
list of patterns p_{1} ... p_{n} is equivalent to the sequence of
introductions over the patterns namely:
intros p_{1};...; intros p_{n}, the goal should start with
at least n products;
 introduction over a
disjunction of list of patterns
[p_{11} ... p_{1m1}  ...  p_{11} ... p_{nmn}]. It introduces a new variable X, its type should be an inductive
definition with n
constructors, then it performs a case analysis over X
(which generates n subgoals), it
clears X and performs on each generated subgoals the corresponding
intros p_{i1} ... p_{imi} tactic;
 introduction over a
conjunction of patterns (p_{1},...,p_{n}), it
introduces a new variable X, its type should be an inductive
definition with 1
constructor with (at least) n arguments, then it performs a case
analysis over X
(which generates 1 subgoal with at least n products), it
clears X and performs an introduction over the list of patterns p_{1} ... p_{n}.
Remark: The pattern (p_{1}, ..., p_{n})
is a synonym for the pattern [p_{1} ... p_{n}], i.e. it
corresponds to the decomposition of an hypothesis typed by an
inductive type with a single constructor.
Coq < Lemma intros_test : forall A B C:Prop, A \/ B /\ C > (A > C) > C.
1 subgoal
============================
forall A B C : Prop, A \/ B /\ C > (A > C) > C
Coq < intros A B C [a [_ c]] f.
2 subgoals
A : Prop
B : Prop
C : Prop
a : A
f : A > C
============================
C
subgoal 2 is:
C
Coq < apply (f a).
1 subgoal
A : Prop
B : Prop
C : Prop
c : C
f : A > C
============================
C
Coq < Proof c.
intros_test is defined
8.7.4 double induction ident_{1} ident_{2}
This tactic applies to any goal. If the variables ident_{1} and
ident_{2} of the goal have an inductive type, then this tactic
performs double induction on these variables. For instance, if the
current goal is forall n m:nat, P n m
then, double induction n
m yields the four cases with their respective inductive hypotheses.
In particular the case for (P (S n) (S m))
with the induction
hypotheses (P (S n) m)
and (m:nat)(P n m)
(hence
(P n m)
and (P n (S m))
).
Remark: When the induction hypothesis (P (S n) m)
is not
needed, induction ident_{1}; destruct ident_{2} produces
more concise subgoals.
Variant:  double induction num_{1} num_{2}
This applies double induction on the num_{1}^{th} and num_{2}^{th} non dependent premises of the goal. More generally, any combination of an
ident and an num is valid.
8.7.5 decompose [ qualid_{1} ... qualid_{n} ] term
This tactic allows to recursively decompose a
complex proposition in order to obtain atomic ones.
Example:
Coq < Lemma ex1 : forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A > C.
1 subgoal
============================
forall A B C : Prop, A /\ B /\ C \/ B /\ C \/ C /\ A > C
Coq < intros A B C H; decompose [and or] H; assumption.
Proof completed.
Coq < Qed.
decompose does not work on righthand sides of implications or products.
Variants:  decompose sum term
This decomposes sum types (like or).
 decompose record term
This decomposes record types (inductive types with one constructor,
like and and exists and those defined with the
Record macro, see p. ??).
8.7.6 functional induction ident term_{1} ... term_{n}.
The experimental tactic functional induction
performs case analysis and induction following the definition of
a (not mutually recursive) function.
Coq < Lemma le_minus : forall n m:nat, (n  m <= n).
1 subgoal
============================
forall n m : nat, n  m <= n
Coq < intros n m.
1 subgoal
n : nat
m : nat
============================
n  m <= n
Coq < functional induction minus n m; simpl; auto.
Proof completed.
Coq < Qed.
functional induction is a shorthand for the more general
command Functional Scheme which builds induction
principles following the recursive structure of (possibly
mutually recursive)
functions.
See also: 10.4 for the difference
between using one or the other.
Remark: functional induction may fail on functions built by
tactics. In particular case analysis of a function are considered
only if they are not inside an application.
Remark: Arguments of the function must be given, including
implicits. If the function is recursive, arguments must be
variables, otherwise they may be any term.
See also: 8.14,10.4
8.8 Equality
These tactics use the equality eq:forall A:Type, A>A>Prop
defined in file Logic.v (see Section 3.1.2). The
notation for eq T t u is simply t=u dropping the
implicit type of t and u.
8.8.1 rewrite term
This tactic applies to any goal. The type of term
must have the form
(x_{1}:A_{1}) ... (x_{n}:A_{n})term_{1}=term_{2}.
Then rewrite term replaces every occurrence of
term_{1} by term_{2} in the goal. Some of the variables x_{1} are
solved by unification, and some of the types A_{1}, ...,
A_{n} become new subgoals.
Remark: In case the type of
term_{1} contains occurrences of variables bound in the
type of term, the tactic tries first to find a subterm of the goal
which matches this term in order to find a closed instance term'_{1}
of term_{1}, and then all instances of term'_{1} will be replaced.
Error messages: 
The term provided does not end with an equation
 Tactic generated a subgoal identical to the original goal
This happens if term_{1} does not occur in the goal.
Variants: 
rewrite > term
Is equivalent to rewrite term
 rewrite < term
Uses the equality term_{1}=term_{2} from right to left
 rewrite term in ident
Analogous to rewrite term but rewriting is done in the
hypothesis named ident.
 rewrite > term in ident
Behaves as rewrite term in ident.
 rewrite < term in ident
Uses the equality term_{1}=term_{2} from right to left to
rewrite in the hypothesis named ident.
8.8.2 cutrewrite > term_{1} = term_{2}
This tactic acts like replace term_{1} with term_{2}
(see below).
8.8.3 replace term_{1} with term_{2}
This tactic applies to any goal. It replaces all free occurrences of
term_{1} in the current goal with term_{2} and generates the
equality term_{2}=term_{1} as a subgoal. It is equivalent
to cut term_{2}=term_{1}; intro Hn; rewrite < Hn;
clear Hn.
Variants:  replace term_{1} with term_{2} in ident
This replaces term_{1} with term_{2} in the hypothesis named
ident, and generates the subgoal term_{2}=term_{1}.
Error messages: 
No such hypothesis : ident
 Nothing to rewrite in ident
8.8.4 reflexivity
This tactic applies to a goal which has the form t=u. It checks
that t and u are convertible and then solves the goal.
It is equivalent to apply refl_equal.
Error messages: 
The conclusion is not a substitutive equation
 Impossible to unify ... with ..
This tactic applies to a goal which has the form t=u and changes it
into u=t.
Variant: symmetry in ident
If the statement of the hypothesis ident has the form t=u,
the tactic changes it to u=t.
8.8.6 transitivity term
This tactic applies to a goal which has the form t=u
and transforms it into the two subgoals
t=term and term=u.
8.8.7 subst ident
This tactic applies to a goal which has ident in its context and
(at least) one hypothesis, say H, of type ident=t or t=ident. Then it replaces
ident by t everywhere in the goal (in the hypotheses
and in the conclusion) and clears ident and H from the context.
Remark: When several hypotheses have the form ident=t or t=ident, the first one is used.
Variants: 
subst ident_{1} ...ident_{n}
Is equivalent to subst ident_{1}; ...; subst ident_{n}.
 subst
Applies subst repeatedly to all identifiers from the context
for which an equality exists.
8.8.8 stepl term
This tactic is for chaining rewriting steps. It assumes a goal of the
form ``R term_{1} term_{2}'' where R is a binary relation
and relies on a database of lemmas of the form forall x y
z, R x y > eq x z > R z y where eq
is typically a setoid equality. The application of stepl term
then replaces the goal by ``R term term_{2}'' and adds a new
goal stating ``eq term term_{1}''.
Lemmas are added to the database using the command
Declare Left Step qualid.
where qualid is the name of the lemma.
The tactic is especially useful for parametric setoids which are not
accepted as regular setoids for rewrite and setoid_replace (see chapter 20).
Variants: 
stepl term by tactic
This applies stepl term then applies tactic to the second goal.
 stepr term
stepr term by tactic
This behaves as stepl but on the righthandside of the binary relation.
Lemmas are expected to be of the form
``forall x y
z, R x y > eq y z > R x z''
and are registered using the command
Declare Right Step qualid.
8.9 Equality and inductive sets
We describe in this section some special purpose tactics dealing with
equality and inductive sets or types. These tactics use the equality
eq:forall (A:Type), A>A>Prop, simply written with the
infix symbol =.
8.9.1 decide equality
This tactic solves a goal of the form
forall x y:R, {x=y}+{~
x=y}, where R
is an inductive type such that its constructors do not take proofs or
functions as arguments, nor objects in dependent types.
Variants: 
decide equality term_{1} term_{2} .
Solves a goal of the form {term_{1}=term_{2}}+{~
term_{1}=term_{2}}.
8.9.2 compare term_{1} term_{2}
This tactic compares two given objects term_{1} and term_{2}
of an inductive datatype. If G is the current goal, it leaves the subgoals
term_{1}=term_{2} > G and ~
term_{1}=term_{2}
> G. The type
of term_{1} and term_{2} must satisfy the same restrictions as in the tactic
decide equality.
8.9.3 discriminate ident
This tactic proves any goal from an absurd hypothesis stating that two
structurally different terms of an inductive set are equal. For
example, from the hypothesis (S (S O))=(S O) we can derive by
absurdity any proposition. Let ident be a hypothesis of type
term_{1} = term_{2} in the local context, term_{1} and
term_{2} being elements of an inductive set. To build the proof,
the tactic traverses the normal forms^{4} of
term_{1} and term_{2} looking for a couple of subterms u
and w (u subterm of the normal form of term_{1} and
w subterm of the normal form of term_{2}), placed at the same
positions and whose head symbols are two different constructors. If
such a couple of subterms exists, then the proof of the current goal
is completed, otherwise the tactic fails.
Remark: If ident does not denote an hypothesis in the local context
but refers to an hypothesis quantified in the goal, then the
latter is first introduced in the local context using
intros until ident.
Error messages: 
ident Not a discriminable equality
occurs when the type of the specified hypothesis is not an equation.
Variants: 
discriminate num
This does the same thing as intros until num then
discriminate ident where ident is the identifier for the last
introduced hypothesis.
 discriminate
It applies to a goal of the form ~
term_{1}=term_{2} and it is equivalent to:
unfold not; intro ident; discriminate
ident.
Error messages: 
No discriminable equalities
occurs when the goal does not verify the expected preconditions.
8.9.4 injection ident
The injection tactic is based on the fact that constructors of
inductive sets are injections. That means that if c is a constructor
of an inductive set, and if (c t_{1}) and (c t_{2}) are two
terms that are equal then t_{1} and t_{2} are equal
too.
If ident is an hypothesis of type term_{1} = term_{2},
then injection behaves as applying injection as deep as possible to
derive the equality of all the subterms of term_{1} and term_{2}
placed in the same positions. For example, from the hypothesis (S
(S n))=(S (S (S m)) we may derive n=(S m). To use this
tactic term_{1} and term_{2} should be elements of an inductive
set and they should be neither explicitly equal, nor structurally
different. We mean by this that, if n_{1} and n_{2} are
their respective normal forms, then:

n_{1} and n_{2} should not be syntactically equal,
 there must not exist any couple of subterms u and w,
u subterm of n_{1} and w subterm of n_{2} ,
placed in the same positions and having different constructors as
head symbols.
If these conditions are satisfied, then, the tactic derives the
equality of all the subterms of term_{1} and term_{2} placed in
the same positions and puts them as antecedents of the current goal.
Example: Consider the following goal:
Coq < Inductive list : Set :=
Coq <  nil : list
Coq <  cons : nat > list > list.
Coq < Variable P : list > Prop.
Coq < Show.
1 subgoal
l : list
n : nat
H : P nil
H0 : cons n l = cons 0 nil
============================
P l
Coq < injection H0.
1 subgoal
l : list
n : nat
H : P nil
H0 : cons n l = cons 0 nil
============================
l = nil > n = 0 > P l
Beware that injection yields always an equality in a sigma type
whenever the injected object has a dependent type.
Remark: If ident does not denote an hypothesis in the local context
but refers to an hypothesis quantified in the goal, then the
latter is first introduced in the local context using
intros until ident.
Error messages: 
ident is not a projectable equality
occurs when the type of
the hypothesis id does not verify the preconditions.
 Not an equation occurs when the type of the
hypothesis id is not an equation.
Variants: 
injection num
This does the same thing as intros until num then
injection ident where ident is the identifier for the last
introduced hypothesis.
 injection
If the current goal is of the form term_{1} <> term_{2},
the tactic computes the head normal form of the goal and then
behaves as the sequence: unfold not; intro ident; injection
ident.
Error message: goal does not satisfy the expected preconditions
8.9.5 simplify_eq ident
Let ident be the name of an hypothesis of type term_{1}=term_{2} in the local context. If term_{1} and
term_{2} are structurally different (in the sense described for the
tactic discriminate), then the tactic simplify_eq behaves as discriminate ident otherwise it behaves as injection
ident.
Remark: If ident does not denote an hypothesis in the local context
but refers to an hypothesis quantified in the goal, then the
latter is first introduced in the local context using
intros until ident.
Variants: 
simplify_eq num
This does the same thing as intros until num then
simplify_eq ident where ident is the identifier for the last
introduced hypothesis.
 simplify_eq
If the current goal has form
~
t_{1}=t_{2}, then this tactic does
hnf; intro ident; simplify_eq ident.
8.9.6 dependent rewrite > ident
This tactic applies to any goal. If ident has type
(existS A B a b)=(existS A B a' b')
in the local context (i.e. each term of the
equality has a sigma type { a:A & (B a)}) this tactic rewrites
a
into a'
and b
into b'
in the current
goal. This tactic works even if B is also a sigma type. This kind
of equalities between dependent pairs may be derived by the injection
and inversion tactics.
Variants: 
dependent rewrite < ident
Analogous to dependent rewrite > but uses the equality from
right to left.
8.10 Inversion
8.10.1 inversion ident
Let the type of ident in the local context be (I t),
where I is a (co)inductive predicate. Then,
inversion applied to ident derives for each possible
constructor c_{i} of (I t), all the necessary
conditions that should hold for the instance (I t) to be
proved by c_{i}.
Remark: If ident does not denote an hypothesis in the local context
but refers to an hypothesis quantified in the goal, then the
latter is first introduced in the local context using
intros until ident.
Variants: 
inversion numThis does the same thing as intros until num then
inversion ident where ident is the identifier for the
last introduced hypothesis.
 inversion_clear ident
This behaves as inversion and then erases ident from the
context.
 inversion ident as intro_pattern
This behaves as inversion but using names in
intro_pattern for naming hypotheses. The intro_pattern must have
the form [ p_{11} ...p_{1n1}  ... 
p_{m1} ...p_{mnm} ] with m being the number of
constructors of the type of ident. Be careful that the list must
be of length m even if inversion discards some cases (which
is precisely one of its roles): for the discarded cases, just use an
empty list (i.e. n_{i}=0).
The arguments of the i^{th} constructor and the
equalities that inversion introduces in the context of the
goal corresponding to the i^{th} constructor, if it exists, get
their names from the list p_{i1} ...p_{ini} in order. If
there are not enough names, induction invents names for the
remaining variables to introduce. In case an equation splits into
several equations (because inversion applies injection
on the equalities it generates), the corresponding name p_{ij} in
the list must be replaced by a sublist of the form [p_{ij1}
...p_{ijq}] (or, equivalently, (p_{ij1},
..., p_{ijq})) where q is the number of subequations
obtained from splitting the original equation. Here is an example.
Coq < Inductive contains0 : list nat > Prop :=
Coq <  in_hd : forall l, contains0 (0 :: l)
Coq <  in_tl : forall l b, contains0 l > contains0 (b :: l).
contains0 is defined
contains0_ind is defined
Coq < Goal forall l:list nat, contains0 (1 :: l) > contains0 l.
1 subgoal
============================
forall l : list nat, contains0 (1 :: l) > contains0 l
Coq < intros l H; inversion H as [  l' p Hl' [Heqp Heql'] ].
1 subgoal
l : list nat
H : contains0 (1 :: l)
l' : list nat
p : nat
Hl' : contains0 l
Heqp : p = 1
Heql' : l' = l
============================
contains0 l
 inversion num as intro_pattern
This allows to name the hypotheses introduced by
inversion num in the context.
 inversion_clear
ident as intro_pattern
This allows to name the hypotheses introduced by
inversion_clear in the context.
 inversion ident
in ident_{1} ... ident_{n}
Let ident_{1} ... ident_{n}, be identifiers in the local context. This
tactic behaves as generalizing ident_{1} ... ident_{n}, and
then performing inversion.
 inversion
ident as intro_pattern in ident_{1} ...
ident_{n}
This allows to name the hypotheses introduced in the context by
inversion ident in ident_{1} ...
ident_{n}.
 inversion_clear
ident in ident_{1} ...ident_{n}
Let ident_{1} ... ident_{n}, be identifiers in the local context. This
tactic behaves as generalizing ident_{1} ... ident_{n}, and
then performing inversion_clear.

inversion_clear ident as intro_pattern
in ident_{1} ...ident_{n}
This allows to name the hypotheses introduced in the context by
inversion_clear ident in ident_{1} ...ident_{n}.
 dependent inversion
ident
That must be used when ident appears in the current goal. It acts
like inversion and then substitutes ident for the
corresponding term in the goal.
 dependent
inversion ident as intro_pattern
This allows to name the hypotheses introduced in the context by
dependent inversion ident.
 dependent
inversion_clear ident
Like dependent inversion, except that ident is cleared
from the local context.

dependent inversion_clear identas intro_pattern
This allows to name the hypotheses introduced in the context by
dependent inversion_clear ident
 dependent
inversion ident with termThis variant allow to give the good generalization of the goal. It
is useful when the system fails to generalize the goal automatically. If
ident has type (I t) and I has type
forall (x:T), s, then term must be of type
I:forall (x:T), I x> s' where s' is the
type of the goal.

dependent inversion ident as intro_pattern
with termThis allows to name the hypotheses introduced in the context by
dependent inversion ident with term.

dependent inversion_clear ident with termLike dependent inversion ... with but clears identfrom
the local context.

dependent inversion_clear ident as
intro_pattern with termThis allows to name the hypotheses introduced in the context by
dependent inversion_clear ident with term.
 simple inversion ident
It is a very primitive inversion tactic that derives all the necessary
equalities but it does not simplify the constraints as
inversion do.
 simple inversion
ident as intro_pattern
This allows to name the hypotheses introduced in the context by
simple inversion.
 inversion ident using ident'
Let ident have type (I t) (I an inductive
predicate) in the local context, and ident' be a (dependent) inversion
lemma. Then, this tactic refines the current goal with the specified
lemma.
 inversion
ident using ident' in ident_{1}... ident_{n}
This tactic behaves as generalizing ident_{1}... ident_{n},
then doing inversionidentusing ident'.
See also: 10.5 for detailed examples
8.10.2 Derive Inversion ident with
forall (x:T), I t Sort sort
This command generates an inversion principle for the
inversion ... using tactic.
Let I be an inductive predicate and x the variables
occurring in t. This command generates and stocks the
inversion lemma for the sort sort corresponding to the instance
forall (x:T), I t with the name ident in the global environment. When applied it is equivalent to have inverted
the instance with the tactic inversion.
Variants: 
Derive Inversion_clear ident with
forall (x:T), I t Sort sort
When applied it is equivalent to having
inverted the instance with the tactic inversion
replaced by the tactic inversion_clear.
 Derive Dependent Inversion ident with
forall (x:T), I t Sort sort
When applied it is equivalent to having
inverted the instance with the tactic dependent inversion.
 Derive Dependent Inversion_clear ident with
forall (x:T), I t Sort sort
When applied it is equivalent to having
inverted the instance with the tactic dependent inversion_clear.
See also: 10.5 for examples
This kind of inversion has nothing to do with the tactic
inversion above. This tactic does change (ident
t), where t is a term build in order to ensure the
convertibility. In other words, it does inversion of the function
ident. This function must be a fixpoint on a simple recursive
datatype: see 10.7 for the full details.
Error messages: 
quote: not a simple fixpoint
Happens when quote is not able to perform inversion properly.
Variants: 
quote ident [ ident_{1} ...ident_{n} ]
All terms that are build only with ident_{1} ...ident_{n} will be
considered by quote as constants rather than variables.
8.11 Automatizing
This tactic implements a Prologlike resolution procedure to solve the
current goal. It first tries to solve the goal using the assumption tactic, then it reduces the goal to an atomic one using
intros and introducing the newly generated hypotheses as hints.
Then it looks at the list of tactics associated to the head symbol of
the goal and tries to apply one of them (starting from the tactics
with lower cost). This process is recursively applied to the generated
subgoals.
By default, auto only uses the hypotheses of the current goal and the
hints of the database named core.
Variants:  auto num
Forces the search depth to be num. The maximal search depth is 5 by
default.
 auto with ident_{1} ... ident_{n}
Uses the hint databases ident_{1} ... ident_{n} in addition to
the database core. See Section 8.12 for the
list of predefined databases and the way to create or extend a
database. This option can be combined with the previous one.
 auto with *
Uses all existing hint databases, minus the special database
v62. See Section 8.12
 trivial
This tactic is a restriction of auto that is not recursive and
tries only hints which cost is 0. Typically it solves trivial
equalities like X=X.
 trivial with ident_{1} ... ident_{n}
 trivial with *
Remark: auto either solves completely the goal or else leave it
intact. auto and trivial never fail.
See also: Section 8.12
This tactic generalizes auto. In contrast with
the latter, eauto uses unification of the goal
against the hints rather than patternmatching
(in other words, it uses eapply instead of
apply).
As a consequence, eauto can solve such a goal:
Coq < Hint Resolve ex_intro.
Warning: the hint: EApply ex_intro will only be used by EAuto
Coq < Goal forall P:nat > Prop, P 0 > exists n, P n.
1 subgoal
============================
forall P0 : nat > Prop, P0 0 > exists n : nat, P0 n
Coq < eauto.
Proof completed.
Note that ex_intro should be declared as an
hint.
See also: Section 8.12
This tactic implements a decision procedure for intuitionistic propositional
calculus based on the contractionfree sequent calculi LJT* of Roy Dyckhoff
[49]. Note that tauto succeeds on any instance of an
intuitionistic tautological proposition. tauto unfolds negations
and logical equivalence but does not unfold any other definition.
The following goal can be proved by tauto whereas auto
would fail:
Coq < Goal forall (x:nat) (P:nat > Prop), x = 0 \/ P x > x <> 0 > P x.
1 subgoal
============================
forall (x : nat) (P0 : nat > Prop), x = 0 \/ P0 x > x <> 0 > P0 x
Coq < intros.
1 subgoal
x : nat
P0 : nat > Prop
H : x = 0 \/ P0 x
H0 : x <> 0
============================
P0 x
Coq < tauto.
Proof completed.
Moreover, if it has nothing else to do, tauto performs
introductions. Therefore, the use of intros in the previous
proof is unnecessary. tauto can for instance prove the
following:
Coq < (* auto would fail *)
Coq < Goal forall (A:Prop) (P:nat > Prop),
Coq < A \/ (forall x:nat, ~ A > P x) > forall x:nat, ~ A > P x.
1 subgoal
============================
forall (A : Prop) (P0 : nat > Prop),
A \/ (forall x : nat, ~ A > P0 x) > forall x : nat, ~ A > P0 x
Coq <
Coq < tauto.
Proof completed.
Remark: In contrast, tauto cannot solve the following goal
Coq < Goal forall (A:Prop) (P:nat > Prop),
Coq < A \/ (forall x:nat, ~ A > P x) > forall x:nat, ~ ~ (A \/ P x).
because (forall x:nat, ~ A > P x)
cannot be treated as atomic and an
instantiation of x
is necessary.
8.11.4 intuition tactic
The tactic intuition takes advantage of the searchtree builded
by the decision procedure involved in the tactic tauto. It uses
this information to generate a set of subgoals equivalent to the
original one (but simpler than it) and applies the tactic
tactic to them [89]. If this tactic fails on some goals then
intuition fails. In fact, tauto is simply intuition
fail.
For instance, the tactic intuition auto applied to the goal
(forall (x:nat), P x)/\B > (forall (y:nat),P y)/\ P O \/B/\ P O
internally replaces it by the equivalent one:
(forall (x:nat), P x), B  P O
and then uses auto which completes the proof.
Originally due to César Muñoz, these tactics (tauto and intuition)
have been completely reenginered by David Delahaye using mainly the tactic
language (see chapter 9). The code is now quite shorter and
a significant increase in performances has been noticed. The general behavior
with respect to dependent types, unfolding and introductions has
slightly changed to get clearer semantics. This may lead to some
incompatibilities.
Variants: 
intuition
Is equivalent to intuition auto with *.
The tactic firstorder is an experimental extension of
tauto to
firstorder reasoning, written by Pierre Corbineau.
It is not restricted to usual logical connectives but
instead may reason about any firstorder class inductive definition.
Variants: 
firstorder tactic
Tries to solve the goal with tactic when no logical rule may apply.
 firstorder with ident_{1} ... ident_{n}
Adds lemmata ident_{1} ... ident_{n} to the proofsearch
environment.
 firstorder using ident_{1} ... ident_{n}
Adds lemmata in auto hints bases ident_{1} ... ident_{n}
to the proofsearch environment.
Proofsearch is bounded by a depth parameter which can be set by typing the
Set Firstorder Depth n
vernacular command.
The tactic congruence, by Pierre Corbineau, implements the standard Nelson and Oppen
congruence closure algorithm, which is a decision procedure for ground
equalities with uninterpreted symbols. It also include the constructor theory
(see 8.9.4 and 8.9.3).
If the goal is a nonquantified equality, congruence tries to
prove it with nonquantified equalities in the context. Otherwise it
tries to infer a discriminable equality from those in the context.
Coq < Theorem T:
Coq < a=(f a) > (g b (f a))=(f (f a)) > (g a b)=(f (g b a)) > (g a b)=a.
1 subgoal
============================
a = f a > g b (f a) = f (f a) > g a b = f (g b a) > g a b = a
Coq < intros.
1 subgoal
H : a = f a
H0 : g b (f a) = f (f a)
H1 : g a b = f (g b a)
============================
g a b = a
Coq < congruence.
Proof completed.
Coq < Theorem inj : f = pair a > Some (f c) = Some (f d) > c=d.
1 subgoal
============================
f = pair (B:=A) a > Some (f c) = Some (f d) > c = d
Coq < intros.
1 subgoal
H : f = pair (B:=A) a
H0 : Some (f c) = Some (f d)
============================
c = d
Coq < congruence.
Proof completed.
Error messages: 
I don't know how to handle dependent equality
The decision procedure managed to find a proof of the goal or of
a discriminable equality but this proof couldn't be built in Coq
because of dependentlytyped functions.
 I couldn't solve goal
The decision procedure didn't managed to find a proof of the goal or of
a discriminable equality.
The tactic omega, due to Pierre Crégut,
is an automatic decision procedure for Prestburger
arithmetic. It solves quantifierfree
formulae build with ~
, \/
, /\
,
>
on top of equations and inequations on
both the type nat of natural numbers and Z of binary
integers. This tactic must be loaded by the command Require Import
Omega. See the additional documentation about omega
(chapter 17).
8.11.8 ring term_{1} ... term_{n}
This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
associative commutative rewriting on every ring. The tactic must be
loaded by Require Import Ring. The ring must be declared in
the Add Ring command (see 19). The ring of booleans
is predefined; if one wants to use the tactic on nat one must
first require the module ArithRing; for Z, do
Require Import ZArithRing; for N, do Require
Import NArithRing.
The terms term_{1}, ..., term_{n} must be subterms of the goal
conclusion. The tactic ring normalizes these terms
w.r.t. associativity and commutativity and replace them by their
normal form.
Variants: 
ring When the goal is an equality t_{1}=t_{2}, it
acts like ring t_{1} t_{2} and then simplifies or solves
the equality.
 ring_nat is a tactic macro for repeat rewrite
S_to_plus_one; ring. The theorem S_to_plus_one is a
proof that forall (n:nat), S n = plus (S O) n.
Example:
Coq < Require Import ZArithRing.
Coq < Goal forall a b c:Z,
Coq < (a + b + c) * (a + b + c) =
Coq < a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
1 subgoal
============================
forall a b c : Z,
(a + b + c) * (a + b + c) =
a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c
Coq < intros; ring.
Proof completed.
You can have a look at the files Ring.v,
ArithRing.v, ZArithRing.v to see examples of the
Add Ring command.
See also: Chapter 19 for more detailed explanations about this tactic.
This tactic written by David Delahaye and Micaela Mayero solves equalities
using commutative field theory. Denominators have to be non equal to zero and,
as this is not decidable in general, this tactic may generate side conditions
requiring some expressions to be non equal to zero. This tactic must be loaded
by Require Import Field. Field theories are declared (as for ring) with
the Add Field command.
Example:
Coq < Require Import Reals.
Coq < Goal forall x y:R,
Coq < (x * y > 0)%R >
Coq < (x * (1 / x + x / (x + y)))%R =
Coq < (( 1 / y) * y * ( x * (x / (x + y))  1))%R.
Coq < intros; field.
1 subgoal
x : R
y : R
H : (x * y > 0)%R
============================
(x * ((x + y) * y))%R <> 0%R
This vernacular command adds a commutative field theory to the database for the
tactic field. You must provide this theory as follows:
Add Field A Aplus Amult Aone Azero Aopp Aeq Ainv Rth Tinvl
where A is a term of type Type, Aplus is
a term of type A>A>A, Amult is a term of type A>A>A, Aone is a term of type A, Azero is a term of type A, Aopp is a term of
type A>A, Aeq is a term of type A>bool, Ainv is a term of type A>A, Rth is a term
of type (Ring_Theory A Aplus Amult Aone Azero Ainv Aeq),
and Tinvl is a term of type forall n:A,
~(n=Azero)>(Amult (Ainv n) n)=Aone.
To build a ring theory, refer to Chapter 19 for more details.
This command adds also an entry in the ring theory table if this theory is not
already declared. So, it is useless to keep, for a given type, the Add
Ring command if you declare a theory with Add Field, except if you plan
to use specific features of ring (see Chapter 19). However, the
module ring is not loaded by Add Field and you have to make a Require Import Ring if you want to call the ring tactic.
Variants:  Add Field A Aplus Amult Aone Azero
Aopp Aeq Ainv Rth Tinvl
with minus:=Aminus
Adds also the term Aminus which must be a constant expressed by
means of Aopp.
 Add Field A Aplus Amult Aone Azero
Aopp Aeq Ainv Rth Tinvl
with div:=Adiv
Adds also the term Adiv which must be a constant expressed by
means of Ainv.
See also: file theories/Reals/Rbase.v for an example of instantiation,
theory theories/Reals for many examples of use of field.
See also: [37] for more details regarding the implementation of field.
This tactic written by Loïc Pottier solves linear inequations on
real numbers using Fourier's method [58]. This tactic must
be loaded by Require Import Fourier.
Example:
Coq < Require Import Reals.
Coq < Require Import Fourier.
Coq < Goal forall x y:R, (x < y)%R > (y + 1 >= x  1)%R.
Coq < intros; fourier.
Proof completed.
8.11.12 autorewrite with ident_{1} ...ident_{n}.
This tactic ^{5} carries out rewritings according
the rewriting rule bases ident_{1} ...ident_{n}.
Each rewriting rule of a base ident_{i} is applied to the main subgoal until
it fails. Once all the rules have been processed, if the main subgoal has
progressed (e.g., if it is distinct from the initial main goal) then the rules
of this base are processed again. If the main subgoal has not progressed then
the next base is processed. For the bases, the behavior is exactly similar to
the processing of the rewriting rules.
The rewriting rule bases are built with the Hint Rewrite vernacular
command.
Warning: This tactic may loop if you build non terminating rewriting systems.
Variant: 
autorewrite with ident_{1} ...ident_{n} using tactic
Performs, in the same way, all the rewritings of the bases ident_{1} ...
ident_{n} applying tactic to the main subgoal after each rewriting step.
8.11.13 Hint Rewrite term_{1} ...term_{n} : ident
This vernacular command adds the terms term_{1} ...term_{n}
(their types must be equalities) in the rewriting base ident
with the default orientation (left to right). Notice that the
rewriting bases are distinct from the auto hint bases and that
auto does not take them into account.
This command is synchronous with the section mechanism (see 2.3):
when closing a section, all aliases created by Hint Rewrite in that
section are lost. Conversely, when loading a module, all Hint Rewrite
declarations at the global level of that module are loaded.
Variants: 
Hint Rewrite > term_{1} ...term_{n} : ident
This is strictly equivalent to the command above (we only make explicit the
orientation which otherwise defaults to >).
 Hint Rewrite < term_{1} ...term_{n} : ident
Adds the rewriting rules term_{1} ...term_{n} with a righttoleft
orientation in the base ident.
 Hint Rewrite term_{1} ...term_{n} using tactic : ident
When the rewriting rules term_{1} ...term_{n} in ident will
be used, the tactic tactic will be applied to the generated subgoals, the
main subgoal excluded.
See also: 10.6 for examples showing the use of
this tactic.
8.12 The hints databases for auto and eauto
The hints for auto and eauto are stored in
databases. Each databases maps head symbols to list of hints. One can
use the command Print Hint ident to display the hints
associated to the head symbol ident (see 8.12.2). Each
hint has a cost that is an nonnegative integer, and a pattern. The
hint is tried by auto if the conclusion of current goal
matches its pattern, and after hints with a lower cost. The general
command to add a hint to some databases ident_{1}, ..., ident_{n}
is:
Hint hint_definition : ident_{1} ... ident_{n}

where hint_definition is one of the following expressions:
where hint_definition is one of the following expressions:

Resolve term
This command adds apply term to the hint list
with the head symbol of the type of term. The cost of that hint is
the number of subgoals generated by apply term.
In case the inferred type of term does not start with a product the
tactic added in the hint list is exact term. In case this
type can be reduced to a type starting with a product, the tactic apply term is also stored in the hints list.
If the inferred type of term does contain a dependent
quantification on a predicate, it is added to the hint list of eapply instead of the hint list of apply. In this case, a
warning is printed since the hint is only used by the tactic eauto (see 8.11.2). A typical example of hint that is used
only by eauto is a transitivity lemma.
Error messages: 
Bound head variable
The head symbol of the type of term is a bound variable such
that this tactic cannot be associated to a constant.
 term cannot be used as a hint
The type of term contains products over variables which do not
appear in the conclusion. A typical example is a transitivity axiom.
In that case the apply tactic fails, and thus is useless.
Variants:  Resolve term_{1} ...term_{m}
Adds each Resolve term_{i}.
 Immediate term
This command adds apply term; trivial to the hint list
associated with the head symbol of the type of identin the given
database. This tactic will fail if all the subgoals generated by
apply term are not solved immediately by the trivial
tactic which only tries tactics with cost 0.
This command is useful for theorems such that the symmetry of equality
or n+1=m+1 > n=m that we may like to introduce with a
limited use in order to avoid useless proofsearch.
The cost of this tactic (which never generates subgoals) is always 1,
so that it is not used by trivial itself.
Error messages:  Bound head variable
 term cannot be used as a hint
Variants:  Immediate term_{1} ...term_{m}
Adds each Immediate term_{i}.
 Constructors ident
If ident is an inductive type, this command adds all its
constructors as hints of type Resolve. Then, when the
conclusion of current goal has the form (ident ...),
auto will try to apply each constructor.
Error messages:  ident is not an inductive type
 ident not declared
Variants:  Constructors ident_{1} ...ident_{m}
Adds each Constructors ident_{i}.
 Unfold qualid
This adds the tactic unfold qualid to the hint list that
will only be used when the head constant of the goal is ident. Its
cost is 4.
Variants:  Unfold ident_{1} ...ident_{m}
Adds each Unfold ident_{i}.
 Extern num pattern => tactic
This hint type is to extend auto with tactics other than
apply and unfold. For that, we must specify a
cost, a pattern and a tactic to execute. Here is an example:
Hint Extern 4 ~(?=?) => discriminate.
Now, when the head of the goal is a disequality, auto will
try discriminate if it does not succeed to solve the goal
with hints with a cost less than 4.
One can even use some subpatterns of the pattern in the tactic
script. A subpattern is a question mark followed by an ident, like
?X1 or ?X2. Here is an example:
Coq < Require Import List.
Coq < Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) =>
Coq < generalize X1 X2; decide equality : eqdec.
Coq < Goal
Coq < forall a b:list (nat * nat), {a = b} + {a <> b}.
1 subgoal
============================
forall a b : list (nat * nat), {a = b} + {a <> b}
Coq < info auto with eqdec.
== intro a; intro b; generalize a b; decide equality;
generalize a0 p; decide equality.
generalize b0 n0; decide equality.
generalize a1 n; decide equality.
Proof completed.
Remark: There is currently (in the 8.0 release) no way to do
patternmatching on hypotheses.
Variants: 
Hint hint_definition
No database name is given : the hint is registered in the core
database.
 Hint Local hint_definition :
ident_{1} ... ident_{n}
This is used to declare hints that must not be exported to the other
modules that require and import the current module. Inside a
section, the option Local is useless since hints do not
survive anyway to the closure of sections.
 Hint Local hint_definition
Idem for the core database.
8.12.1 Hint databases defined in the Coq standard library
Several hint databases are defined in the Coq standard
library. There is no systematic relation between the directories of the
library and the databases.
 core
 This special database is automatically used by
auto. It contains only basic lemmas about negation,
conjunction, and so on from. Most of the hints in this database come
from the Init and Logic directories.
 arith
 This database contains all lemmas about Peano's
arithmetic proven in the directories Init and
Arith
 zarith
 contains lemmas about binary signed integers from the
directories theories/ZArith and
contrib/omega. It contains also a hint with a high
cost that calls omega.
 bool
 contains lemmas about booleans, mostly from directory
theories/Bool.
 datatypes
 is for lemmas about lists, streams and so on that
are mainly proven in the Lists subdirectory.
 sets
 contains lemmas about sets and relations from the
directories Sets and Relations.
There is also a special database called v62. It collects all
hints that were declared in the versions of Coq prior to version
6.2.4 when the databases core, arith, and so on were
introduced. The purpose of the database v62 is to ensure
compatibility with further versions of Coq for developments done in
versions prior to 6.2.4 (auto being replaced by auto with v62).
The database v62 is intended not to be extended (!). It is not
included in the hint databases list used in the auto with * tactic.
Furthermore, you are advised not to put your own hints in the
core database, but use one or several databases specific to your
development.
This command displays all hints that apply to the current goal. It
fails if no proof is being edited, while the two variants can be used at
every moment.
Variants:  Print Hint ident
This command displays only tactics associated with ident in the
hints list. This is independent of the goal being edited, to this
command will not fail if no goal is being edited.
 Print Hint *
This command displays all declared hints.
 Print HintDb ident
This command displays all hints from database ident.
8.12.3 Hints and sections
Hints provided by the Hint commands are erased when closing a
section. Conversely, all hints of a module A that are not
defined inside a section (and not defined with option Local) become
available when the module A is imported (using
e.g. Require Import A.).
8.13 Generation of induction principles with Scheme
The Scheme command is a highlevel tool for generating
automatically (possibly mutual) induction principles for given types
and sorts. Its syntax follows the schema:
Scheme ident_{1} := Induction for ident'_{1} Sort sort_{1}
with
...
with ident_{m} := Induction for ident'_{m} Sort
sort_{m}

ident'_{1} ... ident'_{m} are different inductive type
identifiers belonging to the same package of mutual inductive
definitions. This command generates ident_{1}... ident_{m}
to be mutually recursive definitions. Each term ident_{i} proves a
general principle of mutual induction for objects in type term_{i}.
Variants: 
Scheme ident_{1} := Minimality for ident'_{1} Sort sort_{1}
with
...
with ident_{m} := Minimality for ident'_{m} Sort
sort_{m}
Same as before but defines a nondependent elimination principle more
natural in case of inductively defined relations.
See also: 10.3
See also: Section 10.3
8.14 Generation of induction principles with Functional Scheme
The Functional Scheme command is a highlevel experimental
tool for generating automatically induction principles
corresponding to (possibly mutually recursive) functions. Its
syntax follows the schema:
Functional Scheme ident_{i} := Induction for
ident'_{i} with ident'_{1} ... ident'_{m}.

ident'_{1} ... ident'_{m} are the names of mutually recursive
functions (they must be in the same order as when they were defined),
ident'_{i} being one of them. This command generates the induction
principle ident_{i}, following the recursive structure and case
analyses of the functions ident'_{1} ... ident'_{m}, and having
ident'_{i} as entry point.
Variants: 
Functional Scheme ident_{1} := Induction for ident'_{1}.
This command is a shortcut for:
Functional Scheme ident_{1} := Induction for
ident'_{1} with ident'_{1}.

This variant can be used for non mutually recursive functions only.
See also: Section 10.4
8.15 Simple tactic macros
A simple example has more value than a long explanation:
Coq < Ltac Solve := simpl; intros; auto.
Solve is defined
Coq < Ltac ElimBoolRewrite b H1 H2 :=
Coq < elim b; [ intros; rewrite H1; eauto  intros; rewrite H2; eauto ].
ElimBoolRewrite is defined
The tactics macros are synchronous with the Coq section mechanism:
a tactic definition is deleted from the current environment
when you close the section (see also 2.3)
where it was defined. If you want that a
tactic macro defined in a module is usable in the modules that
require it, you should put it outside of any section.
The chapter 9 gives examples of more complex
userdefined tactics.
 1
 but it does not rename the hypothesis in the
proofterm...
 2
 Actually, only the second subgoal will be
generated since the other one can be automatically checked.
 3
 This corresponds to the
cut rule of sequent calculus.
 4
 Recall: opaque
constants will not be expanded by delta reductions
 5
 The behavior of this tactic has much changed compared to
the versions available in the previous distributions (V6). This may cause
significant changes in your theories to obtain the same result. As a drawback
of the reenginering of the code, this tactic has also been completely revised
to get a very compact and readable version.