\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \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}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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¶

Tactics¶

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. This process is recursively applied to the generated subgoals.

Within each hintbase, lower cost tactics are tried before higher-cost tactics. When multiple hintbases are specified, all hints in the first database are tried before any in the second database (and so forth) regardless of their cost (unlike eauto and typeclasses eauto).

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.

Hint databases¶

Hints used by auto, eauto and other tactics are stored in hint databases. Each database maps head symbols to a list of hints. Use the Print Hint command to view a database.

Each hint has a cost and an optional pattern. Hints with lower cost are tried first. (Cost is not used to limit the scope of searches.) 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 a filter to select the lemmas that will be applied. When discriminated, the DT uses transparency information to decide if a constant should considered rigid for filtering, making the retrieval more efficient. By contrast, undiscriminated databases treat all constants as transparent, resulting in a larger number of selected lemmas to be applied, and thus putting more pressure on unification.

By default, hint databases are undiscriminated.

Hint databases defined in the Rocq standard library¶

Several hint databases are defined in the Rocq standard library. The database contains all hints declared to belong to it in the currently loaded modules. In particular, requiring new modules may extend the database. At Rocq startup, only the core database is nonempty and ready to be used immediately.

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: all lemmas about Peano’s arithmetic proved in the directories Init and Arith.
zarith: 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: lemmas about booleans, mostly from directory theories/Bool.
datatypes: lemmas about lists, streams and so on that are mainly proved in the Lists subdirectory.
sets: lemmas about sets and relations from the directories Sets and Relations.
typeclass_instances: special database containing all 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 more databases specific to your development.

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

Hints in hint databases are ordered, which is the order in which they're tried, as shown by the Print HintDb command. Hints with lower costs are tried first. Hints with the same cost are tried in reverse of their order of definition, i.e., last to first.

Outside of sections, these commands support the local, export and global attributes. export is the default.

Inside sections, some commands only support the local attribute. These are Hint Immediate, Hint Resolve, Hint Constructors, Hint Unfold, Hint Extern and Hint Rewrite. local is the default for all hint commands inside 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.

global hints are visible from other modules when they Import or Require the current module.

Changed in version 8.18: The default value for hint locality outside sections is now export. It used to be global.

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. This is deprecated.

Warning Declaring arbitrary terms as hints is fragile and deprecated; 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+?¶

For each specified qualid, adds the tactic simple apply qualid; solve [ trivial ] to the hint list associated with the head symbol of the type of qualid. 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.

Error Cannot coerce qualid to an evaluable reference.¶

Command Hint ConstantsProjectionsVariables TransparentOpaque : ident+?¶

Sets the transparency flag for constants, projections 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_pattern is the pattern to match and ltac_expr is the action to apply.

Usage tip: tactics that can succeed even if they don't change the context, such as most of the conversion tactics, should be prefaced with progress to avoid needless repetition of the tactic.

Usage tip: Use a Hint Extern with no pattern to do pattern matching on hypotheses using match goal with inside the tactic.

Example

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

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 goal ============================ 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

The regexp matches the entire path. Most hints will start with a leading ( _* ) to match the tail of the path. (Note that (_*) misparses since *) would end a comment.)

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 resolution 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, depending on a criterion on the arguments. 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. Mode - matches any term, mode + matches a term if and only if it does not contain existential variables, while mode ! matches a term if and only if the head of the term is not an existential variable. The head of a term is understood here as the applicative head, recursively, ignoring casts. For a mode declaration to match a list of arguments, each argument should match its corresponding mode.

Hint Mode is especially useful for typeclasses, when one does not want to support default instances and wants to 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.

Warning This hint is not local but depends on a section variable. It will disappear when the section is closed.¶

A hint with a non-local attribute was added inside a section, but it refers to a local variable that will go out of scope when closing the section. As a result the hint will not survive either.

Example: Logic programming with addition on natural numbers

This example illustrates the use of modes to control how resolutions can be triggered during proof search.

Parameter plus : nat -> nat -> nat -> Prop.
plus is declared

Hint Mode plus ! - - : plus.
Hint Mode plus - ! - : plus.

Axiom plus0l : forall m : nat, plus 0 m m.
plus0l is declared

Axiom plus0r : forall n : nat, plus n 0 n.
plus0r is declared

Axiom plusSl : forall n m r : nat, plus n m r -> plus (S n) m (S r).
plusSl is declared

Axiom plusSr : forall n m r : nat, plus n m r -> plus m (S m) (S r).
plusSr is declared

Hint Resolve plus0l plus0r plusSl plusSr : plus.
The hint plusSr will only be used by eauto, because applying plusSr would leave variable n as unresolved existential variable.

The previous commands define the addition predicate and set its mode so it can resolve goals if and only if one of the first two arguments is headed by a constructor or constant. The last argument of the predicate will be the inferred result.

Goal exists x y, plus x y 12.
1 goal ============================ exists x y : nat, plus x y 12

Proof. eexists ?[x], ?[y].
1 focused goal (shelved: 2) ============================ plus ?x ?y 12

   Fail typeclasses eauto with plus.
The command has indeed failed with message: Tactic failure: Proof search failed.

   instantiate (y := 1).
1 focused goal (shelved: 1) ============================ plus ?x 1 12

   typeclasses eauto with plus.
No more goals.

Defined.

In the proof script, the first call to typeclasses eauto fails as the two arguments are headed by an existential variable, while when we instantiate the second argument with 1, typeclass resolution succeeds as the second declared mode is matched, and instantiates x with 11.

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. Hints in each group ("For ... ->") are shown in the order in which they will be tried (first to last). The groups are shown ordered alphabetically on the last component of the symbol name. Note that hints with the same cost are tried in reverse of the order they're defined in, i.e., last to first.

Hint locality¶

As explained at the beginning of Creating Hints, hints outside sections have three possible localities: local, export, and global, with export now being the default. The default used to be global, so old code bases may still use it. The following option may be useful to help transition hints from the global to the export locality, as it can provide an over-approximation of where these hints are used:

Option Loose Hint Behavior "Lax""Warn""Strict"¶

This option accepts three values:

"Lax": no scope errors or warnings are generated for hints. This is the default.
"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": fails when a non-imported hint is used, with the same caveats as "Warn".

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.