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.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.
- Auto with *
Uses all existing hint databases, minus the special database
"v62". See section 7.13
- 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.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:
-
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:
-
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:
-
Not provable in Direct Predicate Calculus
- 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:
-
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.
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:
-
AutoRewrite [ident1... identn]
Step=[tactic1|...|tacticm]
Each time a rewriting rule is successful, it tries to solve with the tactics of
Step.
- AutoRewrite [rewriting_rule ... rewriting_rule]
Step=[tactic1|...|tacticm] with Solve
This is equivalent to the previous variant.
- 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.
- 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.
- 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.
- AutoRewrite [rewriting_rule ... rewriting_rule]
Rest=[tactic1|...|tacticm] with Solve
This is equivalent to the previous variant.
- 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.
- 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