7.11 Automatizing

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. The maximal search depth is 5 by default.


Variants:
  1. Auto num
    Forces the search depth to be num.
  2. Trivial This tactic is a restriction of Auto for doing hypotheses and hints of cost 0. Typically it solves goals such as trivial equalities X=X.

Remark: Auto either solves the goal or else acts as Idtac and does not change the goal.


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 < Hint ex_intro.
Warning: Tactic EApply ex_intro in hints list is 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 ETrivial

That is the existential version of Trivial. It acts like EAuto but tries only goals of cost 0.

7.11.4 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.5 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 that 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.6 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 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 which completes the proof.

7.11.7 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.6) 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.8 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.9 Ring term1 ...termn

This tactic, written by Patrick Loiseleur and Samuel Boutin, 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 19). They are 3 pre-defined rings: naturals, booleans and integers. To use the tactic on one of these rings, the user must type the command Require NatRing or Require BoolRing or Require ZRing instead of Require Ring.

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



Example:
Coq < Require ZRing.

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 scripts NatRing.v, ZRing.v and Bool_Ring.v to see examples of the Add Ring command.


See also: 19

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.2.10.html at 8/10/98