Previous Up Next

Chapter 8  Tactics

A deduction rule is a link between some (unique) formula, that we call the conclusion and (several) formulæ 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

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 Cic 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

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 ident1 ... identn.

    This is equivalent to clear ident1. ... clear identn.

  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.

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 ident1 after ident2

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.


Error messages:
  1. identi not found

  2. Cannot move ident1 after ident2: it occurs in ident2

  3. Cannot move ident1 after ident2: it depends on ident2

8.3.4  rename ident1 into ident2

This renames hypothesis ident1 into ident2 in the current context1


Error messages:
  1. ident2 not found

  2. ident2 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 Hn:T (if T is of type Set or Prop) or Xn:T (if the type of T is Type). The optional index n is such that Hn or Xn is a fresh identifier. In both cases the new subgoal is U.

If the goal is 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.5.2).

  3. intros ident1 ... identn

    Is equivalent to the composed tactic intro ident1; ... ; intro identn.

    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 premise. For instance, on the subgoal forall x y:nat, x=y -> forall z:nat,z=x->z=y the tactic intros until 2 is equivalent to intros x y H z H0 (assuming x, y, H, z and H0 do not already occur in context).


    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

    Applies intro but puts the introduced hypothesis after the hypothesis ident in the hypotheses.


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


  7. intro ident1 after ident2

    Behaves as previously but ident1 is the name of the introduced hypothesis. It is equivalent to intro ident1; move ident1 after ident2.


    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. The tactic apply relies on first-order pattern-matching with dependent types. See pattern in section 8.5.7 to transform a second-order pattern-matching problem into a first-order one.


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

  2. generated subgoal term' has metavariables in it

    This occurs when some instantiations of 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 term1 ... termn

    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 (ref1 := term1) ... (refn := termn)

    This also provides apply with values for instantiating premises. But variables are referred by names and non dependent products by order (see syntax in Section 8.3.11).

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

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


Warning: V8 updating to do




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 *

    This is equivalent to the above form but applies everywhere in the goal (both in conclusion and hypotheses).

  2. set ( ident := term ) in * |-

    This is equivalent to the above form but applies everywhere in the hypotheses.

  3. set ( ident := term ) in |- *

    This is equivalent to the default behaviour of set.

  4. set ( ident0 := term ) in ident1

    This behaves the same but substitutes term not in the goal but in the hypothesis named ident1.

  5. set ( ident0 := term ) in ident1 at num1 ... numn

    This notation allows to specify which occurrences of the hypothesis named ident1 (or the goal if ident1 is the word Goal) should be substituted. The occurrences are numbered from left to right. A negative occurrence number means an occurrence which should not be substituted.

  6. set ( ident0 := term ) in ident1 at num11 ... numn11, ...identm at num1m ...numnmm

    It substitutes term at occurrences num1i ... numnii of hypothesis identi. One of the ident's may be the word Goal.

  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.

  8. 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 U3. 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.

8.3.9  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 accordingly to T.


Variants:
  1. generalize term1 ... termn

    Is equivalent to generalize termn; ... ; generalize term1. Note that the sequence of termi's are processed from n to 1.

  2. generalize dependent term

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

8.3.10  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 term1 with term2

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

  2. change term1 at num1 ... numi with term2

    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 term1 with term2 in ident

  5. change term1 at num1 ... numi with term2 in ident

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

See also: 8.5

8.3.11  Bindings list

A bindings list is generally used after the keyword with in tactics. The general shape of a bindings list is (ref1 := term1) ... (refn := termn) where ref is either an ident or a num. It is used to provide a tactic with a list of values (term1, ..., termn) that have to be substituted respectively to ref1, ..., refn. For all i in [1... n], if refi is identi then it references the dependent product identi:T (for some type T); if refi is numi then it references the numi-th non dependent premise.

A bindings list can also be a simple list of terms term1 term2 ...termn. In that case the references to which these terms correspond are determined by the tactic. In case of elim (see section 4) the terms should correspond to all the dependent products in the type of term while in the case of apply only the dependent products which are not bound in the conclusion of the type are given.

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

8.5  Conversion tactics

This set of tactics implements different specialized usages of the tactic change.

All conversion tactics (including change) can be parameterised by the parts of the goal where the conversion can occur. The specification of such parts are called clauses. It can be either the conclusion, or an hypothesis. In the case of a defined hypothesis it is possible to specify if the conversion should occur on the type part, the body part or both (default).

