Programmable proof search¶
-
Tactic
auto nat_or_var? auto_using? hintbases?
¶ 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 usingintros
and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated with the head symbol of the goal and tries to apply one of them. Lower cost tactics are tried before higher-cost tactics. This process is recursively applied to the generated subgoals.nat_or_var
Specifies the maximum search depth. The default is 5.
using one_term+,
Uses lemmas
one_term+,
in addition to hints. Ifone_term
is an inductive type, the collection of its constructors are added as hints.Note that hints passed through the
using
clause are used in the same way as if they were passed through a hint database. Consequently, they use a weaker version ofapply
andauto using one_term
may fail whereapply one_term
succeeds.with *
Use all existing hint databases. Using this variant is highly discouraged in finished scripts since it is both slower and less robust than explicitly selecting the required databases.
with ident+
Use the hint databases
ident+
in addition to the databasecore
. Use the fake databasenocore
to omitcore
.
If no
with
clause is given,auto
only uses the hypotheses of the current goal and the hints of the database namedcore
.auto
generally either completely solves the goal or leaves it unchanged. Usesolve
[ auto ]
if you want a failure when they don't solve the goal.auto
will fail iffail
orgfail
are invoked directly or indirectly, in which case setting theLtac Debug
may help you debug the failure.Warning
auto
uses a weaker version ofapply
that is closer tosimple apply
so it is expected that sometimesauto
will fail even if applying manually one of the hints would succeed.See also
The hints databases for auto and eauto for the list of pre-defined databases and the way to create or extend a database.
-
Tactic
info_auto nat_or_var? auto_using? hintbases?
¶ Behaves like
auto
but shows the tactics it uses to solve the goal. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used.
-
Tactic
debug auto nat_or_var? auto_using? hintbases?
¶ Behaves like
auto
but shows the tactics it tries to solve the goal, including failing paths.
-
Tactic
trivial auto_using? hintbases?
¶ -
Tactic
debug trivial auto_using? hintbases?
¶ -
Tactic
info_trivial auto_using? hintbases?
¶ Like
auto
, but is not recursive and only tries hints with zero cost. Typically used to solve goals for which a lemma is already available in the specifiedhintbases
.
-
Flag
Info Auto
¶ -
Flag
Debug Auto
¶ -
Flag
Info Trivial
¶ -
Flag
Debug Trivial
¶ These flags enable printing of informative or debug information for the
auto
andtrivial
tactics.
-
Tactic
eauto nat_or_var? auto_using? hintbases?
¶ Generalizes
auto
. Whileauto
does not try resolution hints which would leave existential variables in the goal,eauto
does try them (informally speaking, it internally uses a tactic close tosimple eapply
instead of a tactic close tosimple apply
in the case ofauto
). As a consequence,eauto
can solve such a goal:Example
- Set Warnings "-deprecated-hint-without-locality".
- Hint Resolve ex_intro : core.
- The hint ex_intro will only be used by eauto, because applying ex_intro would leave variable x as unresolved existential variable.
- Goal forall P:nat -> Prop, P 0 -> exists n, P n.
- 1 subgoal ============================ forall P : nat -> Prop, P 0 -> exists n : nat, P n
- eauto.
- No more subgoals.
ex_intro
is declared as a hint so the proof succeeds.-
Tactic
info_eauto nat_or_var? auto_using? hintbases?
¶ The various options for
info_eauto
are the same as forinfo_auto
.
eauto
also obeys the following flags:-
Tactic
debug eauto nat_or_var? auto_using? hintbases?
¶ Behaves like
eauto
but shows the tactics it tries to solve the goal, including failing paths.
-
Tactic
bfs eauto nat_or_var? auto_using? hintbases?
¶ Like
eauto
, but uses a breadth-first search.
-
Tactic
autounfold hintbases? occurrences?
¶ Unfolds constants that were declared through a
Hint Unfold
in the given databases.occurrences
Performs the unfolding in the specified occurrences. The
at occs_nums
clause ofoccurrences
is not supported.
-
Tactic
autorewrite *? with ident+ occurrences? using ltac_expr?
¶ *
If present, rewrite all occurrences whose side conditions are solved.
with ident+
Specifies the rewriting rule bases to use.
occurrences
Performs rewriting in the specified occurrences. Note: the
at
clause is currently not supported.-
Error
The "at" syntax isn't available yet for the autorewrite tactic.
¶ Appears when there is an
at
clause on the conclusion.
-
Error
using ltac_expr
ltac_expr
is applied to the main subgoal after each rewriting step.
Applies rewritings according to the rewriting rule bases
ident+
.For each rule base, applies each rewriting to the main subgoal until it fails. Once all the rules have been processed, if the main subgoal has changed then the rules of this base are processed again. If the main subgoal has not changed then the next base is processed. For the bases, the behavior is very similar to the processing of the rewriting rules.
The rewriting rule bases are built with the
Hint Rewrite
command.
Warning
This tactic may loop if you build non terminating rewriting systems.
See also
Hint Rewrite
for feeding the database of lemmas used by
autorewrite
and autorewrite
for examples showing the use of this tactic.
Also see Strategies for rewriting.
-
Tactic
easy
¶ This tactic tries to solve the current goal by a number of standard closing steps. In particular, it tries to close the current goal using the closing tactics
trivial
,reflexivity
,symmetry
,contradiction
andinversion
of hypothesis. If this fails, it tries introducing variables and splitting and-hypotheses, using the closing tactics afterwards, and splitting the goal usingsplit
and recursing.This tactic solves goals that belong to many common classes; in particular, many cases of unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic.
The hints databases for auto and eauto¶
The hints for auto
and eauto
are stored in databases. Each database
maps head symbols to a list of hints. Use the Print Hint
command to view
the database.
Each hint has a cost that is a nonnegative
integer and an optional pattern. Hints with lower costs are tried first.
auto
tries a hint when the conclusion of the current goal matches its
pattern or when the hint has no pattern.
Creating Hint databases¶
Hint databases can be created with the Create HintDb
command or implicitly
by adding a hint to an unknown database. We recommend you always use Create HintDb
and then imediately use Hint Constants
and Hint Variables
to make
those settings explicit.
Note that the default transparency
settings differ between these two methods of creation. Databases created with
Create HintDb
have the default setting Transparent
for both Variables
and Constants
, while implicitly created databases have the Opaque
setting.
-
Command
Create HintDb ident discriminated?
¶ Creates a new hint database named
ident
. The database is implemented by a Discrimination Tree (DT) that serves as an index of all the lemmas. The DT can use transparency information to decide if a constant should be indexed or not making the retrieval more efficient. The legacy implementation (the default one for new databases) uses the DT only on goals without existentials (i.e.,auto
goals), for non-Immediate hints and does not make use of transparency hints, putting more work on the unification that is run after retrieval (it keeps a list of the lemmas in case the DT is not used). The new implementation enabled by the discriminated option makes use of DTs in all cases and takes transparency information into account. However, the order in which hints are retrieved from the DT may differ from the order in which they were inserted, making this implementation observationally different from the legacy one.
Creating Hints¶
The various
Hint
commands share these elements:
: ident+?
specifies the hint database(s) to add to. (Deprecated since version 8.10: If noident
s are given, the hint is added to thecore
database.)Outside of sections, these commands support the
local
,export
andglobal
attributes.global
is the default. Inside sections, only thelocal
attribute is supported because hints are local to sections.
local
hints are never visible from other modules, even if theyImport
orRequire
the current module.
export
hints are visible from other modules when theyImport
the current module, but not when they onlyRequire
it. This attribute is supported by allHint
commands except forHint Rewrite
.
global
hints are visible from other modules when theyImport
orRequire
the current module.Deprecated since version 8.13: The default value for hint locality will change in a future release. Hints added outside of sections without an explicit locality are now deprecated. We recommend using
export
where possible.The
Hint
commands are:
- Command
Hint Resolve qualidone_term+ hint_info? : ident+?
¶- Command
Hint Resolve -><- qualid+ natural? : ident+?
¶The first form adds each
qualid
as a hint with the head symbol of the type ofqualid
to the specified hint databases (ident
s). The cost of the hint is the number of subgoals generated bysimple apply
qualid
or, if specified,natural
. The associated pattern is inferred from the conclusion of the type ofqualid
or, if specified, the givenone_pattern
.If the inferred type of
qualid
does not start with a product,exact
qualid
is added to the hint list. If the type can be reduced to a type starting with a product,simple apply
qualid
is also added to the hints list.If the inferred type of
qualid
contains a dependent quantification on a variable which occurs only in the premises of the type and not in its conclusion, no instance could be inferred for the variable by unification with the goal. In this case, the hint is only used byeauto
/typeclasses eauto
, but not byauto
. A typical hint that would only be used byeauto
is a transitivity lemma.
-><-
The second form adds the left-to-right (
->
) or right-ot-left implication (<-
) of an equivalence as a hint (informally the hint will be used as, respectively,apply
-> qualid
orapply
<- qualid
, although as mentioned before, the tactic actually used is a restricted version ofapply
).one_term
Permits declaring a hint without declaring a new constant first, but this is not recommended.
- Warning
Declaring arbitrary terms as hints is fragile; it is recommended to declare a toplevel constant instead
¶
- Command
Hint Immediate qualidone_term+ : ident+?
¶Adds
simple apply
qualid;
trivial
to the hint list for eachqualid
associated with the head symbol of the type ofident
. This tactic will fail if all the subgoals generated bysimple apply
qualid
are not solved immediately by thetrivial
tactic (which only tries tactics with cost 0). This command is useful for theorems such as the symmetry of equality orn+1=m+1 -> n=m
that we may want to introduce with limited use in order to avoid useless proof search. The cost of this tactic (which never generates subgoals) is always 1, so that it is not used bytrivial
itself.
- Command
Hint Constructors qualid+ : ident+?
¶For each
qualid
that is an inductive type, adds all its constructors as hints of typeResolve
. Then, when the conclusion of current goal has the form(qualid ...)
,auto
will try to apply each constructor.
- Command
Hint Unfold qualid+ : ident+?
¶For each
qualid
, adds the tacticunfold
qualid
to the hint list that will only be used when the head constant of the goal isqualid
. Its cost is 4.
- Command
Hint TransparentOpaque qualid+ : ident+?
¶Adds transparency hints to the database, making each
qualid
a transparent or opaque constant during resolution. This information is used during unification of the goal with any lemma in the database and inside the discrimination network to relax or constrain it in the case of discriminated databases.
- Command
Hint ConstantsVariables TransparentOpaque : ident+?
¶Sets the transparency flag for constants or variables for the specified hint databases. These flags affect the unification of hints in the database. We advise using this just after a
Create HintDb
command.
- Command
Hint Extern natural one_pattern? => ltac_expr : ident+?
¶Extends
auto
with tactics other thanapply
andunfold
.natural
is the cost,one_term
is the pattern to match andltac_expr
is the action to apply.Note
Use a
Hint Extern
with no pattern to do pattern matching on hypotheses usingmatch goal with
inside the tactic.Example
- Set Warnings "-deprecated-hint-without-locality".
- Hint Extern 4 (~(_ = _)) => discriminate : core.
Now, when the head of the goal is a disequality,
auto
will try discriminate if it does not manage to solve the goal with hints with a cost less than 4.One can even use some sub-patterns of the pattern in the tactic script. A sub-pattern is a question mark followed by an identifier, like
?X1
or?X2
. Here is an example:Example
- Set Warnings "-deprecated-hint-without-locality".
- Require Import List.
- Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec.
- Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
- 1 subgoal ============================ forall a b : list (nat * nat), {a = b} + {a <> b}
- info_auto.
- (* info auto: *) idtac.
- Command
Hint Cut [ hints_regexp ] : ident+?
¶ |_(any hint)|emp(empty)|eps(epsilon)Used to cut the proof search tree according to a regular expression that matches the paths to be cut.
During proof search, the path of successive successful hints on a search branch is recorded as a list of identifiers for the hints (note that
Hint Extern
s do not have an associated identifier). For each hintqualid
in the hint database, the current pathp
extended withqualid
is matched against the current cut expressionc
associated with the hint database. If the match succeeds the hint is not applied.
Hint Cut hints_regexp
sets the cut expression toc | hints_regexp
. The initial cut expression isemp
.The output of
Print HintDb
shows the cut expression.Warning
There is no operator precedence during parsing, one can check with
Print HintDb
to verify the current cut expression.Warning
These hints currently only apply to typeclass proof search and the
typeclasses eauto
tactic.
- Command
Hint Mode qualid +!-+ : ident+?
¶Sets an optional mode of use for the identifier
qualid
. When proof search has a goal that ends in an application ofqualid
to argumentsarg ... arg
, the mode tells if the hints associated withqualid
can be applied or not. A mode specification is a list of+
,!
or-
items that specify if an argument of the identifier is to be treated as an input (+
), if its head only is an input (!
) or an output (-
) of the identifier. For a mode to match a list of arguments, input terms and input heads must not contain existential variables or be existential variables respectively, while outputs can be any term.The head of a term is understood here as the applicative head, or the match or projection scrutinee’s head, recursively, casts being ignored.
Hint Mode
is especially useful for typeclasses, when one does not want to support default instances and avoid ambiguity in general. Setting a parameter of a class as an input forces proof search to be driven by that index of the class, with!
allowing existentials to appear in the index but not at its head.Note
Multiple modes can be declared for a single identifier. In that case only one mode needs to match the arguments for the hints to be applied.
If you want to add hints such as
Hint Transparent
,Hint Cut
, orHint Mode
, for typeclass resolution, do not forget to put them in thetypeclass_instances
hint database.
-
Command
Hint Rewrite -><-? one_term+ using ltac_expr? : ident*?
¶ using ltac_expr?
If specified,
ltac_expr
is applied to the generated subgoals, except for the main subgoal.-><-
Arrows specify the orientation; left to right (
->
) or right to left (<-
). If no arrow is given, the default orientation is left to right (->
).
Adds the terms
one_term+
(their types must be equalities) to the rewriting basesident*
. Note that the rewriting bases are distinct from theauto
hint bases and thatauto
does not take them into account.
-
Command
Remove Hints qualid+ : ident+?
¶ Removes the hints associated with the
qualid+
in databasesident+
. Note: hints created withHint Extern
currently can't be removed. The best workaround for this is to make the hints non global and carefully select which modules you import.
-
Command
Print Hint *reference?
¶ -
Displays tactics from the hints list. The default is to show hints that apply to the conclusion of the current goal. The other forms with
*
andreference
can be used even if no proof is open.Each hint has a cost that is a nonnegative integer and an optional pattern. The hints with lower cost are tried first.
Hint databases defined in the Coq standard library¶
Several hint databases are defined in the Coq standard library. The actual content of a database is the collection of hints declared to belong to this database in each of the various modules currently loaded. Especially, requiring new modules may extend the database. At Coq startup, only the core database is nonempty and can be used.
- core
This special database is automatically used by
auto
, except when pseudo-databasenocore
is given toauto
. The core database contains only basic lemmas about negation, conjunction, and so on. Most of the hints in this database come from the Init and Logic directories.- arith
This database contains all lemmas about Peano’s arithmetic proved in the directories Init and Arith.
- zarith
contains lemmas about binary signed integers from the directories theories/ZArith. The database also contains high-cost hints that call
lia
on equations and inequalities innat
orZ
.- bool
contains lemmas about booleans, mostly from directory theories/Bool.
- datatypes
is for lemmas about lists, streams and so on that are mainly proved in the Lists subdirectory.
- sets
contains lemmas about sets and relations from the directories Sets and Relations.
- typeclass_instances
contains all the typeclass instances declared in the environment, including those used for
setoid_rewrite
, from the Classes directory.- fset
internal database for the implementation of the
FSets
library.- ordered_type
lemmas about ordered types (as defined in the legacy
OrderedType
module), mainly used in theFSets
andFMaps
libraries.
You are advised not to put your own hints in the core database, but use one or several databases specific to your development.
Hint locality¶
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 required (using e.g. Require A.
).
As of today, hints only have a binary behavior regarding locality, as
described above: either they disappear at the end of a section scope,
or they remain global forever. This causes a scalability issue,
because hints coming from an unrelated part of the code may badly
influence another development. It can be mitigated to some extent
thanks to the Remove Hints
command,
but this is a mere workaround and has some limitations (for instance, external
hints cannot be removed).
A proper way to fix this issue is to bind the hints to their module scope, as
for most of the other objects Coq uses. Hints should only be made available when
the module they are defined in is imported, not just required. It is very
difficult to change the historical behavior, as it would break a lot of scripts.
We propose a smooth transitional path by providing the Loose Hint Behavior
option which accepts three flags allowing for a fine-grained handling of
non-imported hints.
-
Option
Loose Hint Behavior "Lax""Warn""Strict"
¶ This option accepts three values, which control the behavior of hints w.r.t.
Import
:"Lax": this is the default, and corresponds to the historical behavior, that is, hints defined outside of a section have a global scope.
"Warn": outputs a warning when a non-imported hint is used. Note that this is an over-approximation, because a hint may be triggered by a run that will eventually fail and backtrack, resulting in the hint not being actually useful for the proof.
"Strict": changes the behavior of an unloaded hint to a immediate fail tactic, allowing to emulate an import-scoped hint mechanism.