Tactics¶
Tactics specify how to transform the proof state of an incomplete proof to eventually generate a complete proof.
Proofs can be developed in two basic ways: In forward reasoning,
the proof begins by proving simple statements that are then combined to prove the
theorem statement as the last step of the proof. With forward reasoning,
for example,
the proof of A /\ B
would begin with proofs of A
and B
, which are
then used to prove A /\ B
. Forward reasoning is probably the most common
approach in humangenerated proofs.
In backward reasoning, the proof begins with the theorem statement
as the goal, which is then gradually transformed until every subgoal generated
along the way has been proven. In this case, the proof of A /\ B
begins
with that formula as the goal. This can be transformed into two subgoals,
A
and B
, followed by the proofs of A
and B
. Coq and its tactics
use backward reasoning.
A tactic may fully prove a goal, in which case the goal is removed from the proof state. More commonly, a tactic replaces a goal with one or more subgoals. (We say that a tactic reduces a goal to its subgoals.)
Most tactics require specific elements or preconditions to reduce a goal;
they display error messages if they can't be applied to the goal.
A few tactics, such as auto
, don't fail even if the proof state
is unchanged.
Goals are identified by number. The current goal is number
1. Tactics are applied to the current goal by default. (The
default can be changed with the Default Goal Selector
option.) They can
be applied to another goal or to multiple goals with a
goal selector such as 2: tactic
.
This chapter describes many of the most common builtin tactics. Builtin tactics can be combined to form tactic expressions, which are described in the Ltac chapter. Since tactic expressions can be used anywhere that a builtin tactic can be used, "tactic" may refer to both builtin tactics and tactic expressions.
Common elements of tactics¶
Reserved keywords¶
The tactics described in this chapter reserve the following keywords:
by using
Thus, these keywords cannot be used as identifiers. It also declares the following character sequences as tokens:
** [= 
Invocation of tactics¶
A tactic is applied as an ordinary command. It may be preceded by a goal selector (see Section Goal selectors). If no selector is specified, the default selector is used.

Option
Default Goal Selector "toplevel_selector"
¶ This option controls the default selector, used when no selector is specified when applying a tactic. The initial value is 1, hence the tactics are, by default, applied to the first goal.
Using value
all
will make it so that tactics are, by default, applied to every goal simultaneously. Then, to apply a tactic tac to the first goal only, you can write1:tac
.Using value
!
enforces that all tactics are used either on a single focused goal or with a local selector (’’strict focusing mode’’).Although other selectors are available, only
all
,!
or a single natural number are valid default goal selectors.
Bindings¶
Tactics that take a term as an argument may also accept bindings
to instantiate some parameters of the term by name or position.
The general form of a term with bindings
is
term_{tac} with bindings
where bindings
can take two different forms:
In the first form, if an
ident
is specified, it must be bound in the type ofterm
and provides the tactic with an instance for the parameter of this name. If anatural
is specified, it refers to then
th non dependent premise ofterm_{tac}
.
Error
No such binder.
¶

Error
In the second form, the interpretation of the
one_term
s depend on which tactic they appear in. Forinduction
,destruct
,elim
andcase
, theone_term
s provide instances for all the dependent products in the type ofterm_{tac}
while in the case ofapply
, or ofconstructor
and its variants, only instances for the dependent products that are not bound in the conclusion ofterm_{tac}
are required.
Error
Not the right number of missing arguments.
¶

Error
Intro patterns¶
Intro patterns let you specify the name to assign to variables and hypotheses
introduced by tactics. They also let you split an introduced hypothesis into
multiple hypotheses or subgoals. Common tactics that accept intro patterns
include assert
, intros
and destruct
.
::=
intropattern*
intropattern::=
*

**

simple_intropattern
simple_intropattern::=
simple_intropattern_closed % term0*
simple_intropattern_closed::=
naming_intropattern

_

or_and_intropattern

rewriting_intropattern

injection_intropattern
naming_intropattern::=
ident

?

?ident
or_and_intropattern::=
[ intropattern_list* ]

( simple_intropattern*, )

( simple_intropattern*& )
rewriting_intropattern::=
>

<
injection_intropattern::=
[= intropattern_list ]
or_and_intropattern_loc::=
or_and_intropattern

ident
Note that the intro pattern syntax varies between tactics.
Most tactics use simple_intropattern
in the grammar.
destruct
, edestruct
, induction
,
einduction
, case
, ecase
and the various
inversion
tactics use or_and_intropattern_loc
, while
intros
and eintros
use intropattern_list
.
The eqn:
construct in various tactics uses naming_intropattern
.
Naming patterns
Use these elementary patterns to specify a name:
ident
— use the specified name?
— let Coq choose a name_
— discard the matched part (unless it is required for another hypothesis)if a disjunction pattern omits a name, such as
[H2]
, Coq will choose a name
Splitting patterns
The most common splitting patterns are:
split a hypothesis in the form
A /\ B
into two hypothesesH1: A
andH2: B
using the pattern(H1 & H2)
or(H1, H2)
or[H1 H2]
. Example. This also works onA <> B
, which is just a notation representing(A > B) /\ (B > A)
.split a hypothesis in the form
A \/ B
into two subgoals using the pattern[H1H2]
. The first subgoal will have the hypothesisH1: A
and the second subgoal will have the hypothesisH2: B
. Examplesplit a hypothesis in either of the forms
A /\ B
orA \/ B
using the pattern[]
.
Patterns can be nested: [[HaHb] H]
can be used to split (A \/ B) /\ C
.
Note that there is no equivalent to intro patterns for goals. For a goal A /\ B
,
use the split
tactic to replace the current goal with subgoals A
and B
.
For a goal A \/ B
, use left
to replace the current goal with A
, or
right
to replace the current goal with B
.
( simple_intropattern+,
) — matches a product over an inductive type with a single constructor. If the number of patterns equals the number of constructor arguments, then it applies the patterns only to the arguments, and( simple_intropattern+, )
is equivalent to[simple_intropattern+]
. If the number of patterns equals the number of constructor arguments plus the number ofletins
, the patterns are applied to the arguments andletin
variables.( simple_intropattern+& )
— matches a righthand nested term that consists of one or more nested binary inductive types such asa1 OP1 a2 OP2 ...
(where theOPn
are rightassociative). (If theOPn
are leftassociative, additional parentheses will be needed to make the term righthand nested, such asa1 OP1 (a2 OP2 ...)
.) The splitting pattern can have more than 2 names, for example(H1 & H2 & H3)
matchesA /\ B /\ C
. The inductive types must have a single constructor with two parameters. Example[ intropattern_list+ ]
— splits an inductive type that has multiple constructors such asA \/ B
into multiple subgoals. The number ofintropattern_list
must be the same as the number of constructors for the matched part.[ intropattern+ ]
— splits an inductive type that has a single constructor with multiple parameters such asA /\ B
into multiple hypotheses. Use[H1 [H2 H3]]
to matchA /\ B /\ C
.[]
— splits an inductive type: If the inductive type has multiple constructors, such asA \/ B
, create one subgoal for each constructor. If the inductive type has a single constructor with multiple parameters, such asA /\ B
, split it into multiple hypotheses.
Equality patterns
These patterns can be used when the hypothesis is an equality:
>
— replaces the righthand side of the hypothesis with the lefthand side of the hypothesis in the conclusion of the goal; the hypothesis is cleared; if the lefthand side of the hypothesis is a variable, it is substituted everywhere in the context and the variable is removed. Example<
— similar to>
, but replaces the lefthand side of the hypothesis with the righthand side of the hypothesis.[= intropattern*, ]
— If the product is over an equality type, applies eitherinjection
ordiscriminate
. Ifinjection
is applicable, the intropattern is used on the hypotheses generated byinjection
. If the number of patterns is smaller than the number of hypotheses generated, the pattern?
is used to complete the list. Example
Other patterns
*
— introduces one or more quantified variables from the result until there are no more quantified variables. Example**
— introduces one or more quantified variables or hypotheses from the result until there are no more quantified variables or implications (>
).intros **
is equivalent tointros
. Examplesimple_intropattern_closed % term*
— first applies each of the terms with theapply … in
tactic on the hypothesis to be introduced, then it usessimple_intropattern_closed
. Example
Note
A \/ B
and A /\ B
use infix notation to refer to the inductive
types or
and and
.
or
has multiple constructors (or_introl
and or_intror
),
while and
has a single constructor (conj
) with multiple parameters
(A
and B
).
These are defined in theories/Init/Logic.v
. The "where" clauses define the
infix notation for "or" and "and".
Note
intros p+
is not always equivalent to intros p; ... ; intros p
if some of the p
are _
. In the first form, all erasures are done
at once, while they're done sequentially for each tactic in the second form.
If the second matched term depends on the first matched term and the pattern
for both is _
(i.e., both will be erased), the first intros
in the second
form will fail because the second matched term still has the dependency on the first.
Examples:
Example: intro pattern for /\
 Goal forall (A: Prop) (B: Prop), (A /\ B) > True.
 1 goal ============================ forall A B : Prop, A /\ B > True
 intros.
 1 goal A, B : Prop H : A /\ B ============================ True
 destruct H as (HA & HB).
 1 goal A, B : Prop HA : A HB : B ============================ True
Example: intro pattern for \/
 Goal forall (A: Prop) (B: Prop), (A \/ B) > True.
 1 goal ============================ forall A B : Prop, A \/ B > True
 intros.
 1 goal A, B : Prop H : A \/ B ============================ True
 destruct H as [HAHB]. all: swap 1 2.
 2 goals A, B : Prop HA : A ============================ True goal 2 is: True 2 goals A, B : Prop HB : B ============================ True goal 2 is: True
Example: > intro pattern
 Goal forall (x:nat) (y:nat) (z:nat), (x = y) > (y = z) > (x = z).
 1 goal ============================ forall x y z : nat, x = y > y = z > x = z
 intros * H.
 1 goal x, y, z : nat H : x = y ============================ y = z > x = z
 intros >.
 1 goal x, z : nat H : x = z ============================ x = z
Example: [=] intro pattern
The first
intros [=]
usesinjection
to strip(S ...)
from both sides of the matched equality. The second usesdiscriminate
on the contradiction1 = 2
(internally represented as(S O) = (S (S O))
) to complete the goal.
 Goal forall (n m:nat), (S n) = (S m) > (S O)=(S (S O)) > False.
 1 goal ============================ forall n m : nat, S n = S m > 1 = 2 > False
 intros *.
 1 goal n, m : nat ============================ S n = S m > 1 = 2 > False
 intros [= H].
 1 goal n, m : nat H : n = m ============================ 1 = 2 > False
 intros [=].
 No more goals.
Example: (A & B & ...) intro pattern
 Parameters (A : Prop) (B: nat > Prop) (C: Prop).
 A is declared B is declared C is declared
 Goal A /\ (exists x:nat, B x /\ C) > True.
 1 goal ============================ A /\ (exists x : nat, B x /\ C) > True
 intros (a & x & b & c).
 1 goal a : A x : nat b : B x c : C ============================ True
Example: * intro pattern
 Goal forall (A: Prop) (B: Prop), A > B.
 1 goal ============================ forall A B : Prop, A > B
 intros *.
 1 goal A, B : Prop ============================ A > B
Example: ** pattern ("intros **" is equivalent to "intros")
 Goal forall (A: Prop) (B: Prop), A > B.
 1 goal ============================ forall A B : Prop, A > B
 intros **.
 1 goal A, B : Prop H : A ============================ B
Example: compound intro pattern
 Goal forall A B C:Prop, A \/ B /\ C > (A > C) > C.
 1 goal ============================ forall A B C : Prop, A \/ B /\ C > (A > C) > C
 intros * [a  (_,c)] f.
 2 goals A, B, C : Prop a : A f : A > C ============================ C goal 2 is: C
 all: swap 1 2.
 2 goals A, B, C : Prop c : C f : A > C ============================ C goal 2 is: C
Example: combined intro pattern using [=] > and %
 Require Import Coq.Lists.List.
 Section IntroPatterns.
 Variables (A : Type) (xs ys : list A).
 A is declared xs is declared ys is declared
 Example ThreeIntroPatternsCombined : S (length ys) = 1 > xs ++ ys = xs.
 1 goal A : Type xs, ys : list A ============================ S (length ys) = 1 > xs ++ ys = xs
 intros [=>%length_zero_iff_nil].
 1 goal A : Type xs : list A ============================ xs ++ nil = xs
intros
would addH : S (length ys) = 1
intros [=]
would additionally applyinjection
toH
to yieldH0 : length ys = 0
intros [=>%length_zero_iff_nil]
applies the theorem, making H the equalityl=nil
, which is then applied as for>
.Theorem length_zero_iff_nil (l : list A): length l = 0 <> l=nil.The example is based on Tej Chajed's coqtricks
Occurrence clauses¶
An occurrence is a subterm of a goal or hypothesis that matches a pattern provided by a tactic. Occurrence clauses select a subset of the ocurrences in a goal and/or in one or more of its hypotheses.
occurrences::=
at occs_nums
in goal_occurrencessimple_occurrences
::=
occurrencesoccs_nums
::=
? nat_or_var+nat_or_var
::=
naturalidentgoal_occurrences
::=
hyp_occs+,  concl_occs??
*  concl_occs?
 concl_occs?
concl_occs?hyp_occs
::=
hypident at occs_nums?hypident
::=
ident
( type of ident )
( value of ident )concl_occs
::=
* at occs_nums?
occurrences
The first form of
occurrences
selects occurrences in the conclusion of the goal. The second form can select occurrences in the goal conclusion and in one or more hypotheses.simple_occurrences
A semantically restricted form of
occurrences
that doesn't allow theat
clause anywhere within it.? nat_or_var+
Selects the specified occurrences within a single goal or hypothesis. Occurrences are numbered starting with 1 following a depthfirst traversal of the term's expression, including occurrences in implicit arguments and coercions that are not displayed by default. (Set the
Printing All
flag to show those in the printed term.)For example, when matching the pattern
_ + _
in the term(a + b) + c
, occurrence 1 is(...) + c
and occurrence 2 is(a + b)
. When matching that pattern with terma + (b + c)
, occurrence 1 isa + (...)
and occurrence 2 isb + c
.Specifying

