\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Programmable proof search¶

Tactic auto nat_or_var? auto_using? hintbases?¶

auto_using::=using one_term+,hintbases::=with *|with ident+

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 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. If one_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 of apply and auto using one_term may fail where apply 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 database core. Use the fake database nocore to omit core.

If no with clause is given, auto only uses the hypotheses of the current goal and the hints of the database named core.

auto generally either completely solves the goal or leaves it unchanged. Use solve [ auto ] if you want a failure when they don't solve the goal. auto will fail if fail or gfail are invoked directly or indirectly, in which case setting the Ltac Debug may help you debug the failure.

Warning

auto uses a weaker version of apply that is closer to simple apply so it is expected that sometimes auto will fail even if applying manually one of the hints would succeed.

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 no idents are given, the hint is added to the core database.)

Outside of sections, these commands support the local, export and global attributes. global is the default. Inside sections, only the local attribute is supported because hints are local to sections.

local hints are never visible from other modules, even if they Import or Require the current module.

export hints are visible from other modules when they Import the current module, but not when they only Require it. This attribute is supported by all Hint commands except for Hint Rewrite.

global hints are visible from other modules when they Import or Require 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+?¶

hint_info::=| natural? one_pattern?one_pattern::=one_term
The first form adds each qualid as a hint with the head symbol of the type of qualid to the specified hint databases (idents). The cost of the hint is the number of subgoals generated by simple apply qualid or, if specified, natural. The associated pattern is inferred from the conclusion of the type of qualid or, if specified, the given one_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 by eauto / typeclasses eauto, but not by auto. A typical hint that would only be used by eauto 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 or apply <- qualid, although as mentioned before, the tactic actually used is a restricted version of apply).

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¶

Error qualid cannot be used as a hint¶

The head symbol of the type of qualid is a bound variable such that this tactic cannot be associated with a constant.

Command Hint Immediate qualidone_term+ : ident+?¶

Adds simple apply qualid; trivial to the hint list for each qualid associated with the head symbol of the type of ident. This tactic will fail if all the subgoals generated by simple apply qualid are not solved immediately by the trivial tactic (which only tries tactics with cost 0). This command is useful for theorems such as the symmetry of equality or n+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 by trivial itself.

Command Hint Constructors qualid+ : ident+?¶

For each qualid that is an inductive type, adds all its constructors as hints of type Resolve. Then, when the conclusion of current goal has the form (qualid ...), auto will try to apply each constructor.

Error qualid is not an inductive type¶

Command Hint Unfold qualid+ : ident+?¶

For each qualid, adds the tactic unfold qualid to the hint list that will only be used when the head constant of the goal is qualid. 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 than apply and unfold. natural is the cost, one_term is the pattern to match and ltac_expr is the action to apply.

Note

Use a Hint Extern with no pattern to do pattern matching on hypotheses using match 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+?¶

hints_regexp::=qualid+(hint or instance identifier)|_(any hint)|hints_regexp | hints_regexp(disjunction)|hints_regexp hints_regexp(sequence)|hints_regexp *(Kleene star)|emp(empty)|eps(epsilon)|( hints_regexp )
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 Externs do not have an associated identifier). For each hint qualid in the hint database, the current path p extended with qualid is matched against the current cut expression c associated with the hint database. If the match succeeds the hint is not applied.

Hint Cut hints_regexp sets the cut expression to c | hints_regexp. The initial cut expression is emp.

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 of qualid to arguments arg ... arg, the mode tells if the hints associated with qualid 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, or Hint Mode, for typeclass resolution, do not forget to put them in the typeclass_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 bases ident*. Note that the rewriting bases are distinct from the auto hint bases and that auto does not take them into account.

Command Print Rewrite HintDb ident¶: This command displays all rewrite hints contained in ident.

Command Remove Hints qualid+ : ident+?¶: Removes the hints associated with the qualid+ in databases ident+. Note: hints created with Hint 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?¶

*: Display all declared hints.
reference: Display all hints associated with the head symbol 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 * and reference 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.

Command Print HintDb ident¶: This command displays all hints from database ident.

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-database nocore is given to auto. 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 in nat or Z.
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 the FSets and FMaps 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.

Setting implicit automation tactics¶

Command Proof with ltac_expr using section_var_expr?¶: Starts a proof in which ltac_expr is applied to the active goals after each tactic that ends with ... instead of the usual single period. "tactic..." is equivalent to "tactic; ltac_expr.".

See also

Proof in Entering and exiting proof mode.