Tactics¶
A deduction rule is a link between some (unique) formula, that we call the conclusion and (several) formulas that we call the premises. A deduction rule can be read in two ways. The first one says: “if I know this and this then I can deduce this”. For instance, if I have a proof of A and a proof of B then I have a proof of A ∧ B. This is forward reasoning from premises to conclusion. The other way says: “to prove this I have to prove this and this”. For instance, to prove A ∧ B, I have to prove A and I have to prove B. This is backward reasoning from conclusion to premises. We say that the conclusion is the goal to prove and premises are the subgoals. The tactics implement backward reasoning. When applied to a goal, a tactic replaces this goal with the subgoals it generates. We say that a tactic reduces a goal to its subgoal(s).
Each (sub)goal is denoted with a number. The current goal is numbered 1. By default, a tactic is applied to the current goal, but one can address a particular goal in the list by writing n:tactic which means “apply tactic tactic to goal number n”. We can show the list of subgoals by typing Show (see Section Requesting information).
Since not every rule applies to a given statement, not every tactic can be used to reduce a given goal. In other words, before applying a tactic to a given goal, the system checks that some preconditions are satisfied. If it is not the case, the tactic raises an error message.
Tactics are built from atomic tactics and tactic expressions (which extends the folklore notion of tactical) to combine those atomic tactics. This chapter is devoted to atomic tactics. The tactic language will be described in Chapter Ltac.
Common elements of tactics¶
Invocation of tactics¶
A tactic is applied as an ordinary command. It may be preceded by a goal selector (see Section Semantics). If no selector is specified, the default selector is used.
tactic_invocation ::=toplevel_selector
:tactic
.tactic
.
-
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 more selectors are available, only
all
,!
or a single natural number are valid default goal selectors.
Bindings list¶
Tactics that take a term as an argument may also support a bindings list
to instantiate some parameters of the term by name or position.
The general form of a term with a bindings list is
term with bindings_list
where bindings_list
can take two different forms:
In a bindings list of the form
(ref:= term)+
,ref
is either anident
or anum
. The references are determined according to the type ofterm
. Ifref
is an identifier, this identifier has to be bound in the type ofterm
and the binding provides the tactic with an instance for the parameter of this name. Ifref
is a numbern
, it refers to then
-th non dependent premise of theterm
, as determined by the type ofterm
.-
Error
No such binder.
¶
-
Error
A bindings list can also be a simple list of terms
term*
. In that case the references to which these terms correspond are determined by the tactic. In case ofinduction
,destruct
,elim
andcase
, the terms have to provide instances for all the dependent products in the type of term while in the case ofapply
, or ofconstructor
and its variants, only instances for the dependent products that are not bound in the conclusion of the type 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_list ::=intropattern
...intropattern
empty
empty ::= intropattern ::= * **simple_intropattern
simple_intropattern ::=simple_intropattern_closed
[ %term
... %term
] simple_intropattern_closed ::=naming_intropattern
_or_and_intropattern
rewriting_intropattern
injection_intropattern
naming_intropattern ::=ident
? ?ident
or_and_intropattern ::= [intropattern_list
| ... |intropattern_list
] (simple_intropattern
, ... ,simple_intropattern
) (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?ident
— generate a name that begins withident
_
— 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[H1|H2]
. The first subgoal will have the hypothesisH1: A
and the second subgoal will have the hypothesisH2: B
. Example - split a hypothesis in either of the forms
A /\ B
orA \/ B
using the pattern[]
.
Patterns can be nested: [[Ha|Hb] 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 oflet-ins
, the patterns are applied to the arguments andlet-in
variables.( simple_intropattern+& )
— matches a right-hand nested term that consists of one or more nested binary inductive types such asa1 OP1 a2 OP2 ...
(where theOPn
are right-associative). (If theOPn
are left-associative, additional parentheses will be needed to make the term right-hand 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 right-hand side of the hypothesis with the left-hand side of the hypothesis in the conclusion of the goal; the hypothesis is cleared; if the left-hand 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 left-hand side of the hypothesis with the right-hand 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
-
Flag
Bracketing Last Introduction Pattern
¶ For
intros intropattern_list
, controls how to handle a conjunctive pattern that doesn't give enough simple patterns to match all the arguments in the constructor. If set (the default), Coq generates additional names to match the number of arguments. Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more similar to SSReflect's intro patterns.Deprecated since version 8.10.
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 subgoal ============================ forall A B : Prop, A /\ B -> True
- intros.
- 1 subgoal A, B : Prop H : A /\ B ============================ True
- destruct H as (HA & HB).
- 1 subgoal A, B : Prop HA : A HB : B ============================ True
Example: intro pattern for \/
- Goal forall (A: Prop) (B: Prop), (A \/ B) -> True.
- 1 subgoal ============================ forall A B : Prop, A \/ B -> True
- intros.
- 1 subgoal A, B : Prop H : A \/ B ============================ True
- destruct H as [HA|HB].
- 2 subgoals A, B : Prop HA : A ============================ True subgoal 2 is: True
- all: swap 1 2.
- 2 subgoals A, B : Prop HB : B ============================ True subgoal 2 is: True
Example: -> intro pattern
- Goal forall (x:nat) (y:nat) (z:nat), (x = y) -> (y = z) -> (x = z).
- 1 subgoal ============================ forall x y z : nat, x = y -> y = z -> x = z
- intros * H.
- 1 subgoal x, y, z : nat H : x = y ============================ y = z -> x = z
- intros ->.
- 1 subgoal 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 subgoal ============================ forall n m : nat, S n = S m -> 1 = 2 -> False
- intros *.
- 1 subgoal n, m : nat ============================ S n = S m -> 1 = 2 -> False
- intros [= H].
- 1 subgoal n, m : nat H : n = m ============================ 1 = 2 -> False
- intros [=].
- No more subgoals.
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 subgoal ============================ A /\ (exists x : nat, B x /\ C) -> True
- intros (a & x & b & c).
- 1 subgoal a : A x : nat b : B x c : C ============================ True
Example: * intro pattern
- Goal forall (A: Prop) (B: Prop), A -> B.
- 1 subgoal ============================ forall A B : Prop, A -> B
- intros *.
- 1 subgoal A, B : Prop ============================ A -> B
Example: ** pattern ("intros **" is equivalent to "intros")
- Goal forall (A: Prop) (B: Prop), A -> B.
- 1 subgoal ============================ forall A B : Prop, A -> B
- intros **.
- 1 subgoal A, B : Prop H : A ============================ B
Example: compound intro pattern
- Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
- 1 subgoal ============================ forall A B C : Prop, A \/ B /\ C -> (A -> C) -> C
- intros * [a | (_,c)] f.
- 2 subgoals A, B, C : Prop a : A f : A -> C ============================ C subgoal 2 is: C
- all: swap 1 2.
- 2 subgoals A, B, C : Prop c : C f : A -> C ============================ C subgoal 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 subgoal A : Type xs, ys : list A ============================ S (length ys) = 1 -> xs ++ ys = xs
- intros [=->%length_zero_iff_nil].
- 1 subgoal 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 coq-tricks
Occurrence sets and occurrence clauses¶
An occurrence clause is a modifier to some tactics that obeys the following syntax:
occurrence_clause ::= ingoal_occurrences
goal_occurrences ::= [ident
[at_occurrences
], ... ,ident
[at_occurrences
] [|- [* [at_occurrences
]]]] * |- [* [at_occurrences
]] * at_occurrences ::= atoccurrences
occurrences ::= [-]num
...num
The role of an occurrence clause is to select a set of occurrences of a term
in a goal. In the first case, the ident at num*?
parts indicate
that occurrences have to be selected in the hypotheses named ident
.
If no numbers are given for hypothesis ident
, then all the
occurrences of term
in the hypothesis are selected. If numbers are
given, they refer to occurrences of term
when the term is printed
using the Printing All
flag, counting from left to right. In particular,
occurrences of term
in implicit arguments
(see Implicit arguments) or coercions (see Coercions) are
counted.
If a minus sign is given between at
and the list of occurrences, it
negates the condition so that the clause denotes all the occurrences
except the ones explicitly mentioned after the minus sign.
As an exception to the left-to-right order, the occurrences in the return subexpression of a match are considered before the occurrences in the matched term.
In the second case, the *
on the left of |-
means that all occurrences
of term are selected in every hypothesis.
In the first and second case, if *
is mentioned on the right of |-
, the
occurrences of the conclusion of the goal have to be selected. If some numbers
are given, then only the occurrences denoted by these numbers are selected. If
no numbers are given, all occurrences of term
in the goal are selected.
Finally, the last notation is an abbreviation for * |- *
. Note also
that |-
is optional in the first case when no *
is given.
Here are some tactics that understand occurrence clauses: set
,
remember
, induction
, destruct
.
Applying theorems¶
-
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
-
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
-
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 holes in the 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
. This low-level 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 subgoal ============================ forall x : Option, x <> Fail -> bool
- refine (fun x:Option => match x return x <> Fail -> bool with | Fail => _ | Ok b => fun _ => b end).
- 1 subgoal x : Option ============================ Fail <> Fail -> bool
- intros; absurd (Fail = Fail); trivial.
- No more subgoals.
- Defined.
-
Error
Refine passed ill-formed term.
¶ The term you gave is not a valid proof (not easy to debug in general). This message may also occur in higher-level 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 beta-reduction 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
simple refine
except it performs type checking without resolution of typeclasses.
-
apply term
¶ This tactic applies to any goal. The argument term is a term well-formed 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 non-dependent 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 left-to-right order.The tactic
apply
relies on first-order unification with dependent types unless the conclusion of the type ofterm
is of the formP (t1 ... tn)
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) u1 ... un
and theti
andui
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) u1 ... un
.-
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_list
This also provides apply with values for instantiating premises. Here, variables are referred by names and non-dependent products by increasing numbers (see bindings list).
-
Variant
apply term+,
This is a shortcut for
apply term1; [.. | ... ; [ .. | apply termn] ... ]
, i.e. for the successive applications ofterm
i+1 on the last subgoal generated byapply termi
, starting from the application ofterm1
.
-
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
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 y, id y = y.
- H is declared
- Goal O = O.
- 1 subgoal ============================ 0 = 0
- Fail simple apply H.
- The command has indeed failed with message: Unable to unify "id ?M160 = ?M160" with "0 = 0".
Because it reasons modulo a limited amount of conversion,
simple apply
fails quicker thanapply
and it is then well-suited for uses in user-defined tactics that backtrack often. Moreover, it does not traverse tuples asapply
does.
-
Variant
simple? apply term with bindings_list?+,
¶ -
Variant
simple? eapply term with bindings_list?+,
¶ 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 well-formed in the current context, its type being reducible to a non-dependent 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 subgoal ============================ 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 6-12: > 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 subgoals ============================ R n m subgoal 2 is: R m p
Note that n
can be inferred from the goal, so the following would work
too.
- apply (Rtrans _ m).
- 2 subgoals ============================ R n m subgoal 2 is: R m p
More elegantly, apply Rtrans with (y:=m)
allows only mentioning the
unknown m:
- apply Rtrans with (y := m).
- 2 subgoals ============================ R n m subgoal 2 is: R m p
Another solution is to mention the proof of (R x y)
in Rtrans
- apply Rtrans with (1 := Rnm).
- 1 subgoal ============================ R m p
... or the proof of (R y z)
.
- apply Rtrans with (2 := Rmp).
- 1 subgoal ============================ 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 subgoals (shelved: 1) ============================ R n ?y subgoal 2 is: R ?y p
- apply Rnm.
- 1 subgoal ============================ R m p
- apply Rmp.
- No more subgoals.
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
).
-
apply term in ident
¶ This tactic applies to any goal. The argument
term
is a term well-formed 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 non-dependent 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 non-dependent premises in the type ofterm
and of the non-dependent 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 non-dependent premise matches the conclusion of the type ofident
. Tuples are decomposed in a width-first left-to-right 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 first-order pattern matching with dependent types.-
Error
Statement without assumptions.
¶ This happens if the type of
term
has no non-dependent premise.
-
Error
Unable to apply.
¶ This happens if the conclusion of
ident
does not match any of the non-dependent premises of the type ofterm
.
-
Variant
apply term with bindings_list+, in ident
This does the same but uses the bindings in each
(ident := term)
to instantiate the parameters of the corresponding type ofterm
(see bindings list).
-
Variant
eapply term with bindings_list?+, in ident
This works as
apply ... in
but turns unresolved bindings into existential variables, if any, instead of failing.
-
Variant
apply term with bindings_list?+, in ident as simple_intropattern
¶ This works as
apply ... in
then applies thesimple_intropattern
to the hypothesisident
.
-
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. For instance, ifid := fun x:nat => x
andH: forall y, id y = y -> True
andH0 : O = O
thensimple apply H in H0
does not succeed because it would require the conversion ofid ?x
andO
where?x
is an existential variable to instantiate. Tacticsimple apply term in ident
does not either traverse tuples asapply term in ident
does.
-
Variant
simple? apply term with bindings_list?+, in ident as simple_intropattern?
-
Variant
simple? eapply term with bindings_list?+, in ident as simple_intropattern?
This summarizes the different syntactic variants of
apply term in ident
andeapply term in ident
.
-
Error
-
constructor num
¶ This tactic applies to a goal such that its conclusion is an inductive type (say
I
). The argumentnum
must be less or equal to the numbers of constructor(s) ofI
. Letci
be the i-th constructor ofI
, thenconstructor i
is equivalent tointros; apply ci
.-
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 num with bindings_list
Let
c
be the i-th constructor ofI
, thenconstructor i with bindings_list
is equivalent tointros; apply c with bindings_list
.Warning
The terms in the
bindings_list
are checked in the context where constructor is executed and not in the context whereapply
is executed (the introductions are not taken into account).
-
Variant
split with bindings_list?
¶ This applies only if
I
has a single constructor. It is then equivalent toconstructor 1 with bindings_list?
. It is typically used in the case of a conjunction \(A \wedge B\).-
Variant
exists bindings_list
¶ This applies only if
I
has a single constructor. It is then equivalent tointros; constructor 1 with bindings_list.
It is typically used in the case of an existential quantification \(\exists x, P(x).\)
-
Variant
exists bindings_list+,
This iteratively applies
exists bindings_list
.
-
Error
Not an inductive goal with 1 constructor.
¶
-
Variant
-
Variant
left with bindings_list?
¶ -
Variant
right with bindings_list?
¶ 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_list?
andconstructor 2 with bindings_list?
.-
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
Managing the local context¶
-
intro
¶ This tactic applies to a goal that is either a product or starts with a let-binder. If the goal is a product, the tactic implements the "Lam" rule given in Typing rules [1]. If the goal starts with a let-binder, then the tactic implements a mix of the "Let" and "Conv".
If the current goal is a dependent product
forall x:T, U
(resplet x:=t in U
) thenintro
putsx:T
(respx:=t
) in the local context. The new subgoal isU
.If the goal is a non-dependent 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 head-reducible.-
Error
No product even after head-reduction.
¶
-
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 names).
-
Variant
intros
¶ This repeats
intro
until it meets the head-constant. It never reduces head-constants 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 num
This repeats
intro
until thenum
-th non-dependent 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 non-dependent 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 non-dependent product:forall x y : nat, nat -> x = y -> y = x
.-
Error
No such hypothesis in current goal.
This happens when
num
is 0 or is greater than the number of non-dependent products of the goal.
-
Error
-
Variant
intro ident1? after ident2
-
Variant
intro ident1? before ident2
-
Variant
intro ident1? at top
-
Variant
intro ident1? at bottom
These tactics apply
intro ident1?
and move the freshly introduced hypothesis respectively after the hypothesisident2
, before the hypothesisident2
, 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 ident1?
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
-
intros intropattern_list
¶ Introduces one or more variables or hypotheses from the goal by matching the intro patterns. See the description in Intro patterns.
-
eintros intropattern_list
¶ Works just like
intros ...
except that it creates existential variables for any unresolved variables rather than failing.
-
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
-
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
-
move ident1 after ident2
¶ This moves the hypothesis named
ident1
in the local context after the hypothesis namedident2
, where “after” is in reference to the direction of the move. The proof term is not changed.If
ident1
comes beforeident2
in the order of dependencies, then all the hypotheses betweenident1
andident2
that (possibly indirectly) depend onident1
are moved too, and all of them are thus moved afterident2
in the order of dependencies.If
ident1
comes afterident2
in the order of dependencies, then all the hypotheses betweenident1
andident2
that (possibly indirectly) occur in the type ofident1
are moved too, and all of them are thus moved beforeident2
in the order of dependencies.-
Variant
move ident1 before ident2
¶ This moves
ident1
towards and just before the hypothesis namedident2
. As formove ... after ...
, dependencies overident1
(whenident1
comes beforeident2
in the order of dependencies) or in the type ofident1
(whenident1
comes afterident2
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 subgoal ============================ forall x : nat, x = 0 -> nat -> forall y : nat, y = y -> 0 = x
- intros x H z y H0.
- 1 subgoal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
- move x after H0.
- 1 subgoal z, y : nat H0 : y = y x : nat H : x = 0 ============================ 0 = x
- Undo.
- 1 subgoal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
- move x before H0.
- 1 subgoal z, y, x : nat H : x = 0 H0 : y = y ============================ 0 = x
- Undo.
- 1 subgoal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
- move H0 after H.
- 1 subgoal x, y : nat H0 : y = y H : x = 0 z : nat ============================ 0 = x
- Undo.
- 1 subgoal x : nat H : x = 0 z, y : nat H0 : y = y ============================ 0 = x
- move H0 before H.
- 1 subgoal x : nat H : x = 0 y : nat H0 : y = y z : nat ============================ 0 = x
-
Variant
-
rename ident1 into ident2
¶ This renames hypothesis
ident1
intoident2
in the current context. The name of the hypothesis in the proof-term, however, is left unchanged.-
Variant
rename identi into identj+,
This renames the variables
identi
intoidentj
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.
-
Error
ident is already used.
-
Variant
-
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 binders := term) in goal_occurrences?
This is equivalent to
set (ident := fun binders => 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 binders? := 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
-
remember term as ident1 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 ident1 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 ident1 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
-
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 |-
.
-
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 subgoal ============================ forall A B C : Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C
- intros A B C H; decompose [and or] H.
- 3 subgoals A, B, C : Prop H : A /\ B /\ C \/ B /\ C \/ C /\ A H1 : A H0 : B H3 : C ============================ C subgoal 2 is: C subgoal 3 is: C
- all: assumption.
- No more subgoals.
- Qed.
Note
decompose
does not work on right-hand sides of implications or products.-
Variant
decompose sum term
This decomposes sum types (like
or
).
Controlling the proof flow¶
-
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
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 non-dependent 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_list as simple_intropattern?
This tactic works on local hypothesis
ident
. The premises of this hypothesis (either universal quantifications or non-dependent implications) are instantiated by concrete terms coming either from argumentsterm*
or from a bindings list. 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.
-
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 subgoal ============================ forall x y : nat, 0 <= x + y + y
- Proof.
- intros *.
- 1 subgoal x, y : nat ============================ 0 <= x + y + y
- Show.
- 1 subgoal x, y : nat ============================ 0 <= x + y + y
- generalize (x + y + y).
- 1 subgoal 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 num+
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 num+ 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.
-
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.
-
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 (num := term)
This variant allows to refer to an existential variable which was not named by the user. The
num
argument is the position of the existential variable from right to left in the goal. Because this variant is not robust to slight changes in the goal, its use is strongly discouraged.
-
Variant
instantiate ( num := term ) in ident
-
Variant
instantiate ( num := term ) in ( value of ident )
-
Variant
instantiate ( num := 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.
-
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.
-
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
.
-
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.
-
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
-
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
-
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 co-inductive objects (see Inductive Definitions).
-
destruct term
¶ This tactic applies to any goal. The argument
term
must be of inductive or co-inductive type and the tactic generates subgoals, one for each possible form ofterm
, i.e. one for each constructor of the inductive or co-inductive 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 num
Note
For destruction of a numeral, use syntax
destruct (num)
(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_list
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_list?
This is synonym of
induction term using term with bindings_list?
.
-
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_list? as or_and_intropattern_loc? eqn:naming_intropattern? using term with bindings_list?? in goal_occurrences?
-
Variant
edestruct term with bindings_list? as or_and_intropattern_loc? eqn:naming_intropattern? using term with bindings_list?? in goal_occurrences?
These are the general forms of
destruct
andedestruct
. They combine the effects of thewith
,as
,eqn:
,using
, andin
clauses.
-
Variant
-
case term
¶ The tactic
case
is a more basic tactic to perform case analysis without recursion. It behaves aselim term
but using a case-analysis elimination principle and not a recursive one.
-
Variant
case term with bindings_list
Analogous to
elim term with bindings_list
above.
-
Variant
ecase term with bindings_list?
¶ In case the type of
term
has dependent premises, or dependent premises whose values are not inferable from thewith bindings_list
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 num
This tactic behaves as
intros until num; case ident
whereident
is the name given byintros until num
to thenum
-th non-dependent 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.
-
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 anum
, theninduction num
behaves asintros until num
followed byinduction
applied to the last introduced hypothesis.Note
For simple induction on a numeral, use syntax induction (num) (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 subgoal ============================ forall n : nat, n = n -> n <= n
- intros n H.
- 1 subgoal n : nat H : n = n ============================ n <= n
- induction n.
- 2 subgoals H : 0 = 0 ============================ 0 <= 0 subgoal 2 is: 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 i-th 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_list
This behaves like
induction
providing explicit instances for the premises of the type ofterm
(see bindings list).
-
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_list
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 subgoal x, y : nat ============================ x + y = y + x
- induction y in x |- *.
- 2 subgoals x : nat ============================ x + 0 = 0 + x subgoal 2 is: x + S y = S y + x
- Show 2.
- subgoal 2 is: x, y : nat IHy : forall x : nat, x + y = y + x ============================ x + S y = S y + x
-
Variant
induction term with bindings_list as or_and_intropattern_loc using term with bindings_list in goal_occurrences
-
Variant
einduction term with bindings_list as or_and_intropattern_loc using term with bindings_list 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 proof 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 non-dependent 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_list
¶ Allows to give explicit instances to the premises of the type of
term
(see bindings list).
-
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_list
Allows the user to give explicitly an induction principle
term
that is not the standard one for the underlying inductive type ofterm
. Thebindings_list
clause allows instantiating premises of the type ofterm
.
-
Variant
elim term with bindings_list using term with bindings_list
-
Variant
eelim term with bindings_list using term with bindings_list
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 num
This tactic behaves as
intros until num; elim ident
whereident
is the name given byintros until num
to thenum
-th non-dependent premise of the goal.
-
double induction ident ident
¶ This tactic is deprecated and should be replaced by
induction ident; induction ident
(orinduction ident ; destruct ident
depending on the exact needs).
-
Variant
double induction num1 num2
This tactic is deprecated and should be replaced by
induction num1; induction num3
wherenum3
is the result ofnum2 - num1
-
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 subgoal ============================ forall n : nat, n < 1 -> n = 0
- intros n H ; induction H.
- 2 subgoals n : nat ============================ n = 0 subgoal 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 subgoal ============================ forall n : nat, n < 1 -> n = 0
- intros n H ; dependent induction H.
- 2 subgoals ============================ 0 = 0 subgoal 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 subgoal 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 subgoals.
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.
-
function induction (qualid term+)
¶ The tactic functional induction performs case analysis and induction following the definition of a function. It makes use of a principle generated by
Function
(see Advanced recursive functions) orFunctional Scheme
(see Generation of induction principles with Functional Scheme). Note that this tactic is only available after aRequire Import FunInd
.
Example
- Require Import FunInd.
- [Loading ML file extraction_plugin.cmxs ... done] [Loading ML file recdef_plugin.cmxs ... done]
- Functional Scheme minus_ind := Induction for minus Sort Prop.
- sub_equation is defined minus_ind is defined
- Check minus_ind.
- minus_ind : forall P : nat -> nat -> nat -> Prop, (forall n m : nat, n = 0 -> P 0 m n) -> (forall n m k : nat, n = S k -> m = 0 -> P (S k) 0 n) -> (forall n m k : nat, n = S k -> forall l : nat, m = S l -> P k l (k - l) -> P (S k) (S l) (k - l)) -> forall n m : nat, P n m (n - m)
- Lemma le_minus (n m:nat) : n - m <= n.
- 1 subgoal n, m : nat ============================ n - m <= n
- functional induction (minus n m) using minus_ind; simpl; auto.
- No more subgoals.
- Qed.
Note
(qualid term+)
must be a correct full application
of qualid
. In particular, the rules for implicit arguments are the
same as usual. For example use qualid
if you want to write implicit
arguments explicitly.
Note
functional induction (f x1 x2 x3)
is actually a wrapper for
induction x1, x2, x3, (f x1 x2 x3) using qualid
followed by a cleaning
phase, where qualid
is the induction principle registered for f
(by the Function
(see Advanced recursive functions) or
Functional Scheme
(see Generation of induction principles with Functional Scheme)
command) corresponding to the sort of the goal. Therefore
functional induction
may fail if the induction scheme qualid
is not
defined. See also Advanced recursive functions for the function
terms accepted by Function
.
Note
There is a difference between obtaining an induction scheme
for a function by using Function
(see Advanced recursive functions)
and by using Functional Scheme
after a normal definition using
Fixpoint
or Definition
. See Advanced recursive functions
for details.
See also
Advanced recursive functions, Generation of induction principles with Functional Scheme and inversion
-
Error
Not the right number of induction arguments.
¶
-
Variant
functional induction (qualid term+) as simple_intropattern using term with bindings_list
Similarly to
induction
andelim
, this allows giving explicitly the name of the introduced variables, the induction principle, and the values of dependent premises of the elimination scheme, including predicates for mutual induction whenqualid
is part of a mutually recursive definition.
-
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 num
This does the same thing as
intros until num
followed bydiscriminate ident
whereident
is the identifier for the last introduced hypothesis.
-
Variant
discriminate term with bindings_list
This does the same thing as
discriminate term
but using the given bindings to instantiate parameters or hypotheses ofterm
.
-
Variant
ediscriminate num
¶ -
Variant
ediscriminate term with bindings_list?
This works the same as
discriminate
but if the type ofterm
, or the type of the hypothesis referred to bynum
, 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
-
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 subgoal ============================ forall (l : list) (n : nat), P nil -> cons n l = cons 0 nil -> P l
- intros.
- 1 subgoal l : list n : nat H : P nil H0 : cons n l = cons 0 nil ============================ P l
- injection H0.
- 1 subgoal l : list n : nat H : P nil H0 : cons n l = cons 0 nil ============================ l = nil -> n = 0 -> P l
Beware that injection yields 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 using the commandScheme 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
Not a projectable equality but a discriminable one.
¶
-
Error
Nothing to do, it is an equality between convertible terms.
¶
-
Error
Not a primitive equality.
¶
-
Error
Nothing to inject.
¶
-
Variant
injection num
This does the same thing as
intros until num
followed byinjection ident
whereident
is the identifier for the last introduced hypothesis.
-
Variant
injection term with bindings_list
This does the same as
injection term
but using the given bindings to instantiate parameters or hypotheses ofterm
.
-
Variant
einjection num
¶ -
Variant
einjection term with bindings_list?
This works the same as
injection
but if the type ofterm
, or the type of the hypothesis referred to bynum
, 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_list? as simple_intropattern+
-
Variant
injection num as simple_intropattern+
-
Variant
injection as simple_intropattern+
-
Variant
einjection term with bindings_list? as simple_intropattern+
-
Variant
einjection num 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_list? as injection_intropattern
-
Variant
injection num as injection_intropattern
-
Variant
injection as injection_intropattern
-
Variant
einjection term with bindings_list? as injection_intropattern
-
Variant
einjection num 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+
.
-
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 num
This does the same thing as
intros until num
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 i-th constructor and the equalities thatinversion
introduces in the context of the goal corresponding to the i-th 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 subgoal ============================ forall l : list nat, contains0 (1 :: l) -> contains0 l
- intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ].
- 1 subgoal l : list nat H : contains0 (1 :: l) l' : list nat p : nat Hl' : contains0 l Heqp : p = 1 Heql' : l' = l ============================ contains0 l
-
Variant
inversion num as or_and_intropattern_loc
This allows naming the hypotheses introduced by
inversion num
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
.
-
Variant
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
Non-dependent 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 subgoal 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 subgoal 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 subgoal 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 subgoal 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 subgoal 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 subgoal 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 subgoal 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 subgoal 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 length-indexed 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 subgoal ============================ 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 subgoal 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 subgoal 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 subgoal 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 subgoal 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 subgoal 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 subgoals.
- Qed.
-
fix ident num
¶ This tactic is a primitive tactic to start a proof by induction. In general, it is easier to rely on higher-level 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 numbernum
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 leastnum
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 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 num 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).
-
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 co-inductive hypotheses is correct is done only at the time of registering the lemma in the 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).
Rewriting expressions¶
These tactics use the equality eq:forall A:Type, A->A->Prop
defined in
file Logic.v
(see Logic). The notation for eq T t u
is
simply t=u
dropping the implicit type of t
and u
.
-
rewrite term
¶ This tactic applies to any goal. The type of
term
must have the formforall (x
1:A
1) ... (x
n:A
n), eq term
1term
2.
where
eq
is the Leibniz equality or a registered setoid equality.Then
rewrite term
finds the first subterm matchingterm
1 in the goal, resulting in instancesterm
1' andterm
2' and then replaces every occurrence ofterm
1' byterm
2'. Hence, some of the variablesx
i are solved by unification, and some of the typesA
1, ..., A
n become new subgoals.-
Error
Tactic generated a subgoal identical to the original goal. This happens if term does not occur in the goal.
¶
-
Variant
rewrite term in goal_occurrences
Analogous to
rewrite term
but rewriting is done following the clausegoal_occurrences
. For instance:rewrite H in H'
will rewriteH
in the hypothesisH'
instead of the current goal.rewrite H in H' at 1, H'' at - 2 |- *
meansrewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.
In particular a failure will happen if any of these three simpler tactics fails.rewrite H in * |-
will dorewrite H in H'
for all hypothesesH'
different fromH
. A success will happen as soon as at least one of these simpler tactics succeeds.rewrite H in *
is a combination ofrewrite H
andrewrite H in * |-
that succeeds if at least one of these two tactics succeeds.
Orientation
->
or<-
can be inserted before theterm
to rewrite.
-
Variant
rewrite term at occurrences
Rewrite only the given
occurrences
ofterm
. Occurrences are specified from left to right as for pattern (pattern
). The rewrite is always performed using setoid rewriting, even for Leibniz’s equality, so one has toImport Setoid
to use this variant.
-
Variant
rewrite term by tactic
Use tactic to completely solve the side-conditions arising from the
rewrite
.
-
Variant
rewrite orientation term+, in ident?
Is equivalent to the
n
successive tacticsrewrite term+;
, each one working on the first subgoal generated by the previous one. Anorientation
->
or<-
can be inserted before eachterm
to rewrite. One unique clause can be added at the end after the keyword in; it will then affect all rewrite operations.
In all forms of rewrite described above, a
term
to rewrite can be immediately prefixed by one of the following modifiers:?
: the tacticrewrite ?term
performs the rewrite ofterm
as many times as possible (perhaps zero time). This form never fails.num?
: works similarly, except that it will do at mostnum
rewrites.!
: works as?
, except that at least one rewrite should succeed, otherwise the tactic fails.num!
(or simplynum
) : preciselynum
rewrites ofterm
will be done, leading to failure if thesenum
rewrites are not possible.
-
Variant
erewrite term
¶ This tactic works as
rewrite term
but turning unresolved bindings into existential variables, if any, instead of failing. It has the same variants asrewrite
has.
-
Flag
Keyed Unification
¶ Makes higher-order unification used by
rewrite
rely on a set of keys to drive unification. The subterms, considered as rewriting candidates, must start with the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments are then unified up to full reduction.
-
Error
-
replace term with term’
¶ This tactic applies to any goal. It replaces all free occurrences of
term
in the current goal withterm’
and generates an equalityterm = term’
as a subgoal. This equality is automatically solved if it occurs among the assumptions, or if its symmetric form occurs. It is equivalent tocut term = term’; [intro H
n; rewrite <- H
n; clear H
n|| assumption || symmetry; try assumption]
.-
Error
Terms do not have convertible types.
¶
-
Variant
replace term with term’ by tactic
This acts as
replace term with term’
but appliestactic
to solve the generated subgoalterm = term’
.
-
Variant
replace term
Replaces
term
withterm’
using the first assumption whose type has the formterm = term’
orterm’ = term
.
-
Variant
replace -> term
Replaces
term
withterm’
using the first assumption whose type has the formterm = term’
-
Variant
replace <- term
Replaces
term
withterm’
using the first assumption whose type has the formterm’ = term
-
Variant
replace term with term? in goal_occurrences by tactic?
-
Variant
replace -> term in goal_occurrences
-
Variant
replace <- term in goal_occurrences
Acts as before but the replacements take place in the specified clauses (
goal_occurrences
) (see Performing computations) and not only in the conclusion of the goal. The clause argument must not contain anytype of
norvalue of
.
-
Error
-
subst ident
¶ This tactic applies to a goal that has
ident
in its context and (at least) one hypothesis, sayH
, of typeident = t
ort = ident
withident
not occurring int
. Then it replacesident
byt
everywhere in the goal (in the hypotheses and in the conclusion) and clearsident
andH
from the context.If
ident
is a local definition of the formident := t
, it is also unfolded and cleared.Note
-
Variant
subst
This applies subst repeatedly from top to bottom to all identifiers of the context for which an equality of the form
ident = t
ort = ident
orident := t
exists, withident
not occurring int
.
-
Flag
Regular Subst Tactic
¶ This flag controls the behavior of
subst
. When it is activated (it is by default),subst
also deals with the following corner cases:- A context with ordered hypotheses
ident
1= ident
2 andident
1= t
, ort′ = ident
1` witht′
not a variable, and no other hypotheses of the formident
2= u
oru = ident
2; without the flag, a second call to subst would be necessary to replaceident
2 byt
ort′
respectively. - The presence of a recursive equation which without the flag would
be a cause of failure of
subst
. - A context with cyclic dependencies as with hypotheses
ident
1= f ident
2 andident
2= g ident
1 which without the flag would be a cause of failure ofsubst
.
Additionally, it prevents a local definition such as
ident := t
to be unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the formident = u
, oru′ = ident
withu′
not a variable. Finally, it preserves the initial order of hypotheses, which without the flag it may break. default.- A context with ordered hypotheses
-
Variant
-
stepl term
¶ This tactic is for chaining rewriting steps. It assumes a goal of the form
R term term
whereR
is a binary relation and relies on a database of lemmas of the formforall x y z, R x y -> eq x z -> R z y
whereeq
is typically a setoid equality. The application ofstepl term
then replaces the goal byR term term
and adds a new goal statingeq term term
.This tactic is especially useful for parametric setoids which are not accepted as regular setoids for
rewrite
andsetoid_replace
(see Generalized rewriting).
-
change term
¶ This tactic applies to any goal. It implements the rule
Conv
given in Subtyping rules.change U
replaces the current goalT
withU
providing thatU
is well-formed and thatT
andU
are convertible.-
Error
Not convertible.
¶
-
Variant
change term with term’
This replaces the occurrences of
term
byterm’
in the current goal. The termterm
andterm’
must be convertible.
-
Variant
change term at num+ with term’
This replaces the occurrences numbered
num+
ofterm
byterm’
in the current goal. The termsterm
andterm’
must be convertible.-
Error
Too few occurrences.
¶
-
Error
-
Variant
change term at num+? with term? in ident
This applies the
change
tactic not to the goal but to the hypothesisident
.
-
Variant
now_show term
This is a synonym of
change term
. It can be used to make some proof steps explicit when refactoring a proof script to make it readable.
See also
-
Error
Performing computations¶
This set of tactics implements different specialized usages of the
tactic change
.
All conversion tactics (including change
) can be parameterized by the
parts of the goal where the conversion can occur. This is done using
goal clauses which consists in a list of hypotheses and, optionally,
of a reference to the conclusion of the goal. For defined hypothesis
it is possible to specify if the conversion should occur on the type
part, the body part or both (default).
Goal clauses are written after a conversion tactic (tactics set
,
rewrite
, replace
and autorewrite
also use goal
clauses) and are introduced by the keyword in
. If no goal clause is
provided, the default is to perform the conversion only in the
conclusion.
The syntax and description of the various goal clauses is the following:
in ident+ |-
only in hypothesesident+
in ident+ |- *
in hypothesesident+
and in the conclusionin * |-
in every hypothesisin *
(equivalent to in* |- *
) everywherein (type of ident) (value of ident) ... |-
in type part ofident
, in the value part ofident
, etc.
For backward compatibility, the notation in ident+
performs
the conversion in hypotheses ident+
.
-
cbv flag*
¶ -
lazy flag*
¶ These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. In correspondence with the kinds of reduction considered in Coq namely \(\beta\) (reduction of functional application), \(\delta\) (unfolding of transparent constants, see Controlling the reduction strategies and the conversion algorithm), \(\iota\) (reduction of pattern matching over a constructed term, and unfolding of
fix
andcofix
expressions) and \(\zeta\) (contraction of local definitions), the flags are eitherbeta
,delta
,match
,fix
,cofix
,iota
orzeta
. Theiota
flag is a shorthand formatch
,fix
andcofix
. Thedelta
flag itself can be refined intodelta [ qualid+ ]
ordelta - [ qualid+ ]
, restricting in the first case the constants to unfold to the constants listed, and restricting in the second case the constant to unfold to all but the ones explicitly mentioned. Notice that thedelta
flag does not apply to variables bound by a let-in construction inside theterm
itself (use here thezeta
flag). In any cases, opaque constants are not unfolded (see Controlling the reduction strategies and the conversion algorithm).Normalization according to the flags is done by first evaluating the head of the expression into a weak-head normal form, i.e. until the evaluation is blocked by a variable (or an opaque constant, or an axiom), as e.g. in
x u1 ... un
, ormatch x with ... end
, or(fix f x {struct x} := ...) x
, or is a constructed form (a \(\lambda\)-expression, a constructor, a cofixpoint, an inductive type, a product type, a sort), or is a redex that the flags prevent to reduce. Once a weak-head normal form is obtained, subterms are recursively reduced using the same strategy.Reduction to weak-head normal form can be done using two strategies: lazy (
lazy
tactic), or call-by-value (cbv
tactic). The lazy strategy is a call-by-need strategy, with sharing of reductions: the arguments of a function call are weakly evaluated only when necessary, and if an argument is used several times then it is weakly computed only once. This reduction is efficient for reducing expressions with dead code. For instance, the proofs of a propositionexists x. P(x)
reduce to a pair of a witnesst
, and a proof thatt
satisfies the predicateP
. Most of the time,t
may be computed without computing the proof ofP(t)
, thanks to the lazy strategy.The call-by-value strategy is the one used in ML languages: the arguments of a function call are systematically weakly evaluated first. Despite the lazy strategy always performs fewer reductions than the call-by-value strategy, the latter is generally more efficient for evaluating purely computational expressions (i.e. with little dead code).
-
Variant
compute
¶ -
Variant
cbv
These are synonyms for
cbv beta delta iota zeta
.
-
Variant
lazy
This is a synonym for
lazy beta delta iota zeta
.
-
Variant
compute [ qualid+ ]
-
Variant
cbv [ qualid+ ]
These are synonyms of
cbv beta delta qualid+ iota zeta
.
-
Variant
compute - [ qualid+ ]
-
Variant
cbv - [ qualid+ ]
These are synonyms of
cbv beta delta -qualid+ iota zeta
.
-
Variant
lazy [ qualid+ ]
-
Variant
lazy - [ qualid+ ]
These are respectively synonyms of
lazy beta delta qualid+ iota zeta
andlazy beta delta -qualid+ iota zeta
.
-
Variant
vm_compute
¶ This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine described in [GregoireL02]. This algorithm is dramatically more efficient than the algorithm used for the
cbv
tactic, but it cannot be fine-tuned. It is especially interesting for full evaluation of algebraic objects. This includes the case of reflection-based tactics.
-
Variant
native_compute
¶ This tactic evaluates the goal by compilation to OCaml as described in [BDenesGregoire11]. If Coq is running in native code, it can be typically two to five times faster than
vm_compute
. Note however that the compilation cost is higher, so it is worth using only for intensive computations.-
Flag
NativeCompute Profiling
¶ On Linux, if you have the
perf
profiler installed, this flag makes it possible to profilenative_compute
evaluations.
-
Option
NativeCompute Profile Filename string
¶ This option specifies the profile output; the default is
native_compute_profile.data
. The actual filename used will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means you can individually profile multiple uses ofnative_compute
in a script. From the Linux command line, runperf report
on the profile file to see the results. Consult theperf
documentation for more details.
-
Flag
-
Flag
Debug Cbv
¶ This flag makes
cbv
(and its derivativecompute
) print information about the constants it encounters and the unfolding decisions it makes.
-
red
¶ This tactic applies to a goal that has the form:
forall (x:T1) ... (xk:Tk), T
with
T
\(\beta\)\(\iota\)\(\zeta\)-reducing toc t
1... t
n andc
a constant. Ifc
is transparent then it replacesc
with its definition (sayt
) and then reduces(t t
1... t
n)
according to \(\beta\)\(\iota\)\(\zeta\)-reduction rules.
-
Error
Not reducible.
¶
-
Error
No head constant to reduce.
¶
-
hnf
¶ This tactic applies to any goal. It replaces the current goal with its head normal form according to the \(\beta\)\(\delta\)\(\iota\)\(\zeta\)-reduction rules, i.e. it reduces the head of the goal until it becomes a product or an irreducible term. All inner \(\beta\)\(\iota\)-redexes are also reduced.
Example: The term
fun n : nat => S n + S n
is not reduced byhnf
.
Note
The \(\delta\) rule only applies to transparent constants (see Controlling the reduction strategies and the conversion algorithm on transparency and opacity).
-
cbn
¶ -
simpl
¶ These tactics apply to any goal. They try to reduce a term to something still readable instead of fully normalizing it. They perform a sort of strong normalization with two key differences:
- They unfold a constant if and only if it leads to a \(\iota\)-reduction, i.e. reducing a match or unfolding a fixpoint.
- While reducing a constant unfolding to (co)fixpoints, the tactics use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls.
The
cbn
tactic is claimed to be a more principled, faster and more predictable replacement forsimpl
.The
cbn
tactic accepts the same flags ascbv
andlazy
. The behavior of bothsimpl
andcbn
can be tuned using the Arguments vernacular command as follows:A constant can be marked to be never unfolded by
cbn
orsimpl
:Example
- Arguments minus n m : simpl never.
After that command an expression like
(minus (S x) y)
is left untouched by the tacticscbn
andsimpl
.A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the
/
symbol in the argument list of theArguments
vernacular command.Example
- Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
- fcomp is defined
- Arguments fcomp {A B C} f g x /.
- Notation "f \o g" := (fcomp f g) (at level 50).
After that command the expression
(f \o g)
is left untouched bysimpl
while((f \o g) t)
is reduced to(f (g t))
. The same mechanism can be used to make a constant volatile, i.e. always unfolded.Example
- Definition volatile := fun x : nat => x.
- volatile is defined
- Arguments volatile / x.
A constant can be marked to be unfolded only if an entire set of arguments evaluates to a constructor. The
!
symbol can be used to mark such arguments.Example
- Arguments minus !n !m.
After that command, the expression
(minus (S x) y)
is left untouched bysimpl
, while(minus (S x) (S y))
is reduced to(minus x y)
.A special heuristic to determine if a constant has to be unfolded can be activated with the following command:
Example
- Arguments minus n m : simpl nomatch.
The heuristic avoids to perform a simplification step that would expose a match construct in head position. For example the expression
(minus (S (S x)) (S y))
is simplified to(minus (S x) y)
even if an extra simplification is possible.
In detail, the tactic
simpl
first applies \(\beta\)\(\iota\)-reduction. Then, it expands transparent constants and tries to reduce further using \(\beta\)\(\iota\)-reduction. But, when no \(\iota\) rule is applied after unfolding then \(\delta\)-reductions are not applied. For instance trying to usesimpl
on(plus n O) = n
changes nothing.Notice that only transparent constants whose name can be reused in the recursive calls are possibly unfolded by
simpl
. For instance a constant defined byplus' := plus
is possibly unfolded and reused in the recursive calls, but a constant such assucc := plus (S O)
is never unfolded. This is the main difference betweensimpl
andcbn
. The tacticcbn
reduces whenever it will be able to reuse it or not:succ t
is reduced toS t
.
-
Variant
cbn [ qualid+ ]
-
Variant
cbn - [ qualid+ ]
These are respectively synonyms of
cbn beta delta [ qualid+ ] iota zeta
andcbn beta delta - [ qualid+ ] iota zeta
(seecbn
).
-
Variant
simpl pattern at num+
This applies
simpl
only to thenum+
occurrences of the subterms matchingpattern
in the current goal.-
Error
Too few occurrences.
-
Error
-
Variant
simpl qualid
-
Variant
simpl string
This applies
simpl
only to the applicative subterms whose head occurrence is the unfoldable constantqualid
(the constant can be referred to by its notation usingstring
if such a notation exists).
-
Variant
simpl qualid at num+
-
Variant
simpl string at num+
This applies
simpl
only to thenum+
applicative subterms whose head occurrence isqualid
(orstring
).
-
Flag
Debug RAKAM
¶ This flag makes
cbn
print various debugging information.RAKAM
is the Refolding Algebraic Krivine Abstract Machine.
-
unfold qualid
¶ This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see Definitions and Controlling the reduction strategies and the conversion algorithm). The tactic
unfold
applies the \(\delta\) rule to each occurrence of the constant to whichqualid
refers in the current goal and then replaces it with its \(\beta\iota\zeta\)-normal form. Use the general reduction tactics if you want to avoid this final reduction, for instancecbv delta [qualid]
.-
Error
Cannot coerce qualid to an evaluable reference.
¶ This error is frequent when trying to unfold something that has defined as an inductive type (or constructor) and not as a definition.
Example
- Goal 0 <= 1.
- 1 subgoal ============================ 0 <= 1
- unfold le.
- Toplevel input, characters 0-10: > unfold le. > ^^^^^^^^^^ Error: Cannot coerce le to an evaluable reference.
This error can also be raised if you are trying to unfold something that has been marked as opaque.
Example
- Opaque Nat.add.
- Goal 1 + 0 = 1.
- 1 subgoal ============================ 1 + 0 = 1
- unfold Nat.add.
- Toplevel input, characters 0-15: > unfold Nat.add. > ^^^^^^^^^^^^^^^ Error: Cannot coerce Nat.add to an evaluable reference.
-
Variant
unfold qualid in goal_occurrences
Replaces
qualid
in hypothesis (or hypotheses) designated bygoal_occurrences
with its definition and replaces the hypothesis with its \(\beta\)\(\iota\) normal form.
-
Variant
unfold qualid+,
Replaces
qualid+,
with their definitions and replaces the current goal with its \(\beta\)\(\iota\) normal form.
-
Variant
unfold qualid at occurrences+,
The list
occurrences
specify the occurrences ofqualid
to be unfolded. Occurrences are located from left to right.
-
Variant
unfold string
If
string
denotes the discriminating symbol of a notation (e.g. "+") or an expression defining a notation (e.g."_ + _"
), and this notation denotes an application whose head symbol is an unfoldable constant, then the tactic unfolds it.
-
Variant
unfold string%ident
This is variant of
unfold string
wherestring
gets its interpretation from the scope bound to the delimiting keyident
instead of its default interpretation (see Local interpretation rules for notations).
-
Variant
unfold qualidstring%ident? at occurrences?+, in goal_occurrences?
This is the most general form.
-
Error
-
fold term
¶ This tactic applies to any goal. The term
term
is reduced using thered
tactic. Every occurrence of the resultingterm
in the goal is then replaced byterm
. This tactic is particularly useful when a fixpoint definition has been wrongfully unfolded, making the goal very hard to read. On the other hand, when an unfolded function applied to its argument has been reduced, thefold
tactic won't do anything.Example
- Goal ~0=0.
- 1 subgoal ============================ 0 <> 0
- unfold not.
- 1 subgoal ============================ 0 = 0 -> False
- Fail progress fold not.
- The command has indeed failed with message: Failed to progress.
- pattern (0 = 0).
- 1 subgoal ============================ (fun P : Prop => P -> False) (0 = 0)
- fold not.
- 1 subgoal ============================ 0 <> 0
-
pattern term
¶ This command applies to any goal. The argument
term
must be a free subterm of the current goal. The command pattern performs \(\beta\)-expansion (the inverse of \(\beta\)-reduction) of the current goal (sayT
) by- replacing all occurrences of
term
inT
with a fresh variable - abstracting this variable
- applying the abstracted goal to
term
For instance, if the current goal
T
is expressible as \(\varphi\)(t)
where the notation captures all the instances oft
in \(\varphi\)(t)
, thenpattern t
transforms it into(fun x:A =>
\(\varphi\)(x)) t
. This tactic can be used, for instance, when the tacticapply
fails on matching.- replacing all occurrences of
-
Variant
pattern term at num+
Only the occurrences
num+
ofterm
are considered for \(\beta\)-expansion. Occurrences are located from left to right.
-
Variant
pattern term at - num+
All occurrences except the occurrences of indexes
num+
ofterm
are considered for \(\beta\)-expansion. Occurrences are located from left to right.
-
Variant
pattern term+,
Starting from a goal \(\varphi\)
(t
1... t
m)
, the tacticpattern t
1, ..., t
m generates the equivalent goal(fun (x
1:A
1) ... (x
m:A
m) =>
\(\varphi\)(x
1... x
m)) t
1... t
m. Ift
i occurs in one of the generated typesA
j these occurrences will also be considered and possibly abstracted.
-
Variant
pattern term at num++,
This behaves as above but processing only the occurrences
num+
ofterm
starting fromterm
.
-
Variant
pattern term at -? num+,?+,
This is the most general syntax that combines the different variants.
Conversion tactics applied to hypotheses¶
-
tactic in ident+,
Applies
tactic
(any of the conversion tactics listed in this section) to the hypothesesident+
.If
ident
is a local definition, thenident
can be replaced bytype of ident
to address not the body but the type of the local definition.Example:
unfold not in (type of H1) (type of H3)
.
-
Error
No such hypothesis: ident.
Automation¶
-
auto
¶ This tactic implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the
assumption
tactic, then it reduces the goal to an atomic one usingintros
and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and tries to apply one of them (starting from the tactics with lower cost). This process is recursively applied to the generated subgoals.By default,
auto
only uses the hypotheses of the current goal and the hints of the database namedcore
.Warning
auto
uses a weaker version ofapply
that is closer tosimple apply
so it is expected that sometimesauto
will fail even if applying manually one of the hints would succeed.-
Variant
auto with ident+
Uses the hint databases
ident+
in addition to the databasecore
.Note
Use the fake database
nocore
if you want to not use thecore
database.
-
Variant
auto with *
Uses all existing hint databases. Using this variant is highly discouraged in finished scripts since it is both slower and less robust than the variant where the required databases are explicitly listed.
See also
The Hints Databases for auto and eauto for the list of pre-defined databases and the way to create or extend a database.
-
Variant
auto using qualidi+ with ident+?
Uses lemmas
qualidi
in addition to hints. Ifqualid
is an inductive type, it is the collection of its constructors which are added as hints.Note
The hints passed through the
using
clause are used in the same way as if they were passed through a hint database. Consequently, they use a weaker version ofapply
andauto using qualid
may fail whereapply qualid
succeeds.Given that this can be seen as counter-intuitive, it could be useful to have an option to use full-blown
apply
for lemmas passed through theusing
clause. Contributions welcome!
-
Variant
info_auto
Behaves like
auto
but shows the tactics it uses to solve the goal. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used.
-
Variant
-
Variant
trivial
¶ This tactic is a restriction of
auto
that is not recursive and tries only hints that cost0
. Typically it solves trivial equalities likeX=X
.
Note
auto
and trivial
either solve completely the goal or
else succeed without changing the goal. Use solve [ auto ]
and
solve [ trivial ]
if you would prefer these tactics to fail when
they do not manage to solve the goal.
-
Flag
Info Auto
¶ -
Flag
Debug Auto
¶ -
Flag
Info Trivial
¶ -
Flag
Debug Trivial
¶ These flags enable printing of informative or debug information for the
auto
andtrivial
tactics.
-
eauto
¶ This tactic generalizes
auto
. Whileauto
does not try resolution hints which would leave existential variables in the goal,eauto
does try them (informally speaking, it internally uses a tactic close tosimple eapply
instead of a tactic close tosimple apply
in the case ofauto
). As a consequence,eauto
can solve such a goal:Example
- Hint Resolve ex_intro : core.
- The hint ex_intro will only be used by eauto, because applying ex_intro would leave variable x as unresolved existential variable.
- Goal forall P:nat -> Prop, P 0 -> exists n, P n.
- 1 subgoal ============================ forall P : nat -> Prop, P 0 -> exists n : nat, P n
- eauto.
- No more subgoals.
Note that
ex_intro
should be declared as a hint.eauto
also obeys the following flags:
-
autounfold with ident+
¶ This tactic unfolds constants that were declared through a
Hint Unfold
in the given databases.
-
Variant
autounfold with ident+ in goal_occurrences
Performs the unfolding in the given clause (
goal_occurrences
).
-
Variant
autounfold with *
Uses the unfold hints declared in all the hint databases.
-
autorewrite with ident+
¶ This tactic carries out rewritings according to the rewriting rule bases
ident+
.Each rewriting rule from the base
ident
is applied to the main subgoal until it fails. Once all the rules have been processed, if the main subgoal has progressed (e.g., if it is distinct from the initial main goal) then the rules of this base are processed again. If the main subgoal has not progressed then the next base is processed. For the bases, the behavior is exactly similar to the processing of the rewriting rules.The rewriting rule bases are built with the
Hint Rewrite
command.
Warning
This tactic may loop if you build non terminating rewriting systems.
-
Variant
autorewrite with ident+ using tactic
Performs, in the same way, all the rewritings of the bases
ident+
applying tactic to the main subgoal after each rewriting step.
-
Variant
autorewrite with ident+ in qualid using tactic
Performs all the rewritings in hypothesis
qualid
applyingtactic
to the main subgoal after each rewriting step.
-
Variant
autorewrite with ident+ in goal_occurrences
Performs all the rewriting in the clause
goal_occurrences
.
See also
Hint-Rewrite for feeding the database of lemmas used by
autorewrite
and autorewrite
for examples showing the use of this tactic.
-
easy
¶ This tactic tries to solve the current goal by a number of standard closing steps. In particular, it tries to close the current goal using the closing tactics
trivial
,reflexivity
,symmetry
,contradiction
andinversion
of hypothesis. If this fails, it tries introducing variables and splitting and-hypotheses, using the closing tactics afterwards, and splitting the goal usingsplit
and recursing.This tactic solves goals that belong to many common classes; in particular, many cases of unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic.
Controlling automation¶
The hints databases for auto and eauto¶
The hints for auto
and eauto
are stored in databases. Each database
maps head symbols to a list of hints.
-
Command
Print Hint ident
¶ Use this command to display the hints associated to the head symbol
ident
(see Print Hint). Each hint has a cost that is a nonnegative integer, and an optional pattern. The hints with lower cost are tried first. A hint is tried byauto
when the conclusion of the current goal matches its pattern or when it has no pattern.
Creating Hint databases¶
One can optionally declare a hint database using the command
Create HintDb
. If a hint is added to an unknown database, it will be
automatically created.
-
Command
Create HintDb ident discriminated?
¶ This command creates a new database named
ident
. The database is implemented by a Discrimination Tree (DT) that serves as an index of all the lemmas. The DT can use transparency information to decide if a constant should be indexed or not (c.f. The hints databases for auto and eauto), making the retrieval more efficient. The legacy implementation (the default one for new databases) uses the DT only on goals without existentials (i.e.,auto
goals), for non-Immediate hints and does not make use of transparency hints, putting more work on the unification that is run after retrieval (it keeps a list of the lemmas in case the DT is not used). The new implementation enabled by the discriminated option makes use of DTs in all cases and takes transparency information into account. However, the order in which hints are retrieved from the DT may differ from the order in which they were inserted, making this implementation observationally different from the legacy one.
-
Command
Hint hint_definition : ident+
¶ The general command to add a hint to some databases
ident+
. The various possiblehint_definition
s are given below.-
Variant
Hint hint_definition
No database name is given: the hint is registered in the
core
database.Deprecated since version 8.10.
-
Variant
Local Hint hint_definition : ident+
This is used to declare hints that must not be exported to the other modules that require and import the current module. Inside a section, the flag Local is useless since hints do not survive anyway to the closure of sections.
-
Variant
Hint Resolve term | num? pattern?? : ident
¶ This command adds
simple apply term
to the hint list with the head symbol of the type ofterm
. The cost of that hint is the number of subgoals generated bysimple apply term
ornum
if specified. The associatedpattern
is inferred from the conclusion of the type ofterm
or the givenpattern
if specified. In case the inferred type ofterm
does not start with a product the tactic added in the hint list isexact term
. In case this type can however be reduced to a type starting with a product, the tacticsimple apply term
is also stored in the hints list. If the inferred type ofterm
contains a dependent quantification on a variable which occurs only in the premisses of the type and not in its conclusion, no instance could be inferred for the variable by unification with the goal. In this case, the hint is added to the hint list ofeauto
instead of the hint list of auto and a warning is printed. A typical example of a hint that is used only byeauto
is a transitivity lemma.
-
Variant
Hint Resolve -> term : ident
Adds the left-to-right implication of an equivalence as a hint (informally the hint will be used as
apply <- term
, although as mentioned before, the tactic actually used is a restricted version ofapply
).
-
Variant
Hint Resolve <- term
Adds the right-to-left implication of an equivalence as a hint.
-
Variant
Hint Immediate term : ident
¶ This command adds
simple apply term; trivial
to the hint list associated with the head symbol of the type ofident
in the given database. This tactic will fail if all the subgoals generated bysimple apply term
are not solved immediately by thetrivial
tactic (which only tries tactics with cost 0).This command is useful for theorems such as the symmetry of equality orn+1=m+1 -> n=m
that we may like to introduce with a limited use in order to avoid useless proof-search. The cost of this tactic (which never generates subgoals) is always 1, so that it is not used bytrivial
itself.
-
Error
term cannot be used as a hint
-
Variant
Hint Constructors qualid : ident
¶ If
qualid
is an inductive type, this command adds all its constructors as hints of typeResolve
. Then, when the conclusion of current goal has the form(qualid ...)
,auto
will try to apply each constructor.
-
Variant
Hint Unfold qualid : ident
¶ This adds the tactic
unfold qualid
to the hint list that will only be used when the head constant of the goal isqualid
. Its cost is 4.
-
Variant
Hint Unfold qualid+
Extends the previous command for several defined constants.
-
Variant
Hint Transparent qualid+ : ident
¶ -
Variant
Hint Opaque qualid+ : ident
¶ This adds transparency hints to the database, making
qualid
transparent or opaque constants during resolution. This information is used during unification of the goal with any lemma in the database and inside the discrimination network to relax or constrain it in the case of discriminated databases.
-
Variant
Hint Variables TransparentOpaque : ident
¶ -
Variant
Hint Constants TransparentOpaque : ident
¶ This sets the transparency flag used during unification of hints in the database for all constants or all variables, overwriting the existing settings of opacity. It is advised to use this just after a
Create HintDb
command.
-
Variant
Hint Extern num pattern? => tactic : ident
¶ This hint type is to extend
auto
with tactics other thanapply
andunfold
. For that, we must specify a cost, an optionalpattern
and atactic
to execute.Example
- Hint Extern 4 (~(_ = _)) => discriminate : core.
Now, when the head of the goal is a disequality,
auto
will try discriminate if it does not manage to solve the goal with hints with a cost less than 4.One can even use some sub-patterns of the pattern in the tactic script. A sub-pattern is a question mark followed by an identifier, like
?X1
or?X2
. Here is an example:Example
- Require Import List.
- Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec.
- Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
- 1 subgoal ============================ forall a b : list (nat * nat), {a = b} + {a <> b}
- Info 1 auto with eqdec.
- <ltac_plugin::auto@0> eqdec No more subgoals.
-
Variant
Hint Cut regexp : ident
¶ Warning
These hints currently only apply to typeclass proof search and the
typeclasses eauto
tactic.This command can be used to cut the proof-search tree according to a regular expression matching paths to be cut. The grammar for regular expressions is the following. Beware, there is no operator precedence during parsing, one can check with
Print HintDb
to verify the current cut expression:regexp ::=
ident
(hint or instance identifier) _ (any hint)regexp
|regexp
(disjunction)regexp
regexp
(sequence)regexp
* (Kleene star) emp (empty) eps (epsilon) (regexp
)The
emp
regexp does not match any search path whileeps
matches the empty path. During proof search, the path of successive successful hints on a search branch is recorded, as a list of identifiers for the hints (note thatHint Extern
’s do not have an associated identifier). Before applying any hintident
the current pathp
extended withident
is matched against the current cut expressionc
associated to the hint database. If matching succeeds, the hint is not applied. The semantics ofHint Cut regexp
is to set the cut expression toc | regexp
, the initial cut expression beingemp
.
-
Variant
Hint Mode qualid +!-* : ident
¶ This sets an optional mode of use of the identifier
qualid
. When proof-search faces a goal that ends in an application ofqualid
to argumentsterm ... term
, the mode tells if the hints associated toqualid
can be applied or not. A mode specification is a list of n+
,!
or-
items that specify if an argument of the identifier is to be treated as an input (+
), if its head only is an input (!
) or an output (-
) of the identifier. For a mode to match a list of arguments, input terms and input heads must not contain existential variables or be existential variables respectively, while outputs can be any term. Multiple modes can be declared for a single identifier, in that case only one mode needs to match the arguments for the hints to be applied. The head of a term is understood here as the applicative head, or the match or projection scrutinee’s head, recursively, casts being ignored.Hint Mode
is especially useful for typeclasses, when one does not want to support default instances and avoid ambiguity in general. Setting a parameter of a class as an input forces proof-search to be driven by that index of the class, with!
giving more flexibility by allowing existentials to still appear deeper in the index but not at its head.
Note
- One can use a
Hint Extern
with no pattern to do pattern matching on hypotheses usingmatch goal with
inside the tactic. - If you want to add hints such as
Hint Transparent
,Hint Cut
, orHint Mode
, for typeclass resolution, do not forget to put them in thetypeclass_instances
hint database.
-
Variant
Hint databases defined in the Coq standard library¶
Several hint databases are defined in the Coq standard library. The actual content of a database is the collection of hints declared to belong to this database in each of the various modules currently loaded. Especially, requiring new modules may extend the database. At Coq startup, only the core database is nonempty and can be used.
core: | This special database is automatically used by auto , except when
pseudo-database nocore is given to auto . The core database
contains only basic lemmas about negation, conjunction, and so on.
Most of the hints in this database come from the Init and Logic directories. |
---|---|
arith: | This database contains all lemmas about Peano’s arithmetic proved in the directories Init and Arith. |
zarith: | contains lemmas about binary signed integers from the directories
theories/ZArith. When required, the module Omega also extends the
database zarith with a high-cost hint that calls omega on equations
and inequalities in nat or Z . |
bool: | contains lemmas about booleans, mostly from directory theories/Bool. |
datatypes: | is for lemmas about lists, streams and so on that are mainly proved in the Lists subdirectory. |
sets: | contains lemmas about sets and relations from the directories Sets and Relations. |
typeclass_instances: | |
contains all the typeclass instances declared in the
environment, including those used for setoid_rewrite ,
from the Classes directory. |
|
fset: | internal database for the implementation of the FSets library. |
ordered_type: | lemmas about ordered types (as defined in the legacy OrderedType module),
mainly used in the FSets and FMaps libraries. |
You are advised not to put your own hints in the core database, but use one or several databases specific to your development.
-
Command
Remove Hints term+ : ident+
¶ This command removes the hints associated to terms
term+
in databasesident+
.
-
Command
Print Hint
This command displays all hints that apply to the current goal. It fails if no proof is being edited, while the two variants can be used at every moment.
Variants:
-
Command
Print Hint ident
This command displays only tactics associated with
ident
in the hints list. This is independent of the goal being edited, so this command will not fail if no goal is being edited.
-
Command
Print Hint *
This command displays all declared hints.
-
Command
Hint Rewrite term+ : ident+
¶ This vernacular command adds the terms
term+
(their types must be equalities) in the rewriting basesident+
with the default orientation (left to right). Notice that the rewriting bases are distinct from theauto
hint bases and thatauto
does not take them into account.This command is synchronous with the section mechanism (see Section mechanism): when closing a section, all aliases created by
Hint Rewrite
in that section are lost. Conversely, when loading a module, allHint Rewrite
declarations at the global level of that module are loaded.
Variants:
-
Command
Hint Rewrite -> term+ : ident+
This is strictly equivalent to the command above (we only make explicit the orientation which otherwise defaults to ->).
-
Command
Hint Rewrite <- term+ : ident+
Adds the rewriting rules
term+
with a right-to-left orientation in the basesident+
.
Hint locality¶
Hints provided by the Hint
commands are erased when closing a section.
Conversely, all hints of a module A
that are not defined inside a
section (and not defined with option Local
) become available when the
module A
is imported (using e.g. Require Import A.
).
As of today, hints only have a binary behavior regarding locality, as
described above: either they disappear at the end of a section scope,
or they remain global forever. This causes a scalability issue,
because hints coming from an unrelated part of the code may badly
influence another development. It can be mitigated to some extent
thanks to the Remove Hints
command,
but this is a mere workaround and has some limitations (for instance, external
hints cannot be removed).
A proper way to fix this issue is to bind the hints to their module scope, as
for most of the other objects Coq uses. Hints should only be made available when
the module they are defined in is imported, not just required. It is very
difficult to change the historical behavior, as it would break a lot of scripts.
We propose a smooth transitional path by providing the Loose Hint Behavior
option which accepts three flags allowing for a fine-grained handling of
non-imported hints.
-
Option
Loose Hint Behavior "Lax""Warn""Strict"
¶ This option accepts three values, which control the behavior of hints w.r.t.
Import
:- "Lax": this is the default, and corresponds to the historical behavior, that is, hints defined outside of a section have a global scope.
- "Warn": outputs a warning when a non-imported hint is used. Note that this is an over-approximation, because a hint may be triggered by a run that will eventually fail and backtrack, resulting in the hint not being actually useful for the proof.
- "Strict": changes the behavior of an unloaded hint to a immediate fail tactic, allowing to emulate an import-scoped hint mechanism.
Setting implicit automation tactics¶
-
Command
Proof with tactic
¶ This command may be used to start a proof. It defines a default tactic to be used each time a tactic command
tactic
1 is ended by...
. In this case the tactic command typed by the user is equivalent totactic
1;tactic
.See also
-
Variant
Proof with tactic using ident+
Combines in a single line
Proof with
andProof using
, see Switching on/off the proof editing mode
-
Variant
Proof using ident+ with tactic
Combines in a single line
Proof with
andProof using
, see Switching on/off the proof editing mode
-
Variant
Decision procedures¶
-
tauto
¶ This tactic implements a decision procedure for intuitionistic propositional calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff [Dyc92]. Note that
tauto
succeeds on any instance of an intuitionistic tautological proposition.tauto
unfolds negations and logical equivalence but does not unfold any other definition.
Example
The following goal can be proved by tauto
whereas auto
would
fail:
- Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
- 1 subgoal ============================ forall (x : nat) (P : nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x
- intros.
- 1 subgoal x : nat P : nat -> Prop H : x = 0 \/ P x H0 : x <> 0 ============================ P x
- tauto.
- No more subgoals.
Moreover, if it has nothing else to do, tauto
performs introductions.
Therefore, the use of intros
in the previous proof is unnecessary.
tauto
can for instance for:
Example
- Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x.
- 1 subgoal ============================ forall (A : Prop) (P : nat -> Prop), A \/ (forall x : nat, ~ A -> P x) -> forall x : nat, ~ A -> P x
- tauto.
- No more subgoals.
Note
In contrast, tauto
cannot solve the following goal
Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->
forall x:nat, ~ ~ (A \/ P x).
because (forall x:nat, ~ A -> P x)
cannot be treated as atomic and
an instantiation of x
is necessary.
-
Variant
dtauto
¶ While
tauto
recognizes inductively defined connectives isomorphic to the standard connectivesand
,prod
,or
,sum
,False
,Empty_set
,unit
,True
,dtauto
also recognizes all inductive types with one constructor and no indices, i.e. record-style connectives.
-
intuition tactic
¶ The tactic
intuition
takes advantage of the search-tree built by the decision procedure involved in the tactictauto
. It uses this information to generate a set of subgoals equivalent to the original one (but simpler than it) and applies the tactictactic
to them [Mun94]. If this tactic fails on some goals thenintuition
fails. In fact,tauto
is simplyintuition fail
.Example
For instance, the tactic
intuition auto
applied to the goal:(forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O
internally replaces it by the equivalent one:
(forall (x:nat), P x), B |- P O
and then uses
auto
which completes the proof.
Originally due to César Muñoz, these tactics (tauto
and
intuition
) have been completely re-engineered by David Delahaye using
mainly the tactic language (see Ltac). The code is
now much shorter and a significant increase in performance has been noticed.
The general behavior with respect to dependent types, unfolding and
introductions has slightly changed to get clearer semantics. This may lead to
some incompatibilities.
-
Variant
intuition
Is equivalent to
intuition auto with *
.
-
Variant
dintuition
¶ While
intuition
recognizes inductively defined connectives isomorphic to the standard connectivesand
,prod
,or
,sum
,False
,Empty_set
,unit
,True
,dintuition
also recognizes all inductive types with one constructor and no indices, i.e. record-style connectives.
-
Flag
Intuition Negation Unfolding
¶ Controls whether
intuition
unfolds inner negations which do not need to be unfolded. This flag is on by default.
-
rtauto
¶ The
rtauto
tactic solves propositional tautologies similarly to whattauto
does. The main difference is that the proof term is built using a reflection scheme applied to a sequent calculus proof of the goal. The search procedure is also implemented using a different technique.Users should be aware that this difference may result in faster proof-search but slower proof-checking, and
rtauto
might not solve goals thattauto
would be able to solve (e.g. goals involving universal quantifiers).Note that this tactic is only available after a
Require Import Rtauto
.
-
firstorder
¶ The tactic
firstorder
is an experimental extension oftauto
to first- order reasoning, written by Pierre Corbineau. It is not restricted to usual logical connectives but instead may reason about any first-order class inductive definition.
-
Option
Firstorder Solver tactic
¶ The default tactic used by
firstorder
when no rule applies isauto with *
, it can be reset locally or globally using this option.-
Command
Print Firstorder Solver
¶ Prints the default tactic used by
firstorder
when no rule applies.
-
Command
-
Variant
firstorder tactic
Tries to solve the goal with
tactic
when no logical rule may apply.
-
Variant
firstorder using qualid+
Deprecated since version 8.3: Use the syntax below instead (with commas).
-
Variant
firstorder using qualid+,
Adds lemmas
qualid+,
to the proof-search environment. Ifqualid
refers to an inductive type, it is the collection of its constructors which are added to the proof-search environment.
-
Variant
firstorder with ident+
Adds lemmas from
auto
hint basesident+
to the proof-search environment.
-
Variant
firstorder tactic using qualid+, with ident+
This combines the effects of the different variants of
firstorder
.
-
congruence
¶ The tactic
congruence
, by Pierre Corbineau, implements the standard Nelson and Oppen congruence closure algorithm, which is a decision procedure for ground equalities with uninterpreted symbols. It also includes constructor theory (seeinjection
anddiscriminate
). If the goal is a non-quantified equality, congruence tries to prove it with non-quantified equalities in the context. Otherwise it tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis.congruence
is also able to take advantage of hypotheses stating quantified equalities, but you have to provide a bound for the number of extra equalities generated that way. Please note that one of the sides of the equality must contain all the quantified variables in order for congruence to match against it.
Example
- Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
- 1 subgoal A : Type f : A -> A g : A -> A -> A a, b : A ============================ a = f a -> g b (f a) = f (f a) -> g a b = f (g b a) -> g a b = a
- intros.
- 1 subgoal A : Type f : A -> A g : A -> A -> A a, b : A H : a = f a H0 : g b (f a) = f (f a) H1 : g a b = f (g b a) ============================ g a b = a
- congruence.
- No more subgoals.
- Qed.
- Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d.
- 1 subgoal A : Type f : A -> A * A a, c, d : A ============================ f = pair a -> Some (f c) = Some (f d) -> c = d
- intros.
- 1 subgoal A : Type f : A -> A * A a, c, d : A H : f = pair a H0 : Some (f c) = Some (f d) ============================ c = d
- congruence.
- No more subgoals.
- Qed.
-
Variant
congruence num
Tries to add at most
num
instances of hypotheses stating quantified equalities to the problem in order to solve it. A bigger value ofnum
does not make success slower, only failure. You might consider adding some lemmas as hypotheses using assert in order forcongruence
to use them.
-
Variant
congruence with term+
¶ Adds
term+
to the pool of terms used bycongruence
. This helps in case you have partially applied constructors in your goal.
-
Error
I don’t know how to handle dependent equality.
¶ The decision procedure managed to find a proof of the goal or of a discriminable equality but this proof could not be built in Coq because of dependently-typed functions.
-
Error
Goal is solvable by congruence but some arguments are missing. Try congruence with term+, replacing metavariables by arbitrary terms.
¶ The decision procedure could solve the goal with the provision that additional arguments are supplied for some partially applied constructors. Any term of an appropriate type will allow the tactic to successfully solve the goal. Those additional arguments can be given to congruence by filling in the holes in the terms given in the error message, using the
congruence with
variant described above.
-
Flag
Congruence Verbose
¶ This flag makes
congruence
print debug information.
Checking properties of terms¶
Each of the following tactics acts as the identity if the check succeeds, and results in an error otherwise.
-
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).
¶
-
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).
-
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).
-
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.
¶
-
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.
¶
-
is_var term
¶ This tactic checks whether its argument is a variable or hypothesis in the current goal context or in the opened sections.
-
Error
Not a variable or hypothesis.
¶
Equality¶
-
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
.
-
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
-
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 =
.
-
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.
-
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
.
-
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 num
This does the same thing as
intros until num
thensimplify_eq ident
whereident
is the identifier for the last introduced hypothesis.
-
Variant
simplify_eq term with bindings_list
This does the same as
simplify_eq term
but using the given bindings to instantiate parameters or hypotheses ofterm
.
-
Variant
esimplify_eq num
¶ -
Variant
esimplify_eq term with bindings_list?
This works the same as
simplify_eq
but if the type ofterm
, or the type of the hypothesis referred to bynum
, 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
.
-
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.
Inversion¶
-
functional inversion ident
¶ functional inversion
is a tactic that performs inversion on hypothesisident
of the formqualid term+ = term
orterm = qualid term+
wherequalid
must have been defined using Function (see Advanced recursive functions). Note that this tactic is only available after aRequire Import FunInd
.-
Error
Cannot find inversion information for hypothesis ident.
¶ This error may be raised when some inversion lemma failed to be generated by Function.
-
Error
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.
-
classical_left
¶ -
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.
Automating¶
-
btauto
¶ The tactic
btauto
implements a reflexive solver for boolean tautologies. It solves goals of the formt = u
wheret
andu
are constructed over the following grammar:btauto_term ::=
ident
true false orbbtauto_term
btauto_term
andbbtauto_term
btauto_term
xorbbtauto_term
btauto_term
negbbtauto_term
ifbtauto_term
thenbtauto_term
elsebtauto_term
Whenever the formula supplied is not a tautology, it also provides a counter-example.
Internally, it uses a system very similar to the one of the ring tactic.
Note that this tactic is only available after a
Require Import Btauto
.
-
omega
¶ The tactic
omega
, due to Pierre Crégut, is an automatic decision procedure for Presburger arithmetic. It solves quantifier-free formulas built with~
,\/
,/\
,->
on top of equalities, inequalities and disequalities on both the typenat
of natural numbers andZ
of binary integers. This tactic must be loaded by the commandRequire Import Omega
. See the additional documentation about omega (see Chapter Omega: a solver for quantifier-free problems in Presburger Arithmetic).
-
ring
¶ This tactic solves equations upon polynomial expressions of a ring (or semiring) structure. It proceeds by normalizing both hand sides of the equation (w.r.t. associativity, commutativity and distributivity, constant propagation) and comparing syntactically the results.
-
ring_simplify term*
¶ This tactic applies the normalization procedure described above to the given terms. The tactic then replaces all occurrences of the terms given in the conclusion of the goal by their normal forms. If no term is given, then the conclusion should be an equation and both hand sides are normalized.
See The ring and field tactic families for more information on
the tactic and how to declare new ring structures. All declared field structures
can be printed with the Print Rings
command.
-
field
¶ -
field_simplify term*
¶ -
field_simplify_eq
¶ The field tactic is built on the same ideas as ring: this is a reflexive tactic that solves or simplifies equations in a field structure. The main idea is to reduce a field expression (which is an extension of ring expressions with the inverse and division operations) to a fraction made of two polynomial expressions.
Tactic
field
is used to solve subgoals, whereasfield_simplify term+
replaces the provided terms by their reduced fraction.field_simplify_eq
applies when the conclusion is an equation: it simplifies both hand sides and multiplies so as to cancel denominators. So it produces an equation without division nor inverse.All of these 3 tactics may generate a subgoal in order to prove that denominators are different from zero.
See The ring and field tactic families for more information on the tactic and how to declare new field structures. All declared field structures can be printed with the Print Fields command.
Example
- Require Import Reals.
- [Loading ML file newring_plugin.cmxs ... done] [Loading ML file r_syntax_plugin.cmxs ... done] [Loading ML file zify_plugin.cmxs ... done] [Loading ML file micromega_plugin.cmxs ... done]
- Goal forall x y:R, (x * y > 0)%R -> (x * (1 / x + x / (x + y)))%R = ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R.
- 1 subgoal ============================ forall x y : R, (x * y > 0)%R -> (x * (1 / x + x / (x + y)))%R = (-1 / y * y * (- x * (x / (x + y)) - 1))%R
- intros; field.
- 1 subgoal x, y : R H : (x * y > 0)%R ============================ (x + y)%R <> 0%R /\ y <> 0%R /\ x <> 0%R
See also
File plugins/setoid_ring/RealField.v for an example of instantiation, theory theories/Reals for many examples of use of field.
Non-logical tactics¶
-
cycle num
¶ This tactic puts the
num
first goals at the end of the list of goals. Ifnum
is negative, it will put the last \(|num|\) goals at the beginning of the list.
Example
- Parameter P : nat -> Prop.
- P is declared
- Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
- 1 subgoal ============================ P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5
- repeat split.
- 5 subgoals ============================ P 1 subgoal 2 is: P 2 subgoal 3 is: P 3 subgoal 4 is: P 4 subgoal 5 is: P 5
- all: cycle 2.
- 5 subgoals ============================ P 3 subgoal 2 is: P 4 subgoal 3 is: P 5 subgoal 4 is: P 1 subgoal 5 is: P 2
- all: cycle -3.
- 5 subgoals ============================ P 5 subgoal 2 is: P 1 subgoal 3 is: P 2 subgoal 4 is: P 3 subgoal 5 is: P 4
-
swap num num
¶ This tactic switches the position of the goals of indices
num
andnum
. If eithernum
ornum
is negative then goals are counted from the end of the focused goal list. Goals are indexed from 1, there is no goal with position 0.
Example
- Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
- 1 subgoal ============================ P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5
- repeat split.
- 5 subgoals ============================ P 1 subgoal 2 is: P 2 subgoal 3 is: P 3 subgoal 4 is: P 4 subgoal 5 is: P 5
- all: swap 1 3.
- 5 subgoals ============================ P 3 subgoal 2 is: P 2 subgoal 3 is: P 1 subgoal 4 is: P 4 subgoal 5 is: P 5
- all: swap 1 -1.
- 5 subgoals ============================ P 5 subgoal 2 is: P 2 subgoal 3 is: P 1 subgoal 4 is: P 4 subgoal 5 is: P 3
-
revgoals
¶ This tactics reverses the list of the focused goals.
Example
- Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
- 1 subgoal ============================ P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5
- repeat split.
- 5 subgoals ============================ P 1 subgoal 2 is: P 2 subgoal 3 is: P 3 subgoal 4 is: P 4 subgoal 5 is: P 5
- all: revgoals.
- 5 subgoals ============================ P 5 subgoal 2 is: P 4 subgoal 3 is: P 3 subgoal 4 is: P 2 subgoal 5 is: P 1
-
shelve
¶ This tactic moves all goals under focus to a shelf. While on the shelf, goals will not be focused on. They can be solved by unification, or they can be called back into focus with the command
Unshelve
.-
Variant
shelve_unifiable
¶ Shelves only the goals under focus that are mentioned in other goals. Goals that appear in the type of other goals can be solved by unification.
Example
- Goal exists n, n=0.
- 1 subgoal ============================ exists n : nat, n = 0
- refine (ex_intro _ _ _).
- 1 focused subgoal (shelved: 1) ============================ ?Goal = 0
- all: shelve_unifiable.
- reflexivity.
- No more subgoals.
-
Variant
-
Command
Unshelve
¶ This command moves all the goals on the shelf (see
shelve
) from the shelf into focus, by appending them to the end of the current list of focused goals.
-
unshelve tactic
¶ Performs
tactic
, then unshelves existential variables added to the shelf by the execution oftactic
, prepending them to the current goal.
-
give_up
¶ This tactic removes the focused goals from the proof. They are not solved, and cannot be solved later in the proof. As the goals are not solved, the proof cannot be closed.
The
give_up
tactic can be used while editing a proof, to choose to write the proof script in a non-sequential order.
Delaying solving unification constraints¶
-
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.
Performance-oriented tactic variants¶
-
change_no_check term
¶ For advanced usage. Similar to
change term
, but as an optimization, it skips checking thatterm
is convertible to the goal.Recall that the Coq kernel typechecks proofs again when they are concluded to ensure safety. Hence, using
change
checks convertibility twice overall, whilechange_no_check
can produce ill-typed terms, but checks convertibility only once. Hence,change_no_check
can be useful to speed up certain proof scripts, especially if one knows by construction that the argument is indeed convertible to the goal.In the following example,
change_no_check
replacesFalse
byTrue
, butQed
then rejects the proof, ensuring consistency.Example
- Goal False.
- 1 subgoal ============================ False
- change_no_check True.
- 1 subgoal ============================ True
- exact I.
- No more subgoals.
- Fail Qed.
- The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False".
change_no_check
supports all ofchange
's variants.-
Variant
change_no_check term at num+? with term? in ident
Example
- Goal True -> False.
- 1 subgoal ============================ True -> False
- intro H.
- 1 subgoal H : True ============================ False
- change_no_check False in H.
- 1 subgoal H : False ============================ False
- exact H.
- No more subgoals.
- Fail Qed.
- The command has indeed failed with message: The term "fun H : True => H" has type "True -> True" while it is expected to have type "True -> False".
-
Variant
convert_concl_no_check term
¶ Deprecated since version 8.11.
Deprecated old name for
change_no_check
. Does not support any of its variants.
-
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 explanations.Example
- Goal False.
- 1 subgoal ============================ False
- exact_no_check I.
- No more subgoals.
- 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 subgoal ============================ False
- vm_cast_no_check I.
- No more subgoals.
- 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 the<