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 nondependent 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
.
::=
*

**

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

_

or_and_intropattern

equality_intropattern
naming_intropattern::=
ident

?

?ident
or_and_intropattern::=
[ intropattern** ]

( simple_intropattern*, )

( simple_intropattern & simple_intropattern+& )
equality_intropattern::=
>

<

[= intropattern* ]
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
, while
intros
and eintros
use intropattern*
.
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 generate a fresh 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*+ ]
— splits an inductive type that has multiple constructors such asA \/ B
into multiple subgoals. The number ofintropattern
s 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
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
,move … before …
,move … at top
, ormove … at bottom
.Note
intro at bottom
is a synonym forintro
with no argument.

Error

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

Tactic
eintros intropattern*
¶ 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
, 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
.
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.
¶
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 this flag is set (it is off by default), generated names use the prefix specified in the following option instead of the default prefix.

Flag
Mangle Names Light
¶ When this flag is set (it is off by default), the names generated by
Mangle Names
only add theMangle Names Prefix
to the original name.
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]