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:
-
Auto num
Forces the search depth to be num. The maximal search depth is 5 by default.
- Auto with ident1 ... identn
Uses the hint databases ident1 ... identn in addition to
the database "core". See section 7.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.
- Auto with *
Uses all existing hint databases, minus the special database
"v62". See section 7.12
- 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.
- Trivial with ident1 ... identn
- Trivial with *
Remark: Auto either solves completely the goal or else leave it
intact. Auto and Trivial never fail.
See also: section 7.12
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 be 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.12
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:
-
Prolog failed
The Prolog tactic was not able to prove the subgoal.
7.11.4 Tauto
This tactic implements a decision procedure for intuitionistic propositional
calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
[Dyc92]. Note that Tauto succeeds on any instance of an
intuitionistic tautological proposition. Tauto unfolds negations
and logical equivalence but does not unfold any other definition.
The following goal can be proved by Tauto whereas Auto
would fail:
Coq < Goal (x:nat)(P:nat->Prop)x=O\/(P x)->~x=O->(P x).
1 subgoal
============================
(x:nat; P:(nat->Prop))x=O\/(P x)->~x=O->(P x)
Coq < Intros.
1 subgoal
x : nat
P0 : nat->Prop
H : x=O\/(P0 x)
H0 : ~x=O
============================
(P0 x)
Coq < Tauto. (* Auto would fail *)
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 < Goal (A:Prop)(P:nat->Prop)(A \/ (x:nat) ~A -> (P x)) -> (x:nat) A -> (P x).
Subtree proved!
Coq < Tauto.
Error: repeated Goal not permitted in refining mode
7.11.5 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 [Mun94]. If this tactic fails on some goals then
Intuition fails. In fact, Tauto is simply Intuition
Failtac.
For instance, the tactic Intuition Auto 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.
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 10). 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:
-
Intuition
Is equivalent to Intuition Auto with *.
See also: file contrib/Rocq/DEMOS/Demo_tauto.v
7.11.6 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
(chapter 15).
7.11.7 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 18). 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:
-
Ring When the goal is an equality t1=t2, it
acts like Ring t1 t2 and then simplifies or solves
the equality.
- 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.
Unnamed_thm < Error: repeated Goal not permitted in refining mode
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 18 for more detailed explanations about this tactic.
7.11.8 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 Field. Field theories are declared (as for Ring) with
the Add Field command.
Example:
Coq < Require Reals.
Coq < Goal (x,y:R)``x*y>0`` -> ``x*((1/x)+x/(x+y)) == -(1/y)*y*(-(x*x/(x+y))-1)``.
Coq < Intros; Field.
1 subgoal
============================
(x,y:R)``x*y > 0``->``x*(1/x+x/(x+y)) == -1/y*y*( -(x*x/(x+y))-1)``
7.11.9 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 (n:A)~(n==Azero)->(Amult (Ainv n) n)==Aone.
To build a ring theory, refer to chapter 18 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 18). However, the
module Ring is not loaded by Add Field and you have to make a Require Ring if you want to call the Ring tactic.
Variants:
-
Add Field A Aplus Amult Aone Azero
Aopp Aeq Ainv Rth Tinvl
Add Field with minus:=Aminus
Adds also the term Aminus which must be a constant expressed by means of
Aopp.
- Add Field A Aplus Amult Aone Azero
Aopp Aeq Ainv Rth Tinvl
Add Field 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,
See also: theory theories/Reals for many examples of use of Field.
See also: [DelMay01] for more details regarding the implementation of Field.
7.11.10 Fourier
This tactic written by Loïc Pottier solves linear inequations on real numbers
using Fourier's method ([Fourier]). This tactic must be loaded by
Require Fourier.
Example:
Coq < Require Reals.
Coq < Require Fourier.
Coq < Goal (x,y:R)``x < y``->``y+1 >= x-1``.
Coq < Intros; Fourier.
1 subgoal
============================
(x,y:R)``x < y``->``y+1 >= x-1``
7.11.11 AutoRewrite [ 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:
-
AutoRewrite [ 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.
7.11.12 HintRewrite [ term1 ...termn ] in 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).
This command is synchronous with the section mechanism (see 2.4):
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.
Variants:
-
HintRewrite -> [ term1 ...termn ] in ident
This is strictly equivalent to the command above (we only precise the
orientation which is the default one).
- HintRewrite <- [ term1 ...termn ] in ident
Adds the rewriting rules term1 ...termn with a right-to-left
orientation in the base ident.
- HintRewrite [ term1 ...termn ] in ident using tactic
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: 8.5 for examples showing the use of this tactic.
See also: file contrib/Rocq/DEMOS/Demo_AutoRewrite.v