Chapter 8 Tactics

# Coq Reference Manual

# Chapter 8 Tactics

- 8.1 Invocation of tactics
- 8.2 Explicit proof as a term
- 8.3 Basics
- 8.4 Negation and contradiction
- 8.5 Conversion tactics
- 8.6 Introductions
- 8.7 Induction and Case Analysis
- 8.8 Equality
- 8.9 Equality and inductive sets
- 8.10 Inversion
- 8.11 Classical tactics
- 8.12 Automatizing
- 8.13 Controlling automation
- 8.14 Generation of induction principles with `Scheme`
- 8.15 Generation of induction principles with `Functional Scheme`
- 8.16 Simple tactic macros

A deduction rule is a link between some (unique) formula, that we call the conclusion and (several) formulas that we call the premises. Indeed, a deduction rule can be read in two ways. The first one has the shape: “if I know this and this then I can deduce this”. For instance, if I have a proof of A and a proof of B then I have a proof of A ∧ B. This is forward reasoning from premises to conclusion. The other way says: “to prove this I have to prove this and this”. For instance, to prove A ∧ B, I have to prove A and I have to prove B. This is backward reasoning which proceeds from conclusion to premises. We say that the conclusion is the goal to prove and premises are the subgoals. The tactics implement backward reasoning. When applied to a goal, a tactic replaces this goal with the subgoals it generates. We say that a tactic reduces a goal to its subgoal(s).

Each (sub)goal is denoted with a number. The current goal is numbered 1. By default, a tactic is applied to the current goal, but one can address a particular goal in the list by writing n:tactic which means “apply tactic tactic to goal number n”. We can show the list of subgoals by typing `Show` (see Section 7.3.1).

Since not every rule applies to a given statement, every tactic cannot be used to reduce any goal. In other words, before applying a tactic to a given goal, the system checks that some preconditions are satisfied. If it is not the case, the tactic raises an error message.

Tactics are build from atomic tactics and tactic expressions (which extends the folklore notion of tactical) to combine those atomic tactics. This chapter is devoted to atomic tactics. The tactic language will be described in Chapter 9.

There are, at least, three levels of atomic tactics. The simplest one implements basic rules of the logical framework. The second level is the one of derived rules which are built by combination of other tactics. The third one implements heuristics or decision procedures to build a complete proof of a goal.

## 8.1 Invocation of tactics

A tactic is applied as an ordinary command. If the tactic does not address the first subgoal, the command may be preceded by the wished subgoal number as shown below:

tactic_invocation | ::= | num `:` tactic `.`
| | | tactic `.`

## 8.2 Explicit proof as a term

### 8.2.1 `exact` term``

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

Error messages:

1. `Not an exact proof`

Variants:

1. `eexact` term

   This tactic behaves like `exact` but is able to handle terms with meta-variables.

### 8.2.2 `refine` term`` ``

This tactic allows to give an exact proof but still with some holes. The holes are noted “`_`”.

Error messages:

1. `invalid argument`: the tactic `refine` doesn’t know what to do with the term you gave.
2. `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, which call `refine` internally.
3. `Cannot infer a term for this placeholder` there is a hole in the term you gave which type cannot be inferred. Put a cast around it.

An example of use is given in Section 10.1.

## 8.3 Basics

Tactics presented in this section implement the basic typing rules of pCic given in Chapter 4.

### 8.3.1 `assumption`

This tactic applies to any goal. It implements the “Var” rule given in Section 4.2. It looks in the local context for an hypothesis which type is equal to the goal. If it is the case, the subgoal is proved. Otherwise, it fails.

Error messages:

1. `No such assumption`

Variants:

1. `eassumption`

   This tactic behaves like `assumption` but is able to handle goals with meta-variables.

### 8.3.2 `clear` ident`` ``

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

Variants:

1. `clear` ident`1``` `…``` ident`n`

   This is equivalent to `clear` ident`1``.` `…``clear` ident`n``.`

2. `clearbody` ident

   This tactic expects ident to be a local definition then clears its body. Otherwise said, this tactic turns a definition into an assumption.

3. `clear -` ident`1``` `…``` ident`n`

   This tactic clears all hypotheses except the ones depending in the hypotheses named ident1 … identn and in the goal.

4. `clear`

   This tactic clears all hypotheses except the ones depending in goal.

5. `clear dependent` ident

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

Error messages:

1. ident `not found`
2. ident `is used in the conclusion`
3. ident `is used in the hypothesis` ident`’`

### 8.3.3 `move` ident`1``after` ident`2``` ``

This moves the hypothesis named ident1 in the local context after the hypothesis named ident2.

If ident1 comes before ident2 in the order of dependences, then all hypotheses between ident1 and ident2 which (possibly indirectly) depend on ident1 are moved also.

If ident1 comes after ident2 in the order of dependences, then all hypotheses between ident1 and ident2 which (possibly indirectly) occur in ident1 are moved also.

Variants:

1. `move` ident`1``before` ident`2`

   This moves ident1 towards and just before the hypothesis named ident2.

2. `move` ident `at top`

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

3. `move` ident `at bottom`

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

Error messages:

1. ident`i``not found`
2. `Cannot move` ident`1``after` ident`2``: it occurs in` ident`2`
3. `Cannot move` ident`1``after` ident`2``: it depends on` ident`2`

### 8.3.4 `rename` ident`1``into` ident`2```

This renames hypothesis ident1 into ident2 in the current context1

Variants:

1. `rename` ident`1``into` ident`2``, …,` ident`2k-1``into` ident`2k`

   Is equivalent to the sequence of the corresponding atomic `rename`.

Error messages:

1. ident`1``not found`
2. ident`2``is already used`

### 8.3.5 `intro` ``

This tactic applies to a goal which is either a product or starts with a let binder. If the goal is a product, the tactic implements the “Lam” rule given in Section 4.22. If the goal starts with a let binder then the tactic implements a mix of the “Let” and “Conv”.

If the current goal is a dependent product `forall` `x``:``T``,` `U` (resp `let` `x``:=``t` `in` `U`) then `intro` puts `x``:``T` (resp `x``:=``t`) in the local context. The new subgoal is U.

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

If the goal is neither a product nor starting with a let definition, the tactic `intro` applies the tactic `red` until the tactic `intro` can be applied or the goal is not reducible.

Error messages:

1. `No product even after head-reduction`
2. ident `is already used`

Variants:

1. `intros`

   Repeats `intro` until it meets the head-constant. It never reduces head-constants and it never fails.

2. `intro` ident

   Applies `intro` but forces ident to be the name of the introduced hypothesis.

   Error message: `name` ident `is already used`

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

3. `intros` ident`1``…` ident`n`

   Is equivalent to the composed tactic `intro` ident`1``; … ; intro` ident`n`.

   More generally, the `intros` tactic takes a pattern as argument in order to introduce names for components of an inductive definition or to clear introduced hypotheses; This is explained in 8.7.3.

4. `intros until` ident

   Repeats `intro` until it meets a premise of the goal having form `(` ident `:` term `)` and discharges the variable named ident of the current goal.

   Error message: `No such hypothesis in current goal`

5. `intros until` num

   Repeats `intro` until the num-th non-dependent product. For instance, 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. And 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 message: `No such hypothesis in current goal`

   Happens when num is 0 or is greater than the number of non-dependent products of the goal.

6. `intro after` ident
   `intro before` ident
   `intro at top`
   `intro at bottom`

   Applies `intro` and moves the freshly introduced hypothesis respectively after the hypothesis ident, before the hypothesis ident, 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. Note that `intro at bottom` is a synonym for `intro` with no argument.

   Error messages:

   1. `No product even after head-reduction`
   2. `No such hypothesis` : ident
7. `intro` ident`1``after` ident`2`
   `intro` ident`1``before` ident`2`
   `intro` ident`1``at top`
   `intro` ident`1``at bottom`

   Behaves as previously but naming the introduced hypothesis ident1. It is equivalent to `intro` ident`1` followed by the appropriate call to `move` (see Section 8.3.3).

   Error messages:

   1. `No product even after head-reduction`
   2. `No such hypothesis` : ident

### 8.3.6 `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``` `t``1``…` `t``n``)` 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``)` `u``1``…` `u``n` and the ti and ui unifies, then P is taken to be (fun x => Q). Otherwise, `apply` tries to define P by abstracting over t1 … tn in the goal. See `pattern` in Section 8.5.7 to transform the goal so that it gets the form `(fun` `x``=>` `Q``)` `u``1``…` `u``n`.

Error messages:

1. `Impossible to unify … with …`

   The `apply` tactic failed to match the conclusion of term and the current goal. You can help the `apply` tactic by transforming your goal with the `change` or `pattern` tactics (see sections 8.5.7, 8.3.12).

2. `Unable to find an instance for the variables` ident`…`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:

Variants:

1. `apply` term `with` term`1``…` term`n`

   Provides `apply` with explicit instantiations for all dependent premises of the type of term which do not occur in the conclusion and consequently cannot be found by unification. Notice that term1 … termn must be given according to the order of these dependent premises of the type of term.

   Error message: `Not the right number of missing arguments`

2. `apply` term `with (`ref`1``:=` term`1``) … (`ref`n``:=` term`n``)`

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

3. `apply` term1 `,` …`,` termn

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

4. `eapply` term

   The tactic `eapply` behaves as `apply` but does not fail when no instantiation are deducible for some variables in the premises. Rather, it turns these variables into so-called existential variables which are variables still to instantiate. An existential variable is identified by a name of the form `?``n` where n is a number. The instantiation is intended to be found later in the proof.

   An example of use of `eapply` is given in Section 10.2.

5. `simple apply` term

   This behaves like `apply` but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, if `id := fun x:nat => x` and `H : forall y, id y = y` then `simple apply H` on goal `O = O` does not succeed because it would require the conversion of `f ?y` and `O` where `?y` is a variable to instantiate. Tactic `simple apply` does not either traverse tuples as `apply` does.

   Because it reasons modulo a limited amount of conversion, `simple apply` fails quicker than `apply` and it is then well-suited for uses in used-defined tactics that backtrack often.

6. [`simple`] `apply` term1 [`with` bindings_list1] `,` …`,` termn [`with` bindings_listn]
   [`simple`] `eapply` term1 [`with` bindings_list1] `,` …`,` termn [`with` bindings_listn]

   This summarizes the different syntaxes for `apply` and `eapply`.

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

### 8.3.7 `set (` ident`` `:=``` term`)`

This replaces term by ident in the conclusion or in the hypotheses of the current goal and adds the new definition ident`:=` term to the local context. The default is to make this replacement only in the conclusion.

Variants:

1. `set (` ident `:=` term `) in` goal_occurrences

   This notation allows to specify which occurrences of term have to be substituted in the context. The `in` goal_occurrences clause is an occurrence clause whose syntax and behavior is described in Section 8.3.23.

2. `set (` ident binder … binder `:=` term `)`

   This is equivalent to `set (` ident `:=` `fun` binder … binder `=>` term `)`.

3. `set` term

   This behaves as `set (` ident := term `)` but ident is generated by Coq. This variant also supports an occurrence clause.

4. `set (` ident0 binder … binder `:=` term `) in` goal_occurrences
   `set` term `in` goal_occurrences

   These are the general forms which combine the previous possibilities.

5. `remember` term`` `as``` ident

   This behaves as `set (` ident := term `) in *` and using a logical (Leibniz’s) equality instead of a local definition.

6. `remember` term`` `as``` ident `in` goal_occurrences

   This is a more general form of `remember` that remembers the occurrences of term specified by an occurrences set.

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

8. `pose (` ident binder … binder `:=` term `)`

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

9. `pose` term

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

