$\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{#1[] \vdash #2 \lra #3}} \newcommand{\WEVT}[3]{\mbox{#1[] \vdash #2 \lra}\\ \mbox{ #3}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}$

# 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¶

### Reserved keywords¶

The tactics described in this chapter reserve the following keywords:

by using


Thus, these keywords cannot be used as identifiers. It also declares the following character sequences as tokens:

** [= |-


### Invocation of tactics¶

A tactic is applied as an ordinary command. It may be preceded by a goal selector (see Section Goal selectors). If no selector is specified, the default selector is used.

::=
|
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 write 1:tac.

Using value ! enforces that all tactics are used either on a single focused goal or with a local selector (’’strict focusing mode’’).

Although other selectors are available, only all, ! or a single natural number are valid default goal selectors.

### Bindings¶

Tactics that take a term as an argument may also accept bindings to instantiate some parameters of the term by name or position. The general form of a term with bindings is termtac with bindings where bindings can take two different forms:

::=
( := term )+
|

### 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.

::=
*
|
**
|
_
|
?
|
::=
|
|
|
<-
|
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 with ident

• _ — 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 hypotheses H1: A and H2: B using the pattern (H1 & H2) or (H1, H2) or [H1 H2]. Example. This also works on A <-> 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 hypothesis H1: A and the second subgoal will have the hypothesis H2: B. Example

• split a hypothesis in either of the forms A /\ B or A \/ 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 of let-ins, the patterns are applied to the arguments and let-in variables.

• ( simple_intropattern+& ) — matches a right-hand nested term that consists of one or more nested binary inductive types such as a1 OP1 a2 OP2 ... (where the OPn are right-associative). (If the OPn are left-associative, additional parentheses will be needed to make the term right-hand nested, such as a1 OP1 (a2 OP2 ...).) The splitting pattern can have more than 2 names, for example (H1 & H2 & H3) matches A /\ 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 as A \/ B into multiple subgoals. The number of intropattern_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 as A /\ B into multiple hypotheses. Use [H1 [H2 H3]] to match A /\ B /\ C.

• [] — splits an inductive type: If the inductive type has multiple constructors, such as A \/ B, create one subgoal for each constructor. If the inductive type has a single constructor with multiple parameters, such as A /\ 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 either injection or discriminate. If injection is applicable, the intropattern is used on the hypotheses generated by injection. 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 to intros. Example

• simple_intropattern_closed % term* — first applies each of the terms with the apply … in tactic on the hypothesis to be introduced, then it uses simple_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".

Inductive or (A B:Prop) : Prop :=   | or_introl : A -> A \/ B   | or_intror : B -> A \/ B where "A \/ B" := (or A B) : type_scope. Inductive and (A B:Prop) : Prop :=   conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope.

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]. all: swap 1 2.
2 subgoals A, B : Prop HA : A ============================ True subgoal 2 is: True 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 [=] uses injection to strip (S ...) from both sides of the matched equality. The second uses discriminate on the contradiction 1 = 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 add H : S (length ys) = 1

• intros [=] would additionally apply injection to H to yield H0 : length ys = 0

• intros [=->%length_zero_iff_nil] applies the theorem, making H the equality l=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:

::=
|- ??
|
* |- ?
|
*
::=
-? 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 Implicit 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¶

Tactic exact term

This tactic applies to any goal. It gives directly the exact proof term of the goal. Let T be our goal, let p be a term of type U then exact p succeeds iff T and U are convertible (see Conversion rules).

Error Not an exact proof.
Variant eexact term.

This tactic behaves like exact but is able to handle terms and goals with existential variables.

Tactic assumption

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

Error No such assumption.
Variant eassumption

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

Tactic refine term

This tactic applies to any goal. It behaves like exact with a big difference: the user can leave some holes (denoted by _ or (_ : type)) in the term. refine will generate as many subgoals as there are remaining holes in the elaborated term. The type of holes must be either synthesized by the system or declared by an explicit cast like (_ : nat -> Prop). Any subgoal that occurs in other subgoals is automatically shelved, as if calling shelve_unifiable. The produced subgoals (shelved or not) are not candidates for typeclass resolution, even if they have a type-class type as conclusion, letting the user control when and how typeclass resolution is launched on them. 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 Invalid argument.

The tactic refine does not know what to do with the term you gave.

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 the combination of simple refine and notypeclasses refine: it performs type checking without resolution of typeclasses, does not perform beta reductions or shelve the subgoals.

Flag Debug Unification

Enables printing traces of unification steps used during elaboration/typechecking and the refine tactic.

Tactic 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 of term. 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 of term 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 of term is of the form P (t1 ... tn) with P 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 the ti and ui unify, then P is taken to be (fun x => Q). Otherwise, apply tries to define P by abstracting over t_1 ... t__n in the goal. See pattern 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 of term and the current goal. You can help the apply tactic by transforming your goal with the change or pattern 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.
Variant apply term with bindings

This also provides apply with values for instantiating premises. Here, variables are referred by names and non-dependent products by increasing numbers (see Bindings).

Variant apply term+,

This is a shortcut for apply term1; [.. | ... ; [ .. | apply termn] ... ], i.e. for the successive applications of termi+1 on the last subgoal generated by apply termi , starting from the application of term1.

Variant eapply term

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

Variant rapply term

The tactic rapply behaves like eapply but it uses the proof engine of refine for dealing with existential variables, holes, and conversion problems. This may result in slightly different behavior regarding which conversion problems are solvable. However, like apply but unlike eapply, rapply will fail if there are any holes which remain in term itself after typechecking and typeclass resolution but before unification with the goal. More technically, term is first parsed as a constr rather than as a uconstr or open_constr before being applied to the goal. Note that rapply prefers to instantiate as many hypotheses of term as possible. As a result, if it is possible to apply term to arbitrarily many arguments without getting a type error, rapply will loop.

Note that you need to Require Import Coq.Program.Tactics to make use of rapply.

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 of id ?foo and O.

Example

Definition id (x : nat) := x.
id is defined
Parameter H : forall x y, id x = 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 = ?M161" with "0 = 0".

Because it reasons modulo a limited amount of conversion, simple apply fails quicker than apply and it is then well-suited for uses in user-defined tactics that backtrack often. Moreover, it does not traverse tuples as apply does.

Variant simple? apply term with bindings?+,
Variant simple? eapply term with bindings?+,

This summarizes the different syntaxes for apply and eapply.

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 product A -> B with B possibly containing products. Then it generates two subgoals B->G and A. Applying lapply H (where H has type A->B and B does not start with a product) does the same as giving the sequence cut B. 2:apply H. where cut is described below.

Warning When term contains more than one non dependent product the tactic lapply only takes into account the first product.

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 (see apply … in).

Tactic apply term in ident

This tactic applies to any goal. The argument term is a term well-formed in the local context and the argument ident is an hypothesis of the context. The tactic apply term in ident tries to match the conclusion of the type of ident against a non-dependent premise of the type of term, trying them from right to left. If it succeeds, the statement of hypothesis ident is replaced by the conclusion of the type of term. The tactic also returns as many subgoals as the number of other non-dependent premises in the type of term and of the non-dependent premises of the type of ident. If the conclusion of the type of term 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 of ident. Tuples are decomposed in a width-first left-to-right order (for instance if the type of H1 is A <-> B and the type of H2 is A then apply H1 in H2 transforms the type of H2 into B). The tactic apply 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 of term.

Variant apply term+, in ident

This applies each term in sequence in ident.

Variant apply term with bindings+, in ident

This does the same but uses the bindings in each (ident := term) to instantiate the parameters of the corresponding type of term (see Bindings).

Variant eapply term with bindings?+, in ident

This works as apply … in but turns unresolved bindings into existential variables, if any, instead of failing.

Variant apply term with bindings?+, in ident as simple_intropattern

This works as apply … in then applies the simple_intropattern to the hypothesis ident.

Variant simple apply term in ident

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

Variant simple? apply term with bindings?+, in ident as simple_intropattern?
Variant simple? eapply term with bindings?+, in ident as simple_intropattern?

This summarizes the different syntactic variants of apply term in ident and eapply term in ident.

Tactic constructor num

This tactic applies to a goal such that its conclusion is an inductive type (say I). The argument num must be less or equal to the numbers of constructor(s) of I. Let ci be the i-th constructor of I, then constructor i is equivalent to intros; apply ci.

Error Not an inductive product.
Error Not enough constructors.
Variant constructor

This tries constructor 1 then constructor 2, ..., then constructor n where n is the number of constructors of the head of the goal.

Variant constructor num with bindings

Let c be the i-th constructor of I, then constructor i with bindings is equivalent to intros; apply c with bindings.

Warning

The terms in bindings are checked in the context where constructor is executed and not in the context where apply is executed (the introductions are not taken into account).

Variant split with bindings?

This applies only if I has a single constructor. It is then equivalent to constructor 1 with bindings?. It is typically used in the case of a conjunction $$A \wedge B$$.

Variant exists bindings

This applies only if I has a single constructor. It is then equivalent to intros; constructor 1 with bindings. It is typically used in the case of an existential quantification $$\exists x, P(x).$$

Variant exists bindings+,

This iteratively applies exists bindings.

Error Not an inductive goal with 1 constructor.
Variant left with bindings?
Variant right with bindings?

These tactics apply only if I has two constructors, for instance in the case of a disjunction $$A \vee B$$. Then, they are respectively equivalent to constructor 1 with bindings? and constructor 2 with bindings?.

Error Not an inductive goal with 2 constructors.
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 and apply).