Clauses are written after a conversion tactic (tactic set 8.3.7 also uses clasues) and are introduced by the keyword in. If no clause is provided, the default is to perform the conversion only in the conclusion.

The syntax and description of the various clauses follows:
in H1 ... Hn |-
only in hypotheses H1 ...Hn
in H1 ... Hn |- *
in hypotheses H1 ... Hn and in the conclusion
in * |-
in every hypothesis
in *
(equivalent to in * |- *) everywhere
in (type of H1) (value of H2) ... |-
in type part of H1, in the value part of H2, etc.
For backward compatibility, the notation in H1... Hn performs the conversion in hypotheses H1... Hn.

8.5.1  cbv flag1 ... flagn, lazy flag1 ... flagn and compute

These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. Since the reduction considered in Coq include beta (reduction of functional application), delta (unfolding of transparent constants, see 6.2.5), iota (reduction of Cases, Fix and CoFix expressions) and zeta (removal of local definitions), every flag is one of beta, delta, iota, zeta, [qualid1...qualidk] and -[qualid1...qualidk]. The last two flags give the list of constants to unfold, or the list of constants not to unfold. These two flags can occur only after the delta flag. If alone (i.e. not followed by [qualid1...qualidk] or -[qualid1...qualidk]), the delta flag means that all constants must be unfolded. However, the delta flag does not apply to variables bound by a let-in construction whose unfolding is controlled by the zeta flag only. In addition, there is a flag Evar to perform instantiation of existential variables (``?'') when an instantiation actually exists.

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, but if an argument is used several times, it is computed only once. This reduction is efficient for reducing expressions with dead code. For instance, the proofs of a proposition there existsT  x. P(x) reduce to a pair of a witness t, and a proof that t verifies 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 lambda-abstractions). Despite the lazy strategy always performs fewer reductions than the call-by-value strategy, the latter should be preferred for evaluating purely computational expressions (i.e. with few dead code).


Variants:
  1. compute

    This tactic is an alias for cbv beta delta evar iota zeta.

Error messages:
  1. Delta must be specified before

    A list of constants appeared before the delta flag.

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 betaiota-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 betadeltaiota-reduction rules. hnf does not produce a real head normal form but either a product or an applicative term in head normal form or a variable.


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


Remark: The delta rule only applies to transparent constants (see section 6.2.4 on transparency and opacity).

8.5.4  simpl

This tactic applies to any goal. The tactic simpl first applies betaiota-reduction rule. Then it expands transparent constants and tries to reduce T' according, once more, to betaiota rules. But when the iota rule is not applicable then possible delta-reductions are not applied. For instance trying to use simpl on (plus n O)=n does change nothing.


Variants:
  1. simpl term

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

  2. simpl term at num1 ... numi

    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 num1 ... numi

    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.2.5). The tactic unfold applies the delta rule to each occurrence of the constant to which qualid refers in the current goal and then replaces it with its betaiota-normal form.


Error messages:
  1. qualid does not denote an evaluable constant

