Computing advice to the theorem proving process

General Form of :hints: (hint1 hint2 ... hintk)

Each element, hinti, must be either a common hint or a computed hint.

A common hint is of the form

(goal-spec :key1 val1 ... :keyn valn)

where

A computed hint may be a symbol, in which case it must be a function symbol of three, four or seven arguments. Otherwise, a computed hint is a term with the following properties:

(a) the only free variables allowed in the term are `state`;

(b) the output signature of the term is either

(c) in the former case of (b) above, the term is single-threaded in `state`.

If a computed hint is a function symbol

Note: Error triples are an ACL2 idiom for implementing ``errors''; see
error-triple. If a computation returns `state` and further
computation is aborted. On the other hand, if a computation returns an error
triple in which `state`), and computation continues. For more information
about programming with error triples, see programming-with-state.

The function symbol cases are treated as abbreviations of the term

The semantics of a computed hint term is as follows. On every subgoal, the
term is evaluated in an environment in which the variables mentioned in (a)
above are bound to context-sensitive values explained below. Either the
computed hint signals an error, in which the proof attempt aborts, or else it
returns a value, `state`. Any changes to
those parts of `state` that affect logical soundness are undone; more
specifically, the values of symbols (sometimes called ``state global
variables'') in the list

The exception is that the first keyword in the returned

The evaluation of a hint term is done with guard checking turned off (see
set-guard-checking); e.g., the form

When a non-`er`, or to return a
non-erroneous value triple whose value is the list of keys and values you
would have typed had you supplied a common hint for the subgoal. (In
particular, any theory expressions in it are evaluated with respect to the
global current-theory, not whatever theory is active at the subgoal in
question.) If the generated list of keywords and values is illegal, an error
will be signaled and the proof attempt will be aborted.

The purpose of the

For these purposes, the goals produced by induction and the top-level goals of forcing rounds are not considered children; all original hints are available to them.

Only the first hint applicable to a goal, as specified in the user-supplied
list of `default-hints-table`, will be
applied to that goal. (For an advanced exception, see override-hints.)

It remains only to describe the bindings of the free variables.

Suppose the theorem prover is working on a clause named by some
`goal-spec`, e.g., "Subgoal *1/2'''". Corresponding to the printed

In the case of a common hint, the hint applies if the goal-spec of the hint is the same as the goal-spec of the clause in question.

In the case of a computed hint, the variable

As for `state`, they are provided so that you can pass
them to the `er` macro to print error messages. We recommend not
writing computed hints that otherwise change `state`!

The remaining variables,

For some instruction about how to use computed hints, see using-computed-hints.

- Autohide
- Tell ACL2 to automatically hide some terms.
- Instantiate-thm-for-matching-terms
- A computed hint which produces :use hints of the given theorem, based on occurences of a pattern in the current goal clause.
- Using-computed-hints
- How to use computed hints