Flag Debug Tactic Unification

Enables printing traces of unification steps in tactic unification. Tactic unification is used in tactics such as apply and rewrite.

## Managing the local context¶

Tactic intro

This tactic applies to a goal that is either a product or starts with a 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 (resp let x:=t in U) then intro puts x:T (resp x:=t) in the local context. The new subgoal is U.

If the goal is a non-dependent product $$T \rightarrow U$$, then it puts in the local context either Hn:T (if T is of type Set or Prop) or Xn:T (if the type of T is Type). The optional index n is such that Hn or Xn is a fresh identifier. In both cases, the new subgoal is U.

If the goal is an existential variable, intro forces the resolution of the existential variable into a dependent product $$\forall$$ x:?X, ?Y, puts x:?X in the local context and leaves ?Y as a new subgoal allowed to depend on x.

The tactic intro applies the tactic hnf until intro can be applied or the goal is not head-reducible.

Error No product even after head-reduction.
Variant intro ident

This applies intro but forces ident to be the name of the introduced hypothesis.

Error ident is already used.

Note

If a name used by intro hides the base name of a global constant then the latter can still be referred to by a qualified name (see Qualified identifiers).

Variant intros

This repeats intro until it meets the head-constant. It never reduces head-constants and it never fails.

Variant intros ident+.

This is equivalent to the composed tactic intro ident; ... ; intro ident.

Variant intros until ident

This repeats intro until it meets a premise of the goal having the form (ident : type) and discharges the variable named ident of the current goal.

Error No such hypothesis in current goal.
Variant intros until num

This repeats intro until the num-th non-dependent product.

Example

On the subgoal forall x y : nat, x = y -> y = x the tactic intros until 1 is equivalent to intros x y H, as x = y -> y = x is the first non-dependent product.

On the subgoal forall x y z : nat, x = y -> y = x the tactic intros until 1 is equivalent to intros x y z as the product on z 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.

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 hypothesis ident2, before the hypothesis ident2, 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 to intro ident1? followed by the appropriate call to move … after …, move … before …, move … at top, or move … at bottom.

Note

intro at bottom is a synonym for intro with no argument.

Error No such hypothesis: ident.
Tactic intros intropattern_list

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

Tactic eintros intropattern_list

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

Tactic clear ident

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

Error No such hypothesis.
Error ident is used in the conclusion.
Error ident is used in the hypothesis ident.
Variant clear ident+

This is equivalent to clear ident. ... clear ident.

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.

Variant clear dependent ident

This clears the hypothesis ident and all the hypotheses that depend on it.

Variant clearbody ident+

This tactic expects ident+ to be local definitions and clears their respective bodies. In other words, it turns the given definitions into assumptions.

Error ident is not a local definition.
Tactic revert ident+

This applies to any goal with variables ident+. It moves the hypotheses (possibly defined) to the goal, if this respects dependencies. This tactic is the inverse of intro.

Error No such hypothesis.
Error ident1 is used in the hypothesis ident2.
Variant revert dependent ident

This moves to the goal the hypothesis ident and all the hypotheses that depend on it.

Tactic move ident1 after ident2

This moves the hypothesis named ident1 in the local context after the hypothesis named ident2, where “after” is in reference to the direction of the move. The proof term is not changed.

If ident1 comes before ident2 in the order of dependencies, then all the hypotheses between ident1 and ident2 that (possibly indirectly) depend on ident1 are moved too, and all of them are thus moved after ident2 in the order of dependencies.

If ident1 comes after ident2 in the order of dependencies, then all the hypotheses between ident1 and ident2 that (possibly indirectly) occur in the type of ident1 are moved too, and all of them are thus moved before ident2 in the order of dependencies.

Variant move ident1 before ident2

This moves ident1 towards and just before the hypothesis named ident2. As for move … after …, dependencies over ident1 (when ident1 comes before ident2 in the order of dependencies) or in the type of ident1 (when ident1 comes after ident2 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.
Error Cannot move ident1 after ident2: it occurs in the type of ident2.
Error Cannot move ident1 after ident2: it depends on ident2.

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
Tactic rename ident1 into ident2

This renames hypothesis ident1 into ident2 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 into identj 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.
Tactic set (ident := term)

This replaces term by ident in the conclusion of the current goal and adds the new definition ident := 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.

Error The variable ident is already defined.
Variant set (ident := term) in goal_occurrences

This notation allows specifying which occurrences of term have to be substituted in the context. The in goal_occurrences clause is an occurrence clause whose syntax and behavior are described in goal occurrences.

Variant set (ident binder* := term) in goal_occurrences?

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

Variant set term in goal_occurrences?

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

Variant eset (ident binder* := term) in goal_occurrences?
Variant eset term in goal_occurrences?

While the different variants of set expect that no existential variables are generated by the tactic, eset removes this constraint. In practice, this is relevant only when eset is used as a synonym of epose, i.e. when the term does not occur in the goal.

Tactic 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. Use naming_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 of term 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.

Tactic pose (ident := term)

This adds the local definition ident := term to the current context without performing any replacement in the goal or in the hypotheses. It is equivalent to set (ident := term) in |-.

Variant pose (ident binder* := term)

This is equivalent to pose (ident := fun binder* => term).

Variant pose term

This behaves as pose (ident := term) but ident is generated by Coq.

Variant epose (ident binder* := term)
Variant epose term

While the different variants of pose expect that no existential variables are generated by the tactic, epose removes this constraint.

Tactic decompose [qualid+] term

This tactic recursively decomposes a complex proposition in order to obtain atomic ones.

Example

Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
1 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).