includes all occurrences except the ones listed.hyp_occs*,  concl_occs??
Selects occurrences in the specified hypotheses and the specified occurrences in the conclusion.
*  concl_occs?
Selects all occurrences in all hypotheses and the specified occurrences in the conclusion.
 concl_occs?
Selects the specified occurrences in the conclusion.
goal_occurrences ::= concl_occs?
Selects all occurrences in all hypotheses and in the specified occurrences in the conclusion.
hypident at occs_nums?
Omiting
occs_nums
selects all occurrences within the hypothesis.hypident ::= ident
Selects the hypothesis named
ident
.( type of ident )
Selects the type part of the named hypothesis (e.g.
: nat
).( value of ident )
Selects the value part of the named hypothesis (e.g.
:= 1
).concl_occs ::= * at occs_nums?
Selects occurrences in the conclusion. '*' by itself selects all occurrences.
occs_nums
selects the specified occurrences.Use
in *
to select all occurrences in all hypotheses and the conclusion, which is equivalent toin *  *
. Use* 
to select all occurrences in all hypotheses.Tactics that select a specific hypothesis H to apply to other hypotheses, such as
rewrite
H in * 
, won't apply H to itself.If multiple occurrences are given, such as in
rewrite
H at 1 2 3
, the tactic must match at least one occurrence in order to succeed. The tactic will fail if no occurrences match. Occurrence numbers that are out of range (e.g.at 1 3
when there are only 2 occurrences in the hypothesis or conclusion) are ignored.Tactics that use occurrence clauses include
set
,remember
,induction
anddestruct
.
Applying theorems¶

Tactic
exact term
¶ This tactic applies to any goal. It gives directly the exact proof term of the goal. Let
T
be our goal, letp
be a term of typeU
thenexact p
succeeds iffT
andU
are convertible (see Conversion rules).
Error
Not an exact proof.
¶

Error

Tactic
assumption
¶ This tactic looks in the local context for a hypothesis whose type is convertible to the goal. If it is the case, the subgoal is proved. Otherwise, it fails.

Error
No such assumption.
¶

Variant
eassumption
¶ This tactic behaves like
assumption
but is able to handle goals with existential variables.

Error

Tactic
refine term
¶ This tactic applies to any goal. It behaves like
exact
with a big difference: the user can leave some holes (denoted by_
or(_ : type)
) in the term.refine
will generate as many subgoals as there are remaining holes in the elaborated term. The type of holes must be either synthesized by the system or declared by an explicit cast like(_ : nat > Prop)
. Any subgoal that occurs in other subgoals is automatically shelved, as if callingshelve_unifiable
. The produced subgoals (shelved or not) are not candidates for typeclass resolution, even if they have a typeclass type as conclusion, letting the user control when and how typeclass resolution is launched on them. This lowlevel tactic can be useful to advanced users.Example
 Inductive Option : Set :=  Fail : Option  Ok : bool > Option.
 Option is defined Option_rect is defined Option_ind is defined Option_rec is defined Option_sind is defined
 Definition get : forall x:Option, x <> Fail > bool.
 1 goal ============================ forall x : Option, x <> Fail > bool
 refine (fun x:Option => match x return x <> Fail > bool with  Fail => _  Ok b => fun _ => b end).
 1 goal x : Option ============================ Fail <> Fail > bool
 intros; absurd (Fail = Fail); trivial.
 No more goals.
 Defined.

Error
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 that call
refine
internally.

Error
Cannot infer a term for this placeholder.
¶ There is a hole in the term you gave whose type cannot be inferred. Put a cast around it.

Variant
simple refine term
¶ This tactic behaves like refine, but it does not shelve any subgoal. It does not perform any betareduction either.

Variant
notypeclasses refine term
¶ This tactic behaves like
refine
except it performs type checking without resolution of typeclasses.

Variant
simple notypeclasses refine term
¶ This tactic behaves like the combination of
simple refine
andnotypeclasses refine
: it performs type checking without resolution of typeclasses, does not perform beta reductions or shelve the subgoals.
Debug
"unification"
enables printing traces of unification steps used during elaboration/typechecking and therefine
tactic."hounification"
prints information about higher order heuristics.

Tactic
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 ofterm
. If it succeeds, then the tactic returns as many subgoals as the number of nondependent premises of the type of term. If the conclusion of the type ofterm
does not match the goal and the conclusion is an inductive type isomorphic to a tuple type, then each component of the tuple is recursively matched to the goal in the lefttoright order.The tactic
apply
relies on firstorder unification with dependent types unless the conclusion of the type ofterm
is of the formP (t_{1} ... t_{n})
withP
to be instantiated. In the latter case, the behavior depends on the form of the goal. If the goal is of the form(fun x => Q) u_{1} ... u_{n}
and thet_{i}
andu_{i}
unify, thenP
is taken to be(fun x => Q)
. Otherwise,apply
tries to defineP
by abstracting overt_1 ... t__n
in the goal. Seepattern
to transform the goal so that it gets the form(fun x => Q) u_{1} ... u_{n}
.
Error
Unable to unify term with term.
¶ The
apply
tactic failed to match the conclusion ofterm
and the current goal. You can help theapply
tactic by transforming your goal with thechange
orpattern
tactics.

Error
Unable to find an instance for the variables ident+.
¶ This occurs when some instantiations of the 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:

Variant
apply term with term+
Provides apply with explicit instantiations for all dependent premises of the type of term that do not occur in the conclusion and consequently cannot be found by unification. Notice that the collection
term+
must be given according to the order of these dependent premises of the type of term.
Error
Not the right number of missing arguments.
¶

Error

Variant
apply term with bindings
This also provides apply with values for instantiating premises. Here, variables are referred by names and nondependent products by increasing numbers (see Bindings).

Variant
apply term+,
This is a shortcut for
apply term_{1}; [..  ... ; [ ..  apply term_{n}] ... ]
, i.e. for the successive applications ofterm
_{i+1} on the last subgoal generated byapply term_{i}
, starting from the application ofterm_{1}
.

Variant
eapply term
¶ The tactic
eapply
behaves likeapply
but it does not fail when no instantiations are deducible for some variables in the premises. Rather, it turns these variables into existential variables which are variables still to instantiate (see Existential variables). The instantiation is intended to be found later in the proof.

