7.13 The hints list for Auto and EAuto
The hints list is a data base of tactics for automated proof search It associates to a constant a list of tactics which may be tried when the head symbol of the goal to be solved is this constant.The tactics that can be stored are mainly Apply term (see section 7.3.4), EApply term (see section 3), Exact term (see section 7.2.1), or Unfold ident (see section 7.5.6).
Each tactic is stored with a numerical weight aiming to represent the "cost" of the application of this tactic in an automatic proof search. Tactics with a low cost are tried first.
7.13.1 Hint term
This command adds Apply term to the hint list associated 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, the hint is only used by the tactic EAuto (see 7.11.2).
Error messages:
-
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. - 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.
Variants:
-
Hint term1 ...termn
Is equivalent to Hint term1. ...Hint termn
7.13.2 Immediate term
This command adds Apply term; Trivial to the hint list associated with the head symbol of the type of ident. 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 in the hint list.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:
- Bound head variable
Variants:
-
Immediate term1 ...termn
Is equivalent to Immediate term1. ...Immediate termn
7.13.3 Hint Unfold ident
This command 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.Variants:
-
Hint Unfold ident1 ...identn
Is equivalent to Hint Unfold ident1. ...Hint Unfold identn
7.13.4 Print Hint
This command displays the currently available hints list. If an axiom or theorem has been declared twice, it will appear only once.Variants:
-
Print Hint ident
This command displays only tactics associated with ident in the hints list.