Variant decompose record term

This decomposes record types (inductive types with one constructor, like and and exists and those defined with the Record command.

## Controlling the proof flow¶

Tactic assert (ident : type)

This tactic applies to any goal. assert (H : U) adds a new hypothesis of name H asserting U to the current goal and opens a new subgoal U 2. The subgoal U 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 type Prop, Set nor Type.

Variant assert type

This behaves as assert (ident : type) but ident is generated by Coq.

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.
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, if simple_intropattern is ident, the tactic behaves like assert (ident : type)). If simple_intropattern is an action introduction pattern, the tactic behaves like assert 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.

Variant assert (ident := term)

This behaves as assert (ident : type) by exact term where type is the type of term. This is equivalent to using pose proof. If the head of term is ident, the tactic behaves as specialize.

Error Variable ident is already declared.
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 where type is the type of term. In particular, pose proof term as ident behaves as assert (ident := term) and pose proof term as simple_intropattern is the same as applying the simple_intropattern to term.

Variant epose proof term as simple_intropattern?

While pose proof expects that no existential variables are generated by the tactic, epose proof removes this constraint.

Variant pose proof (ident := term)

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

Variant epose proof (ident := term)

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

Variant enough (ident : type)

This adds a new hypothesis of name ident asserting type to the goal the tactic enough is applied to. A new subgoal stating type is inserted after the initial goal rather than before it as assert would do.

Variant enough type

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

Variant enough type as simple_intropattern

This behaves like enough type using simple_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 assumption type is added and possibly destructed. If the as 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 goal T into the two following subgoals: U -> T and U. The subgoal U -> T comes first in the list of remaining subgoal to prove.

Variant specialize (ident term*) as simple_intropattern?
Variant specialize ident with bindings as simple_intropattern?