Variant
rapply term
¶ The tactic
rapply
behaves likeeapply
but it uses the proof engine ofrefine
for dealing with existential variables, holes, and conversion problems. This may result in slightly different behavior regarding which conversion problems are solvable. However, likeapply
but unlikeeapply
,rapply
will fail if there are any holes which remain interm
itself after typechecking and typeclass resolution but before unification with the goal. More technically,term
is first parsed as aconstr
rather than as auconstr
oropen_constr
before being applied to the goal. Note thatrapply
prefers to instantiate as many hypotheses ofterm
as possible. As a result, if it is possible to applyterm
to arbitrarily many arguments without getting a type error,rapply
will loop.Note that you need to
Require Import Coq.Program.Tactics
to make use ofrapply
.

Variant
simple apply term.
This behaves like
apply
but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, the following example does not succeed because it would require the conversion ofid ?foo
andO
.Example
 Definition id (x : nat) := x.
 id is defined
 Parameter H : forall x y, id x = y.
 H is declared
 Goal O = O.
 1 goal ============================ 0 = 0
 Fail simple apply H.
 The command has indeed failed with message: Unable to unify "id ?M160 = ?M161" with "0 = 0".
Because it reasons modulo a limited amount of conversion,
simple apply
fails quicker thanapply
and it is then wellsuited for uses in userdefined tactics that backtrack often. Moreover, it does not traverse tuples asapply
does.

Variant
simple? apply term with bindings?+,
¶ 
Variant
simple? eapply term with bindings?+,
¶ This summarizes the different syntaxes for
apply
andeapply
.

Variant
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 productA > B
withB
possibly containing products. Then it generates two subgoalsB>G
andA
. Applyinglapply H
(whereH
has typeA>B
andB
does not start with a product) does the same as giving the sequencecut B. 2:apply H.
wherecut
is described below.

Error
Example
Assume we have a transitive relation R
on nat
:
 Parameter R : nat > nat > Prop.
 R is declared
 Axiom Rtrans : forall x y z:nat, R x y > R y z > R x z.
 Rtrans is declared
 Parameters n m p : nat.
 n is declared m is declared p is declared
 Axiom Rnm : R n m.
 Rnm is declared
 Axiom Rmp : R m p.
 Rmp is declared
Consider the goal (R n p)
provable using the transitivity of R
:
 Goal R n p.
 1 goal ============================ R n p
The direct application of Rtrans
with apply
fails because no value
for y
in Rtrans
is found by apply
:
 apply Rtrans.
 Toplevel input, characters 612: > apply Rtrans. > ^^^^^^ Error: Unable to find an instance for the variable y.
A solution is to apply (Rtrans n m p)
or (Rtrans n m)
.
 apply (Rtrans n m p).
 2 goals ============================ R n m goal 2 is: R m p
Note that n
can be inferred from the goal, so the following would work
too.
 apply (Rtrans _ m).
 2 goals ============================ R n m goal 2 is: R m p
More elegantly, apply Rtrans with (y:=m)
allows only mentioning the
unknown m:
 apply Rtrans with (y := m).
 2 goals ============================ R n m goal 2 is: R m p
Another solution is to mention the proof of (R x y)
in Rtrans
 apply Rtrans with (1 := Rnm).
 1 goal ============================ R m p
... or the proof of (R y z)
.
 apply Rtrans with (2 := Rmp).
 1 goal ============================ R n m
On the opposite, one can use eapply
which postpones the problem of
finding m
. Then one can apply the hypotheses Rnm
and Rmp
. This
instantiates the existential variable and completes the proof.
 eapply Rtrans.
 2 focused goals (shelved: 1) ============================ R n ?y goal 2 is: R ?y p
 apply Rnm.
 1 goal ============================ R m p
 apply Rmp.
 No more goals.
Note
When the conclusion of the type of the term to apply
is an inductive
type isomorphic to a tuple type and apply
looks recursively whether a
component of the tuple matches the goal, it excludes components whose
statement would result in applying an universal lemma of the form
forall A, ... > A
. Excluding this kind of lemma can be avoided by
setting the following flag:

Flag
Universal Lemma Under Conjunction
¶ This flag, which preserves compatibility with versions of Coq prior to 8.4 is also available for
apply term in ident
(seeapply … in
).

Tactic
apply term in ident
¶ This tactic applies to any goal. The argument
term
is a term wellformed in the local context and the argumentident
is an hypothesis of the context. The tacticapply term in ident
tries to match the conclusion of the type ofident
against a nondependent premise of the type ofterm
, trying them from right to left. If it succeeds, the statement of hypothesisident
is replaced by the conclusion of the type ofterm
. The tactic also returns as many subgoals as the number of other nondependent premises in the type ofterm
and of the nondependent premises of the type ofident
. If the conclusion of the type ofterm
does not match the goal and the conclusion is an inductive type isomorphic to a tuple type, then the tuple is (recursively) decomposed and the first component of the tuple of which a nondependent premise matches the conclusion of the type ofident
. Tuples are decomposed in a widthfirst lefttoright order (for instance if the type ofH1
isA <> B
and the type ofH2
isA
thenapply H1 in H2
transforms the type ofH2
intoB
). The tacticapply
relies on firstorder pattern matching with dependent types.
Error
Statement without assumptions.
¶ This happens if the type of
term
has no nondependent premise.

Error
Unable to apply.
¶ This happens if the conclusion of
ident
does not match any of the nondependent premises of the type ofterm
.

Variant
apply term with bindings+, in ident+,
This does the same but uses the bindings to instantiate parameters of
term
(see Bindings).

Variant
eapply term with bindings?+, in ident+,
This works as
apply … in
but turns unresolved bindings into existential variables, if any, instead of failing.

Variant
apply term with bindings?+, in ident as simple_intropattern?+,
¶ This works as
apply … in
but applying an associatedsimple_intropattern
to each hypothesisident
that comes with such clause.

Variant
simple apply term in ident+,
This behaves like
apply … in
but it reasons modulo conversion only on subterms that contain no variables to instantiate and does not traverse tuples. See the corresponding example.

Error

Tactic
constructor natural
¶ This tactic applies to a goal such that its conclusion is an inductive type (say
I
). The argumentnatural
must be less or equal to the numbers of constructor(s) ofI
. Letc_{i}
be the ith constructor ofI
, thenconstructor i
is equivalent tointros; apply c_{i}
.
Error
Not an inductive product.
¶

Error
Not enough constructors.
¶

Variant
constructor
This tries
constructor 1
thenconstructor 2
, ..., thenconstructor n
wheren
is the number of constructors of the head of the goal.

Variant
constructor natural with bindings
Let
c
be the ith constructor ofI
, thenconstructor i with bindings
is equivalent tointros; apply c with bindings
.

Variant
split with bindings?
¶ This applies only if
I
has a single constructor. It is then equivalent toconstructor 1 with bindings?
. It is typically used in the case of a conjunction \(A \wedge B\).
Variant
exists bindings
¶ This applies only if
I
has a single constructor. It is then equivalent tointros; constructor 1 with bindings.
It is typically used in the case of an existential quantification \(\exists x, P(x).\)

Error
Not an inductive goal with 1 constructor.
¶

Variant

Variant
left with bindings?
¶ 
Variant
right with bindings?
¶ These tactics apply only if
I
has two constructors, for instance in the case of a disjunction \(A \vee B\). Then, they are respectively equivalent toconstructor 1 with bindings?
andconstructor 2 with bindings?
.
Error
Not an inductive goal with 2 constructors.
¶

Error

Variant
econstructor
¶ 
Variant
eexists
¶ 
Variant
esplit
¶ 
Variant
eleft
¶ 
Variant
eright
¶ These tactics and their variants behave like
constructor
,exists
,split
,left
,right
and their variants but they introduce existential variables instead of failing when the instantiation of a variable cannot be found (cf.eapply
andapply
).

Error
Debug
"tacticunification"
enables printing traces of
unification steps in tactic unification. Tactic unification is used in
tactics such as apply
and rewrite
.
Managing the local context¶

Tactic
intro
¶ This tactic applies to a goal that is either a product or starts with a letbinder. If the goal is a product, the tactic implements the "Lam" rule given in Typing rules 1. If the goal starts with a letbinder, then the tactic implements a mix of the "Let" and "Conv".
If the current goal is a dependent product
forall x:T, U
(resplet x:=t in U
) thenintro
putsx:T
(respx:=t
) in the local context. The new subgoal isU
.If the goal is a nondependent product \(T \rightarrow U\), then it puts in the local context either
Hn:T
(ifT
is of typeSet
orProp
) orXn:T
(if the type ofT
isType
). The optional indexn
is such thatHn
orXn
is a fresh identifier. In both cases, the new subgoal isU
.If the goal is an existential variable,
intro
forces the resolution of the existential variable into a dependent product \(\forall\)x:?X, ?Y
, putsx:?X
in the local context and leaves?Y
as a new subgoal allowed to depend onx
.The tactic
intro
applies the tactichnf
untilintro
can be applied or the goal is not headreducible.
Error
No product even after headreduction.
¶

Variant
intro ident
This applies
intro
but forcesident
to be the name of the introduced hypothesis.
Note
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 Qualified identifiers).

Variant
intros
¶ This repeats
intro
until it meets the headconstant. It never reduces headconstants and it never fails.

Variant
intros until ident
This repeats intro until it meets a premise of the goal having the form
(ident : type)
and discharges the variable namedident
of the current goal.
Error
No such hypothesis in current goal.
¶

Error

Variant
intros until natural
This repeats
intro
until thenatural
th nondependent product.Example
On the subgoal
forall x y : nat, x = y > y = x
the tacticintros until 1
is equivalent tointros x y H
, asx = y > y = x
is the first nondependent product.On the subgoal
forall x y z : nat, x = y > y = x
the tacticintros until 1
is equivalent tointros x y z
as the product onz
can be rewritten as a nondependent product:forall x y : nat, nat > x = y > y = x
.

Variant
intro ident_{1}? after ident_{2}

Variant
intro ident_{1}? before ident_{2}

Variant
intro ident_{1}? at top

Variant
intro ident_{1}? at bottom
These tactics apply
intro ident_{1}?
and move the freshly introduced hypothesis respectively after the hypothesisident_{2}
, before the hypothesisident_{2}
, at the top of the local context, or at the bottom of the local context. All hypotheses on which the new hypothesis depends are moved too so as to respect the order of dependencies between hypotheses. It is equivalent tointro ident_{1}?
followed by the appropriate call tomove … after …
,move … before …
,move … at top
, ormove … at bottom
.Note
intro at bottom
is a synonym forintro
with no argument.

Error

Tactic
intros intropattern_list
¶ Introduces one or more variables or hypotheses from the goal by matching the intro patterns. See the description in Intro patterns.

Tactic
eintros intropattern_list
¶ Works just like
intros …
except that it creates existential variables for any unresolved variables rather than failing.

Tactic
clear ident
¶ This tactic erases the hypothesis named
ident
in the local context of the current goal. As a consequence,ident
is no more displayed and no more usable in the proof development.
Error
No such hypothesis.
¶

Variant
clear  ident+
This variant clears all the hypotheses except the ones depending in the hypotheses named
ident+
and in the goal.

Variant
clear
This variants clears all the hypotheses except the ones the goal depends on.

Error

Tactic
revert ident+
¶ This applies to any goal with variables
ident+
. It moves the hypotheses (possibly defined) to the goal, if this respects dependencies. This tactic is the inverse ofintro
.
Error
No such hypothesis.
¶

Error

Tactic
move ident_{1} after ident_{2}
¶ This moves the hypothesis named
ident_{1}
in the local context after the hypothesis namedident_{2}
, where “after” is in reference to the direction of the move. The proof term is not changed.If
ident_{1}
comes beforeident_{2}
in the order of dependencies, then all the hypotheses betweenident_{1}
andident_{2}
that (possibly indirectly) depend onident_{1}
are moved too, and all of them are thus moved afterident_{2}
in the order of dependencies.If
ident_{1}
comes afterident_{2}
in the order of dependencies, then all the hypotheses betweenident_{1}
andident_{2}
that (possibly indirectly) occur in the type ofident_{1}
are moved too, and all of them are thus moved beforeident_{2}
in the order of dependencies.
Variant
move ident_{1} before ident_{2}
¶ This moves
ident_{1}
towards and just before the hypothesis namedident_{2}
. As formove … after …
, dependencies overident_{1}
(whenident_{1}
comes beforeident_{2}
in the order of dependencies) or in the type ofident_{1}
(whenident_{1}
comes afterident_{2}
in the order of dependencies) are moved too.

Variant
move ident at top
¶ This moves
ident
at the top of the local context (at the beginning of the context).

Variant
move ident at bottom
¶ This moves
ident
at the bottom of the local context (at the end of the context).

Error
No such hypothesis.
¶
Example
 Goal forall x :nat, x = 0 > forall z y:nat, y=y> 0=x.
 1 goal ============================ forall x : nat, x = 0 > nat > forall y : nat, y = y > 0 = x
 intros x H z y H0.
 1 goal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
 move x after H0.
 1 goal z, y : nat H0 : y = y x : nat H : x = 0 ============================ 0 = x
 Undo.
 1 goal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
 move x before H0.
 1 goal z, y, x : nat H : x = 0 H0 : y = y ============================ 0 = x
 Undo.
 1 goal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
 move H0 after H.
 1 goal x, y : nat H0 : y = y H : x = 0 z : nat ============================ 0 = x
 Undo.
 1 goal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
 move H0 before H.
 1 goal x : nat H : x = 0 y : nat H0 : y = y z : nat ============================ 0 = x

Variant

Tactic
rename ident_{1} into ident_{2}
¶ This renames hypothesis
ident_{1}
intoident_{2}
in the current context. The name of the hypothesis in the proofterm, however, is left unchanged.
Variant
rename ident_{i} into ident_{j}+,
This renames the variables
ident_{i}
intoident_{j}
in parallel. In particular, the target identifiers may contain identifiers that exist in the source context, as long as the latter are also renamed by the same tactic.

Error
No such hypothesis.
¶

Variant

Tactic
set (ident := term)
¶ This replaces
term
byident
in the conclusion of the current goal and adds the new definitionident := term
to the local context.If
term
has holes (i.e. subexpressions of the form “_
”), the tactic first checks that all subterms matching the pattern are compatible before doing the replacement using the leftmost subterm matching the pattern.
Variant
set (ident := term) in goal_occurrences
This notation allows specifying which occurrences of
term
have to be substituted in the context. Thein goal_occurrences
clause is an occurrence clause whose syntax and behavior are described in goal occurrences.

Variant
set (ident binder* := term) in goal_occurrences?
This is equivalent to
set (ident := fun binder* => term) in goal_occurrences?
.

Variant
set term in goal_occurrences?
This behaves as
set (ident := term) in goal_occurrences?
butident
is generated by Coq.

Variant
eset (ident binder* := term) in goal_occurrences?
¶ 
Variant
eset term in goal_occurrences?
¶ While the different variants of
set
expect that no existential variables are generated by the tactic,eset
removes this constraint. In practice, this is relevant only wheneset
is used as a synonym ofepose
, i.e. when theterm
does not occur in the goal.

Variant

Tactic
remember term as ident_{1} eqn:naming_intropattern?
¶ This behaves as
set (ident := term) in *
, using a logical (Leibniz’s) equality instead of a local definition. Usenaming_intropattern
to name or split up the new equation.
Variant
remember term as ident_{1} eqn:naming_intropattern? in goal_occurrences
This is a more general form of
remember
that remembers the occurrences ofterm
specified by an occurrence set.

Variant
eremember term as ident_{1} eqn:naming_intropattern? in goal_occurrences?
¶ While the different variants of
remember
expect that no existential variables are generated by the tactic,eremember
removes this constraint.

Variant

Tactic
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. It is equivalent toset (ident := term) in 
.

Tactic
decompose [qualid+] term
¶ This tactic recursively decomposes a complex proposition in order to obtain atomic ones.
Example
 Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A > C.
 1 goal ============================ forall A B C : Prop, A /\ B /\ C \/ B /\ C \/ C /\ A > C
 intros A B C H; decompose [and or] H.
 3 goals A, B, C : Prop H : A /\ B /\ C \/ B /\ C \/ C /\ A H1 : A H0 : B H3 : C ============================ C goal 2 is: C goal 3 is: C
 all: assumption.
 No more goals.
 Qed.
Note
decompose
does not work on righthand sides of implications or products.
Variant
decompose sum term
This decomposes sum types (like
or
).
Controlling the proof flow¶

Tactic
assert (ident : type)
¶ This tactic applies to any goal.
assert (H : U)
adds a new hypothesis of nameH
assertingU
to the current goal and opens a new subgoalU
2. The subgoalU
comes first in the list of subgoals remaining to prove.
Error
Not a proposition or a type.
¶ Arises when the argument
type
is neither of typeProp
,Set
norType
.

Variant
assert type by tactic
This tactic behaves like
assert
but applies tactic to solve the subgoals generated by assert.
Error
Proof is not complete.
¶

Error

Variant
assert type as simple_intropattern
If
simple_intropattern
is an intro pattern (see Intro patterns), the hypothesis is named after this introduction pattern (in particular, ifsimple_intropattern
isident
, the tactic behaves likeassert (ident : type)
). Ifsimple_intropattern
is an action introduction pattern, the tactic behaves likeassert type
followed by the action done by this introduction pattern.

Variant
assert type as simple_intropattern by tactic
This combines the two previous variants of
assert
.

Error

Variant
eassert type as simple_intropattern by tactic
¶ While the different variants of
assert
expect that no existential variables are generated by the tactic,eassert
removes this constraint. This lets you avoid specifying the asserted statement completely before starting to prove it.

Variant
pose proof term as simple_intropattern?
¶ This tactic behaves like
assert type as simple_intropattern? by exact term
wheretype
is the type ofterm
. In particular,pose proof term as ident
behaves asassert (ident := term)
andpose proof term as simple_intropattern
is the same as applying thesimple_intropattern
toterm
.

Variant
epose proof term as simple_intropattern?
¶ While
pose proof
expects that no existential variables are generated by the tactic,epose proof
removes this constraint.

Variant
pose proof (ident := term)
This is an alternative syntax for
assert (ident := term)
andpose proof term as ident
, following the model ofpose (ident := term)
but dropping the value ofident
.

Variant
epose proof (ident := term)
This is an alternative syntax for
eassert (ident := term)
andepose proof term as ident
, following the model ofepose (ident := term)
but dropping the value ofident
.

Variant
enough (ident : type)
¶ This adds a new hypothesis of name
ident
assertingtype
to the goal the tacticenough
is applied to. A new subgoal statingtype
is inserted after the initial goal rather than before it asassert
would do.

Variant
enough type
This behaves like
enough (ident : type)
with the nameident
of the hypothesis generated by Coq.

Variant
enough type as simple_intropattern
This behaves like
enough type
usingsimple_intropattern
to name or destruct the new hypothesis.

Variant
enough (ident : type) by tactic

Variant
enough type as simple_intropattern? by tactic
This behaves as above but with
tactic
expected to solve the initial goal after the extra assumptiontype
is added and possibly destructed. If theas simple_intropattern
clause generates more than one subgoal,tactic
is applied to all of them.

Variant
eenough type as simple_intropattern? by tactic?
¶ 
Variant
eenough (ident : type) by tactic?
¶ While the different variants of
enough
expect that no existential variables are generated by the tactic,eenough
removes this constraint.

Variant
cut type
¶ This tactic applies to any goal. It implements the nondependent case of the “App” rule given in Typing rules. (This is Modus Ponens inference rule.)
cut U
transforms the current goalT
into the two following subgoals:U > T
andU
. The subgoalU > T
comes first in the list of remaining subgoal to prove.

Variant
specialize (ident term*) as simple_intropattern?
¶ 
Variant
specialize ident with bindings as simple_intropattern?
¶ This tactic works on local hypothesis
ident
. The premises of this hypothesis (either universal quantifications or nondependent implications) are instantiated by concrete terms coming either from argumentsterm*
or from Bindings. In the first form the application toterm*
can be partial. The first form is equivalent toassert (ident := ident term*)
. In the second form, instantiation elements can also be partial. In this case the uninstantiated arguments are inferred by unification if possible or left quantified in the hypothesis otherwise. With theas
clause, the local hypothesisident
is left unchanged and instead, the modified hypothesis is introduced as specified by thesimple_intropattern
. The nameident
can also refer to a global lemma or hypothesis. In this case, for compatibility reasons, the behavior ofspecialize
is close to that ofgeneralize
: the instantiated statement becomes an additional premise of the goal. Theas
clause is especially useful in this case to immediately introduce the instantiated statement as a local hypothesis.

Tactic
generalize term
¶ This tactic applies to any goal. It generalizes the conclusion with respect to some term.
Example
 Goal forall x y:nat, 0 <= x + y + y.
 1 goal ============================ forall x y : nat, 0 <= x + y + y
 Proof. intros *.
 1 goal x, y : nat ============================ 0 <= x + y + y
 Show.
 1 goal x, y : nat ============================ 0 <= x + y + y
 generalize (x + y + y).
 1 goal x, 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 based on T
.

Variant
generalize term+
This is equivalent to
generalize term; ... ; generalize term
. Note that the sequence of term _{i} 's are processed from n to 1.

Variant
generalize term at natural+
This is equivalent to
generalize term
but it generalizes only over the specified occurrences ofterm
(counting from left to right on the expression printed using thePrinting All
flag).

Variant
generalize term as ident
This is equivalent to
generalize term
but it usesident
to name the generalized hypothesis.

Variant
generalize term at natural+ as ident+,
This is the most general form of
generalize
that combines the previous behaviors.

Variant
generalize dependent term
This generalizes term but also all hypotheses that depend on
term
. It clears the generalized hypotheses.

Tactic
evar (ident : term)
¶ The
evar
tactic creates a new local definition namedident
with typeterm
in the context. The body of this binding is a fresh existential variable.

Tactic
instantiate (ident := term )
¶ The instantiate tactic refines (see
refine
) an existential variableident
with the termterm
. It is equivalent toonly [ident]: refine term
(preferred alternative).Note
To be able to refer to an existential variable by name, the user must have given the name explicitly (see Existential variables).
Note
When you are referring to hypotheses which you did not name explicitly, be aware that Coq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors.

Variant
instantiate (natural := term)
This variant selects an existential variable by its position. The
natural
argument is the position of the existential variable from right to left in the conclusion of the goal. (Use one of the variants below to select an existential variable in a hypothesis.) Counting starts at 1 and multiple occurrences of the same existential variable are counted multiple times. Because this variant is not robust to slight changes in the goal, its use is strongly discouraged.

Variant
instantiate ( natural := term ) in ident

Variant
instantiate ( natural := term ) in ( value of ident )

Variant
instantiate ( natural := term ) in ( type of ident )
These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition (named
ident
).

Variant
instantiate
Without argument, the instantiate tactic tries to solve as many existential variables as possible, using information gathered from other tactics in the same tactical. This is automatically done after each complete tactic (i.e. after a dot in proof mode), but not, for example, between each tactic when they are sequenced by semicolons.

Tactic
admit
¶ This tactic allows temporarily skipping a subgoal so as to progress further in the rest of the proof. A proof containing admitted goals cannot be closed with
Qed
but only withAdmitted
.

Variant
give_up
Synonym of
admit
.

Tactic
absurd term
¶ This tactic applies to any goal. The argument term is any proposition
P
of typeProp
. This tactic applies False elimination, that is it deduces the current goal from False, and generates as subgoals∼P
andP
. 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.

Tactic
contradiction
¶ This tactic applies to any goal. The contradiction tactic attempts to find in the current context (after all intros) a hypothesis that is equivalent to an empty inductive type (e.g.
False
), to the negation of a singleton inductive type (e.g.True
orx=x
), or two contradictory hypotheses.
Error
No such assumption.
¶

Error

Tactic
contradict ident
¶ This tactic allows manipulating negated hypothesis and goals. The name
ident
should correspond to a hypothesis. Withcontradict H
, the current goal and context is transformed in the following way:H:¬A ⊢ B becomes ⊢ A
H:¬A ⊢ ¬B becomes H: B ⊢ A
H: A ⊢ B becomes ⊢ ¬A
H: A ⊢ ¬B becomes H: B ⊢ ¬A

Tactic
exfalso
¶ This tactic implements the “ex falso quodlibet” logical principle: an elimination of False is performed on the current goal, and the user is then required to prove that False is indeed provable in the current context. This tactic is a macro for
elimtype False
.
Case analysis and induction¶
The tactics presented in this section implement induction or case analysis on inductive or coinductive objects (see Theory of inductive definitions).

Tactic
destruct term
¶ This tactic applies to any goal. The argument
term
must be of inductive or coinductive type and the tactic generates subgoals, one for each possible form ofterm
, i.e. one for each constructor of the inductive or coinductive type. Unlikeinduction
, no induction hypothesis is generated bydestruct
.
Variant
destruct ident
If
ident
denotes a quantified variable of the conclusion of the goal, thendestruct ident
behaves asintros until ident; destruct ident
. Ifident
is not anymore dependent in the goal after application ofdestruct
, it is erased (to avoid erasure, use parentheses, as indestruct (ident)
).If
ident
is a hypothesis of the context, andident
is not anymore dependent in the goal after application ofdestruct
, it is erased (to avoid erasure, use parentheses, as indestruct (ident)
).

Variant
destruct natural
Note
For destruction of a number, use syntax
destruct (natural)
(not very interesting anyway).

Variant
destruct pattern
The argument of
destruct
can also be a pattern of which holes are denoted by “_”. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are compatible and performs case analysis using this subterm.

Variant
destruct term as or_and_intropattern_loc
This behaves as
destruct term
but uses the names inor_and_intropattern_loc
to name the variables introduced in the context. Theor_and_intropattern_loc
must have the form[p11 ... p1n  ...  pm1 ... pmn ]
withm
being the number of constructors of the type ofterm
. Each variable introduced bydestruct
in the context of thei
th goal gets its name from the listpi1 ... pin
in order. If there are not enough names,destruct
invents names for the remaining variables to introduce. More generally, thepij
can be any introduction pattern (seeintros
). This provides a concise notation for chaining destruction of a hypothesis.

Variant
destruct term eqn:naming_intropattern
¶ This behaves as
destruct term
but adds an equation betweenterm
and the value that it takes in each of the possible cases. The name of the equation is specified bynaming_intropattern
(seeintros
), in particular?
can be used to let Coq generate a fresh name.

Variant
destruct term with bindings
This behaves like
destruct term
providing explicit instances for the dependent premises of the type ofterm
.

Variant
edestruct term
¶ This tactic behaves like
destruct term
except that it does not fail if the instance of a dependent premises of the type ofterm
is not inferable. Instead, the unresolved instances are left as existential variables to be inferred later, in the same way aseapply
does.

Variant
destruct term using term with bindings?
This is synonym of
induction term using term with bindings?
.

Variant
destruct term in goal_occurrences
This syntax is used for selecting which occurrences of
term
the case analysis has to be done on. Thein goal_occurrences
clause is an occurrence clause whose syntax and behavior is described in occurrences sets.

Variant
destruct term with bindings? as or_and_intropattern_loc? eqn:naming_intropattern? using term with bindings?? in goal_occurrences?

Variant
edestruct term with bindings? as or_and_intropattern_loc? eqn:naming_intropattern? using term with bindings?? in goal_occurrences?
These are the general forms of
destruct
andedestruct
. They combine the effects of thewith
,as
,eqn:
,using
, andin
clauses.

Variant

Tactic
case term
¶ The tactic
case
is a more basic tactic to perform case analysis without recursion. It behaves aselim term
but using a caseanalysis elimination principle and not a recursive one.

Variant
ecase term with bindings?
¶ In case the type of
term
has dependent premises, or dependent premises whose values are not inferable from thewith bindings
clause,ecase
turns them into existential variables to be resolved later on.

Variant
simple destruct ident
¶ This tactic behaves as
intros until ident; case ident
whenident
is a quantified variable of the goal.

Variant
simple destruct natural
This tactic behaves as
intros until natural; case ident
whereident
is the name given byintros until natural
to thenatural
th nondependent premise of the goal.

Variant
case_eq term
The tactic
case_eq
is a variant of thecase
tactic that allows to perform case analysis on a term without completely forgetting its original form. This is done by generating equalities between the original form of the term and the outcomes of the case analysis.

Tactic
induction term
¶ This tactic applies to any goal. The argument
term
must be of inductive type and the tacticinduction
generates subgoals, one for each possible form ofterm
, i.e. one for each constructor of the inductive type.If the argument is dependent in either the conclusion or some hypotheses of the goal, the argument is replaced by the appropriate constructor form in each of the resulting subgoals and induction hypotheses are added to the local context using names whose prefix is IH.
There are particular cases:
If term is an identifier
ident
denoting a quantified variable of the conclusion of the goal, then inductionident behaves asintros until ident; induction ident
. Ifident
is not anymore dependent in the goal after application ofinduction
, it is erased (to avoid erasure, use parentheses, as ininduction (ident)
).If
term
is anatural
, theninduction natural
behaves asintros until natural
followed byinduction
applied to the last introduced hypothesis.Note
For simple induction on a number, use syntax induction (number) (not very interesting anyway).
In case term is a hypothesis
ident
of the context, andident
is not anymore dependent in the goal after application ofinduction
, it is erased (to avoid erasure, use parentheses, as ininduction (ident)
).The argument
term
can also be a pattern of which holes are denoted by “_”. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are compatible and performs induction using this subterm.
Example
 Lemma induction_test : forall n:nat, n = n > n <= n.
 1 goal ============================ forall n : nat, n = n > n <= n
 intros n H.
 1 goal n : nat H : n = n ============================ n <= n
 induction n.
 2 goals H : 0 = 0 ============================ 0 <= 0 goal 2 is: S n <= S n
 exact (le_n 0).
 1 goal n : nat H : S n = S n IHn : n = n > n <= n ============================ S n <= S n

Error
Not an inductive product.
¶

Error
Unable to find an instance for the variables ident ... ident.
¶ Use in this case the variant
elim … with
below.

Variant
induction term as or_and_intropattern_loc
This behaves as
induction
but uses the names inor_and_intropattern_loc
to name the variables introduced in the context. Theor_and_intropattern_loc
must typically be of the form[ p
_{11}... p
_{1n} ...  p
_{m1}... p
_{mn}]
withm
being the number of constructors of the type ofterm
. Each variable introduced by induction in the context of the ith goal gets its name from the listp
_{i1}... p
_{in} in order. If there are not enough names, induction invents names for the remaining variables to introduce. More generally, thep
_{ij} can be any disjunctive/conjunctive introduction pattern (seeintros …
). For instance, for an inductive type with one constructor, the pattern notation(p
_{1}, ... , p
_{n})
can be used instead of[ p
_{1}... p
_{n}]
.