### 8.3.8 `assert (` ident`:` form`)`

This tactic applies to any goal. `assert (H : U)` adds a new hypothesis of name `H` asserting `U` to the current goal and opens a new subgoal `U`3. The subgoal `U` comes first in the list of subgoals remaining to prove.

Error messages:

1. `Not a proposition or a type`

   Arises when the argument form is neither of type `Prop`, `Set` nor `Type`.

Variants:

1. `assert` form

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

2. `assert (` ident := term `)`

   This behaves as `assert (`ident`:` type`);[exact` term`|idtac]` where type is the type of term.

3. `cut` form

   This tactic applies to any goal. It implements the non dependent case of the “App” rule given in Section 4.2. (This is Modus Ponens inference rule.) `cut U` transforms the current goal `T` into the two following subgoals: `U -> T` and `U`. The subgoal `U -> T` comes first in the list of remaining subgoal to prove.

4. `assert` form `by` tactic

   This tactic behaves like `assert` but applies tactic to solve the subgoals generated by `assert`.

5. `assert` form `as` intro_pattern

   If intro_pattern is a naming introduction pattern (see Section 8.7.3), the hypothesis is named after this introduction pattern (in particular, if intro_pattern is ident, the tactic behaves like `assert (`ident`:` form`)`).

   If intro_pattern is a disjunctive/conjunctive introduction pattern, the tactic behaves like `assert` form then destructing the resulting hypothesis using the given introduction pattern.

6. `assert` form `as` intro_pattern `by` tactic

   This combines the two previous variants of `assert`.

7. `pose proof` term `as` intro_pattern

   This tactic behaves like `assert T as` intro_pattern `by exact` term where `T` is the type of term.

   In particular, `pose proof` term `as` ident behaves as `assert (`ident`:T) by exact` term (where `T` is the type of term) and `pose proof` term `as` disj_conj_intro_pattern behaves like `destruct` term `as` disj_conj_intro_pattern.

8. `specialize (`ident`` term`1``` `…``` term`n``)`
   `specialize` ident `with` bindings_list

   The tactic `specialize` 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 term1 … termn or from a bindings list (see Section 8.3.22 for more about bindings lists). In the second form, all instantiation elements must be given, whereas in the first form the application to term1 … termn can be partial. The first form is equivalent to `assert (`ident`’:=`ident term`1``` `…``` term`n``); clear` ident`; rename` ident`’ into` ident.

   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.

### 8.3.9 `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 `A <-> B` statement, 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 messages:

1. `Statement without assumptions`

   This happens if the type of term has no non dependent premise.

2. `Unable to apply`

   This happens if the conclusion of ident does not match any of the non dependent premises of the type of term.

Variants:

1. `apply` term`` `,``` `…``` `,``` term `in` ident

   This applies each of term in sequence in ident.

2. `apply` term `with` bindings_list`` `,``` `…``` `,``` term `with` bindings_list `in` ident

   This does the same but uses the bindings in each bindings_list to instantiate the parameters of the corresponding type of term (see syntax of bindings in Section 8.3.22).

3. `eapply` term `with` bindings_list`` `,``` `…``` `,``` term `with` bindings_list `in` ident

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

4. `apply` term`,``with` bindings_list`` `,``` `…``` `,``` term`,``with` bindings_list `in` ident `as` disj_conj_intro_pattern

   This works as `apply` term`,``with` bindings_list`` `,``` `…``` `,``` term`,``with` bindings_list `in` ident then destructs the hypothesis ident along disj_conj_intro_pattern as `destruct` ident `as` disj_conj_intro_pattern would.

5. `eapply` term`,``with` bindings_list`` `,``` `…``` `,``` term`,``with` bindings_list `in` ident `as` disj_conj_intro_pattern

   This works as `apply` term`,``with` bindings_list`` `,``` `…``` `,``` term`,``with` bindings_list `in` ident `as` disj_conj_intro_pattern but using `eapply`.

6. `simple apply` term `in` ident

   This behaves like `apply` term `in` ident but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, if `id := fun x:nat => x` and `H : forall y, id y = y -> True` and `H0 : O = O` then `simple apply H in H0` does not succeed because it would require the conversion of `f ?y` and `O` where `?y` is a variable to instantiate. Tactic `simple apply` term `in` ident does not either traverse tuples as `apply` term `in` ident does.

7. `[``simple``]``apply` term`` `[``with` bindings_list`]``` `,``` `…``` `,``` term`` `[``with` bindings_list`]``in` ident`` `[``as` disj_conj_intro_pattern`]`
   `[``simple``]``eapply` term`` `[``with` bindings_list`]``` `,``` `…``` `,``` term`` `[``with` bindings_list`]``in` ident`` `[``as` disj_conj_intro_pattern`]`

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

### 8.3.10 `generalize` term``

This tactic applies to any goal. It generalizes the conclusion w.r.t. one subterm of it. For example:

`Coq` `<``Show.`
`1 subgoal`
``
`x : nat`
`y : nat`
`============================`
`0` `<``= x + y + y`
`Coq` `<``generalize (x + y + y).`
`1 subgoal`
``
`x : nat`
`y : nat`
`============================`
`forall n : nat, 0` `<``= n`

If the goal is G and t is a subterm of type T in the goal, then `generalize` t replaces the goal by `forall (x:``T``),` `G′` where G′ is obtained from G by replacing all occurrences of t by `x`. The name of the variable (here `n`) is chosen based on T.

Variants:

1. `generalize` term`1``, … ,` term`n`

   Is equivalent to `generalize` term`n``; … ; generalize` term`1`. Note that the sequence of termi’s are processed from n to 1.

2. `generalize` term `at` num`1``…` num`i`

   Is equivalent to `generalize` term but generalizing only over the specified occurrences of term (counting from left to right on the expression printed using option `Set Printing All`).

3. `generalize` term `as` ident

   Is equivalent to `generalize` term but use ident to name the generalized hypothesis.

4. `generalize` term`1``at` num`11``…` num`1i``1``as` ident`1``,` `…``,` term`n``at` num`n1``…` num`ni``n``as` ident`2`

   This is the most general form of `generalize` that combines the previous behaviors.

5. `generalize dependent` term

   This generalizes term but also all hypotheses which depend on term. It clears the generalized hypotheses.

### 8.3.11 `revert` ident`1``…` ident`n``` ``

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

Error messages:

1. ident `is used in the hypothesis` ident`’`

Variants:

1. `revert dependent` ident

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

### 8.3.12 `change` term``

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

Error messages:

1. `Not convertible`

Variants:

1. `change` term`1``with` term`2`

   This replaces the occurrences of term1 by term2 in the current goal. The terms term1 and term2 must be convertible.

2. `change` term`1``at` num`1``…` num`i``with` term`2`

   This replaces the occurrences numbered num1 … numi of term1 by term2 in the current goal. The terms term1 and term2 must be convertible.

   Error message: `Too few occurrences`

3. `change` term `in` ident
4. `change` term`1``with` term`2``in` ident
5. `change` term`1``at` num`1``…` num`i``with` term`2``in` ident

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

See also: 8.5

### 8.3.13 `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 Section 8.7.

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 and counting both dependent and non dependent products. 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 7.3.2).

Variants:

1. `fix` ident1 num `with (` ident2 binder2 … binder2 [`{ struct` ident`′``2``}`] `:` type2 `)` … `(` ident1 bindern … bindern [`{ struct` ident`′``n``}`] `:` typen `)`

   This starts a proof by mutual induction. The statements to be simultaneously proved are respectively `forall` binder2 … binder2`,` type2, …, `forall` bindern … bindern`,` typen. The identifiers ident1 … identn are the names of the induction hypotheses. The identifiers ident′2 … ident′n 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).

### 8.3.14 `cofix` ident`` ``

This tactic starts a proof by coinduction. The identifier ident is the name given to the coinduction hypothesis. Like in a `cofix` expression, the use of induction hypotheses have to guarded by a constructor. The verification that the use of coinductive hypotheses is correct is done only at the time of registering the lemma in the 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 7.3.2).

Variants:

1. `cofix` ident1 `with (` ident2 binder2 … binder2 `:` type2 `)` … `(` ident1 binder1 … binder1 `:` typen `)`

   This starts a proof by mutual coinduction. The statements to be simultaneously proved are respectively `forall` binder2 … binder2`,` type2, …, `forall` bindern … bindern`,` typen. The identifiers ident1 … identn are the names of the coinduction hypotheses.

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

### 8.3.16 `instantiate (`num`:=` term`)` ``

The `instantiate` tactic allows to solve an existential variable with the term term. The num argument is the position of the existential variable from right to left in the conclusion. This cannot be the number of the existential variable since this number is different in every session.

Variants:

1. `instantiate (`num`:=`term`) in` ident
2. `instantiate (`num`:=`term`) in (Value of` ident`)`
3. `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.

4. `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.

### 8.3.17 `admit` ``

The `admit` tactic “solves” the current subgoal by an axiom. This typically allows to temporarily skip a subgoal so as to progress further in the rest of the proof. To know if some proof still relies on unproved subgoals, one can use the command `Print Assumptions` (see Section 6.3.5). Admitted subgoals have names of the form ident`_admitted` possibly followed by a number.

### 8.3.18 `constr_eq` term`1``` term`2``` ``

This tactic applies to any goal. It checks whether its arguments are equal modulo alpha conversion and casts.

Error message: `Not equal`

### 8.3.19 `is_evar` term``

This tactic applies to any goal. It checks whether its argument is an existential variable. Existential variables are uninstantiated variables generated by e.g. `eapply` (see Section 8.3.6).

Error message: `Not an evar`

### 8.3.20 `has_evar` term``

This tactic applies to any goal. It 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 message: `No evars`

### 8.3.21 `is_var` term``

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

Error message: `Not a variable or hypothesis`

### 8.3.22 Bindings list

Tactics that take a term as argument may also support a bindings list, so as to instantiate some parameters of the term by name or position. The general form of a term equipped with a bindings list is term `with` bindings_list where bindings_list may be of two different forms:

- In a bindings list of the form `(`ref`1``:=` term`1``) … (`ref`n``:=` term`n``)`, ref is either an ident or a num. The references are determined according to the type of term. If refi is an identifier, this identifier has to be bound in the type of term and the binding provides the tactic with an instance for the parameter of this name. If refi is some number n, this number denotes the n-th non dependent premise of the term, as determined by the type of term.

  Error message: `No such binder`

- A bindings list can also be a simple list of terms term`1``…`term`n`. In that case the references to which these terms correspond are determined by the tactic. In case of `induction`, `destruct`, `elim` and `case` (see Section 11) the terms have to provide instances for all the dependent products in the type of term while in the case of `apply`, or of `constructor` and its variants, only instances for the dependent products which are not bound in the conclusion of the type are required.

  Error message: `Not the right number of missing arguments`

### 8.3.23 Occurrences sets and occurrences clauses

An occurrences clause is a modifier to some tactics that obeys the following syntax:

occurrence_clause | ::= | `in` goal_occurrences
goal_occurrences | ::= | [ident1 [at_occurrences] `,`
|  | … `,`
|  | identm [at_occurrences]]
|  | [`|-` [`*` [at_occurrences]]]
| | | `*` `|-` [`*` [at_occurrences]]
| | | `*`
at_occurrences | ::= | `at` occurrences
occurrences | ::= | [`-`] num1 … numn

The role of an occurrence clause is to select a set of occurrences of a term in a goal. In the first case, the identi [`at` num1i … numnii] parts indicate that occurrences have to be selected in the hypotheses named identi. If no numbers are given for hypothesis identi, then all occurrences of term in the hypothesis are selected. If numbers are given, they refer to occurrences of term when the term is printed using option `Set Printing All` (see Section 2.9), counting from left to right. In particular, occurrences of term in implicit arguments (see Section 2.7) or coercions (see Section 2.8) 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. In 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 occurrences clauses: `set`, `remember`, `induction`, `destruct`.

See also: Sections 8.3.7, 8.7, 2.9.

## 8.4 Negation and contradiction

### 8.4.1 `absurd` term``

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

### 8.4.2 `contradiction` ``

This tactic applies to any goal. The `contradiction` tactic attempts to find in the current context (after all `intros`) one hypothesis which is equivalent to `False`. It permits to prune irrelevant cases. This tactic is a macro for the tactics sequence `intros; elimtype False; assumption`.

Error messages:

1. `No such assumption`

Variants:

1. `contradiction` ident

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

### 8.4.3 `contradict` ident

This tactic allows to manipulate 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`

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

## 8.5 Conversion tactics

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` 8.3.7, `rewrite` 8.8.1, `replace` 8.8.3 and `autorewrite` 8.12.13 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`1``` `…``` ident`n``|-` only in hypotheses ident1 …identn
  `in` ident`1``` `…``` ident`n``|- *` in hypotheses ident1 …identn and in the conclusion
  `in * |-` in every hypothesis
  `in *` (equivalent to `in * |- *`) everywhere
  `in (type of` ident`1``) (value of` ident`2``)` `…``|-` in type part of ident1, in the value part of ident2, etc.

For backward compatibility, the notation `in` ident1…identn performs the conversion in hypotheses ident1…identn.

### 8.5.1 `cbv` flag`1``…` flag`n`, `lazy` flag`1``…` flag`n` and `compute`

These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. In correspondence with the kinds of reduction considered in Coq namely β (reduction of functional application), δ (unfolding of transparent constants, see 6.10.2), ι (reduction of pattern-matching over a constructed term, and unfolding of `fix` and `cofix` expressions) and ζ (contraction of local definitions), the flag are either `beta`, `delta`, `iota` or `zeta`. The `delta` flag itself can be refined into `delta [`qualid`1``…`qualid`k``]` or `delta -[`qualid`1``…`qualid`k``]`, 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 Section 6.10.1).

The goal may be normalized with 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 partially evaluated only when necessary, and if an argument is used several times then it is 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 evaluated first, using a weak reduction (no reduction under the λ-abstractions). 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 few dead code).

Variants:

1. `compute`
   `cbv`

   These are synonyms for `cbv beta delta iota zeta`.

2. `lazy`

   This is a synonym for `lazy beta delta iota zeta`.

3. `compute [`qualid`1``…`qualid`k``]`
   `cbv [`qualid`1``…`qualid`k``]`

   These are synonyms of `cbv beta delta [`qualid`1``…`qualid`k``] iota zeta`.

4. `compute -[`qualid`1``…`qualid`k``]`
   `cbv -[`qualid`1``…`qualid`k``]`

   These are synonyms of `cbv beta delta -[`qualid`1``…`qualid`k``] iota zeta`.

5. `lazy [`qualid`1``…`qualid`k``]`
   `lazy -[`qualid`1``…`qualid`k``]`

   These are respectively synonyms of `cbv beta delta [`qualid`1``…`qualid`k``] iota zeta` and `cbv beta delta -[`qualid`1``…`qualid`k``] iota zeta`.

6. `vm_compute`

   This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine. This algorithm is dramatically more efficient than the algorithm used for the `cbv` tactic, but it cannot be fine-tuned. It is specially interesting for full evaluation of algebraic objects. This includes the case of reflexion-based tactics.

### 8.5.2 `red`

This tactic applies to a goal which has the form `forall (x:T1)…(xk:Tk), c t1 … tn` where `c` is a constant. If `c` is transparent then it replaces `c` with its definition (say `t`) and then reduces `(t t1 … tn)` according to βιζ-reduction rules.

Error messages:

1. `Not reducible`

### 8.5.3 `hnf`

This tactic applies to any goal. It replaces the current goal with its head normal form according to the βδιζ-reduction rules, i.e. it reduces the head of the goal until it becomes a product or an irreducible term.

Example: The term `forall n:nat, (plus (S n) (S n))` is not reduced by `hnf`.

Remark: The δ rule only applies to transparent constants (see Section 6.10.1 on transparency and opacity).

### 8.5.4 `simpl`

This tactic applies to any goal. The tactic `simpl` first applies βι-reduction rule. Then it expands transparent constants and tries to reduce `T’` according, once more, to βι rules. But when the ι rule is not applicable then possible δ-reductions are not applied. For instance trying to use `simpl` on `(plus n O)=n` changes nothing. Notice that only transparent constants whose name can be reused as such in the recursive calls are possibly unfolded. 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.

Variants:

1. `simpl` term

   This applies `simpl` only to the occurrences of term in the current goal.

2. `simpl` term `at` num`1``…` num`i`

   This applies `simpl` only to the num1, …, numi occurrences of term in the current goal.

   Error message: `Too few occurrences`

3. `simpl` ident

   This applies `simpl` only to the applicative subterms whose head occurrence is ident.

4. `simpl` ident `at` num`1``…` num`i`

   This applies `simpl` only to the num1, …, numi applicative subterms whose head occurrence is ident.

### 8.5.5 `unfold` qualid``

This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see Sections 1.3.2 and 6.10.2). The tactic `unfold` applies the δ rule to each occurrence of the constant to which qualid refers in the current goal and then replaces it with its βι-normal form.

Error messages:

1. qualid `does not denote an evaluable constant`

Variants:

1. `unfold` qualid`1``, …,` qualid`n`

   Replaces simultaneously qualid1, …, qualidn with their definitions and replaces the current goal with its βι normal form.

2. `unfold` qualid`1``at` num`1``1``, …,` num`i``1``, …,` qualid`n``at` num`1``n``…` num`j``n`

   The lists num11, …, numi1 and num1n, …, numjn specify the occurrences of qualid1, …, qualidn to be unfolded. Occurrences are located from left to right.

   Error message: `bad occurrence number of` qualid`i`

   Error message: qualidi `does not occur`

3. `unfold` string

   If string denotes the discriminating symbol of a notation (e.g. `"+"`) or an expression defining a notation (e.g. `"_ + _"`), and this notation refers to an unfoldable constant, then the tactic unfolds it.

4. `unfold` string`%`key

   This is variant of `unfold` string where string gets its interpretation from the scope bound to the delimiting key key instead of its default interpretation (see Section 12.2.2).

5. `unfold` qualid_or_string`1``at` num`1``1``, …,` num`i``1``, …,` qualid_or_string`n``at` num`1``n``…` num`j``n`

   This is the most general form, where qualid_or_string is either a qualid or a string referring to a notation.

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

Variants:

1. `fold` term1 … termn

   Equivalent to `fold` term1`;`…`; fold` termn.

### 8.5.7 `pattern` term

This command applies to any goal. The argument term must be a free subterm of the current goal. The command `pattern` performs β-expansion (the inverse of β-reduction) of the current goal (say `T`) by

1. replacing all occurrences of term in `T` with a fresh variable
2. abstracting this variable
3. applying the abstracted goal to term

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

Variants:

1. `pattern` term `at` num`1``…` num`n`

   Only the occurrences num1 … numn of term are considered for β-expansion. Occurrences are located from left to right.

2. `pattern` term `at -` num`1``…` num`n`

   All occurrences except the occurrences of indexes num1 … numn of term are considered for β-expansion. Occurrences are located from left to right.

3. `pattern` term`1``, …,` term`m`

   Starting from a goal φ(t1 … tm), the tactic `pattern` `t``1``, …,` `t``m` generates the equivalent goal `(fun (x``1``:``A``1``) … (x``m``:``A``m``) =>` `φ(``x``1``… x``m``)``)` `t``1``…` `t``m`.
   If ti occurs in one of the generated types Aj these occurrences will also be considered and possibly abstracted.

4. `pattern` term`1``at` num`1``1``…` num`n``1``1``, …,` term`m``at` num`1``m``…` num`n``m``m`

   This behaves as above but processing only the occurrences num11, …, numi1 of term1, …, num1m, …, numjm of termm starting from termm.

5. `pattern` term1 [`at` `[``-``]` num11 … numn11] `,` …`,` termm [`at` `[``-``]` num1m … numnmm]

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

### 8.5.8 Conversion tactics applied to hypotheses

conv_tactic `in` ident1 … identn

Applies the conversion tactic conv_tactic to the hypotheses ident1, …, identn. The tactic conv_tactic is any of the conversion tactics listed in this section.

If identi is a local definition, then identi can be replaced by (Type of identi) to address not the body but the type of the local definition. Example: `unfold not in (Type of H1) (Type of H3).`

Error messages:

1. `No such hypothesis` : ident.

## 8.6 Introductions

Introduction tactics address goals which are inductive constants. They are used when one guesses that the goal can be obtained with one of its constructors’ type.

### 8.6.1 `constructor` num``

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

Error messages:

1. `Not an inductive product`
2. `Not enough constructors`

Variants:

1. `constructor`

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

2. `constructor` num `with` bindings_list

   Let `ci` be the `i`-th constructor of `I`, then `constructor i with` bindings_list is equivalent to `intros; apply ci with` bindings_list.

   Warning: the terms in the bindings_list are checked in the context where `constructor` is executed and not in the context where `apply` is executed (the introductions are not taken into account).

3. `split`

   Applies if `I` has only one constructor, typically in the case of conjunction A∧ B. Then, it is equivalent to `constructor 1`.

4. `exists` bindings_list

   Applies if `I` has only one constructor, for instance in the case of existential quantification ∃ x· P(x). Then, it is equivalent to `intros; constructor 1 with` bindings_list.

5. `exists` bindings_list`` `,``` `…``` `,``` bindings_list

   This iteratively applies `exists` bindings_list.

6. `left`
   `right`

   Apply if `I` has two constructors, for instance in the case of disjunction A∨ B. Then, they are respectively equivalent to `constructor 1` and `constructor 2`.

7. `left with` bindings_list
   `right with` bindings_list
   `split with` bindings_list

   As soon as the inductive type has the right number of constructors, these expressions are equivalent to calling `constructor` `i` `with` bindings_list for the appropriate i.

8. `econstructor`
   `eexists`
   `esplit`
   `eleft`
   `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 Section 10.2).

## 8.7 Induction and Case Analysis

The tactics presented in this section implement induction or case analysis on inductive or coinductive objects (see Section 4.5).

### 8.7.1 `induction` term

This tactic applies to any goal. The type of the argument term must be an inductive constant. Then, the tactic `induction` generates subgoals, one for each possible form of term, i.e. one for each constructor of the inductive type.

The tactic `induction` automatically replaces every occurrences of term in the conclusion and the hypotheses of the goal. It automatically adds induction hypotheses (using names of the form `IHn1`) to the local context. If some hypothesis must not be taken into account in the induction hypothesis, then it needs to be removed first (you can also use the tactics `elim` or `simple induction`, see below).

There are particular cases:

- If term is an identifier ident denoting a quantified variable of the conclusion of the goal, then `induction` ident behaves as `intros until` ident`; induction` ident.
- If term is a num, then `induction` num behaves as `intros until` num followed by `induction` applied to the last introduced hypothesis.

  Remark: For simple induction on a numeral, use syntax `induction (`num`)` (not very interesting anyway).

Example:

`Coq` `<``Lemma induction_test : forall n:nat, n = n -``>``n` `<``= n.`
`1 subgoal`
``
`============================`
`forall n : nat, n = n -``>``n` `<``= n`
`Coq` `<``intros n H.`
`1 subgoal`
``
`n : nat`
`H : n = n`
`============================`
`n` `<``= n`
`Coq` `<``induction n.`
`2 subgoals`
``
`H : 0 = 0`
`============================`
`0` `<``= 0`
`subgoal 2 is:`
`S n` `<``= S n`

Error messages:

1. `Not an inductive product`
2. `Unable to find an instance for the variables` ident`…`ident

   Use in this case the variant `elim … with …` below.

Variants:

1. `induction` term `as` disj_conj_intro_pattern

   This behaves as `induction` term but uses the names in disj_conj_intro_pattern to name the variables introduced in the context. The disj_conj_intro_pattern must typically be of the form `[` p11 …p1n1 `|` … `|` pm1 …pmnm `]` with m being the number of constructors of the type of term. Each variable introduced by `induction` in the context of the ith goal gets its name from the list pi1 …pini 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 Section 8.7.3). For instance, for an inductive type with one constructor, the pattern notation `(``p``1``,…,``p``n``)` can be used instead of `[` p1 …pn `]`.

2. `induction` term `as` naming_intro_pattern

   This behaves as `induction` term but adds an equation between term and the value that term takes in each of the induction case. The name of the equation is built according to naming_intro_pattern which can be an identifier, a “?”, etc, as indicated in Section 8.7.3.

3. `induction` term `as` naming_intro_pattern`` disj_conj_intro_pattern

   This combines the two previous forms.

4. `induction` term `with` bindings_list

   This behaves like `induction` term providing explicit instances for the premises of the type of term (see the syntax of bindings in Section 8.3.22).

5. `einduction` term

   This tactic behaves like `induction` term excepts 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 (see Section 10.2).

6. `induction` term`1``using` term`2`

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

7. `induction` term`1``using` term`2``with` bindings_list

   This behaves as `induction` term`1``using` term`2` but also providing instances for the premises of the type of term2.

8. `induction` term`1``` `…``` term`n``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.

9. `induction` term `in` goal_occurrences

   This syntax is used for selecting which occurrences of term the induction has to be carried on. The `in` at_occurrences clause is an occurrence clause whose syntax and behavior is described in Section 8.3.23.

   When an occurrence clause is given, an equation between term and the value it gets in each case of the induction is added to the context of the subgoals corresponding to the induction cases (even if no clause `as` naming_intro_pattern is given).

10. `induction` term`1``with` bindings_list`1``as` naming_intro_pattern`` disj_conj_intro_pattern `using` term`2``with` bindings_list`2``in` goal_occurrences
    `einduction` term`1``with` bindings_list`1``as` naming_intro_pattern`` disj_conj_intro_pattern `using` term`2``with` bindings_list`2``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.

11. `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.

12. `elim` term `with` bindings_list

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

13. `eelim` term

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

14. `elim` term`1``using` term`2`
    `elim` term`1``using` term`2``with` bindings_list

    Allows the user to give explicitly an elimination predicate term2 which is not the standard one for the underlying inductive type of term1. The bindings_list clause allows to instantiate premises of the type of term2.

15. `elim` term`1``with` bindings_list`1``using` term`2``with` bindings_list`2`
    `eelim` term`1``with` bindings_list`1``using` term`2``with` bindings_list`2`

    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.

16. `elimtype` form

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

17. `simple induction` ident

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

18. `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.

### 8.7.2 `destruct` term

The tactic `destruct` is used to perform case analysis without recursion. Its behavior is similar to `induction` except that no induction hypothesis is generated. It applies to any goal and the type of term must be inductively defined. There are particular cases:

- If term is an identifier ident denoting a quantified variable of the conclusion of the goal, then `destruct` ident behaves as `intros until` ident`; destruct` ident.
- If term is a num, then `destruct` num behaves as `intros until` num followed by `destruct` applied to the last introduced hypothesis.

  Remark: For destruction of a numeral, use syntax `destruct (`num`)` (not very interesting anyway).

Variants:

1. `destruct` term `as` disj_conj_intro_pattern

   This behaves as `destruct` term but uses the names in intro_pattern to name the variables introduced in the context. The intro_pattern must have the form `[` p11 …p1n1 `|` … `|` pm1 …pmnm `]` with m being the number of constructors of the type of term. Each variable introduced by `destruct` in the context of the ith goal gets its name from the list pi1 …pini in order. If there are not enough names, `destruct` invents names for the remaining variables to introduce. More generally, the pij can be any disjunctive/conjunctive introduction pattern (see Section 8.7.3). This provides a concise notation for nested destruction.

2. `destruct` term `as` disj_conj_intro_pattern`_eqn`

   This behaves as `destruct` term but adds an equation between term and the value that term takes in each of the possible cases. The name of the equation is chosen by Coq. If disj_conj_intro_pattern is simply `[]`, it is automatically considered as a disjunctive pattern of the appropriate size.

3. `destruct` term `as` disj_conj_intro_pattern`_eqn:` naming_intro_pattern

   This behaves as `destruct` term `as` disj_conj_intro_pattern`_eqn` but use naming_intro_pattern to name the equation (see Section 8.7.3). Note that spaces can generally be removed around `_eqn`.

4. `destruct` term `with` bindings_list

   This behaves like `destruct` term providing explicit instances for the dependent premises of the type of term (see syntax of bindings in Section 8.3.22).

5. `edestruct` term

   This tactic behaves like `destruct` term excepts 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 (see Section 10.2).

6. `destruct` term`1``using` term`2`
   `destruct` term`1``using` term`2``with` bindings_list

   These are synonyms of `induction` term`1``using` term`2` and `induction` term`1``using` term`2``with` bindings_list.

7. `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 Section 8.3.23.

   When an occurrence clause is given, an equation between term and the value it gets in each case of the analysis is added to the context of the subgoals corresponding to the cases (even if no clause `as` naming_intro_pattern is given).

8. `destruct` term`1``with` bindings_list`1``as` disj_conj_intro_pattern`_eqn:` naming_intro_pattern `using` term`2``with` bindings_list`2``in` goal_occurrences
   `edestruct` term`1``with` bindings_list`1``as` disj_conj_intro_pattern`_eqn:` naming_intro_pattern `using` term`2``with` bindings_list`2``in` goal_occurrences

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

9. `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.

10. `case_eq` term

    The tactic `case_eq` is a variant of the `case` tactic that allow 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. The effect of this tactic is similar to the effect of `destruct` term `in |- *` with the exception that no new hypotheses are introduced in the context.

11. `case` term `with` bindings_list

    Analogous to `elim` term `with` bindings_list above.

12. `ecase` term
    `ecase` term `with` bindings_list

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

13. `simple destruct` ident

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

14. `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.

### 8.7.3 `intros` intro_pattern`` `…``` intro_pattern`` ``

This extension of the tactic `intros` combines introduction of variables or hypotheses and case analysis. An introduction pattern is either:

- A naming introduction pattern, i.e. either one of:
  - the pattern `?`
  - the pattern `?`ident
  - an identifier
- A disjunctive/conjunctive introduction pattern, i.e. either one of:
  - a disjunction of lists of patterns: `[``p``11``` `…``` `p``1m``1``|` `…``|` `p``11``` `…``` `p``nm``n``]`
  - a conjunction of patterns: `(` p1 `,` … `,` pn `)`
  - a list of patterns `(` p1 `&` … `&` pn `)` for sequence of right-associative binary constructs
- the wildcard: `_`
- the rewriting orientations: `->` or `<-`

Assuming a goal of type `Q``->` `P` (non dependent product), or of type `forall` `x``:``T``,` `P` (dependent product), the behavior of `intros` `p` is defined inductively over the structure of the introduction pattern p:

- introduction on `?` performs the introduction, and lets Coq choose a fresh name for the variable;
- introduction on `?`ident performs the introduction, and lets Coq choose a fresh name for the variable based on ident;
- introduction on ident behaves as described in Section 8.3.5;
- introduction over a disjunction of list of patterns `[``p``11``` `…``` `p``1m``1``|` `…``|` `p``11``` `…``` `p``nm``n``]` expects the product to be over an inductive type whose number of constructors is n (or more generally over a type of conclusion an inductive type built from n constructors, e.g. `C -> A``\``/B if` `n=2`): it destructs the introduced hypothesis as `destruct` (see Section 8.7.2) would and applies on each generated subgoal the corresponding tactic; `intros` pi1 … pimi; if the disjunctive pattern is part of a sequence of patterns and is not the last pattern of the sequence, then Coq completes the pattern so as all the argument of the constructors of the inductive type are introduced (for instance, the list of patterns `[``` `|``` `] H` applied on goal `forall x:nat, x=0 -> 0=x` behaves the same as the list of patterns `[``` `|``` `?``` `] H`);
- introduction over a conjunction of patterns `(``p``1``, …,` `p``n``)` expects the goal to be a product over an inductive type I with a single constructor that itself has at least n arguments: it performs a case analysis over the hypothesis, as `destruct` would, and applies the patterns p1 … pn to the arguments of the constructor of I (observe that `(``p``1``,` `…``,` `p``n``)` is an alternative notation for `[``p``1``` `…``` `p``n``]`);
- introduction via `(` `p``1``& …&` `p``n``)` is a shortcut for introduction via `(``p``1``,(…,(…,``p``n``)…))`; it expects the hypothesis to be a sequence of right-associative binary inductive constructors such as `conj` or `ex_intro`; for instance, an hypothesis with type `A```/\```exists x, B```/\```C```/\```D` can be introduced via pattern `(a & x & b & c & d)`;
- introduction on the wildcard depends on whether the product is dependent or not: in the non dependent case, it erases the corresponding hypothesis (i.e. it behaves as an `intro` followed by a `clear`, cf Section 8.3.2) while in the dependent case, it succeeds and erases the variable only if the wildcard is part of a more complex list of introduction patterns that also erases the hypotheses depending on this variable;
- introduction over `->` (respectively `<-`) expects the hypothesis to be an equality and the right-hand-side (respectively the left-hand-side) is replaced by the left-hand-side (respectively the right-hand-side) in both the conclusion and the context of the goal; if moreover the term to substitute is a variable, the hypothesis is removed.

Remark: `intros` `p``1``… p``n` is not equivalent to `intros` `p``1``;…; intros` `p``n` for the following reasons:

- A wildcard pattern never succeeds when applied isolated on a dependent product, while it succeeds as part of a list of introduction patterns if the hypotheses that depends on it are erased too.
- A disjunctive or conjunctive pattern followed by an introduction pattern forces the introduction in the context of all arguments of the constructors before applying the next pattern while a terminal disjunctive or conjunctive pattern does not. Here is an example
  `Coq` `<``Goal forall n:nat, n = 0 -``>``n = 0.`
  `1 subgoal`
  ``
  `============================`
  `forall n : nat, n = 0 -``>``n = 0`
  `Coq` `<``intros [ | ] H.`
  `2 subgoals`
  ``
  `H : 0 = 0`
  `============================`
  `0 = 0`
  `subgoal 2 is:`
  `S n = 0`
  `Coq` `<``Show 2.`
  `subgoal 2 is:`
  ``
  `n : nat`
  `H : S n = 0`
  `============================`
  `S n = 0`
  `Coq` `<``Undo.`
  `1 subgoal`
  ``
  `============================`
  `forall n : nat, n = 0 -``>``n = 0`
  `Coq` `<``intros [ | ]; intros H.`
  `2 subgoals`
  ``
  `H : 0 = 0`
  `============================`
  `0 = 0`
  `subgoal 2 is:`
  `S H = 0 -``>``S H = 0`
  `Coq` `<``Show 2.`
  `subgoal 2 is:`
  ``
  `H : nat`
  `============================`
  `S H = 0 -``>``S H = 0`

`Coq` `<``Lemma intros_test : forall A B C:Prop, A` `\``/ B /``\``C -``>``(A -``>``C) -``>``C.`
`1 subgoal`
``
`============================`
`forall A B C : Prop, A` `\``/ B /``\``C -``>``(A -``>``C) -``>``C`
`Coq` `<``intros A B C [a| [_ c]] f.`
`2 subgoals`
``
`A : Prop`
`B : Prop`
`C : Prop`
`a : A`
`f : A -``>``C`
`============================`
`C`
`subgoal 2 is:`
`C`
`Coq` `<``apply (f a).`
`1 subgoal`
``
`A : Prop`
`B : Prop`
`C : Prop`
`c : C`
`f : A -``>``C`
`============================`
`C`
`Coq` `<``exact c.`
`Proof completed.`
`Coq` `<``Qed.`
`intros A B C [a| (_, c)] f.`
`apply (f a).`
``
`exact c.`
``
`intros_test is defined`

### 8.7.4 `double induction` ident`1``` ident`2`

This tactic is deprecated and should be replaced by `induction` ident`1``; induction` ident`2` (or `induction` ident`1``; destruct` ident`2` depending on the exact needs).

Variant:

1. `double induction` num`1``` num`2`

   This tactic is deprecated and should be replaced by `induction` num`1``; induction` num`3` where num3 is the result of num2-num1.

### 8.7.5 `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 [98] and the work of Cristina Cornes around inversion [35]. 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. A simple example is the following:

`Coq` `<``Lemma le_minus : forall n:nat, n` `<``1 -``>``n = 0.`
`1 subgoal`
``
`============================`
`forall n : nat, n` `<``1 -``>``n = 0`
`Coq` `<``intros n H ; induction H.`
`2 subgoals`
``
`n : nat`
`============================`
`n = 0`
`subgoal 2 is:`
`n = 0`

Here we didn’t 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.

`Coq` `<``Require Import Coq.Program.Equality.`
`Coq` `<``Lemma le_minus : forall n:nat, n` `<``1 -``>``n = 0.`
`1 subgoal`
``
`============================`
`forall n : nat, n` `<``1 -``>``n = 0`
`Coq` `<``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.

`Coq` `<``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.

`Coq` `<``inversion H.`
`Proof completed.`

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`. Common useful variants are the following, defined in the same file:

Variants:

1. `dependent induction` ident `generalizing` ident`1``…`ident`n`

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

2. `dependent destruction` ident

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

A larger example of dependent induction and an explanation of the underlying technique are developed in section 10.6.

### 8.7.6 `decompose [` qualid`1``…` qualid`n``]` term``

This tactic allows to recursively decompose a complex proposition in order to obtain atomic ones. Example:

`Coq` `<``Lemma ex1 : forall A B C:Prop, A /``\``B /``\``C` `\``/ B /``\``C` `\``/ C /``\``A -``>``C.`
`1 subgoal`
``
`============================`
`forall A B C : Prop, A /``\``B /``\``C` `\``/ B /``\``C` `\``/ C /``\``A -``>``C`
`Coq` `<``intros A B C H; decompose [and or] H; assumption.`
`Proof completed.`
`Coq` `<``Qed.`

`decompose` does not work on right-hand sides of implications or products.

Variants:

1. `decompose sum` term This decomposes sum types (like `or`).
2. `decompose record` term This decomposes record types (inductive types with one constructor, like `and` and `exists` and those defined with the `Record` macro, see Section 2.1).

### 8.7.7 `functional induction (`qualid`` term`1``…` term`n``).` ``

The experimental tactic `functional induction` performs case analysis and induction following the definition of a function. It makes use of a principle generated by `Function` (see Section 2.3) or `Functional Scheme` (see Section 8.15).

`Coq` `<``Functional Scheme minus_ind := Induction for minus Sort Prop.`
`minus_equation is defined`
`minus_ind is defined`
`Coq` `<```
`Coq` `<``Lemma le_minus : forall n m:nat, (n - m` `<``= n).`
`1 subgoal`
``
`============================`
`forall n m : nat, n - m` `<``= n`
`Coq` `<``intros n m.`
`1 subgoal`
``
`n : nat`
`m : nat`
`============================`
`n - m` `<``= n`
`Coq` `<``functional induction (minus n m); simpl; auto.`
`Proof completed.`
`Coq` `<``Qed.`

Remark: `(`qualid`` term`1``…` term`n``)` must be a correct full application of qualid. In particular, the rules for implicit arguments are the same as usual. For example use `@`qualid if you want to write implicit arguments explicitly.

Remark: Parenthesis over qualid…termn are mandatory.

Remark: `functional induction (f x1 x2 x3)` is actually a wrapper for `induction x1 x2 x3 (f x1 x2 x3) using` qualid followed by a cleaning phase, where qualid is the induction principle registered for f (by the `Function` (see Section 2.3) or `Functional Scheme` (see Section 8.15) command) corresponding to the sort of the goal. Therefore `functional induction` may fail if the induction scheme (qualid) is not defined. See also Section 2.3 for the function terms accepted by `Function`.

Remark: There is a difference between obtaining an induction scheme for a function by using `Function` (see Section 2.3) and by using `Functional Scheme` after a normal definition using `Fixpoint` or `Definition`. See 2.3 for details.

See also: 2.3,8.15,10.4, 8.10.3

Error messages:

1. `Cannot find induction information on` qualid

2. `Not the right number of induction arguments`

Variants:

1. `functional induction (`qualid`` term`1``…` term`n``) using` term`m+1``with` term`n+1``…`term`m`

   Similar to `Induction` and `elim` (see Section 8.7), allows to give explicitly the induction principle and the values of dependent premises of the elimination scheme, including predicates for mutual induction when qualid is part of a mutually recursive definition.

2. `functional induction (`qualid`` term`1``…` term`n``) using` term`m+1``with` ref`1``:=` term`n+1``…` ref`m``:=` term`n`

   Similar to `induction` and `elim` (see Section 8.7).

3. All previous variants can be extended by the usual `as` intro_pattern construction, similar for example to `induction` and `elim` (see Section 8.7).

## 8.8 Equality

These tactics use the equality `eq:forall A:Type, A->A->Prop` defined in file `Logic.v` (see Section 3.1.2). The notation for `eq` T t u is simply `t``=``u` dropping the implicit type of t and u.

### 8.8.1 `rewrite` term``

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

`forall (x``1``:A``1``) … (x``n``:A``n``)``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 `A`1, …, `A`n become new subgoals.

Error messages:

1. `The term provided does not end with an equation`
2. `Tactic generated a subgoal identical to the original goal`
   This happens if term1 does not occur in the goal.

Variants:

1. `rewrite ->` term
   Is equivalent to `rewrite` term
2. `rewrite <-` term
   Uses the equality term1`=`term2 from right to left
3. `rewrite` term `in` `clause`
   Analogous to `rewrite` term but rewriting is done following clause (similarly to 8.5). For instance:
   - `rewrite H in H1` will rewrite `H` in the hypothesis `H1` instead of the current goal.
   - `rewrite H in H1 at 1, H2 at - 2 |- *` means `rewrite H; rewrite H in H1 at 1; rewrite H in H2 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``i` for all hypothesis `H``i``<> 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.
4. `rewrite` term `at` occurrences

   Rewrite only the given occurrences of term1′. Occurrences are specified from left to right as for `pattern` (§8.5.7). The rewrite is always performed using setoid rewriting, even for Leibniz’s equality, so one has to `Import Setoid` to use this variant.

5. `rewrite` term `by` tactic

   Use tactic to completely solve the side-conditions arising from the rewrite.

6. `rewrite` term`1``, …,` term`n`
   Is equivalent to the n successive tactics `rewrite` term`1` up to `rewrite` term`n`, each one working on the first subgoal generated by the previous one. 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.
7. 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.
   - `n``?` : works similarly, except that it will do at most n rewrites.
   - `!` : works as `?`, except that at least one rewrite should succeed, otherwise the tactic fails.
   - `n``!` (or simply `n`) : precisely n rewrites of term will be done, leading to failure if these n rewrites are not possible.
8. `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.

### 8.8.2 `cutrewrite ->` term`1``=` term`2``` ``

This tactic acts like `replace` term`1``with` term`2` (see below).

### 8.8.3 `replace` term`1``with` term`2``` ``

This tactic applies to any goal. It replaces all free occurrences of term1 in the current goal with term2 and generates the equality term2`=`term1 as a subgoal. This equality is automatically solved if it occurs amongst the assumption, or if its symmetric form occurs. It is equivalent to `cut` term`2``=`term`1``; [intro H` `n``; rewrite <- H` `n``; clear H` `n``| assumption || symmetry; try assumption]`.

Error messages:

1. `terms do not have convertible types`

Variants:

1. `replace` term`1``with` term`2``by` tactic
   This acts as `replace` term`1``with` term`2` but applies tactic to solve the generated subgoal term`2``=`term`1`.
2. `replace` term
   Replace term with term’ using the first assumption whose type has the form term`=`term`’` or term`’=`term
3. `replace ->` term
   Replace term with term’ using the first assumption whose type has the form term`=`term`’`
4. `replace <-` term
   Replace term with term’ using the first assumption whose type has the form term`’=`term
5. `replace` term`1``with` term`2``` `clause```
   `replace` term`1``with` term`2``` `clause` `by` tactic
   `replace` term`` `clause`
   `replace ->` term`` `clause`
   `replace <-` term`` `clause`
   Act as before but the replacements take place in clause (see Section 8.5) and not only in the conclusion of the goal.
   The clause argument must not contain any `type of` nor `value of`.

### 8.8.4 `reflexivity` ``

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

Error messages:

1. `The conclusion is not a substitutive equation`
2. `Impossible to unify … with ….`

### 8.8.5 `symmetry` ``

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

Variant: `symmetry in` ident
If the statement of the hypothesis ident has the form `t=u`, the tactic changes it to `u=t`.

### 8.8.6 `transitivity` term

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

### 8.8.7 `subst` ident``

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

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

Variants:

1. `subst` ident`1``…`ident`n`
   Is equivalent to `subst` ident`1``; …; subst` ident`n`.
2. `subst`
   Applies `subst` repeatedly to all identifiers from the context for which an equality exists.

### 8.8.8 `stepl` term

This tactic is for chaining rewriting steps. It assumes a goal of the form “R term1 term2” 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 term2” and adds a new goal stating “eq term term1”.

Lemmas are added to the database using the command

> `Declare Left Step` term`.`

The tactic is especially useful for parametric setoids which are not accepted as regular setoids for `rewrite` and `setoid_replace` (see Chapter 25).

Variants:

1. `stepl` term `by` tactic
   This applies `stepl` term then applies tactic to the second goal.
2. `stepr` term
   `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” and are registered using the command

   > `Declare Right Step` term`.`

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

## 8.9 Equality and inductive sets

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

### 8.9.1 `decide equality` ``

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

Variants:

1. `decide equality` term`1``` term`2``` .
   Solves a goal of the form `{`term1`=`term2`}+{```~``term1`=`term2`}`.

### 8.9.2 `compare` term`1``` term`2```

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

### 8.9.3 `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`1``=` term`2` with term1 and term2 being elements of an inductive set. To build the proof, the tactic traverses the normal forms4 of term1 and term2 looking for a couple of subterms `u` and `w` (`u` subterm of the normal form of term1 and `w` subterm of the normal form of term2), placed at the same positions and whose head symbols are two different constructors. If such a couple of subterms exists, then the proof of the current goal is completed, otherwise the tactic fails.

Remark: 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 messages:

1. `No primitive equality found`
2. `Not a discriminable equality`

Variants:

1. `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.

2. `discriminate` term `with` bindings_list

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

3. `ediscriminate` num
   `ediscriminate` term [`with` bindings_list]

   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.

4. `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 term1 `<>` term2, this behaves as `intro` ident`; injection` ident.

   Error messages:

   1. `No discriminable equalities`
      occurs when the goal does not verify the expected preconditions.

### 8.9.4 `injection` term`` `` ``

The `injection` tactic is based on the fact that constructors of inductive sets are injections. That means that if c is a constructor of an inductive set, and if (c t1) and (c t2) are two terms that are equal then t1 and t2 are equal too.

If term is a proof of a statement of conclusion term`1``=` term`2`, then `injection` applies injectivity as deep as possible to derive the equality of all the subterms of term1 and term2 placed in the same positions. For example, from `(S (S n))=(S (S (S m))` we may derive `n=(S m)`. To use this tactic term1 and term2 should be elements of an inductive set and they should be neither explicitly equal, nor structurally different. We mean by this that, if `n``1` and `n``2` are their respective normal forms, then:

- `n``1` and `n``2` should not be syntactically equal,
- there must not exist any pair of subterms `u` and `w`, `u` subterm of `n``1` and `w` subterm of `n``2` , placed in the same positions and having different constructors as head symbols.

If these conditions are satisfied, then, the tactic derives the equality of all the subterms of term1 and term2 placed in the same positions and puts them as antecedents of the current goal.

Example: Consider the following goal:

`Coq` `<``Inductive list : Set :=`
`Coq` `<``| nil : list`
`Coq` `<``| cons : nat -``>``list -``>``list.`
`Coq` `<``Variable P : list -``>``Prop.`
`Coq` `<``Show.`
`1 subgoal`
``
`l : list`
`n : nat`
`H : P nil`
`H0 : cons n l = cons 0 nil`
`============================`
`P l`
`Coq` `<``injection H0.`
`1 subgoal`
``
`l : list`
`n : nat`
`H : P nil`
`H0 : cons n l = cons 0 nil`
`============================`
`l = nil -``>``n = 0 -``>``P l`

Beware that `injection` yields always an equality in a sigma type whenever the injected object has a dependent type.

Remark: There is a special case for dependent pairs. If we have a decidable equality over the type of the first argument, then it is safe to do the projection on the second one, and so `injection` will work fine. To define such an equality, you have to use the `Scheme` command (see 8.14).

Remark: 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 messages:

1. `Not a projectable equality but a discriminable one`
2. `Nothing to do, it is an equality between convertible terms`
3. `Not a primitive equality`

Variants:

1. `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.

2. `injection` term `with` bindings_list

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

3. `einjection` num
   `einjection` term [`with` bindings_list]

   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.

4. `injection`

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

   Error message: `goal does not satisfy the expected preconditions`

5. `injection` term [`with` bindings_list] `as` intro_pattern … intro_pattern
   `injection` num `as` intro_pattern … intro_pattern
   `injection` `as` intro_pattern … intro_pattern
   `einjection` term [`with` bindings_list] `as` intro_pattern … intro_pattern
   `einjection` num `as` intro_pattern … intro_pattern
   `einjection` `as` intro_pattern … intro_pattern

   These variants apply `intros` intro_pattern … intro_pattern after the call to `injection` or `einjection`.

### 8.9.5 `simplify_eq` term`` `` ``

Let term be the proof of a statement of conclusion term`1``=`term`2`. If term1 and term2 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.

Remark: 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.

Variants:

1. `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.

2. `simplify_eq` term `with` bindings_list

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

3. `esimplify_eq` num
   `esimplify_eq` term [`with` bindings_list]

   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.

4. `simplify_eq`

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

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

Variants:

1. `dependent rewrite <-` ident
   Analogous to `dependent rewrite ->` but uses the equality from right to left.

## 8.10 Inversion

### 8.10.1 `inversion` ident``

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

Remark: 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.

Variants:

1. `inversion` num

   This does the same thing as `intros until` num then `inversion` ident where ident is the identifier for the last introduced hypothesis.

2. `inversion_clear` ident

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

3. `inversion` ident `as` intro_pattern

   This behaves as `inversion` but using names in intro_pattern for naming hypotheses. The intro_pattern must have the form `[` p11 …p1n1 `|` … `|` pm1 …pmnm `]` 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. ni=0).

   The arguments of the ith constructor and the equalities that `inversion` introduces in the context of the goal corresponding to the ith constructor, if it exists, get their names from the list pi1 …pini in order. If there are not enough names, `induction` invents names for the remaining variables to introduce. In case an equation splits into several equations (because `inversion` applies `injection` on the equalities it generates), the corresponding name pij in the list must be replaced by a sublist of the form `[``p``ij1``…``p``ijq``]` (or, equivalently, `(``p``ij1``, …,` `p``ijq``)`) where q is the number of subequalities obtained from splitting the original equation. Here is an example.

   `Coq` `<``Inductive contains0 : list nat -``>``Prop :=`
   `Coq` `<``| in_hd : forall l, contains0 (0 :: l)`
   `Coq` `<``| in_tl : forall l b, contains0 l -``>``contains0 (b :: l).`
   `contains0 is defined`
   `contains0_ind is defined`
   `Coq` `<``Goal forall l:list nat, contains0 (1 :: l) -``>``contains0 l.`
   `1 subgoal`
   ``
   `============================`
   `forall l : Datatypes.list nat, contains0 (1 :: l) -``>``contains0 l`
   `Coq` `<``intros l H; inversion H as [ | l’ p Hl’ [Heqp Heql’] ].`
   `1 subgoal`
   ``
   `l : Datatypes.list nat`
   `H : contains0 (1 :: l)`
   `l’ : Datatypes.list nat`
   `p : nat`
   `Hl’ : contains0 l`
   `Heqp : p = 1`
   `Heql’ : l’ = l`
   `============================`
   `contains0 l`
4. `inversion` num `as` intro_pattern

   This allows to name the hypotheses introduced by `inversion` num in the context.

5. `inversion_clear` ident `as` intro_pattern

   This allows to name the hypotheses introduced by `inversion_clear` in the context.

6. `inversion` ident `in` ident1 … identn

   Let ident1 … identn, be identifiers in the local context. This tactic behaves as generalizing ident1 … identn, and then performing `inversion`.

7. `inversion` ident `as` intro_pattern `in` ident1 … identn

   This allows to name the hypotheses introduced in the context by `inversion` ident `in` ident1 … identn.

8. `inversion_clear` ident `in` ident1 …identn

   Let ident1 … identn, be identifiers in the local context. This tactic behaves as generalizing ident1 … identn, and then performing `inversion_clear`.

9. `inversion_clear` ident `as` intro_pattern `in` ident1 …identn

   This allows to name the hypotheses introduced in the context by `inversion_clear` ident `in` ident1 …identn.

10. `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.

11. `dependent inversion` ident `as` intro_pattern

    This allows to name the hypotheses introduced in the context by `dependent inversion` ident.

12. `dependent inversion_clear` ident

    Like `dependent inversion`, except that ident is cleared from the local context.

13. `dependent inversion_clear` ident `as` intro_pattern

    This allows to name the hypotheses introduced in the context by `dependent inversion_clear` ident.

14. `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.

15. `dependent inversion` ident `as` intro_pattern `with` term

    This allows to name the hypotheses introduced in the context by `dependent inversion` ident `with` term.

16. `dependent inversion_clear` ident `with` term

    Like `dependent inversion … with` but clears ident from the local context.

17. `dependent inversion_clear` ident `as` intro_pattern `with` term

    This allows to name the hypotheses introduced in the context by `dependent inversion_clear` ident `with` term.

18. `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.

19. `simple inversion` ident `as` intro_pattern

    This allows to name the hypotheses introduced in the context by `simple inversion`.

20. `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.

21. `inversion` ident `using` ident′ `in` ident1… identn

    This tactic behaves as generalizing ident1… identn, then doing `inversion` ident `using` ident′.

See also: 10.5 for detailed examples

### 8.10.2 `Derive Inversion` ident `with` `forall (``x``:``T``),``I` `t` `Sort` sort``

This command generates an inversion principle for the `inversion … using` tactic. Let I be an inductive predicate and x the variables occurring in t. This command generates and stocks the inversion lemma for the sort sort corresponding to the instance forall (x:T), I t with the name ident in the global environment. When applied it is equivalent to have inverted the instance with the tactic `inversion`.

Variants:

1. `Derive Inversion_clear` ident `with` forall (x:T), I t `Sort` sort
   When applied it is equivalent to having inverted the instance with the tactic `inversion` replaced by the tactic `inversion_clear`.
2. `Derive Dependent Inversion` ident `with` forall (x:T), I t `Sort` sort
   When applied it is equivalent to having inverted the instance with the tactic `dependent inversion`.
3. `Derive Dependent Inversion_clear` ident `with` forall (x:T), I t `Sort` sort
   When applied it is equivalent to having inverted the instance with the tactic `dependent inversion_clear`.

See also: 10.5 for examples

### 8.10.3 `functional inversion` ident

`functional inversion` is a highly experimental tactic which performs inversion on hypothesis ident of the form qualid`` term`1``…`term`n``=` term or term`=` qualid`` term`1``…`term`n` where qualid must have been defined using `Function` (see Section 2.3).

Error messages:

1. `Hypothesis` ident `must contain at least one Function`
2. `Cannot find inversion information for hypothesis` ident This error may be raised when some inversion lemma failed to be generated by Function.

Variants:

1. `functional inversion` num

   This does the same thing as `intros until` num then `functional inversion` ident where ident is the identifier for the last introduced hypothesis.

2. `functional inversion` ident`` qualid
   `functional inversion` num`` qualid

   In case the hypothesis ident (or num) has a type of the form qualid`1``` term`1``…`term`n``=` qualid`2``` term`n+1``…`term`n+m` where qualid1 and qualid2 are valid candidates to functional inversion, this variant allows to choose which must be inverted.

### 8.10.4 `quote` ident``

This kind of inversion has nothing to do with the tactic `inversion` above. This tactic does `change (`ident `t)`, where `t` is a term built in order to ensure the convertibility. In other words, it does inversion of the function ident. This function must be a fixpoint on a simple recursive datatype: see 10.8 for the full details.

Error messages:

1. `quote: not a simple fixpoint`
   Happens when `quote` is not able to perform inversion properly.

Variants:

1. `quote` ident`[` ident`1``…`ident`n``]`
   All terms that are built only with ident1 …identn will be considered by `quote` as constants rather than variables.

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

### 8.11.1 `classical_left, classical_right`

The tactics `classical_left` and `classical_right` are the analog of the `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.

## 8.12 Automatizing

### 8.12.1 `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 introducing the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and tries to apply one of them (starting from the tactics with lower cost). This process is recursively applied to the generated subgoals.

By default, `auto` only uses the hypotheses of the current goal and the hints of the database named `core`.

Variants:

1. `auto` num

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

2. `auto with` ident`1``…` ident`n`

   Uses the hint databases ident1 … identn in addition to the database `core`. See Section 8.13.1 for the list of pre-defined databases and the way to create or extend a database. This option can be combined with the previous one.

3. `auto with *`

   Uses all existing hint databases, minus the special database `v62`. See Section 8.13.1

4. `auto using` lemma`1``, …,` lemma`n`

   Uses lemma1, …, lemman in addition to hints (can be combined with the `with` ident option). If lemmai is an inductive type, it is the collection of its constructors which is added as hints.

5. `auto using` lemma`1``, …,` lemma`n``with` ident`1``…` ident`n`

   This combines the effects of the `using` and `with` options.

6. `trivial`

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

7. `trivial with` ident`1``…` ident`n`
8. `trivial with *`

Remark: `auto` either solves completely the goal or else leaves it intact. `auto` and `trivial` never fail.

See also: Section 8.13.1

### 8.12.2 `eauto` ``

This tactic generalizes `auto`. In contrast with the latter, `eauto` uses unification of the goal against the hints rather than pattern-matching (in other words, it uses `eapply` instead of `apply`). As a consequence, `eauto` can solve such a goal:

`Coq` `<``Hint Resolve ex_intro.`
`Warning: the hint: eapply ex_intro will only be used by eauto`
`Coq` `<``Goal forall P:nat -``>``Prop, P 0 -``>``exists n, P n.`
`1 subgoal`
``
`============================`
`forall P0 : nat -``>``Prop, P0 0 -``>``exists n : nat, P0 n`
`Coq` `<``eauto.`
`Proof completed.`

Note that `ex_intro` should be declared as an hint.

See also: Section 8.13.1

### 8.12.3 `autounfold with` ident`1``…` ident`n``` ``

This tactic unfolds constants that were declared through a `Hint Unfold` in the given databases.

Variants:

1. `autounfold with` ident`1``…` ident`n``in` `clause`

   Perform the unfolding in the given clause.

2. `autounfold with *`

   Uses the unfold hints declared in all the hint databases.

### 8.12.4 `tauto` ``

This tactic implements a decision procedure for intuitionistic propositional calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff [54]. Note that `tauto` succeeds on any instance of an intuitionistic tautological proposition. `tauto` unfolds negations and logical equivalence but does not unfold any other definition.

The following goal can be proved by `tauto` whereas `auto` would fail:

`Coq` `<``Goal forall (x:nat) (P:nat -``>``Prop), x = 0` `\``/ P x -``>``x` `<``>``0 -``>``P x.`
`1 subgoal`
``
`============================`
`forall (x : nat) (P0 : nat -``>``Prop), x = 0` `\``/ P0 x -``>``x` `<``>``0 -``>``P0 x`
`Coq` `<``intros.`
`1 subgoal`
``
`x : nat`
`P0 : nat -``>``Prop`
`H : x = 0` `\``/ P0 x`
`H0 : x` `<``>``0`
`============================`
`P0 x`
`Coq` `<``tauto.`
`Proof completed.`

Moreover, if it has nothing else to do, `tauto` performs introductions. Therefore, the use of `intros` in the previous proof is unnecessary. `tauto` can for instance prove the following:

`Coq` `<``(* auto would fail *)`
`Coq` `<``Goal forall (A:Prop) (P:nat -``>``Prop),`
`Coq` `<``A` `\``/ (forall x:nat,` `~``A -``>``P x) -``>``forall x:nat,` `~``A -``>``P x.`
`1 subgoal`
``
`============================`
`forall (A : Prop) (P0 : nat -``>``Prop),`
`A` `\``/ (forall x : nat,` `~``A -``>``P0 x) -``>``forall x : nat,` `~``A -``>``P0 x`
`Coq` `<```
`Coq` `<``tauto.`
`Proof completed.`

Remark: In contrast, `tauto` cannot solve the following goal

`Coq` `<``Goal forall (A:Prop) (P:nat -``>``Prop),`
`Coq` `<``A` `\``/ (forall x:nat,` `~``A -``>``P x) -``>``forall x:nat,` `~``` `~``(A` `\``/ P x).`

because `(forall x:nat, ~ A -> P x)` cannot be treated as atomic and an instantiation of `x` is necessary.

### 8.12.5 `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 [104]. If this tactic fails on some goals then `intuition` fails. In fact, `tauto` is simply `intuition fail`.

For instance, the tactic `intuition auto` applied to the goal

    (forall (x:nat), P x)/\B -> (forall (y:nat),P y)/\ P O \/B/\ P O

internally replaces it by the equivalent one:

    (forall (x:nat), P x), B |- P O

and then uses `auto` which completes the proof.

Originally due to César Muñoz, these tactics (`tauto` and `intuition`) have been completely re-engineered by David Delahaye using mainly the tactic language (see Chapter 9). 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.

Variants:

1. `intuition`
   Is equivalent to `intuition auto with *`.

### 8.12.6 `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).

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

Variants:

1. `firstorder` tactic

   Tries to solve the goal with tactic when no logical rule may apply.

2. `firstorder with` ident`1``…` ident`n```

   Adds lemmas ident1 … identn to the proof-search environment.

3. `firstorder using` qualid`1``, … ,` qualid`n```

   Adds lemmas in `auto` hints bases qualid1 … qualidn to the proof-search environment. If qualidi refers to an inductive type, it is the collection of its constructors which is added as hints.

4. `firstorder using` qualid`1``, … ,` qualid`n``with` ident`1``…` ident`n`

   This combines the effects of the `using` and `with` options.

Proof-search is bounded by a depth parameter which can be set by typing the `Set Firstorder Depth` `n` vernacular command.

### 8.12.8 `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 include the constructor theory (see 8.9.4 and 8.9.3). 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, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the members of the equality must contain all the quantified variables in order for `congruence` to match against it.

`Coq` `<``Theorem T:`
`Coq` `<``a=(f a) -``>``(g b (f a))=(f (f a)) -``>``(g a b)=(f (g b a)) -``>``(g a b)=a.`
`1 subgoal`
``
`============================`
`a = f a -``>``g b (f a) = f (f a) -``>``g a b = f (g b a) -``>``g a b = a`
`Coq` `<``intros.`
`1 subgoal`
``
`H : a = f a`
`H0 : g b (f a) = f (f a)`
`H1 : g a b = f (g b a)`
`============================`
`g a b = a`
`Coq` `<``congruence.`
`Proof completed.`
`Coq` `<``Theorem inj : f = pair a -``>``Some (f c) = Some (f d) -``>``c=d.`
`1 subgoal`
``
`============================`
`f = pair a -``>``Some (f c) = Some (f d) -``>``c = d`
`Coq` `<``intros.`
`1 subgoal`
``
`H : f = pair a`
`H0 : Some (f c) = Some (f d)`
`============================`
`c = d`
`Coq` `<``congruence.`
`Proof completed.`

Variants:

1. `congruence` `n`
   Tries to add at most `n` instances of hypotheses stating quantified equalities to the problem in order to solve it. A bigger value of `n` does not make success slower, only failure. You might consider adding some lemmas as hypotheses using `assert` in order for congruence to use them.

Variants:

1. `congruence with` term`1``…` term`n`
   Adds term`1``…` term`n` to the pool of terms used by `congruence`. This helps in case you have partially applied constructors in your goal.

Error messages:

1. `I don’t know how to handle dependent equality`
   The decision procedure managed to find a proof of the goal or of a discriminable equality but this proof couldn’t be built in Coq because of dependently-typed functions.
2. `I couldn’t solve goal`
   The decision procedure didn’t find any way to solve the goal.
3. `Goal is solvable by congruence but some arguments are missing. Try "congruence with …", 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 `with` variant described above.

### 8.12.9 `omega` ``

The tactic `omega`, due to Pierre Crégut, is an automatic decision procedure for Presburger arithmetic. It solves quantifier-free formulas built with `~`, `\/`, `/\`, `->` on top of equalities, inequalities and disequalities on both the type `nat` of natural numbers and `Z` of binary integers. This tactic must be loaded by the command `Require Import Omega`. See the additional documentation about `omega` (see Chapter 19).

### 8.12.10 `ring` and `ring_simplify` term`1``…` term`n`

The `ring` tactic solves equations upon polynomial expressions of a ring (or semi-ring) structure. It proceeds by normalizing both hand sides of the equation (w.r.t. associativity, commutativity and distributivity, constant propagation) and comparing syntactically the results.

`ring_simplify` applies the normalization procedure described above to the terms given. The tactic then replaces all occurrences of the terms given in the conclusion of the goal by their normal forms. If no term is given, then the conclusion should be an equation and both hand sides are normalized.

See Chapter 23 for more information on the tactic and how to declare new ring structures.

### 8.12.11 `field`, `field_simplify` term`1``…` term`n` and `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`1``…`term`n` replaces the provided terms by their reduced fraction. `field_simplify_eq` applies when the conclusion is an equation: it simplifies both hand sides and multiplies so as to cancel denominators. So it produces an equation without division nor inverse.

All of these 3 tactics may generate a subgoal in order to prove that denominators are different from zero.

See Chapter 23 for more information on the tactic and how to declare new field structures.

Example:

`Coq` `<``Require Import Reals.`
`Coq` `<``Goal forall x y:R,`
`Coq` `<``(x * y` `>``0)%R -``>`
`Coq` `<``(x * (1 / x + x / (x + y)))%R =`
`Coq` `<``((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R.`
`Coq` `<``intros; field.`
`1 subgoal`
``
`x : R`
`y : R`
`H : (x * y` `>``0)%R`
`============================`
`(x + y)%R` `<``>``0%R /``\``y` `<``>``0%R /``\``x` `<``>``0%R`

See also: file `plugins/setoid_ring/RealField.v` for an example of instantiation,
theory `theories/Reals` for many examples of use of `field`.

### 8.12.12 `fourier`

This tactic written by Loïc Pottier solves linear inequalities on real numbers using Fourier’s method [63]. This tactic must be loaded by `Require Import Fourier`.

Example:

`Coq` `<``Require Import Reals.`
`Coq` `<``Require Import Fourier.`
`Coq` `<``Goal forall x y:R, (x` `<``y)%R -``>``(y + 1` `>``= x - 1)%R.`
`Coq` `<``intros; fourier.`
`Proof completed.`

### 8.12.13 `autorewrite with` ident`1``…`ident`n``.` ``

This tactic 5 carries out rewritings according the rewriting rule bases ident`1``…`ident`n`.

Each rewriting rule of a base identi is applied to the main subgoal until it fails. Once all the rules have been processed, if the main subgoal has progressed (e.g., if it is distinct from the initial main goal) then the rules of this base are processed again. If the main subgoal has not progressed then the next base is processed. For the bases, the behavior is exactly similar to the processing of the rewriting rules.

The rewriting rule bases are built with the `Hint Rewrite` vernacular command.

Warning: This tactic may loop if you build non terminating rewriting systems.

Variant:

1. `autorewrite with` ident`1``…`ident`n``using` tactic
   Performs, in the same way, all the rewritings of the bases ident`1``` `...``` ident`n` applying tactic to the main subgoal after each rewriting step.
2. `autorewrite with` ident`1``…`ident`n``in` qualid

   Performs all the rewritings in hypothesis qualid.

3. `autorewrite with` ident`1``…`ident`n``in` qualid `using` tactic

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

4. `autorewrite with` ident`1``…`ident`n``in` `clause` Performs all the rewritings in the clause clause.
   The clause argument must not contain any `type of` nor `value of`.

See also: Section 8.13.4 for feeding the database of lemmas used by `autorewrite`.

See also: Section 10.7 for examples showing the use of this tactic.

## 8.13 Controlling automation

### 8.13.1 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. One can use the command `Print Hint` ident to display the hints associated to the head symbol ident (see 8.13.3). Each hint has a cost that is an 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.

`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. 8.13.1), 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 do 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 observationaly different from the legacy one.

Variants:

1. `Local Hint` hint_definition `:` ident1 … identn

   This is used to declare a hint database that must not be exported to the other modules that require and import the current module. Inside a section, the option `Local` is useless since hints do not survive anyway to the closure of sections.

The general command to add a hint to some database ident1, …, identn is:

`Hint` hint_definition `:` ident1 … identn

where hint_definition is one of the following expressions:

- `Resolve` term

  This command adds `apply` term to the hint list with the head symbol of the type of term. The cost of that hint is the number of subgoals generated by `apply` term.

  In case the inferred type of term does not start with a product the tactic added in the hint list is `exact` term. In case this type can be reduced to a type starting with a product, the tactic `apply` term is also stored in the hints list.

  If the inferred type of term contains a dependent quantification on a predicate, it is added to the hint list of `eapply` instead of the hint list of `apply`. In this case, a warning is printed since the hint is only used by the tactic `eauto` (see 8.12.2). A typical example of a hint that is used only by `eauto` is a transitivity lemma.

  Error messages:

  1. `Bound head variable`

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

  2. term `cannot be used as a hint`

     The type of term contains products over variables which do not appear in the conclusion. A typical example is a transitivity axiom. In that case the `apply` tactic fails, and thus is useless.

  Variants:

  1. `Resolve` term1 …termm

     Adds each `Resolve` termi.

- `Immediate` term

  This command adds `apply` term`; 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 `apply` term 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 messages:

  1. `Bound head variable`
  2. term `cannot be used as a hint`

  Variants:

  1. `Immediate` term1 …termm

     Adds each `Immediate` termi.

- `Constructors` ident

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

  Error messages:

  1. ident `is not an inductive type`
  2. ident `not declared`

  Variants:

  1. `Constructors` ident1 …identm

     Adds each `Constructors` identi.

- `Unfold` qualid

  This adds the tactic `unfold` qualid to the hint list that will only be used when the head constant of the goal is ident. Its cost is 4.

  Variants:

  1. `Unfold` ident1 …identm

     Adds each `Unfold` identi.

- `Transparent`, `Opaque` qualid

  This adds a transparency hint to the database, making qualid a transparent or opaque constant 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.

  Variants:

  1. `Transparent`, `Opaque` ident1 …identm

     Declares each identi as a transparent or opaque constant.

- `Extern` num`[`pattern`] =>` tactic

  This hint type is to extend `auto` with tactics other than `apply` and `unfold`. For that, we must specify a cost, an optional pattern and a tactic to execute. Here is an example:

  >     Hint Extern 4 (~(_ = _)) => discriminate.

  Now, when the head of the goal is a disequality, `auto` will try `discriminate` if it does not 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 ident, like `?X1` or `?X2`. Here is an example:

  `Coq` `<``Require Import List.`
  `Coq` `<``Hint Extern 5 ({?X1 = ?X2} + {?X1` `<``>``?X2}) =``>`
  `Coq` `<``generalize X1, X2; decide equality : eqdec.`
  `Coq` `<``Goal`
  `Coq` `<``forall a b:list (nat * nat), {a = b} + {a` `<``>``b}.`
  `1 subgoal`
  ``
  `============================`
  `forall a b : list (nat * nat), {a = b} + {a` `<``>``b}`
  `Coq` `<``info auto with eqdec.`
  `== intro a; intro b; generalize a, b; decide equality;`
  `generalize a1, p; decide equality.`
  `generalize b1, n0; decide equality.`
  ``
  `generalize a3, n; decide equality.`
  ``
  `Proof completed.`

Remark: One can use an `Extern` hint with no pattern to do pattern-matching on hypotheses using `match goal with` inside the tactic.

Variants:

1. `Hint` hint_definition

   No database name is given: the hint is registered in the `core` database.

2. `Hint Local` hint_definition `:` ident1 … identn

   This is used to declare hints that must not be exported to the other modules that require and import the current module. Inside a section, the option `Local` is useless since hints do not survive anyway to the closure of sections.

3. `Hint Local` hint_definition

   Idem for the `core` database.

### 8.13.2 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 the hints declared to belong to this database in each of the various modules currently loaded. Especially, requiring new modules potentially extend a database. At Coq startup, only the `core` and `v62` databases are non empty and can be used.

`core`
  This special database is automatically used by `auto`. It contains only basic lemmas about negation, conjunction, and so on from. Most of the hints in this database come from the `Init` and `Logic` directories.
`arith`
  This database contains all lemmas about Peano’s arithmetic proved in the directories `Init` and `Arith`
`zarith`
  contains lemmas about binary signed integers from the directories `theories/ZArith`. When required, the module `Omega` also extends the database `zarith` with a high-cost hint that calls `omega` on equations and inequalities in `nat` or `Z`.
`bool`
  contains lemmas about booleans, mostly from directory `theories/Bool`.
`datatypes`
  is for lemmas about lists, streams and so on that are mainly proved in the `Lists` subdirectory.
`sets`
  contains lemmas about sets and relations from the directories `Sets` and `Relations`.
`typeclass_instances`
  contains all the type class instances declared in the environment, including those used for `setoid_rewrite`, from the `Classes` directory.

There is also a special database called `v62`. It collects all hints that were declared in the versions of Coq prior to version 6.2.4 when the databases `core`, `arith`, and so on were introduced. The purpose of the database `v62` is to ensure compatibility with further versions of Coq for developments done in versions prior to 6.2.4 (`auto` being replaced by `auto with v62`). The database `v62` is intended not to be extended (!). It is not included in the hint databases list used in the `auto with *` tactic.

Furthermore, you are advised not to put your own hints in the `core` database, but use one or several databases specific to your development.

### 8.13.3 `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:

1. `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.

2. `Print Hint *`

   This command displays all declared hints.

3. `Print HintDb` ident``

   This command displays all hints from database ident.

### 8.13.4 `Hint Rewrite` term`1``…`term`n``:` ident``

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

This command is synchronous with the section mechanism (see 2.4): 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:

1. `Hint Rewrite ->` term`1``…`term`n``:` ident
   This is strictly equivalent to the command above (we only make explicit the orientation which otherwise defaults to `->`).
2. `Hint Rewrite <-` term`1``…`term`n``:` ident
   Adds the rewriting rules term`1``…`term`n` with a right-to-left orientation in the base ident.
3. `Hint Rewrite` term`1``…`term`n``using` tactic`:` ident
   When the rewriting rules term`1``…`term`n` in ident will be used, the tactic tactic will be applied to the generated subgoals, the main subgoal excluded.
4. `Print Rewrite HintDb` ident

   This command displays all rewrite hints contained in ident.

### 8.13.5 Hints and sections

Hints provided by the `Hint` commands are erased when closing a section. Conversely, all hints of a module `A` that are not defined inside a section (and not defined with option `Local`) become available when the module `A` is imported (using e.g. `Require Import A.`).

### 8.13.6 Setting implicit automation tactics

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

See also: `Proof.` in Section 7.1.4.

#### `Declare Implicit Tactic` tactic`.`

This command declares a tactic to be used to solve implicit arguments that Coq does not know how to solve by unification. It is used every time the term argument of a tactic has one of its holes not fully resolved.

Here is an example:

`Coq` `<``Parameter quo : nat -``>``forall n:nat, n``<``>``0 -``>``nat.`
`quo is assumed`
`Coq` `<``Notation "x // y" := (quo x y _) (at level 40).`
`Coq` `<```
`Coq` `<``Declare Implicit Tactic assumption.`
`Coq` `<``Goal forall n m, m``<``>``0 -``>``{ q:nat & { r | q * m + r = n } }.`
`1 subgoal`
``
`============================`
`forall n m : nat, m` `<``>``0 -``>``{q : nat & {r : nat | q * m + r = n}}`
`Coq` `<``intros.`
`1 subgoal`
``
`n : nat`
`m : nat`
`H : m` `<``>``0`
`============================`
`{q : nat & {r : nat | q * m + r = n}}`
`Coq` `<``exists (n // m).`
`1 subgoal`
``
`n : nat`
`m : nat`
`H : m` `<``>``0`
`============================`
`{r : nat | n // m * m + r = n}`

The tactic `exists (n // m)` did not fail. The hole was solved by `assumption` so that it behaved as `exists (quo n m H)`.

## 8.14 Generation of induction principles with `Scheme`

The `Scheme` command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema:

> `Scheme` ident`1``:= Induction for` ident`’``1``Sort` sort`1``
> with
> …
> with` ident`m``:= Induction for` ident`’``m``Sort` sort`m`

where ident’1 … ident’m are different inductive type identifiers belonging to the same package of mutual inductive definitions. This command generates ident1… identm to be mutually recursive definitions. Each term identi proves a general principle of mutual induction for objects in type termi.

Variants:

1. `Scheme` ident`1``:= Minimality for` ident`’``1``Sort` sort`1``
   with
   …
   with` ident`m``:= Minimality for` ident`’``m``Sort` sort`m`

   Same as before but defines a non-dependent elimination principle more natural in case of inductively defined relations.

2. `Scheme Equality for` ident`1`

   Tries to generate a boolean equality and a proof of the decidability of the usual equality.

3. `Scheme Induction for` ident`1``Sort` sort`1``
   with
   …
   with Induction for` ident`m``Sort` sort`m`

   If you do not provide the name of the schemes, they will be automatically computed from the sorts involved (works also with Minimality).

See also: Section 10.3

### 8.14.1 Automatic declaration of schemes

It is possible to deactivate the automatic declaration of the induction principles when defining a new inductive type with the `Unset Elimination Schemes` command. It may be reactivated at any time with `Set Elimination Schemes`.
You can also activate the automatic declaration of those boolean equalities (see the second variant of `Scheme`) with the `Set Equality Schemes` command. However you have to be careful with this option since Coq may now reject well-defined inductive types because it cannot compute a boolean equality for them.

### 8.14.2 `Combined Scheme```

The `Combined Scheme` command is a tool for combining induction principles generated by the `Scheme` command. Its syntax follows the schema :

`Combined Scheme` ident`0``from` ident`1``, ..,` ident`n`
ident1 …identn are different inductive principles that must belong to the same package of mutual inductive principle definitions. This command generates ident0 to be the conjunction of the principles: it is built from the common premises of the principles and concluded by the conjunction of their conclusions.

See also: Section 10.3.1

## 8.15 Generation of induction principles with `Functional Scheme`

The `Functional Scheme` command is a high-level experimental tool for generating automatically induction principles corresponding to (possibly mutually recursive) functions. Its syntax follows the schema:

> `Functional Scheme` ident`1``:= Induction for` ident`’``1``Sort` sort`1``
> with
> …
> with` ident`m``:= Induction for` ident`’``m``Sort` sort`m`

where ident’1 … ident’m are different mutually defined function names (they must be in the same order as when they were defined). This command generates the induction principles ident1…identm, following the recursive structure and case analyses of the functions ident’1 … ident’m.

##### `Functional Scheme`

There is a difference between obtaining an induction scheme by using `Functional Scheme` on a function defined by `Function` or not. Indeed `Function` generally produces smaller principles, closer to the definition written by the user.

See also: Section 10.4

## 8.16 Simple tactic macros

A simple example has more value than a long explanation:

`Coq` `<``Ltac Solve := simpl; intros; auto.`
`Solve is defined`
`Coq` `<``Ltac ElimBoolRewrite b H1 H2 :=`
`Coq` `<``elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ].`
`ElimBoolRewrite is defined`

The tactics macros are synchronous with the Coq section mechanism: a tactic definition is deleted from the current environment when you close the section (see also 2.4) where it was defined. If you want that a tactic macro defined in a module is usable in the modules that require it, you should put it outside of any section.

Chapter 9 gives examples of more complex user-defined tactics.

1
  but it does not rename the hypothesis in the proof-term...
2
  Actually, only the second subgoal will be generated since the other one can be automatically checked.
3
  This corresponds to the cut rule of sequent calculus.
4
  Reminder: opaque constants will not be expanded by δ reductions
5
  The behavior of this tactic has much changed compared to the versions available in the previous distributions (V6). This may cause significant changes in your theories to obtain the same result. As a drawback of the re-engineering of the code, this tactic has also been completely revised to get a very compact and readable version.