7.11 Automatizing

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

7.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 < Hints Resolve ex_intro.
Warning: the hint: EApply ex_intro will only used by EAuto

Coq < Goal (P:nat->Prop)(P O)->(EX n | (P n)).
1 subgoal
  
  ============================
   (P:(nat->Prop))(P O)->(EX n:nat | (P n))

Coq < EAuto.
Subtree proved!

Note that ex_intro should be declared as an hint.
See also: section 7.13

7.11.3 Prolog [ term1 ... termn ] num

This tactic, implemented by Chet Murthy, is based upon the concept of existential variables of Gilles Dowek, stating that resolution is a kind of unification. It tries to solve the current goal using the Assumption tactic, the Intro tactic, and applying hypotheses of the local context and terms of the given list [ term1 ... termn ]. It is more powerful than Auto since it may apply to any theorem, even those of the form (x:A)(P x) -> Q where x does not appear free in Q. The maximal search depth is num.


Error messages:
  1. Prolog failed
    The Prolog tactic was not able to prove the subgoal.

7.11.4 Tauto

This tactic, due to César Muñoz [73], implements a decision procedure for intuitionistic propositional calculus based on the contraction-free sequent calculi LJT* of R. Dyckhoff [41]. Note tha t Tauto succeeds on any instance of an intuitionistic tautological proposition. For instance it succeeds on (x:nat)(P:nat->Prop)x=O\/(P x)->~x=O->(P x) while Auto fails.

7.11.5 Intuition

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 Auto with * to them [73]. At the end, Intuition performs Intros.

For instance, the tactic Intuition applied to the goal 
((x:nat)(P x))/\B->((y:nat)(P y))/\(P O)\/B/\(P O)
internally replaces it by the equivalent one: 
((x:nat)(P x) -> B -> (P O))
and then uses Auto with * which completes the proof.

7.11.6 Linear

The tactic Linear, due to Jean-Christophe Filliâatre [42], implements a decision procedure for Direct Predicate Calculus, that is first-order Gentzen's Sequent Calculus without contraction rules [63, 10]. Intuitively, a first-order goal is provable in Direct Predicate Calculus if it can be proved using each hypothesis at most once.

Unlike the previous tactics, the Linear tactic does not belong to the initial state of the system, and it must be loaded explicitly with the command

Coq < Require Linear.

For instance, assuming that even and odd are two predicates on natural numbers, and a of type nat, the tactic Linear solves the following goal

Coq < Lemma example : (even a) 
Coq <               -> ((x:nat)((even x)->(odd (S x))))
Coq <               -> (EX y | (odd y)).

You can find examples of the use of Linear in theories/DEMOS/DemoLinear.v.


Variants:
  1. Linear with ident1 ... identn
    Is equivalent to apply first Generalize ident1 ...identn (see section 7.3.8) then the Linear tactic. So one can use axioms, lemmas or hypotheses of the local context with Linear in this way.

Error messages:
  1. Not provable in Direct Predicate Calculus
  2. Found n classical proof(s) but no intuitionistic one
    The decision procedure looks actually for classical proofs of the goals, and then checks that they are intuitionistic. In that case, classical proofs have been found, which do not correspond to intuitionistic ones.

7.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 Omega. See the additional documentation about Omega.

7.11.8 Ring term1 ... termn

This tactic, written by Samuel Boutin and Patrick Loiseleur, does AC rewriting on every ring. The tactic must be loaded by Require Ring under coqtop or coqtop -full. The ring must be declared in the Add Ring command (see 20). The ring of booleans is predefined; if one wants to use the tactic on nat one must do Require ArithRing; for Z, do Require ZArithRing.

term1, ..., termn must be subterms of the goal conclusion. Ring normalize 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. NatRing is a tactic macro for Repeat Rewrite S_to_plus_one; Ring. The theorem S_to_plus_one is a proof that (n:nat)(S n)=(plus (S O) n).

Example:
Coq < Require ZArithRing.

Coq < Goal (a,b,c:Z)`(a+b+c)*(a+b+c) 
Coq <                = a*a + b*b + c*c + 2*a*b + 2*a*c + 2*b*c`.
Coq < Intros; Ring.
Subtree proved!

You can have a look at the files Ring.v, ArithRing.v, ZarithRing.v to see examples of the Add Ring command.
See also: 20 for more detailed explanations about this tactic

7.11.9 AutoRewrite [rewriting_rule ... rewriting_rule]

This tactic carries out rewritings according the given rewriting rules.

A rewriting rule is, by definition, a list of terms which type is an equality, each term being followed by the keyword LR (for left-to-right) or RL (for right-to-left):

rewriting_rule ::= [term switch ... term switch ]
switch ::= LR
switch | RL

AutoRewrite tries each rewriting of each rule, until it succeeds; then the rewriting is processed and AutoRewrite tries again all rewritings from the first one. This tactic may not terminate and warnings are produced every 100 rewritings.


Variants:
  1. AutoRewrite [ident1... identn] Step=[tactic1|...|tacticm]
    Each time a rewriting rule is successful, it tries to solve with the tactics of Step.

  2. AutoRewrite [rewriting_rule ... rewriting_rule] Step=[tactic1|...|tacticm] with Solve
    This is equivalent to the previous variant.

  3. AutoRewrite [rewriting_rule ... rewriting_rule] Step=[tactic1|...|tacticm] with Use
    Each time a rewriting rule is successful, it tries to apply a tactic of Step.

  4. AutoRewrite [rewriting_rule ... rewriting_rule] Step=[tactic1|...|tacticm] with All
    Each time a rewriting rule is successful, it tries to solve with the tactics of Step, if it fails, it tries to apply a tactic of Step. In fact, it behaves like the Solve switch first and the Use switch next in case of failure.

  5. AutoRewrite [rewriting_rule ... rewriting_rule] Rest=[tactic1|...|tacticm]
    If subgoals are generated by a conditional rewriting, it tries to solve each of them with the tactics in Rest.

  6. AutoRewrite [rewriting_rule ... rewriting_rule] Rest=[tactic1|...|tacticm] with Solve
    This is equivalent to the previous variant.

  7. AutoRewrite [rewriting_rule ... rewriting_rule] Rest=[tactic1|...|tacticm] with Cond
    Each time subgoals are generated by a successful conditional rewriting, it tries to solve all of them, if it fails, it considers that the rewriting rule fails and takes the next one in the bases.

  8. AutoRewrite [rewriting_rule ... rewriting_rule] Depth=num
    Produces a warning giving the number of rewritings carried out every num rewritings.
The three options Step, Solve et Depth can be combined.

7.11.10 HintRewrite ident rewriting_rule

This vernacular command makes an alias for a rewriting rule. Then, instead of AutoRewrite [rewriting_rule ...] you can type: AutoRewrite [ident ...]

This vernacular command is synchronous with the section mechanism (see 2.5): when closing a section, all aliases created by HintRewrite in that section are lost. Conversely, when loading a module, all HintRewrite declarations at the global level of that module are loaded.
See also: 8.5 for examples showing the use of this tactic.
See also: file theories/DEMOS/DemoAutoRewrite.v