Variant
induction term with bindings
This behaves like
induction
providing explicit instances for the premises of the type ofterm
(see Bindings).

Variant
einduction term
¶ This tactic behaves like
induction
except that it does not fail if some dependent premise of the type ofterm
is not inferable. Instead, the unresolved premises are posed as existential variables to be inferred later, in the same way aseapply
does.

Variant
induction term using term
¶ This behaves as
induction
but usingterm
as induction scheme. It does not expect the conclusion of the type of the firstterm
to be inductive.

Variant
induction term using term with bindings
This behaves as
induction … using …
but also providing instances for the premises of the type of the secondterm
.

Variant
induction term+, using qualid
This syntax is used for the case
qualid
denotes an induction principle with complex predicates as the induction principles generated byFunction
orFunctional Scheme
may be.

Variant
induction term in goal_occurrences
This syntax is used for selecting which occurrences of
term
the induction has to be carried on. Thein goal_occurrences
clause is an occurrence clause whose syntax and behavior is described in occurrences sets. If variables or hypotheses not mentioningterm
in their type are listed ingoal_occurrences
, those are generalized as well in the statement to prove.Example
 Lemma comm x y : x + y = y + x.
 1 goal x, y : nat ============================ x + y = y + x
 induction y in x  *.
 2 goals x : nat ============================ x + 0 = 0 + x goal 2 is: x + S y = S y + x
 Show 2.
 goal 2 is: x, y : nat IHy : forall x : nat, x + y = y + x ============================ x + S y = S y + x

Variant
induction term with bindings as or_and_intropattern_loc using term with bindings in goal_occurrences

Variant
einduction term with bindings as or_and_intropattern_loc using term with bindings in goal_occurrences
These are the most general forms of
induction
andeinduction
. It combines the effects of the with, as, using, and in clauses.

Variant
elim term
¶ This is a more basic induction tactic. Again, the type of the argument
term
must be an inductive type. Then, according to the type of the goal, the tacticelim
chooses the appropriate destructor and applies it as the tacticapply
would do. For instance, if the local context containsn:nat
and the current goal isT
of typeProp
, thenelim n
is equivalent toapply nat_ind with (n:=n)
. The tacticelim
does not modify the context of the goal, neither introduces the induction loading into the context of hypotheses. More generally,elim term
also works when the type ofterm
is a statement with premises and whose conclusion is inductive. In that case the tactic performs induction on the conclusion of the type ofterm
and leaves the nondependent premises of the type as subgoals. In the case of dependent products, the tactic tries to find an instance for which the elimination lemma applies and fails otherwise.

Variant
elim term with bindings
¶ Allows to give explicit instances to the premises of the type of
term
(see Bindings).

Variant
eelim term
¶ In case the type of
term
has dependent premises, this turns them into existential variables to be resolved later on.

Variant
elim term using term

Variant
elim term using term with bindings
Allows the user to give explicitly an induction principle
term
that is not the standard one for the underlying inductive type ofterm
. Thebindings
clause allows instantiating premises of the type ofterm
.

Variant
elim term with bindings using term with bindings

Variant
eelim term with bindings using term with bindings
These are the most general forms of
elim
andeelim
. It combines the effects of theusing
clause and of the two uses of thewith
clause.

Variant
elimtype type
¶ The argument
type
must be inductively defined.elimtype I
is equivalent tocut I. intro Hn; elim Hn; clear Hn.
Therefore the hypothesisHn
will not appear in the context(s) of the subgoal(s). Conversely, ift
is aterm
of (inductive) typeI
that does not occur in the goal, thenelim t
is equivalent toelimtype I; 2:exact t.

Variant
simple induction ident
¶ This tactic behaves as
intros until ident; elim ident
whenident
is a quantified variable of the goal.

Variant
simple induction natural
This tactic behaves as
intros until natural; elim ident
whereident
is the name given byintros until natural
to thenatural
th nondependent premise of the goal.

Tactic
dependent induction ident
¶ The experimental tactic dependent induction performs induction inversion on an instantiated inductive predicate. One needs to first require the Coq.Program.Equality module to use this tactic. The tactic is based on the BasicElim tactic by Conor McBride [McB00] and the work of Cristina Cornes around inversion [CT95]. From an instantiated inductive predicate and a goal, it generates an equivalent goal where the hypothesis has been generalized over its indexes which are then constrained by equalities to be the right instances. This permits to state lemmas without resorting to manually adding these equalities and still get enough information in the proofs.
Example
 Lemma lt_1_r : forall n:nat, n < 1 > n = 0.
 1 goal ============================ forall n : nat, n < 1 > n = 0
 intros n H ; induction H.
 2 goals n : nat ============================ n = 0 goal 2 is: n = 0
Here we did not get any information on the indexes to help fulfill
this proof. The problem is that, when we use the induction
tactic, we
lose information on the hypothesis instance, notably that the second
argument is 1 here. Dependent induction solves this problem by adding
the corresponding equality to the context.
 Require Import Coq.Program.Equality.
 Lemma lt_1_r : forall n:nat, n < 1 > n = 0.
 1 goal ============================ forall n : nat, n < 1 > n = 0
 intros n H ; dependent induction H.
 2 goals ============================ 0 = 0 goal 2 is: n = 0
The subgoal is cleaned up as the tactic tries to automatically simplify the subgoals with respect to the generated equalities. In this enriched context, it becomes possible to solve this subgoal.
 reflexivity.
 1 goal n : nat H : S n <= 0 IHle : 0 = 1 > n = 0 ============================ n = 0
Now we are in a contradictory context and the proof can be solved.
 inversion H.
 No more goals.
This technique works with any inductive predicate. In fact, the
dependent induction
tactic is just a wrapper around the induction
tactic. One can make its own variant by just writing a new tactic
based on the definition found in Coq.Program.Equality
.

Variant
dependent induction ident generalizing ident+
This performs dependent induction on the hypothesis
ident
but first generalizes the goal by the given variables so that they are universally quantified in the goal. This is generally what one wants to do with the variables that are inside some constructors in the induction hypothesis. The other ones need not be further generalized.

Variant
dependent destruction ident
¶ This performs the generalization of the instance
ident
but usesdestruct
instead of induction on the generalized hypothesis. This gives results equivalent toinversion
ordependent inversion
if the hypothesis is dependent.
See also the larger example of dependent induction
and an explanation of the underlying technique.
See also

Tactic
discriminate term
¶ This tactic proves any goal from an assumption stating that two structurally different
term
s of an inductive set are equal. For example, from(S (S O))=(S O)
we can derive by absurdity any proposition.The argument
term
is assumed to be a proof of a statement of conclusionterm = term
with the two terms being elements of an inductive set. To build the proof, the tactic traverses the normal forms 3 of the terms looking for a couple of subtermsu
andw
(u
subterm of the normal form ofterm
andw
subterm of the normal form ofterm
), 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.
Note
The syntax discriminate ident
can be used to refer to a hypothesis
quantified in the goal. In this case, the quantified hypothesis whose name is
ident
is first introduced in the local context using
intros until ident
.

Error
No primitive equality found.
¶

Error
Not a discriminable equality.
¶

Variant
discriminate natural
This does the same thing as
intros until natural
followed bydiscriminate ident
whereident
is the identifier for the last introduced hypothesis.

Variant
discriminate term with bindings
This does the same thing as
discriminate term
but using the given bindings to instantiate parameters or hypotheses ofterm
.

Variant
ediscriminate natural
¶ 
Variant
ediscriminate term with bindings?
¶ This works the same as
discriminate
but if the type ofterm
, or the type of the hypothesis referred to bynatural
, has uninstantiated parameters, these parameters are left as existential variables.

Variant
discriminate
This behaves like
discriminate ident
if ident is the name of an hypothesis to whichdiscriminate
is applicable; if the current goal is of the formterm <> term
, this behaves asintro ident; discriminate ident
.
Error
No discriminable equalities.
¶

Error

Tactic
injection term
¶ The injection tactic exploits the property that constructors of inductive types are injective, i.e. that if
c
is a constructor of an inductive type andc t
_{1} andc t
_{2} are equal thent
_{1} andt
_{2} are equal too.If
term
is a proof of a statement of conclusionterm = term
, theninjection
applies the injectivity of constructors as deep as possible to derive the equality of all the subterms ofterm
andterm
at positions where the terms start to differ. For example, from(S p, S n) = (q, S (S m))
we may deriveS p = q
andn = S m
. For this tactic to work, the terms should be typed with an inductive type and they should be neither convertible, nor having a different head constructor. If these conditions are satisfied, the tactic derives the equality of all the subterms at positions where they differ and adds them as antecedents to the conclusion of the current goal.Example
Consider the following goal:
 Inductive list : Set :=  nil : list  cons : nat > list > list.
 list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined
 Parameter P : list > Prop.
 P is declared
 Goal forall l n, P nil > cons n l = cons 0 nil > P l.
 1 goal ============================ forall (l : list) (n : nat), P nil > cons n l = cons 0 nil > P l
 intros.
 1 goal l : list n : nat H : P nil H0 : cons n l = cons 0 nil ============================ P l
 injection H0.
 1 goal l : list n : nat H : P nil H0 : cons n l = cons 0 nil ============================ l = nil > n = 0 > P l
Beware that injection yields an equality in a sigma type whenever the injected object has a dependent type
P
with its two instances in different types(P t
_{1}... t
_{n})
and(P u
_{1}... u
_{n} _{)}. Ift
_{1} andu
_{1} are the same and have for type an inductive type for which a decidable equality has been declared usingScheme
Equality ...
(see Generation of induction principles with Scheme), the use of a sigma type is avoided.Note
If some quantified hypothesis of the goal is named
ident
, theninjection ident
first introduces the hypothesis in the local context usingintros until ident
.
Error
Nothing to do, it is an equality between convertible terms.
¶

Error
Not a primitive equality.
¶

Error
Nothing to inject.
¶ This error is given when one side of the equality is not a constructor.

Variant
injection natural
This does the same thing as
intros until natural
followed byinjection ident
whereident
is the identifier for the last introduced hypothesis.

Variant
injection term with bindings
This does the same as
injection term
but using the given bindings to instantiate parameters or hypotheses ofterm
.

Variant
einjection natural
¶ 
Variant
einjection term with bindings?
¶ This works the same as
injection
but if the type ofterm
, or the type of the hypothesis referred to bynatural
, has uninstantiated parameters, these parameters are left as existential variables.

Variant
injection
If the current goal is of the form
term <> term
, this behaves asintro ident; injection ident
.
Error
goal does not satisfy the expected preconditions.
¶

Error

Variant
injection term with bindings? as simple_intropattern+

Variant
injection natural as simple_intropattern+

Variant
injection as simple_intropattern+

Variant
einjection term with bindings? as simple_intropattern+

Variant
einjection natural as simple_intropattern+

Variant
einjection as simple_intropattern+
These variants apply
intros simple_intropattern+
after the call toinjection
oreinjection
so that all equalities generated are moved in the context of hypotheses. The number ofsimple_intropattern
must not exceed the number of equalities newly generated. If it is smaller, fresh names are automatically generated to adjust the list ofsimple_intropattern
to the number of new equalities. The original equality is erased if it corresponds to a hypothesis.

Variant
injection term with bindings? as injection_intropattern

Variant
injection natural as injection_intropattern

Variant
injection as injection_intropattern

Variant
einjection term with bindings? as injection_intropattern

Variant
einjection natural as injection_intropattern

Variant
einjection as injection_intropattern
These are equivalent to the previous variants but using instead the syntax
injection_intropattern
whichintros
uses. In particularas [= simple_intropattern+]
behaves the same asas simple_intropattern+
.

Tactic
inversion ident
¶ Let the type of
ident
in the local context be(I t)
, whereI
is a (co)inductive predicate. Then,inversion
applied toident
derives for each possible constructorc i
of(I t)
, all the necessary conditions that should hold for the instance(I t)
to be proved byc i
.
Note
If ident
does not denote a hypothesis in the local context but
refers to a hypothesis quantified in the goal, then the latter is
first introduced in the local context using intros until ident
.
Note
As inversion
proofs may be large in size, we recommend the
user to stock the lemmas whenever the same instance needs to be
inverted several times. See Generation of inversion principles with Derive Inversion.
Note
Part of the behavior of the inversion
tactic is to generate
equalities between expressions that appeared in the hypothesis that is
being processed. By default, no equalities are generated if they
relate two proofs (i.e. equalities between term
s whose type is in sort
Prop
). This behavior can be turned off by using the
Keep Proof Equalities
setting.

Variant
inversion natural
This does the same thing as
intros until natural
theninversion ident
whereident
is the identifier for the last introduced hypothesis.