This tactic works on local hypothesis ident. The premises of this hypothesis (either universal quantifications or non-dependent implications) are instantiated by concrete terms coming either from arguments term* or from Bindings. In the first form the application to term* can be partial. The first form is equivalent to assert (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 the as clause, the local hypothesis ident is left unchanged and instead, the modified hypothesis is introduced as specified by the simple_intropattern. The name ident can also refer to a global lemma or hypothesis. In this case, for compatibility reasons, the behavior of specialize is close to that of generalize: the instantiated statement becomes an additional premise of the goal. The as clause is especially useful in this case to immediately introduce the instantiated statement as a local hypothesis.

Error ident is used in hypothesis ident.
Error ident is used in conclusion.
Tactic generalize term

This tactic applies to any goal. It generalizes the conclusion with respect to some term.

Example

Goal forall x y:nat, 0 <= x + y + y.
1 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 of term (counting from left to right on the expression printed using the Printing All flag).

Variant generalize term as ident

This is equivalent to generalize term but it uses ident 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.

Tactic evar (ident : term)

The evar tactic creates a new local definition named ident with type term in the context. The body of this binding is a fresh existential variable.

Tactic instantiate (ident := term )

The instantiate tactic refines (see refine) an existential variable ident with the term term. It is equivalent to only [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.

Tactic admit

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

Variant give_up

Synonym of admit.

Tactic absurd term

This tactic applies to any goal. The argument term is any proposition P of type Prop. This tactic applies False elimination, that is it deduces the current goal from False, and generates as subgoals ∼P and P. It is very useful in proofs by cases, where some cases are impossible. In most cases, P or ∼P is one of the hypotheses of the local context.

Tactic contradiction

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

Error No such assumption.
Variant contradiction ident

The proof of False is searched in the hypothesis named ident.

Tactic contradict ident

This tactic allows manipulating negated hypothesis and goals. The name ident should correspond to a hypothesis. With contradict H, the current goal and context is transformed in the following way:

• H:¬A ⊢ B becomes ⊢ A

• H:¬A ⊢ ¬B becomes H: B ⊢ A

• H: A ⊢ B becomes ⊢ ¬A

• H: A ⊢ ¬B becomes H: B ⊢ ¬A

Tactic exfalso

This tactic implements the “ex falso quodlibet” logical principle: an elimination of False is performed on the current goal, and the user is then required to prove that False is indeed provable in the current context. This tactic is a macro for elimtype False.

## Case analysis and induction¶

The tactics presented in this section implement induction or case analysis on inductive or co-inductive objects (see Theory of inductive definitions).

Tactic 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 of term, i.e. one for each constructor of the inductive or co-inductive type. Unlike induction, no induction hypothesis is generated by destruct.

Variant destruct ident

If ident denotes a quantified variable of the conclusion of the goal, then destruct ident behaves as intros until ident; destruct ident. If ident is not anymore dependent in the goal after application of destruct, it is erased (to avoid erasure, use parentheses, as in destruct (ident)).

If ident is a hypothesis of the context, and ident is not anymore dependent in the goal after application of destruct, it is erased (to avoid erasure, use parentheses, as in destruct (ident)).

Variant destruct num

destruct num behaves as intros until num followed by destruct applied to the last introduced hypothesis.

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+,

This is a shortcut for destruct term; ...; destruct term.

Variant destruct term as or_and_intropattern_loc

This behaves as destruct term but uses the names in or_and_intropattern_loc to name the variables introduced in the context. The or_and_intropattern_loc must have the form [p11 ... p1n | ... | pm1 ... pmn ] with m being the number of constructors of the type of term. Each variable introduced by destruct in the context of the i-th goal gets its name from the list pi1 ... pin in order. If there are not enough names, destruct invents names for the remaining variables to introduce. More generally, the pij can be any introduction pattern (see intros). 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 between term and the value that it takes in each of the possible cases. The name of the equation is specified by naming_intropattern (see intros), in particular ? can be used to let Coq generate a fresh name.

Variant destruct term with bindings

This behaves like destruct term providing explicit instances for the dependent premises of the type of term.

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 of term is not inferable. Instead, the unresolved instances are left as existential variables to be inferred later, in the same way as eapply does.

Variant destruct term using term with bindings?

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

Variant destruct term in goal_occurrences

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

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

These are the general forms of destruct and edestruct. They combine the effects of the with, as, eqn:, using, and in clauses.

Tactic case term

The tactic case is a more basic tactic to perform case analysis without recursion. It behaves as elim term but using a case-analysis elimination principle and not a recursive one.

Variant case term with bindings

Analogous to elim term with bindings above.

Variant ecase term with bindings?

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

Variant simple destruct ident

This tactic behaves as intros until ident; case ident when ident is a quantified variable of the goal.

Variant simple destruct num

This tactic behaves as intros until num; case ident where ident is the name given by intros until num to the num -th non-dependent premise of the goal.

Variant case_eq term

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

Tactic induction term

This tactic applies to any goal. The argument term must be of inductive type and the tactic induction generates subgoals, one for each possible form of term, 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 as intros until ident; induction ident. If ident is not anymore dependent in the goal after application of induction, it is erased (to avoid erasure, use parentheses, as in induction (ident)).

• If term is a num, then induction num behaves as intros until num followed by induction 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, and ident is not anymore dependent in the goal after application of induction, it is erased (to avoid erasure, use parentheses, as in induction (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
exact (le_n 0).
1 subgoal n : nat H : S n = S n IHn : n = n -> n <= n ============================ S n <= S n
Error Not an inductive product.
Error Unable to find an instance for the variables ident ... ident.

Use in this case the variant elim … with below.

Variant induction term as or_and_intropattern_loc

This behaves as induction but uses the names in or_and_intropattern_loc to name the variables introduced in the context. The or_and_intropattern_loc must typically be of the form [ p 11 ... p 1n | ... | pm1 ... pmn ] with m being the number of constructors of the type of term. Each variable introduced by induction in the context of the i-th goal gets its name from the list pi1 ... pin in order. If there are not enough names, induction invents names for the remaining variables to introduce. More generally, the pij can be any disjunctive/conjunctive introduction pattern (see intros …). For instance, for an inductive type with one constructor, the pattern notation (p1 , ... , pn ) can be used instead of [ p1 ... pn ].

Variant induction term with bindings

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

Variant einduction term

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

Variant induction term using term

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

Variant induction term using term with bindings

This behaves as induction … using … but also providing instances for the premises of the type of the second term.

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 by Function or Functional 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. The in goal_occurrences clause is an occurrence clause whose syntax and behavior is described in occurrences sets. If variables or hypotheses not mentioning term in their type are listed in goal_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 as or_and_intropattern_loc using term with bindings in goal_occurrences
Variant einduction term with bindings as or_and_intropattern_loc using term with bindings in goal_occurrences

These are the most general forms of induction and einduction. 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 tactic elim chooses the appropriate destructor and applies it as the tactic apply would do. For instance, if the proof context contains n:nat and the current goal is T of type Prop, then elim n is equivalent to apply nat_ind with (n:=n). The tactic elim 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 of term is a statement with premises and whose conclusion is inductive. In that case the tactic performs induction on the conclusion of the type of term 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

Allows to give explicit instances to the premises of the type of term (see Bindings).

Variant eelim term

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

Variant elim term using term
Variant elim term using term with bindings

Allows the user to give explicitly an induction principle term that is not the standard one for the underlying inductive type of term. The bindings clause allows instantiating premises of the type of term.

Variant elim term with bindings using term with bindings
Variant eelim term with bindings using term with bindings

These are the most general forms of elim and eelim. It combines the effects of the using clause and of the two uses of the with clause.

Variant elimtype type

The argument type must be inductively defined. elimtype I is equivalent to cut I. intro Hn; elim Hn; clear Hn. Therefore the hypothesis Hn will not appear in the context(s) of the subgoal(s). Conversely, if t is a term of (inductive) type I that does not occur in the goal, then elim t is equivalent to elimtype I; 2:exact t.

Variant simple induction ident

This tactic behaves as intros until ident; elim ident when ident is a quantified variable of the goal.

Variant simple induction num

This tactic behaves as intros until num; elim ident where ident is the name given by intros until num to the num-th non-dependent premise of the goal.

Tactic double induction ident ident

This tactic is deprecated and should be replaced by induction ident; induction ident (or induction 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 where num3 is the result of num2 - num1

Tactic dependent induction ident

The experimental tactic dependent induction performs induction- inversion on an instantiated inductive predicate. One needs to first require the Coq.Program.Equality module to use this tactic. The tactic is based on the BasicElim tactic by Conor McBride [McB00] and the work of Cristina Cornes around inversion [CT95]. From an instantiated inductive predicate and a goal, it generates an equivalent goal where the hypothesis has been generalized over its indexes which are then constrained by equalities to be the right instances. This permits to state lemmas without resorting to manually adding these equalities and still get enough information in the proofs.

Example

Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
1 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 uses destruct instead of induction on the generalized hypothesis. This gives results equivalent to inversion or dependent inversion if the hypothesis is dependent.

See also the larger example of dependent induction and an explanation of the underlying technique.

Tactic discriminate term

This tactic proves any goal from an assumption stating that two structurally different terms 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 conclusion term = 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 subterms u and w (u subterm of the normal form of term and w subterm of the normal form of term), 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 by discriminate ident where ident is the identifier for the last introduced hypothesis.

Variant discriminate term with bindings

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

Variant ediscriminate num
Variant ediscriminate term with bindings?

This works the same as discriminate but if the type of term, or the type of the hypothesis referred to by num, 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 which discriminate is applicable; if the current goal is of the form term <> term, this behaves as intro ident; discriminate ident.

Error No discriminable equalities.
Tactic injection term

The injection tactic exploits the property that constructors of inductive types are injective, i.e. that if c is a constructor of an inductive type and c t1 and c t2 are equal then t1 and t2 are equal too.

If term is a proof of a statement of conclusion term = term, then injection applies the injectivity of constructors as deep as possible to derive the equality of all the subterms of term and term at positions where the terms start to differ. For example, from (S p, S n) = (q, S (S m)) we may derive S p = q and n = 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 t1 ... tn ) and (P u1 ... un ). If t1 and u1 are the same and have for type an inductive type for which a decidable equality has been declared using Scheme 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, then injection ident first introduces the hypothesis in the local context using intros 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 by injection ident where ident is the identifier for the last introduced hypothesis.

Variant injection term with bindings

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

Variant einjection num
Variant einjection term with bindings?

This works the same as injection but if the type of term, or the type of the hypothesis referred to by num, has uninstantiated parameters, these parameters are left as existential variables.

Variant injection

If the current goal is of the form term <> term , this behaves as intro ident; injection ident.

Error goal does not satisfy the expected preconditions.
Variant injection term with bindings? as simple_intropattern+
Variant injection num as simple_intropattern+
Variant injection as simple_intropattern+
Variant einjection term with bindings? as simple_intropattern+
Variant einjection num as simple_intropattern+
Variant einjection as simple_intropattern+

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

Variant injection term with bindings? as injection_intropattern
Variant injection num as injection_intropattern
Variant injection as injection_intropattern
Variant einjection term with bindings? 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 which intros uses. In particular as [= simple_intropattern+] behaves the same as as simple_intropattern+.

Flag Structural Injection

This flag ensures that injection term erases the original hypothesis and leaves the generated equalities in the context rather than putting them as antecedents of the current goal, as if giving injection term as (with an empty list of names). This flag is off by default.

Flag Keep Proof Equalities

By default, injection only creates new equalities between terms whose type is in sort Type or Set, thus implementing a special behavior for objects that are proofs of a statement in Prop. This flag controls this behavior.

Tactic inversion ident

Let the type of ident in the local context be (I t), where I is a (co)inductive predicate. Then, inversion applied to ident derives for each possible constructor c i of (I t), all the necessary conditions that should hold for the instance (I t) to be proved by c i.

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 terms 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 then inversion ident where ident is the identifier for the last introduced hypothesis.

Variant inversion_clear ident

This behaves as inversion and then erases ident from the context.

Variant inversion ident as or_and_intropattern_loc

This generally behaves as inversion but using names in or_and_intropattern_loc for naming hypotheses. The or_and_intropattern_loc must have the form [p11 ... p1n | ... | pm1 ... pmn ] with m being the number of constructors of the type of ident. Be careful that the list must be of length m even if inversion discards some cases (which is precisely one of its roles): for the discarded cases, just use an empty list (i.e. n = 0).The arguments of the i-th constructor and the equalities that inversion introduces in the context of the goal corresponding to the i-th constructor, if it exists, get their names from the list pi1 ... pin 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 (because inversion applies injection on the equalities it generates), the corresponding name pij in the list must be replaced by a sublist of the form [pij1 ... pijq ] (or, equivalently, (pij1 , ..., pijq )) where q is the number of subequalities obtained from splitting the original equation. Here is an example. The inversion ... as variant of inversion generally behaves in a slightly more expectable way than inversion (no artificial duplication of some hypotheses referring to other hypotheses). To take benefit of these improvements, it is enough to use inversion ... 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 if inversion were called, even though the inversion_clear will eventually erase the hypotheses.

Variant inversion ident in ident+

Let ident+ be identifiers in the local context. This tactic behaves as generalizing ident+, and then performing inversion.

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 generalizing ident+, and then performing inversion_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 like inversion and then substitutes ident 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 that ident 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) and I has type forall (x:T), s, then term must be of type I:forall (x:T), I x -> s' where s' is the type of the goal.

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 clears ident from the local context.

Variant dependent inversion_clear ident as or_and_intropattern_loc with term

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

Variant simple inversion ident

It is a very primitive inversion tactic that derives all the necessary equalities but it does not simplify the constraints as inversion does.

Variant simple inversion ident as or_and_intropattern_loc

This allows naming the hypotheses introduced in the context by simple inversion.

Tactic inversion ident using ident

Let ident have type (I t) (I an inductive predicate) in the local context, and ident 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 doing inversion 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 hypothesis H : x = y and a hypothesis of type rew H in p = q); these hypotheses can subsequently be simplified using subst, 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 invoke induction H as [H1 H2] using eq_sigT_rect. This tactic also works for sig, sigT2, and sig2, and there are similar eq_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.
Tactic 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 number num 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 least num 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 identifiers ident are the names of the induction hypotheses. The identifiers ident are the respective names of the premises on which the induction is performed in the statements to be simultaneously proved (if not given, the system tries to guess itself what they are).

Tactic cofix ident

This tactic starts a proof by coinduction. The identifier ident is the name given to the coinduction hypothesis. Like in a cofix expression, the use of induction hypotheses have to guarded by a constructor. The verification that the use of 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 command Guarded (see Section Requesting information).

Variant cofix ident with (ident binder+ : type)+

This starts a proof by mutual coinduction. The statements to be simultaneously proved are respectively forall binder ... binder, type The identifiers ident are the names of the coinduction hypotheses.

## 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.

Tactic rewrite term

This tactic applies to any goal. The type of term must have the form

forall (x1 :A1 ) ... (xn :An ), eq term1 term2 .

where eq is the Leibniz equality or a registered setoid equality.

Then rewrite term finds the first subterm matching term1 in the goal, resulting in instances term1' and term2' and then replaces every occurrence of term1' by term2'. Hence, some of the variables xi are solved by unification, and some of the types A1, ..., An become new subgoals.

Error The term provided does not end with an equation.
Error Tactic generated a subgoal identical to the original goal. This happens if term does not occur in the goal.
Variant rewrite -> term

Is equivalent to rewrite term

Variant rewrite <- term

Uses the equality term1 = term 2 from right to left

Variant rewrite term in goal_occurrences

Analogous to rewrite term but rewriting is done following the clause goal_occurrences. For instance:

• rewrite H in H' will rewrite H in the hypothesis H' instead of the current goal.

• rewrite H in H' at 1, H'' at - 2 |- * means rewrite 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 do rewrite H in H' for all hypotheses H' different from H. A success will happen as soon as at least one of these simpler tactics succeeds.

• rewrite H in * is a combination of rewrite H and rewrite H in * |- that succeeds if at least one of these two tactics succeeds.

Orientation -> or <- can be inserted before the term to rewrite.

Variant rewrite term at occurrences

Rewrite only the given occurrences of term. 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 to Import 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 tactics rewrite term+;, each one working on the first subgoal generated by the previous one. An orientation -> or <- can be inserted before each term 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 tactic rewrite ?term performs the rewrite of term as many times as possible (perhaps zero time). This form never fails.

• num? : works similarly, except that it will do at most num rewrites.

• ! : works as ?, except that at least one rewrite should succeed, otherwise the tactic fails.

• num! (or simply num) : precisely num rewrites of term will be done, leading to failure if these num 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 as rewrite 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.

Tactic replace term with term’

This tactic applies to any goal. It replaces all free occurrences of term in the current goal with term’ and generates an equality term = term’ as a subgoal. This equality is automatically solved if it occurs among the assumptions, or if its symmetric form occurs. It is equivalent to cut term = term’; [intro Hn ; rewrite <- Hn ; clear Hn|| 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 applies tactic to solve the generated subgoal term = term’.

Variant replace term

Replaces term with term’ using the first assumption whose type has the form term = term’ or term’ = term.

Variant replace -> term

Replaces term with term’ using the first assumption whose type has the form term = term’

Variant replace <- term

Replaces term with term’ using the first assumption whose type has the form term’ = 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 any type of nor value of.

Variant cutrewrite <-​->? (term1 = term2) in ident?

Deprecated since version 8.5: Use replace instead.

Tactic subst ident

This tactic applies to a goal that has ident in its context and (at least) one hypothesis, say H, of type ident = t or t = ident with ident not occurring in t. Then it replaces ident by t everywhere in the goal (in the hypotheses and in the conclusion) and clears ident and H from the context.

If ident is a local definition of the form ident := t, it is also unfolded and cleared.

If ident is a section variable it is expected to have no indirect occurrences in the goal, i.e. that no global declarations implicitly depending on the section variable must be present in the goal.

Note

• When several hypotheses have the form ident = t or t = ident, the first one is used.

• If H is itself dependent in the goal, it is replaced by the proof of reflexivity of equality.

Variant subst ident+

This is equivalent to subst ident1; ...; subst identn.

Variant subst

This applies subst repeatedly from top to bottom to all hypotheses of the context for which an equality of the form ident = t or t = ident or ident := t exists, with ident not occurring in t and ident not a section variable with indirect dependencies in the goal.

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 ident1 = ident2 and ident1 = t, or t′ = ident1 with t′ not a variable, and no other hypotheses of the form ident2 = u or u = ident2; without the flag, a second call to subst would be necessary to replace ident2 by t or t′ 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 ident1 = f ident2 and ident2 = g ident1 which without the flag would be a cause of failure of subst.

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 form ident = u, or u′ = ident with u′ not a variable. Finally, it preserves the initial order of hypotheses, which without the flag it may break. default.

Error Cannot find any non-recursive equality over :n:ident.
Error Section variable :n:ident occurs implicitly in global declaration :n:qualid present in hypothesis :n:ident.
Error Section variable :n:ident occurs implicitly in global declaration :n:qualid present in the conclusion.

Raised when the variable is a section variable with indirect dependencies in the goal.

Tactic stepl term

This tactic is for chaining rewriting steps. It assumes a goal of the form R term term where R is a binary relation and relies on a database of lemmas of the form forall x y z, R x y -> eq x z -> R z y where eq is typically a setoid equality. The application of stepl term then replaces the goal by R term term and adds a new goal stating eq term term.

Command Declare Left Step term

Adds term to the database used by stepl.

This tactic is especially useful for parametric setoids which are not accepted as regular setoids for rewrite and setoid_replace (see Generalized rewriting).

Variant stepl term by tactic

This applies stepl term then applies tactic to the second goal.

Variant stepr term by tactic

This behaves as stepl but on the right-hand-side of the binary relation. Lemmas are expected to be of the form forall x y z, R x y -> eq y z -> R x z.

Command Declare Right Step term

Adds term to the database used by stepr.

Tactic change term

This tactic applies to any goal. It implements the rule Conv given in Subtyping rules. change U replaces the current goal T with U providing that U is well-formed and that T and U are convertible.

Error Not convertible.
Variant change term with term’

This replaces the occurrences of term by term’ in the current goal. The term term and term’ must be convertible.

Variant change term at num+ with term’

This replaces the occurrences numbered num+ of term by term’ in the current goal. The terms term and term’ must be convertible.

Error Too few occurrences.
Variant change term at num+? with term? in ident

This applies the change tactic not to the goal but to the hypothesis ident.

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.

## Performing computations¶

::=
red
|
hnf
|
simpl
|
cbv
|
cbn
|
lazy
|
compute
|
vm_compute
|
native_compute
|
unfold
|
fold
|
pattern
::=
-? [ ]
::=
beta
|
iota
|
match
|
fix
|
cofix
|
zeta
|
delta
|
::=
+
|
::=
::=

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 hypotheses ident+

• in ident+ |- * in hypotheses ident+ and in the conclusion

• in * |- in every hypothesis

• in * (equivalent to in * |- *) everywhere

• in (type of ident) (value of ident) ... |- in type part of ident, in the value part of ident, etc.

For backward compatibility, the notation in ident+ performs the conversion in hypotheses ident+.

Tactic cbv strategy_flag?
Tactic lazy strategy_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 and cofix expressions) and $$\zeta$$ (contraction of local definitions), the flags are either beta, delta, match, fix, cofix, iota or zeta. The iota flag is a shorthand for match, fix and cofix. The delta flag itself can be refined into delta [ qualid+ ] or delta - [ 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 the delta flag does not apply to variables bound by a let-in construction inside the term itself (use here the zeta 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 , or match 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 proposition exists x. P(x) reduce to a pair of a witness t, and a proof that t satisfies the predicate P. Most of the time, t may be computed without computing the proof of P(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 and lazy 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 Timing

This flag causes all calls to the native compiler to print timing information for the conversion to native code, compilation, execution, and reification phases of native compilation. Timing is printed in units of seconds of wall-clock time.

Flag NativeCompute Profiling

On Linux, if you have the perf profiler installed, this flag makes it possible to profile native_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 of native_compute in a script. From the Linux command line, run perf report on the profile file to see the results. Consult the perf documentation for more details.

Flag Debug Cbv

This flag makes cbv (and its derivative compute) print information about the constants it encounters and the unfolding decisions it makes.

Tactic red

This tactic applies to a goal that has the form:

forall (x:T1) ... (xk:Tk), T


with T $$\beta$$$$\iota$$$$\zeta$$-reducing to c t1 ... tn and c a constant. If c is transparent then it replaces c with its definition (say t) and then reduces (t t1 ... tn ) according to $$\beta$$$$\iota$$$$\zeta$$-reduction rules.

Error Not reducible.
Error No head constant to reduce.
Tactic 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. The behavior of both hnf can be tuned using the Arguments command.

Example: The term fun n : nat => S n + S n is not reduced by hnf.

Note

The $$\delta$$ rule only applies to transparent constants (see Controlling the reduction strategies and the conversion algorithm on transparency and opacity).

Tactic cbn
Tactic 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 for simpl.

The cbn tactic accepts the same flags as cbv and lazy. The behavior of both simpl and cbn can be tuned using the Arguments command.

Notice that only transparent constants whose name can be reused in the recursive calls are possibly unfolded by simpl. For instance a constant defined by plus' := plus is possibly unfolded and reused in the recursive calls, but a constant such as succ := plus (S O) is never unfolded. This is the main difference between simpl and cbn. The tactic cbn reduces whenever it will be able to reuse it or not: succ t is reduced to S t.

Variant cbn [ qualid+ ]
Variant cbn - [ qualid+ ]

These are respectively synonyms of cbn beta delta [ qualid+ ] iota zeta and cbn beta delta - [ qualid+ ] iota zeta (see cbn).

Variant simpl pattern

This applies simpl only to the subterms matching pattern in the current goal.

Variant simpl pattern at num+

This applies simpl only to the num+ occurrences of the subterms matching pattern in the current goal.

Error Too few occurrences.
Variant simpl qualid
Variant simpl string

This applies simpl only to the applicative subterms whose head occurrence is the unfoldable constant qualid (the constant can be referred to by its notation using string if such a notation exists).

Variant simpl qualid at num+
Variant simpl string at num+

This applies simpl only to the num+ applicative subterms whose head occurrence is qualid (or string).

Flag Debug RAKAM

This flag makes cbn print various debugging information. RAKAM is the Refolding Algebraic Krivine Abstract Machine.

Tactic unfold qualid

This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see Top-level definitions and Controlling the reduction strategies and the conversion algorithm). The tactic unfold applies the $$\delta$$ rule to each occurrence of the constant to which qualid refers in the current goal and then replaces it with its $$\beta\iota\zeta$$-normal form. Use the general reduction tactics if you want to avoid this final reduction, for instance cbv 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 7-9: > unfold le. > ^^ Error: Cannot turn inductive le into an evaluable reference.

This error can also be raised if you are trying to unfold something that has been marked as opaque.

Example

Goal 1 + 0 = 1.
1 subgoal ============================ 1 + 0 = 1
Toplevel input, characters 0-14: > unfold Nat.add. > ^^^^^^^^^^^^^^ Error: Nat.add is opaque.
Variant unfold qualid in goal_occurrences

Replaces qualid in hypothesis (or hypotheses) designated by goal_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 of qualid to be unfolded. Occurrences are located from left to right.

Error Bad occurrence number of qualid.
Error qualid does not occur.
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 where string gets its interpretation from the scope bound to the delimiting key ident instead of its default interpretation (see Local interpretation rules for notations).

Variant unfold qualid​string%ident? at occurrences?+, in goal_occurrences?

This is the most general form.

Tactic fold term

This tactic applies to any goal. The term term is reduced using the red tactic. Every occurrence of the resulting term in the goal is then replaced by term. 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, the fold 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
Variant fold term+

Equivalent to fold term ; ... ; fold term.

Tactic 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 (say T) by

• replacing all occurrences of term in T with a fresh variable

• abstracting this variable

• applying the abstracted goal to term

For instance, if the current goal T is expressible as $$\varphi$$(t) where the notation captures all the instances of t in $$\varphi$$(t), then pattern t transforms it into (fun x:A => $$\varphi$$(x)) t. This tactic can be used, for instance, when the tactic apply fails on matching.

Variant pattern term at num+

Only the occurrences num+ of term 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+ of term are considered for $$\beta$$-expansion. Occurrences are located from left to right.

Variant pattern term+,

Starting from a goal $$\varphi$$(t1 ... tm), the tactic pattern t1, ..., tm generates the equivalent goal (fun (x1:A1) ... (xm :Am ) =>$$\varphi$$(x1 ... xm )) t1 ... tm. If ti occurs in one of the generated types Aj these occurrences will also be considered and possibly abstracted.

Variant pattern term at num++,

This behaves as above but processing only the occurrences num+ of term starting from term.

Variant pattern term at -? num+,?+,

This is the most general syntax that combines the different variants.

Tactic with_strategy strategy_level_or_var [ reference+ ] ltac_expr3

Executes ltac_expr3, applying the alternate unfolding behavior that the Strategy command controls, but only for ltac_expr3. This can be useful for guarding calls to reduction in tactic automation to ensure that certain constants are never unfolded by tactics like simpl and cbn or to ensure that unfolding does not fail.

Example

Opaque id.
Goal id 10 = 10.
1 subgoal ============================ id 10 = 10
Fail unfold id.
The command has indeed failed with message: id is opaque.
with_strategy transparent [id] unfold id.
1 subgoal ============================ 10 = 10

Warning

Use this tactic with care, as effects do not persist past the end of the proof script. Notably, this fine-tuning of the conversion strategy is not in effect during Qed nor Defined, so this tactic is most useful either in combination with abstract, which will check the proof early while the fine-tuning is still in effect, or to guard calls to conversion in tactic automation to ensure that, e.g., unfold does not fail just because the user made a constant Opaque.

This can be illustrated with the following example involving the factorial function.

Fixpoint fact (n : nat) : nat :=   match n with   | 0 => 1   | S n' => n * fact n'   end.
fact is defined fact is recursively defined (guarded on 1st argument)

Suppose now that, for whatever reason, we want in general to unfold the id function very late during conversion:

Strategy 1000 [id].

If we try to prove id (fact n) = fact n by reflexivity, it will now take time proportional to $$n!$$, because Coq will keep unfolding fact and * and + before it unfolds id, resulting in a full computation of fact n (in unary, because we are using nat), which takes time $$n!$$. We can see this cross the relevant threshold at around $$n = 9$$:

Goal True.
1 subgoal ============================ True
Time assert (id (fact 8) = fact 8) by reflexivity.
Finished transaction in 0.523 secs (0.307u,0.215s) (successful) 1 subgoal H : id (fact 8) = fact 8 ============================ True
Time assert (id (fact 9) = fact 9) by reflexivity.
Finished transaction in 1.936 secs (1.755u,0.18s) (successful) 1 subgoal H : id (fact 8) = fact 8 H0 : id (fact 9) = fact 9 ============================ True

Note that behavior will be the same if you mark id as Opaque because while most reduction tactics refuse to unfold Opaque constants, conversion treats Opaque as merely a hint to unfold this constant last.

We can get around this issue by using with_strategy:

Goal True.
1 subgoal ============================ True
Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity.
The command has indeed failed with message: Timeout!
Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity.
Finished transaction in 0.002 secs (0.003u,0.s) (successful) 1 subgoal H : id (fact 100) = fact 100 ============================ True

However, when we go to close the proof, we will run into trouble, because the reduction strategy changes are local to the tactic passed to with_strategy.

exact I.
No more subgoals.
Timeout 1 Defined.
Toplevel input, characters 0-18: > Timeout 1 Defined. > ^^^^^^^^^^^^^^^^^^ Error: Timeout!

We can fix this issue by using abstract:

Goal True.
1 subgoal ============================ True
Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity.
Finished transaction in 0.007 secs (0.007u,0.s) (successful) 1 subgoal H : id (fact 100) = fact 100 ============================ True
exact I.
No more subgoals.
Time Defined.
Finished transaction in 0.002 secs (0.003u,0.s) (successful)

On small examples this sort of behavior doesn't matter, but because Coq is a super-linear performance domain in so many places, unless great care is taken, tactic automation using with_strategy may not be robustly performant when scaling the size of the input.

Warning

In much the same way this tactic does not play well with Qed and Defined without using abstract as an intermediary, this tactic does not play well with coqchk, even when used with abstract, due to the inability of tactics to persist information about conversion hints in the proof term. See #12200 for more details.

### Conversion tactics applied to hypotheses¶

Tactic tactic in ident+,

Applies tactic (any of the conversion tactics listed in this section) to the hypotheses ident+.

If ident is a local definition, then ident can be replaced by type 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¶

Tactic 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 using intros 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 named core.

Warning

auto uses a weaker version of apply that is closer to simple apply so it is expected that sometimes auto will fail even if applying manually one of the hints would succeed.

Variant auto num

Forces the search depth to be num. The maximal search depth is 5 by default.

Variant auto with ident+

Uses the hint databases ident+ in addition to the database core.

Note

Use the fake database nocore if you want to not use the core 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.

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. If qualid 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 of apply and auto using qualid may fail where apply 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 the using 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 debug auto

Behaves like auto but shows the tactics it tries to solve the goal, including failing paths.

Variant info_?auto num? using qualid+? with ident+?

This is the most general form, combining the various options.

Variant trivial

This tactic is a restriction of auto that is not recursive and tries only hints that cost 0. Typically it solves trivial equalities like X=X.

Variant trivial with ident+
Variant trivial with *
Variant trivial using qualid+
Variant debug trivial
Variant info_trivial
Variant info_?trivial using qualid+? with ident+?

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 and trivial tactics.

Tactic eauto

This tactic generalizes auto. While auto 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 to simple eapply instead of a tactic close to simple apply in the case of auto). 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.

Variant info_?eauto num? using qualid+? with ident+?

The various options for eauto are the same as for auto.

eauto also obeys the following flags:

Flag Info Eauto
Flag Debug Eauto
Tactic 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.

Tactic 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

Performs all the rewritings in hypothesis qualid.

Variant autorewrite with ident+ in qualid using tactic

Performs all the rewritings in hypothesis qualid applying tactic to the main subgoal after each rewriting step.

Variant autorewrite with ident+ in goal_occurrences

Performs all the rewriting in the clause goal_occurrences.

Hint-Rewrite for feeding the database of lemmas used by autorewrite and autorewrite for examples showing the use of this tactic.

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 and inversion of hypothesis. If this fails, it tries introducing variables and splitting and-hypotheses, using the closing tactics afterwards, and splitting the goal using split 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.

Variant now tactic

Run tactic followed by easy. This is a notation for tactic; easy.

## 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 by auto 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+.

This command supports the local, global and export locality attributes. When no locality is explictly given, the command is local inside a section and global otherwise.

The various possible hint_definitions 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 Hint Resolve qualid | num? pattern?? : ident

This command adds simple apply qualid to the hint list with the head symbol of the type of qualid. The cost of that hint is the number of subgoals generated by simple apply qualid or num if specified. The associated pattern is inferred from the conclusion of the type of qualid or the given pattern if specified. In case the inferred type of qualid does not start with a product the tactic added in the hint list is exact qualid. In case this type can however be reduced to a type starting with a product, the tactic simple apply qualid is also stored in the hints list. If the inferred type of qualid 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 of eauto instead of the hint list of auto and a warning is printed. A typical example of a hint that is used only by eauto is a transitivity lemma.

Error qualid cannot be used as a hint

The head symbol of the type of qualid is a bound variable such that this tactic cannot be associated to a constant.

Variant Hint Resolve qualid+ : ident

Adds each Hint Resolve qualid.

Variant Hint Resolve -> qualid : ident

Adds the left-to-right implication of an equivalence as a hint (informally the hint will be used as apply <- qualid, although as mentioned before, the tactic actually used is a restricted version of apply).

Variant Hint Resolve <- qualid

Adds the right-to-left implication of an equivalence as a hint.

Variant Hint Immediate qualid : ident

This command adds simple apply qualid; trivial to the hint list associated with the head symbol of the type of ident in the given database. This tactic will fail if all the subgoals generated by simple apply qualid are not solved immediately by the trivial tactic (which only tries tactics with cost 0).This command is useful for theorems such as the symmetry of equality or n+1=m+1 -> n=m that we may like to introduce with a limited use in order to avoid useless proof-search. The cost of this tactic (which never generates subgoals) is always 1, so that it is not used by trivial itself.

Error qualid cannot be used as a hint
Variant Hint Immediate qualid+ : ident

Adds each Hint Immediate qualid.

Variant Hint Constructors qualid : ident

If qualid is an inductive type, this command adds all its constructors as hints of type Resolve. Then, when the conclusion of current goal has the form (qualid ...), auto will try to apply each constructor.

Error qualid is not an inductive type
Variant Hint Constructors qualid+ : ident

Extends the previous command for several inductive types.

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 is qualid. 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 Transparent​Opaque : ident
Variant Hint Constants Transparent​Opaque : 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 than apply and unfold. For that, we must specify a cost, an optional pattern and a tactic 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:

::=
(hint or instance identifier)
|
_
(any hint)
|
(disjunction)
|
(sequence)
|
(Kleene star)
|
emp
(empty)
|
eps
(epsilon)
|
( regexp )

The emp regexp does not match any search path while eps 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 that Hint Extern’s do not have an associated identifier). Before applying any hint ident the current path p extended with ident is matched against the current cut expression c associated to the hint database. If matching succeeds, the hint is not applied. The semantics of Hint Cut regexp is to set the cut expression to c | regexp, the initial cut expression being emp.

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 of qualid to arguments term ... term, the mode tells if the hints associated to qualid 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

### 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. The database also contains high-cost hints that call lia 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 databases ident+.

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 Print HintDb ident

This command displays all hints from database ident.

Command Hint Rewrite term+ : ident+

This vernacular command adds the terms term+ (their types must be equalities) in the rewriting bases ident+ with the default orientation (left to right). Notice that the rewriting bases are distinct from the auto hint bases and that auto does not take them into account.

This command is synchronous with the section mechanism (see Section mechanism): when closing a section, all aliases created by Hint Rewrite in that section are lost. Conversely, when loading a module, all Hint Rewrite declarations at the global level of that module are loaded.

Variants:

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 bases ident+.

Command Hint Rewrite ->​<-? one_term+ using ltac_expr? : ident*?

When the rewriting rules term+ in ident+ will be used, the tactic tactic will be applied to the generated subgoals, the main subgoal excluded.

Command Print Rewrite HintDb ident

This command displays all rewrite hints contained in ident.

### 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 required (using e.g. Require 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 tactic1 is ended by .... In this case the tactic command typed by the user is equivalent to tactic1 ;tactic.

Variant Proof with tactic using ident+

Combines in a single line Proof with and Proof using, see Entering and leaving proof editing mode

Variant Proof using ident+ with tactic

Combines in a single line Proof with and Proof using, see Entering and leaving proof editing mode

## Decision procedures¶

Tactic 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 connectives and, 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.

Tactic intuition tactic

The tactic intuition takes advantage of the search-tree built by the decision procedure involved in the tactic tauto. It uses this information to generate a set of subgoals equivalent to the original one (but simpler than it) and applies the tactic tactic to them [Mun94]. If this tactic fails on some goals then intuition fails. In fact, tauto is simply intuition 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 connectives and, 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.

Tactic rtauto

The rtauto tactic solves propositional tautologies similarly to what tauto 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 that tauto would be able to solve (e.g. goals involving universal quantifiers).

Note that this tactic is only available after a Require Import Rtauto.

Tactic firstorder

The tactic firstorder is an experimental extension of tauto 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 is auto with core, 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.

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. If qualid 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 bases ident+ to the proof-search environment.

Variant firstorder tactic using qualid+, with ident+

This combines the effects of the different variants of firstorder.

Option Firstorder Depth num

This option controls the proof-search depth bound.

Tactic 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 (see injection and discriminate). 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 of num does not make success slower, only failure. You might consider adding some lemmas as hypotheses using assert in order for congruence to use them.

Variant congruence with term+

Adds term+ to the pool of terms used by congruence. 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.

Tactic constr_eq term term

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

Error Not equal.
Error Not equal (due to universes).
Tactic constr_eq_strict term term

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

Error Not equal.
Error Not equal (due to universes).
Tactic unify term term

This tactic checks whether its arguments are unifiable, potentially instantiating existential variables.

Error Unable to unify term with term.
Variant unify term term with ident

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

Tactic is_evar term

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

Error Not an evar.
Tactic has_evar term

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

Error No evars.
Tactic is_var term

This tactic checks whether its argument is a variable or hypothesis in the current goal context or in the opened sections.

Error Not a variable or hypothesis.

## Equality¶

Tactic f_equal

This tactic applies to a goal of the form f a1 ... an = f′a′1 ... a′n. Using f_equal on such a goal leads to subgoals f=f′ and a1 = a′1 and so on up to an = a′n. Amongst these subgoals, the simple ones (e.g. provable by reflexivity or congruence) are automatically solved by f_equal.

Tactic reflexivity

This tactic applies to a goal that has the form t=u. It checks that t and u are convertible and then solves the goal. It is equivalent to apply refl_equal.

Error The conclusion is not a substitutive equation.
Error Unable to unify ... with ...
Tactic symmetry

This tactic applies to a goal that has the form t=u and changes it into u=t.

Variant symmetry in ident

If the statement of the hypothesis ident has the form t=u, the tactic changes it to u=t.

Tactic transitivity term

This tactic applies to a goal that has the form t=u and transforms it into the two subgoals t=term and term=u.

Variant etransitivity

This tactic behaves like transitivity, using a fresh evar instead of a concrete term.

## Equality and inductive sets¶

We describe in this section some special purpose tactics dealing with equality and inductive sets or types. These tactics use the equality eq:forall (A:Type), A->A->Prop, simply written with the infix symbol =.

Tactic decide equality

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

Tactic compare term term

This tactic compares two given objects term and term of an inductive datatype. If G is the current goal, it leaves the sub- goals term =term -> G and ~ term = term -> G. The type of term and term must satisfy the same restrictions as in the tactic decide equality.

Tactic simplify_eq term

Let term be the proof of a statement of conclusion term = term. If term and term are structurally different (in the sense described for the tactic discriminate), then the tactic simplify_eq behaves as discriminate term, otherwise it behaves as injection 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 then simplify_eq ident where ident is the identifier for the last introduced hypothesis.

Variant simplify_eq term with bindings

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

Variant esimplify_eq num
Variant esimplify_eq term with bindings?

This works the same as simplify_eq but if the type of term, or the type of the hypothesis referred to by num, has uninstantiated parameters, these parameters are left as existential variables.

Variant simplify_eq

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

Tactic dependent rewrite -> ident

This tactic applies to any goal. If ident has type (existT B a b)=(existT B a' b') in the local context (i.e. each term of the equality has a sigma type { a:A & (B a)}) this tactic rewrites a into a' and b into b' in the current goal. This tactic works even if B is also a sigma type. This kind of equalities between dependent pairs may be derived by the injection and inversion tactics.

Variant dependent rewrite <- ident

Analogous to dependent rewrite -> but uses the equality from right to left.

## Classical tactics¶

In order to ease the proving process, when the Classical module is loaded, a few more tactics are available. Make sure to load the module using the Require Import command.

Tactic classical_left
Tactic classical_right

These tactics are the analog of left and right but using classical logic. They can only be used for disjunctions. Use classical_left to prove the left part of the disjunction with the assumption that the negation of right part holds. Use classical_right to prove the right part of the disjunction with the assumption that the negation of left part holds.

## Automating¶

Tactic btauto

The tactic btauto implements a reflexive solver for boolean tautologies. It solves goals of the form t = u where t and u are constructed over the following grammar:

|
true
|
false
|
|
|
|

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.

Error Cannot recognize a boolean equality.

The goal is not of the form t = u. Especially note that btauto doesn't introduce variables into the context on its own.

Variant field
Variant field_simplify term*
Variant 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, whereas field_simplify term+ replaces the provided terms by their reduced fraction. field_simplify_eq` applies when the conclusion is an equation: