7.13 The hints databases for Auto and EAuto

The hints for Auto and EAuto have been reorganized since Coq 6.2.3. They are stored in several databases. Each databases maps head symbols to list of hints. One can use the command Print Hint ident to display the hints associated to the head symbol ident (see 7.13.2). Each hint has a name, a cost that is an nonnegative integer, and a pattern. The hint is tried by Auto if the conclusion of current goal matches its pattern, and after hints with a lower cost. The general command to add a hint to a database is:

Hint name : database := hint_definition

where hint_definition is one of the following expressions:

Resolve term
This command adds Apply term to the hint list with the head symbol of the type of term. The cost of that hint is the number of subgoals generated by Apply term. In case the inferred type of term does not start with a product the tactic added in the hint list is Exact term. In case this type can be reduced to a type starting with a product, the tactic Apply term is also stored in the hints list. If the inferred type of term does contain a dependent quantification on a predicate, it is added to the hint list of EApply instead of the hint list of Apply. In this case, a warning is printed since the hint is only used by the tactic EAuto (see 7.11.2). A typical example of hint that is used only by EAuto is a transitivity lemma.

Error messages:
1. Bound head variable
  The head symbol of the type of term is a bound variable such that this tactic cannot be associated to a constant.
2. term cannot be used as a hint
  The type of term contains products over variables which do not appear in the conclusion. A typical example is a transitivity axiom. In that case the Apply tactic fails, and thus is useless.
Immediate term
This command adds Apply term; Trivial to the hint list associated with the head symbol of the type of identin the given database. This tactic will fail if all the subgoals generated by Apply term are not solved immediately by the Trivial tactic which only tries tactics with cost 0. This command is useful for theorems such that the symmetry of equality or n+1=m+1 Ž n=m that we may like to introduce with a 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.

Error messages:
1. Bound head variable
2. term cannot be used as a hint
Constructors ident
If ident is an inductive type, this command adds all its constructors as hints of type Resolve. Then, when the conclusion of current goal has the form (ident ...), Auto will try to apply each constructor.

Error messages:
1. ident is not an inductive type
2. ident not declared
Unfold ident
This adds the tactic Unfold ident to the hint list that will only be used when the head constant of the goal is ident. Its cost is 4.
Extern num pattern tactic
This hint type is to extend Auto with tactics other than Apply and Unfold. For that, we must specify a cost, a pattern and a tactic to execute. Here is an example:
```
Hint discr : core := Extern 4 ~(?=?) Discriminate.
```
Now, when the head of the goal is a disequality, Auto will try Discriminate if it does not succeed 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 a number like ?1 or ?2. Here is an example:

Coq < Require EqDecide.

Coq < Require PolyList.

Coq < Hint eqdec1 : eqdec := Extern 5 {?1=?2}+{~ (?1=?2)}
Coq <                                 Generalize ?1 ?2; Decide Equality.

Coq <
Coq < Goal (a,b:(list nat*nat)){a=b}+{~a=b}.
1 subgoal

  ============================
   (a,b:(list nat*nat)){a=b}+{~a=b}

Coq < Info Auto with eqdec.
== Intro a; Intro b; Generalize a b; Decide Equality; Generalize a0 p;
       Decide Equality.
    Generalize y0 n0; Decide Equality.

    Generalize y n; Decide Equality.

Subtree proved!

Remark: There is currently (in the 6.3.1 release) no way to do pattern-matching on hypotheses.

Variants:

Hint ident : ident₁ ... ident_n:=hint_expression
This syntax allows to put the same hint in several databases.

Remark: The current implementation of Auto has no optimization about hint duplication: if the same hint is present in two databases given as arguments to Auto, it will be tried twice. We recommend to put the same hint in two different databases only if you never use those databases together.
Hint ident := hint_expression
If no database name is given, the hint is registered in the "core" database.

Remark: We do not recommend to put hints in this database in your developpements, except when the Hint command is inside a section. In this case the hint will be thrown when closing the section (see 7.13.3)

There are shortcuts that allow to define several goal at once:

Hints Resolve ident₁ ... ident_n : ident.
This command is a shortcut for the following ones:
Hint ident₁ : ident := Resolve ident₁
...
Hint ident₁ : ident:= Resolve ident₁
Notice that the hint name is the same that the theorem given as hint.
Hints Immediate ident₁ ... ident_n : ident.
Hints Unfold ident₁ ... ident_n : ident.

7.13.1 Hint databases defined in the Coq standard library

Several hint databases are defined in the Coq standard library. There is no systematic relation between the directories of the library and the databases.

core: This special database is automatically used by Auto. It contains only basic lemmas about negation, conjunction, and so on from. Most of the hints in this database come from the INIT and LOGIC directories.
arith: This databases contains all lemmas about Peano's arithmetic proven in the directories INIT and ARITH
zarith: contains lemmas about binary signed integers from the directories theories/ZARITH and tactics/contrib/Omega. It contains also a hint with a high cost that calls Omega.
bool: contains lemmas about booleans, mostly from directory theories/BOOL.
datatypes: is for lemmas about about lists, trees, streams and so on that are proven in LISTS, TREES subdirectories.
sets: contains lemmas about sets and relations from the directory SETS and RELATIONS.

There is also a special database called "v62". It contains all things that are currently hinted in the 6.2.x releases. It will not be extended later. It is not included in the hint databases list used in the "Auto with *" tactic.

The only purpose of the database "v62" is to ensure compatibility for old developpements with further versions of Coq. If you have a developpement that used to compile with 6.2.2 and that not compiles with 6.2.4, try to replace "Auto" with "Auto with v62" using the script documented below. This will ensure your developpement will compile will further releases of Coq.

To write a new developpement, or to update a developpement not finished yet, you are strongly advised NOT to use this database, but the pre-defined databases. Furthermore, you are advised not to put your own Hints in the "core" database, but use one or several databases specific to your developpement.

7.13.2 `Print Hint`

This command displays all hints that apply to the current goal. It fails if no proof is being edited, while the two variants can be used at every moment.

Variants:

Print Hint ident
This command displays only tactics associated with ident in the hints list. This is independent of the goal being edited, to this command will not fail if no goal is being edited.
Print Hint *
This command displays all declared hints.

7.13.3 Hints and sections

Like grammar rules and structures for the Ring tactic, things added by the Hint command will be erased when closing a section.

Conversely, when the user does Require A., all hints of the module A that are not defined inside a section are loaded.