Variant
inversion ident as or_and_intropattern_loc
This generally behaves as inversion but using names in
or_and_intropattern_loc
for naming hypotheses. Theor_and_intropattern_loc
must have the form[p
_{11}... p
_{1n} ...  p
_{m1}... p
_{mn}]
withm
being the number of constructors of the type ofident
. Be careful that the list must be of lengthm
even ifinversion
discards some cases (which is precisely one of its roles): for the discarded cases, just use an empty list (i.e.n = 0
).The arguments of the ith constructor and the equalities thatinversion
introduces in the context of the goal corresponding to the ith constructor, if it exists, get their names from the listp
_{i1}... p
_{in} in order. If there are not enough names,inversion
invents names for the remaining variables to introduce. In case an equation splits into several equations (becauseinversion
appliesinjection
on the equalities it generates), the corresponding namep
_{ij} in the list must be replaced by a sublist of the form[p
_{ij1}... p
_{ijq}]
(or, equivalently,(p
_{ij1}, ..., p
_{ijq})
) whereq
is the number of subequalities obtained from splitting the original equation. Here is an example. Theinversion ... as
variant ofinversion
generally behaves in a slightly more expectable way thaninversion
(no artificial duplication of some hypotheses referring to other hypotheses). To take benefit of these improvements, it is enough to useinversion ... as []
, letting the names being finally chosen by Coq.Example
 Inductive contains0 : list nat > Prop :=  in_hd : forall l, contains0 (0 :: l)  in_tl : forall l b, contains0 l > contains0 (b :: l).
 contains0 is defined contains0_ind is defined contains0_sind is defined
 Goal forall l:list nat, contains0 (1 :: l) > contains0 l.
 1 goal ============================ forall l : list nat, contains0 (1 :: l) > contains0 l
 intros l H; inversion H as [  l' p Hl' [Heqp Heql'] ].
 1 goal l : list nat H : contains0 (1 :: l) l' : list nat p : nat Hl' : contains0 l Heqp : p = 1 Heql' : l' = l ============================ contains0 l

Variant
inversion natural as or_and_intropattern_loc
This allows naming the hypotheses introduced by
inversion natural
in the context.

Variant
inversion_clear ident as or_and_intropattern_loc
This allows naming the hypotheses introduced by
inversion_clear
in the context. Notice that hypothesis names can be provided as ifinversion
were called, even though theinversion_clear
will eventually erase the hypotheses.

Variant
inversion ident in ident+
Let
ident+
be identifiers in the local context. This tactic behaves as generalizingident+
, and then performinginversion
.

Variant
inversion ident as or_and_intropattern_loc in ident+
This allows naming the hypotheses introduced in the context by
inversion ident in ident+
.

Variant
inversion_clear ident in ident+
Let
ident+
be identifiers in the local context. This tactic behaves as generalizingident+
, and then performinginversion_clear
.

Variant
inversion_clear ident as or_and_intropattern_loc in ident+
This allows naming the hypotheses introduced in the context by
inversion_clear ident in ident+
.

Variant
dependent inversion ident
¶ That must be used when
ident
appears in the current goal. It acts likeinversion
and then substitutesident
for the corresponding@term
in the goal.

Variant
dependent inversion ident as or_and_intropattern_loc
This allows naming the hypotheses introduced in the context by
dependent inversion ident
.

Variant
dependent inversion_clear ident
Like
dependent inversion
, except thatident
is cleared from the local context.

Variant
dependent inversion_clear ident as or_and_intropattern_loc
This allows naming the hypotheses introduced in the context by
dependent inversion_clear ident
.

Variant
dependent inversion ident with term
¶ This variant allows you to specify the generalization of the goal. It is useful when the system fails to generalize the goal automatically. If
ident
has type(I t)
andI
has typeforall (x:T), s
, thenterm
must be of typeI:forall (x:T), I x > s'
wheres'
is the type of the goal.

Variant
dependent inversion ident as or_and_intropattern_loc with term
This allows naming the hypotheses introduced in the context by
dependent inversion ident with term
.

Variant
dependent inversion_clear ident with term
Like
dependent inversion … with …
with but clearsident
from the local context.

Variant
dependent inversion_clear ident as or_and_intropattern_loc with term
This allows naming the hypotheses introduced in the context by
dependent inversion_clear ident with term
.

Variant
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
does.

Variant
simple inversion ident as or_and_intropattern_loc
This allows naming the hypotheses introduced in the context by
simple inversion
.

Tactic
inversion ident using ident
¶ Let
ident
have type(I t)
(I
an inductive predicate) in the local context, andident
be a (dependent) inversion lemma. Then, this tactic refines the current goal with the specified lemma.

Variant
inversion ident using ident in ident+
This tactic behaves as generalizing
ident+
, then doinginversion ident using ident
.

Variant
inversion_sigma
¶ This tactic turns equalities of dependent pairs (e.g.,
existT P x p = existT P y q
, frequently left over by inversion on a dependent type family) into pairs of equalities (e.g., a hypothesisH : x = y
and a hypothesis of typerew H in p = q
); these hypotheses can subsequently be simplified usingsubst
, without ever invoking any kind of axiom asserting uniqueness of identity proofs. If you want to explicitly specify the hypothesis to be inverted, or name the generated hypotheses, you can invokeinduction H as [H1 H2] using eq_sigT_rect.
This tactic also works forsig
,sigT2
, andsig2
, and there are similareq_sig
***_rect
induction lemmas.
Example
Nondependent inversion.
Let us consider the relation Le
over natural numbers:
 Inductive Le : nat > nat > Set :=  LeO : forall n:nat, Le 0 n  LeS : forall n m:nat, Le n m > Le (S n) (S m).
 Le is defined Le_rect is defined Le_ind is defined Le_rec is defined Le_sind is defined
Let us consider the following goal:
 Section Section.
 Variable P : nat > nat > Prop.
 P is declared
 Variable Q : forall n m:nat, Le n m > Prop.
 Q is declared
 Goal forall n m, Le (S n) m > P n m.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop ============================ forall n m : nat, Le (S n) m > P n m
 intros.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m : nat H : Le (S n) m ============================ P n m
To prove the goal, we may need to reason by cases on H
and to derive
that m
is necessarily of the form (S m0)
for certain m0
and that
(Le n m0)
. Deriving these conditions corresponds to proving that the only
possible constructor of (Le (S n) m)
is LeS
and that we can invert
the arrow in the type of LeS
. This inversion is possible because Le
is the smallest set closed by the constructors LeO
and LeS
.
 inversion_clear H.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m, m0 : nat H0 : Le n m0 ============================ P n (S m0)
Note that m
has been substituted in the goal for (S m0)
and that the
hypothesis (Le n m0)
has been added to the context.
Sometimes it is interesting to have the equality m = (S m0)
in the
context to use it after. In that case we can use inversion
that does
not clear the equalities:
 intros.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m : nat H : Le (S n) m ============================ P n m
 inversion H.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m : nat H : Le (S n) m n0, m0 : nat H1 : Le n m0 H0 : n0 = n H2 : S m0 = m ============================ P n (S m0)
Example
Dependent inversion.
Let us consider the following goal:
 Abort.
 Goal forall n m (H:Le (S n) m), Q (S n) m H.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop ============================ forall (n m : nat) (H : Le (S n) m), Q (S n) m H
 intros.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m : nat H : Le (S n) m ============================ Q (S n) m H
As H
occurs in the goal, we may want to reason by cases on its
structure and so, we would like inversion tactics to substitute H
by
the corresponding @term in constructor form. Neither inversion
nor
inversion_clear
do such a substitution. To have such a behavior we
use the dependent inversion tactics:
 dependent inversion_clear H.
 1 goal P : nat > nat > Prop Q : forall n m : nat, Le n m > Prop n, m, m0 : nat l : Le n m0 ============================ Q (S n) (S m0) (LeS n m0 l)
Note that H
has been substituted by (LeS n m0 l)
and m
by (S m0)
.
Example
Using inversion_sigma.
Let us consider the following inductive type of lengthindexed lists, and a lemma about inverting equality of cons:
 Require Import Coq.Logic.Eqdep_dec.
 Inductive vec A : nat > Type :=  nil : vec A O  cons {n} (x : A) (xs : vec A n) : vec A (S n).
 vec is defined vec_rect is defined vec_ind is defined vec_rec is defined vec_sind is defined
 Lemma invert_cons : forall A n x xs y ys, @cons A n x xs = @cons A n y ys > xs = ys.
 1 goal ============================ forall (A : Type) (n : nat) (x : A) (xs : vec A n) (y : A) (ys : vec A n), cons A x xs = cons A y ys > xs = ys
 Proof.
 intros A n x xs y ys H.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys ============================ xs = ys
After performing inversion, we are left with an equality of existTs:
 inversion H.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H2 : existT (fun n : nat => vec A n) n xs = existT (fun n : nat => vec A n) n ys ============================ xs = ys
We can turn this equality into a usable form with inversion_sigma:
 inversion_sigma.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H0 : n = n H3 : eq_rect n (fun a : nat => vec A a) xs n H0 = ys ============================ xs = ys
To finish cleaning up the proof, we will need to use the fact that that all proofs of n = n for n a nat are eq_refl:
 let H := match goal with H : n = n  _ => H end in pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H3 : eq_rect n (fun a : nat => vec A a) xs n eq_refl = ys ============================ xs = ys
 simpl in *.
 1 goal A : Type n : nat x : A xs : vec A n y : A ys : vec A n H : cons A x xs = cons A y ys H1 : x = y H3 : xs = ys ============================ xs = ys
Finally, we can finish the proof:
 assumption.
 No more goals.
 Qed.
See also

Tactic
fix ident natural
¶ This tactic is a primitive tactic to start a proof by induction. In general, it is easier to rely on higherlevel induction tactics such as the ones described in
induction
.In the syntax of the tactic, the identifier
ident
is the name given to the induction hypothesis. The natural numbernatural
tells on which premise of the current goal the induction acts, starting from 1, counting both dependent and non dependent products, but skipping local definitions. Especially, the current lemma must be composed of at leastnatural
products.Like in a fix expression, the induction hypotheses have to be used on structurally smaller arguments. The verification that inductive proof arguments are correct is done only at the time of registering the lemma in the global environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the command
Guarded
(see Section Requesting information).

Variant
fix ident natural with (ident binder+ [{struct ident}] : type)+
This starts a proof by mutual induction. The statements to be simultaneously proved are respectively
forall binder ... binder, type
. The identifiersident
are the names of the induction hypotheses. The identifiersident
are the respective names of the premises on which the induction is performed in the statements to be simultaneously proved (if not given, the system tries to guess itself what they are).

Tactic
cofix ident
¶ This tactic starts a proof by coinduction. The identifier
ident
is the name given to the coinduction hypothesis. Like in a cofix expression, the use of induction hypotheses have to guarded by a constructor. The verification that the use of coinductive hypotheses is correct is done only at the time of registering the lemma in the global environment. To know if the use of coinduction hypotheses is correct at some time of the interactive development of a proof, use the commandGuarded
(see Section Requesting information).
Checking properties of terms¶
Each of the following tactics acts as the identity if the check succeeds, and results in an error otherwise.

Tactic
constr_eq term term
¶ This tactic checks whether its arguments are equal modulo alpha conversion, casts and universe constraints. It may unify universes.

Error
Not equal.
¶

Error
Not equal (due to universes).
¶

Tactic
constr_eq_strict term term
¶ This tactic checks whether its arguments are equal modulo alpha conversion, casts and universe constraints. It does not add new constraints.

Error
Not equal.
¶

Error
Not equal (due to universes).
¶

Tactic
unify term term
¶ This tactic checks whether its arguments are unifiable, potentially instantiating existential variables.

Variant
unify term term with ident
Unification takes the transparency information defined in the hint database
ident
into account (see the hints databases for auto and eauto).

Tactic
is_evar term
¶ This tactic checks whether its argument is a current existential variable. Existential variables are uninstantiated variables generated by
eapply
and some other tactics.

Error
Not an evar.
¶

Tactic
has_evar term
¶ This tactic checks whether its argument has an existential variable as a subterm. Unlike context patterns combined with
is_evar
, this tactic scans all subterms, including those under binders.

Error
No evars.
¶

Tactic
is_var term
¶ This tactic checks whether its argument is a variable or hypothesis in the current local context.

Error
Not a variable or hypothesis.
¶
Equality¶

Tactic
f_equal
¶ This tactic applies to a goal of the form
f a
_{1}... a
_{n}= f′a′
_{1}... a′
_{n}. Usingf_equal
on such a goal leads to subgoalsf=f′
anda
_{1} =a′
_{1} and so on up toa
_{n}= a′
_{n}. Amongst these subgoals, the simple ones (e.g. provable byreflexivity
orcongruence
) are automatically solved byf_equal
.

Tactic
reflexivity
¶ This tactic applies to a goal that has the form
t=u
. It checks thatt
andu
are convertible and then solves the goal. It is equivalent toapply refl_equal
.
Error
The conclusion is not a substitutive equation.
¶

Error
Unable to unify ... with ...
¶

Error

Tactic
symmetry
¶ This tactic applies to a goal that has the form
t=u
and changes it intou=t
.

Variant
symmetry in ident
If the statement of the hypothesis ident has the form
t=u
, the tactic changes it tou=t
.
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 =
.

Tactic
decide equality
¶ This tactic solves a goal of the form
forall x y : R, {x = y} + {~ x = y}
, whereR
is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types. It solves goals of the form{x = y} + {~ x = y}
as well.

Tactic
compare term term
¶ This tactic compares two given objects
term
andterm
of an inductive datatype. IfG
is the current goal, it leaves the sub goalsterm =term > G
and~ term = term > G
. The type ofterm
andterm
must satisfy the same restrictions as in the tacticdecide equality
.

Tactic
simplify_eq term
¶ Let
term
be the proof of a statement of conclusionterm = term
. Ifterm
andterm
are structurally different (in the sense described for the tacticdiscriminate
), then the tacticsimplify_eq
behaves asdiscriminate term
, otherwise it behaves asinjection term
.
Note
If some quantified hypothesis of the goal is named ident
,
then simplify_eq ident
first introduces the hypothesis in the local
context using intros until ident
.

Variant
simplify_eq natural
This does the same thing as
intros until natural
thensimplify_eq ident
whereident
is the identifier for the last introduced hypothesis.

Variant
simplify_eq term with bindings
This does the same as
simplify_eq term
but using the given bindings to instantiate parameters or hypotheses ofterm
.

Variant
esimplify_eq natural
¶ 
Variant
esimplify_eq term with bindings?
¶ This works the same as
simplify_eq
but if the type ofterm
, or the type of the hypothesis referred to bynatural
, has uninstantiated parameters, these parameters are left as existential variables.

Variant
simplify_eq
If the current goal has form
t1 <> t2
, it behaves asintro ident; simplify_eq ident
.

Tactic
dependent rewrite > ident
¶ This tactic applies to any goal. If
ident
has type(existT B a b)=(existT B a' b')
in the local context (i.e. eachterm
of the equality has a sigma type{ a:A & (B a)}
) this tactic rewritesa
intoa'
andb
intob'
in the current goal. This tactic works even ifB
is also a sigma type. This kind of equalities between dependent pairs may be derived by theinjection
andinversion
tactics.

Variant
dependent rewrite < ident
¶ Analogous to
dependent rewrite >
but uses the equality from right to left.
Classical tactics¶
In order to ease the proving process, when the Classical
module is
loaded, a few more tactics are available. Make sure to load the module
using the Require Import
command.

Tactic
classical_left
¶ 
Tactic
classical_right
¶ These tactics are the analog of
left
andright
but using classical logic. They can only be used for disjunctions. Useclassical_left
to prove the left part of the disjunction with the assumption that the negation of right part holds. Useclassical_right
to prove the right part of the disjunction with the assumption that the negation of left part holds.
Delaying solving unification constraints¶

Tactic
solve_constraints
¶

Flag
Solve Unification Constraints
¶ By default, after each tactic application, postponed typechecking unification problems are resolved using heuristics. Unsetting this flag disables this behavior, allowing tactics to leave unification constraints unsolved. Use the
solve_constraints
tactic at any point to solve the constraints.
Proof maintenance¶
Experimental. Many tactics, such as intros
, can automatically generate names, such
as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps
may explicitly refer to these names. However, future versions of Coq may not assign
names exactly the same way, which could cause the proof to fail because the
new names don't match the explicit references in the proof.
The following "Mangle Names" settings let users find all the places where proofs rely on automatically generated names, which can then be named explicitly to avoid any incompatibility. These settings cause Coq to generate different names, producing errors for references to automatically generated names.

Flag
Mangle Names
¶ When set, generated names use the prefix specified in the following option instead of the default prefix.
Performanceoriented tactic variants¶

Tactic
exact_no_check term
¶ For advanced usage. Similar to
exact
term
, but as an optimization, it skips checking thatterm
has the goal's type, relying on the kernel check instead. Seechange_no_check
for more explanation.Example
 Goal False.
 1 goal ============================ False
 exact_no_check I.
 No more goals.
 Fail Qed.
 The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False".

Variant
vm_cast_no_check term
¶ For advanced usage. Similar to
exact_no_check
term
, but additionally instructs the kernel to usevm_compute
to compare the goal's type with theterm
's type.Example
 Goal False.
 1 goal ============================ False
 vm_cast_no_check I.
 No more goals.
 Fail Qed.
 The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False".

Variant
native_cast_no_check term
¶ for advanced usage. similar to
exact_no_check
term
, but additionally instructs the kernel to usenative_compute
to compare the goal's type with theterm
's type.Example
 Goal False.
 1 goal ============================ False
 native_cast_no_check I.
 No more goals.
 Fail Qed.
 The command has indeed failed with message: Native compiler is disabled, falling back to VM conversion test. [nativecompilerdisabled,nativecompiler]