Variants:
  1. unfold qualid1, ..., qualidn

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

  2. unfold qualid1 at num11, ..., numi1, ..., qualidn at num1n ... numjn

    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 qualidi


    Error message: qualidi does not occur

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 substituted for 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 beta-expansion (the inverse of beta-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 phi(t) where the notation captures all the instances of t in phi(t), then pattern t transforms it into (fun x:A => phi(x)) t. This command can be used, for instance, when the tactic apply fails on matching.


Variants:
  1. pattern term at num1 ... numn

    Only the occurrences num1 ... numn of term will be considered for beta-expansion. Occurrences are located from left to right.

  2. pattern term1, ..., termm

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

  3. pattern term1 at num11 ... numn11, ..., termm at num1m ... numnmm

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

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 there exists x· P(x). Then, it is equivalent to intros; constructor 1 with bindings_list.

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

  6. left bindings_list, right bindings_list, split bindings_list

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

8.7  Eliminations (Induction and Case Analysis)

Elimination tactics are useful to prove statements by induction or case analysis. Indeed, they make use of the elimination (or induction) principles generated with inductive definitions (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:
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. Cannot refine to conclusions with meta-variables

    As induction uses apply, see Section 8.3.6 and the variant elim ... with ... below.

Variants:
  1. induction term as intro_pattern

    This behaves as induction term but uses the names in intro_pattern to names 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 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 p's can be any introduction patterns (see Section 8.7.3). This provides a concise notation for nested induction.


    Remark: for an inductive type with one constructeur, the pattern notation (p1,...,pn) can be used instead of [ p1 ...pn ].

  2. induction term using qualid

    This behaves as induction term but using the induction scheme of name qualid. It does not expect that the type of term is inductive.

  3. induction term using qualid as intro_pattern

    This combines induction term using qualid and induction term as intro_pattern.

  4. elim term

    This is a more basic induction tactic. Again, the type of the argument term must be an inductive constant. Then according to the type of the goal, the tactic elim chooses the right destructor and applies it (as in the case of the apply tactic). For instance, assume that our proof context contains n:nat, assume that our current goal is T of type Prop, then elim n is equivalent to apply nat_ind with (n:=n). The tactic elim does not affect the hypotheses of the goal, neither introduces the induction loading into the context of hypotheses.

  5. elim term

    also works when the type of term starts with products and the head symbol is an inductive definition. In that case the tactic tries both to find an object in the inductive definition and to use this inductive definition for elimination. In case of non-dependent products in the type, subgoals are generated corresponding to the hypotheses. In the case of dependent products, the tactic will try to find an instance for which the elimination lemma applies.

  6. elim term with term1 ... termn Allows the user to give explicitly the values for dependent premises of the elimination schema. All arguments must be given.


    Error message: Not the right number of dependent arguments

  7. elim term with ref1 := term1 ... refn := termn

    Provides also elim with values for instantiating premises by associating explicitly variables (or non dependent products) with their intended instance.

  8. elim term1 using term2

    Allows the user to give explicitly an elimination predicate term2 which is not the standard one for the underlying inductive type of term1. Each of the term1 and term2 is either a simple term or a term with a bindings list (see 8.3.11).

  9. elimtype form

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


    Error message: Impossible to unify ... with ...

    Arises when form needs to be applied to parameters.

  10. simple induction ident

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

  11. 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:
Variants:
  1. destruct term as intro_pattern

    This behaves as destruct term but uses the names in intro_pattern to names 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 p's can be any introduction patterns (see Section 8.7.3). This provides a concise notation for nested destruction.


    Remark: for an inductive type with one constructeur, the pattern notation (p1,...,pn) can be used instead of [ p1 ...pn ].

  2. destruct term using qualid

    This is a synonym of induction term using qualid.

  3. destruct term as intro_pattern using qualid

    This is a synonym of induction term using qualid as intro_pattern.

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

  5. case term with term1 ... termn

    Analogous to elim ... with above.

  6. simple destruct ident

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

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

The tactic intros applied to introduction patterns performs both introduction of variables and case analysis in order to give names to components of an hypothesis.

An introduction pattern is either: The behavior of intros is defined inductively over the structure of the pattern given as argument:
Remark: The pattern (p1, ..., pn) is a synonym for the pattern [p1 ... pn], i.e. it corresponds to the decomposition of an hypothesis typed by an inductive type with a single constructor.

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 < Proof c.
intros_test is defined

8.7.4  double induction ident1 ident2

This tactic applies to any goal. If the variables ident1 and ident2 of the goal have an inductive type, then this tactic performs double induction on these variables. For instance, if the current goal is forall n m:nat, P n m then, double induction n m yields the four cases with their respective inductive hypotheses. In particular the case for (P (S n) (S m)) with the induction hypotheses (P (S n) m) and (m:nat)(P n m) (hence (P n m) and (P n (S m))).


Remark: When the induction hypothesis (P (S n) m) is not needed, induction ident1; destruct ident2 produces more concise subgoals.


Variant:
  1. double induction num1 num2

    This applies double induction on the num1th and num2th non dependent premises of the goal. More generally, any combination of an ident and an num is valid.

8.7.5  decompose [ qualid1 ... qualidn ] 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 p. ??).

8.7.6  functional induction ident term1 ... termn.

The experimental tactic functional induction performs case analysis and induction following the definition of a (not mutually recursive) function.

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.

functional induction is a shorthand for the more general command Functional Scheme which builds induction principles following the recursive structure of (possibly mutually recursive) functions.
See also: 10.4 for the difference between using one or the other.


Remark: functional induction may fail on functions built by tactics. In particular case analysis of a function are considered only if they are not inside an application.


Remark: Arguments of the function must be given, including implicits. If the function is recursive, arguments must be variables, otherwise they may be any term.


See also: 8.14,10.4

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

(x1:A1) ... (xn:An)term1=term2.

Then rewrite term replaces every occurrence of term1 by term2 in the goal. Some of the variables x1 are solved by unification, and some of the types A1, ..., An become new subgoals.


Remark: In case the type of term1 contains occurrences of variables bound in the type of term, the tactic tries first to find a subterm of the goal which matches this term in order to find a closed instance term'1 of term1, and then all instances of term'1 will be replaced.


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 ident
    Analogous to rewrite term but rewriting is done in the hypothesis named ident.

  4. rewrite -> term in ident
    Behaves as rewrite term in ident.

  5. rewrite <- term in ident
    Uses the equality term1=term2 from right to left to rewrite in the hypothesis named ident.

8.8.2  cutrewrite -> term1 = term2

This tactic acts like replace term1 with term2 (see below).

8.8.3  replace term1 with term2

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. It is equivalent to cut term2=term1; intro Hn; rewrite <- Hn; clear Hn.


Variants:
  1. replace term1 with term2 in ident
    This replaces term1 with term2 in the hypothesis named ident, and generates the subgoal term2=term1.


    Error messages:
    1. No such hypothesis : ident
    2. Nothing to rewrite in ident

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 ident1 ...identn
    Is equivalent to subst ident1; ...; subst identn.
  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 qualid.
where qualid is the name of the lemma.

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


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

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 term1 term2 .
    Solves a goal of the form {term1=term2}+{~term1=term2}.

8.9.2  compare term1 term2

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 ident

This tactic proves any goal from an absurd hypothesis stating that two structurally different terms of an inductive set are equal. For example, from the hypothesis (S (S O))=(S O) we can derive by absurdity any proposition. Let ident be a hypothesis of type term1 = term2 in the local context, 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: If ident does not denote an hypothesis in the local context but refers to an hypothesis quantified in the goal, then the latter is first introduced in the local context using intros until ident.


Error messages:
  1. ident Not a discriminable equality
    occurs when the type of the specified hypothesis is not an equation.

Variants:
  1. discriminate num
    This does the same thing as intros until num then discriminate ident where ident is the identifier for the last introduced hypothesis.
  2. discriminate
    It applies to a goal of the form ~term1=term2 and it is equivalent to: unfold not; intro ident; discriminate ident.


    Error messages:
    1. No discriminable equalities
      occurs when the goal does not verify the expected preconditions.

8.9.4  injection ident

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 ident is an hypothesis of type term1 = term2, then injection behaves as applying injection as deep as possible to derive the equality of all the subterms of term1 and term2 placed in the same positions. For example, from the hypothesis (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 n1 and n2 are their respective normal forms, then: 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: If ident does not denote an hypothesis in the local context but refers to an hypothesis quantified in the goal, then the latter is first introduced in the local context using intros until ident.


Error messages:
  1. ident is not a projectable equality occurs when the type of the hypothesis id does not verify the preconditions.
  2. Not an equation occurs when the type of the hypothesis id is not an equation.

Variants:
  1. injection num

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

  2. injection

    If the current goal is of the form term1 <> term2, the tactic computes the head normal form of the goal and then behaves as the sequence: unfold not; intro ident; injection ident.


    Error message: goal does not satisfy the expected preconditions

8.9.5  simplify_eq ident

Let ident be the name of an hypothesis of type term1=term2 in the local context. If term1 and term2 are structurally different (in the sense described for the tactic discriminate), then the tactic simplify_eq behaves as discriminate ident otherwise it behaves as injection ident.


Remark: If ident does not denote an hypothesis in the local context but refers to an hypothesis quantified in the goal, then the latter is first introduced 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 If the current goal has form ~t1=t2, then this tactic does hnf; intro ident; simplify_eq ident.

8.9.6  dependent rewrite -> ident

This tactic applies to any goal. If ident has type (existS A B a b)=(existS A 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 an hypothesis in the local context but refers to an hypothesis quantified in the goal, then the latter is first introduced in the local context using intros until ident.


Variants:
  1. inversion numThis 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 [pij1 ...pijq] (or, equivalently, (pij1, ..., pijq)) where q is the number of subequations 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 : list nat, contains0 (1 :: l) -> contains0 l

    Coq < intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ].
    1 subgoal
      
      l : list nat
      H : contains0 (1 :: l)
      l' : list nat
      p : nat
      Hl' : contains0 l
      Heqp : p = 1
      Heql' : l' = l
      ============================
       contains0 l


  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 identas intro_pattern

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

  14. dependent inversion ident with termThis variant allow to give the good 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 termThis allows to name the hypotheses introduced in the context by dependent inversion ident with term.

  16. dependent inversion_clear ident with termLike dependent inversion ... with but clears identfrom the local context.

  17. dependent inversion_clear ident as intro_pattern with termThis 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 do.

  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 inversionidentusing 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  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 build 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.7 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 [ ident1 ...identn ]
    All terms that are build only with ident1 ...identn will be considered by quote as constants rather than variables.

8.11  Automatizing

8.11.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 ident1 ... identn

    Uses the hint databases ident1 ... identn in addition to the database core. See Section 8.12 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.12

  4. trivial

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

  5. trivial with ident1 ... identn

  6. trivial with *

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


See also: Section 8.12

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

8.11.3  tauto

This tactic implements a decision procedure for intuitionistic propositional calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff [49]. 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.11.4  intuition tactic

The tactic intuition takes advantage of the search-tree builded 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 [89]. 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 reenginered by David Delahaye using mainly the tactic language (see chapter 9). The code is now quite shorter and a significant increase in performances 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.11.5  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 ident1 ... identn

    Adds lemmata ident1 ... identn to the proof-search environment.

  3. firstorder using ident1 ... identn

    Adds lemmata in auto hints bases ident1 ... identn to the proof-search environment.
Proof-search is bounded by a depth parameter which can be set by typing the Set Firstorder Depth n vernacular command.

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

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 (B:=A) a -> Some (f c) = Some (f d) -> c = d

Coq < intros.
1 subgoal
  
  H : f = pair (B:=A) a
  H0 : Some (f c) = Some (f d)
  ============================
   c = d

Coq < congruence.
Proof completed.


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 managed to find a proof of the goal or of a discriminable equality.

8.11.7  omega

The tactic omega, due to Pierre Crégut, is an automatic decision procedure for Prestburger arithmetic. It solves quantifier-free formulae build with ~, \/, /\, -> on top of equations and inequations 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 (chapter 17).

8.11.8  ring term1 ... termn

This tactic, written by Samuel Boutin and Patrick Loiseleur, applies associative commutative rewriting on every ring. The tactic must be loaded by Require Import Ring. The ring must be declared in the Add Ring command (see 19). The ring of booleans is predefined; if one wants to use the tactic on nat one must first require the module ArithRing; for Z, do Require Import ZArithRing; for N, do Require Import NArithRing.

The terms term1, ..., termn must be subterms of the goal conclusion. The tactic ring normalizes these terms w.r.t. associativity and commutativity and replace them by their normal form.


Variants:
  1. ring When the goal is an equality t1=t2, it acts like ring t1 t2 and then simplifies or solves the equality.

  2. ring_nat is a tactic macro for repeat rewrite S_to_plus_one; ring. The theorem S_to_plus_one is a proof that forall (n:nat), S n = plus (S O) n.

Example:
Coq < Require Import ZArithRing.

Coq < Goal forall a b c:Z,
Coq <   (a + b + c) * (a + b + c) =
Coq <   a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
1 subgoal
  
  ============================
   forall a b c : Z,
   (a + b + c) * (a + b + c) =
   a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c

Coq < intros; ring.
Proof completed.

You can have a look at the files Ring.v, ArithRing.v, ZArithRing.v to see examples of the Add Ring command.


See also: Chapter 19 for more detailed explanations about this tactic.

8.11.9  field

This tactic written by David Delahaye and Micaela Mayero solves equalities using commutative field theory. Denominators have to be non equal to zero and, as this is not decidable in general, this tactic may generate side conditions requiring some expressions to be non equal to zero. This tactic must be loaded by Require Import Field. Field theories are declared (as for ring) with the Add Field command.


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 * ((x + y) * y))%R <> 0%R

8.11.10  Add Field

This vernacular command adds a commutative field theory to the database for the tactic field. You must provide this theory as follows:
Add Field A Aplus Amult Aone Azero Aopp Aeq Ainv Rth Tinvl
where A is a term of type Type, Aplus is a term of type A->A->A, Amult is a term of type A->A->A, Aone is a term of type A, Azero is a term of type A, Aopp is a term of type A->A, Aeq is a term of type A->bool, Ainv is a term of type A->A, Rth is a term of type (Ring_Theory A Aplus Amult Aone Azero Ainv Aeq), and Tinvl is a term of type forall n:A, ~(n=Azero)->(Amult (Ainv n) n)=Aone. To build a ring theory, refer to Chapter 19 for more details.

This command adds also an entry in the ring theory table if this theory is not already declared. So, it is useless to keep, for a given type, the Add Ring command if you declare a theory with Add Field, except if you plan to use specific features of ring (see Chapter 19). However, the module ring is not loaded by Add Field and you have to make a Require Import Ring if you want to call the ring tactic.


Variants:
  1. Add Field A Aplus Amult Aone Azero Aopp Aeq Ainv Rth Tinvl
        with minus:=Aminus

    Adds also the term Aminus which must be a constant expressed by means of Aopp.

  2. Add Field A Aplus Amult Aone Azero Aopp Aeq Ainv Rth Tinvl
        with div:=Adiv

    Adds also the term Adiv which must be a constant expressed by means of Ainv.

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


See also: [37] for more details regarding the implementation of field.

8.11.11  fourier

This tactic written by Loïc Pottier solves linear inequations on real numbers using Fourier's method [58]. 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.11.12  autorewrite with ident1 ...identn.

This tactic 5 carries out rewritings according the rewriting rule bases ident1 ...identn.

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 ident1 ...identn using tactic
    Performs, in the same way, all the rewritings of the bases ident1 ... identn applying tactic to the main subgoal after each rewriting step.

8.11.13  Hint Rewrite term1 ...termn : ident

This vernacular command adds the terms term1 ...termn (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.3): 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 -> term1 ...termn : ident
    This is strictly equivalent to the command above (we only make explicit the orientation which otherwise defaults to ->).

  2. Hint Rewrite <- term1 ...termn : ident
    Adds the rewriting rules term1 ...termn with a right-to-left orientation in the base ident.

  3. Hint Rewrite term1 ...termn using tactic : ident
    When the rewriting rules term1 ...termn in ident will be used, the tactic tactic will be applied to the generated subgoals, the main subgoal excluded.

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

8.12  The hints databases for auto and eauto

The hints for auto and eauto are stored in databases. Each databases maps head symbols to list of hints. One can use the command Print Hint ident to display the hints associated to the head symbol ident (see 8.12.2). Each hint has a cost that is an nonnegative integer, and a pattern. The hint is tried by auto if the conclusion of current goal matches its pattern, and after hints with a lower cost. The general command to add a hint to some databases ident1, ..., identn is:
Hint hint_definition : ident1 ... identn
where hint_definition is one of the following expressions:

where hint_definition is one of the following expressions:
Remark: There is currently (in the 8.0 release) no way to do pattern-matching on hypotheses.


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.12.1  Hint databases defined in the Coq standard library

Several hint databases are defined in the Coq standard library. There is no systematic relation between the directories of the library and the databases.
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 proven in the directories Init and Arith

zarith
contains lemmas about binary signed integers from the directories theories/ZArith and contrib/omega. It contains also a hint with a high cost that calls omega.

bool
contains lemmas about booleans, mostly from directory theories/Bool.

datatypes
is for lemmas about lists, streams and so on that are mainly proven in the Lists subdirectory.

sets
contains lemmas about sets and relations from the directories Sets and Relations.
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.12.2  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, to 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.12.3  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  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 ident1 := Induction for ident'1 Sort sort1
with
...
with identm := Induction for ident'm Sort sortm
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 ident1 := Minimality for ident'1 Sort sort1
    with
    ...
    with     identm := Minimality for ident'm Sort sortm

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

See also: 10.3


See also: Section 10.3

8.14  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 identi := Induction for ident'i with ident'1 ... ident'm.
ident'1 ... ident'm are the names of mutually recursive functions (they must be in the same order as when they were defined), ident'i being one of them. This command generates the induction principle identi, following the recursive structure and case analyses of the functions ident'1 ... ident'm, and having ident'i as entry point.


Variants:
  1. Functional Scheme ident1 := Induction for ident'1.

    This command is a shortcut for:
    Functional Scheme ident1 := Induction for ident'1 with ident'1.

    This variant can be used for non mutually recursive functions only.

See also: Section 10.4

8.15  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.3) 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.

The 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
Recall: opaque constants will not be expanded by delta 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 reenginering of the code, this tactic has also been completely revised to get a very compact and readable version.
Previous Up Next