Major Section: MISCELLANEOUS

Examples: The following :hints value is nonsensical. Nevertheless, it illustrates all of the available hint keywords:A very common hint is the:hints (("Goal" :do-not-induct t :do-not '(generalize fertilize) :expand ((assoc x a) (member y z)) :restrict ((<-trans ((x x) (y (foo x))))) :hands-off (length binary-append) :in-theory (set-difference-theories (current-theory :here) '(assoc)) :induct (and (nth n a) (nth n b)) :use ((:instance assoc-of-append (x a) (y b) (z c)) (:functional-instance (:instance p-f (x a) (y b)) (p consp) (f assoc))) :bdd (:vars (c a0 b0 a1 b1) :prove nil :bdd-constructors (cons)) :cases ((true-listp a) (consp a)) :by (:instance rev-rev (x (cdr z)))))

`:use`

hint, which in general takes as its
value a list of ``lemma instances'' (see lemma-instance) but
which allows a single lemma name as a special case:
:hints (("[1]Subgoal *1/1.2'" :use lemma23))

ACL2 also provides ``computed hints'' for the advanced user. See computed-hints

Background: `Hints`

are allowed in all events that use the theorem
prover. During `defun`

events there are two different uses of the
theorem prover: one to prove termination and another to verify the
guards. To pass a hint to the theorem prover during termination
proofs, use the `:hints`

keyword in the `defun`

's `xargs`

declaration. To
pass a hint to the theorem prover during the guard verification of
`defun`

, use the `:guard-hints`

keyword in the `defun`

's `xargs`

declaration. The `verify-guards`

event and the `defthm`

event also use
the theorem prover. To pass hints to them, use the `:hints`

keyword
argument to the event.

General Form of Common :hints: ((goal-spec :key1 val1 ... :keyn valn) ... (goal-spec :key1 val1 ... :keyn valn))where

`goal-spec`

is as described in the documentation for
goal-spec and the keys and their respective values are shown
below with their interpretations. (We also provide ``computed hints''
but discuss them separately; see computed-hints.)
`:DO-NOT-INDUCT`

`Value`

is `t`

, `name`

or `nil`

, indicating whether induction is permitted
under the specified goal. If `value`

is `t`

, then the attempt to apply
induction to the indicated goal or any subgoal under the indicated
goal will immediately cause the theorem prover to report failure.
Thus, the indicated goal must be proved entirely by simplification,
destructor elimination, and the other ``waterfall'' processes.
Induction to prove the indicated goal (or any subgoal) is not
permitted. See however the `:induct`

hint below. If `value`

is a
symbol other than `t`

or `nil`

, the theorem prover will give a
``bye'' to any subgoal that would otherwise be attacked with
induction. This will cause the theorem prover to fail eventually
but will collect the necessary subgoals. If `value`

is `nil`

, this
hint means induction is permitted. Since that is the default,
there is no reason to use the value `nil`

.

`:DO-NOT`

`Value`

is a term having at most the single free variable `world`

, which
when evaluated (with `world`

bound to the current ACL2 logical world)
produces a list of symbols that is a subset of the list

(preprocess ;propositional logic, simple rules simplify ;as above plus rewriting, linear arithmetic eliminate-destructors fertilize ;use of equalities generalize eliminate-irrelevance).The hint indicates that the ``processes'' named should not be used at or below the goal in question. Thus, to prevent generalization and fertilization, say, include the hint

:do-not '(generalize fertilize)If

`value`

is a single symbol, as in
:do-not generalize,it is taken to be

`'(value)`

.
`:EXPAND`

`Value`

is a true list of terms, each of which is of one of the forms
`(let ((v1 t1)...) b)`

or `(fn t1 ... tn)`

, where `fn`

is a defined
function symbol with formals `v1, ..., vn,`

and `body`

`b`

. Such a term
is said to be ``expandable:'' it can be replaced by the result of
substituting the `ti`

's for the `vi`

's in `b`

. The terms listed in the
`:expand`

hint are expanded when they are encountered by the
simplifier while working on the specified goal or any of its
subgoals. We permit `value`

to be a single such term instead of a
singleton list. **Note**: Also allowed are ``terms'' of the form
`(:free (var1 var2 ... varn) pattern)`

where the indicated variables
are distinct and `pattern`

is a term. Such ``terms'' indicate that we
consider the indicated variables to be instantiatable, in the
following sense: whenever the simplifier encounters a term that can
be obtained from `pattern`

by instantiating the variables
`(var1 var2 ... varn)`

, then it expands that term.

`:HANDS-OFF`

`Value`

is a true list of function symbols or lambda expressions,
indicating that under the specified goal applications of these
functions are not to be rewritten. `value`

may also be a single
function symbol or lambda expression instead of a list.

`:`

`IN-THEORY`

`Value`

is a ``theory expression,'' i.e., a term having at most the
single free variable `world`

which when evaluated (with `world`

bound to
the current ACL2 logical world (see world)) will produce a
theory to use as the current theory for the goal specified.
See theories.

`:INDUCT`

`Value`

is either `t`

or a term containing at least one recursively
defined function symbol; if `t`

, this hint indicates that the system
should proceed to apply its induction heuristic to the specified
goal produced (without trying simplification, etc.); if `value`

is
a term other than `t`

, then not only should the system apply
induction immediately, but it should analyze `value`

rather than
the goal to generate its induction scheme. Merging and the
other induction heuristics are applied. Thus, if `value`

contains several mergeable inductions, the ``best'' will be
created and chosen. E.g., the `:induct`

hint

(and (nth i a) (nth j a))suggests simultaneous induction on

`i`

, `j`

, and `a`

.
If both an `:induct`

and a `:do-not-induct`

hint are supplied for a
given goal then the indicated induction is applied to the goal and
the `:do-not-induct`

hint is inherited by all subgoals generated.

`:USE`

`Value`

is a lemma-instance or a true list of lemma-instances,
indicating that the propositions denoted by the instances be added
as hypotheses to the specified goal. See lemma-instance. Note
that `:use`

makes the given instances available as ordinary hypotheses
of the formula to be proved. The `:instance`

form of a lemma-instance
permits you to instantiate the free variables of previously proved
theorems any way you wish; but it is up to you to provide the
appropriate instantiations because once the instances are added as
hypotheses their variables are no longer instantiable. These new
hypotheses participate fully in all subsequent rewriting, etc. If
the goal in question is in fact an instance of a previously proved
theorem, you may wish to use `:by`

below.

`:`

BDD

This hint indicates that ordered binary decision diagrams (BDDs)
with rewriting are to be used to prove or simplify the goal.
See bdd for an introduction to the ACL2 BDD algorithm.

`Value`

is a list of even length, such that every other element,
starting with the first, is one of the keywords `:vars`

,
`:bdd-constructors`

, `:prove`

, or `:literal`

. Each keyword that
is supplied should be followed by a value of the appropriate form,
as shown below; for others, a default is used. Although `:vars`

must always be supplied, we expect that most users will be content
with the defaults used for the other values.

`:vars`

-- A list of ACL2 variables, which are to be treated as
Boolean variables. The prover must be able to check, using trivial
reasoning (see type-set), that each of these variables is
Boolean in the context of the current goal. Note that the prover
will use very simple heuristics to order any variables that do not
occur in `:vars`

(so that they are ``greater than'' the variables
that do occur in `:vars`

), and these heuristics are often far from
optimal. In addition, any variables not listed may fail to be
assumed Boolean by the prover, which is likely to seriously impede
the effectiveness of ACL2's BDD algorithm. Thus, users are
encouraged *not* to rely on the default order, but to supply a
list of variables instead. Finally, it is allowed to use a value of
`t`

for `vars`

. This means the same as a `nil`

value, except
that the BDD algorithm is directed to fail unless it can guarantee
that all variables in the input term are known to be Boolean (in a
sense discussed elsewhere; see bdd-algorithm).

`:literal`

-- An indication of which part of the current goal
should receive BDD processing. Possible values are:

:all treat entire goal as a single literal (the default) :conc process the conclusion n process the hypothesis with index n (1, 2, ...)

`:bdd-constructors`

-- When supplied, this value should be a
list of function symbols in the current ACL2 world; it is
`(cons)`

by default, unless `:bdd-constructors`

has a value in
the `acl2-defaults-table`

by default, in which case that value is
the default. We expect that most users will be content with the
default. See bdd-algorithm for information about how this
value is used.

`:prove`

-- When supplied, this value should be `t`

or `nil`

; it
is `t`

by default. When the goal is not proved and this value is
`t`

, the entire proof will abort. Use the value `nil`

if you are
happy to the proof to go on with the simplified term.

`:CASES`

`Value`

is a non-empty list of terms. For each term in the list, a
new goal is created from the current goal by assuming that term; and
also, in essence, one additional new goal is created by assuming all
the terms in the list false. We say ``in essence'' because if the
disjunction of the terms supplied is a tautology, then that final
goal will be a tautology and hence will in fact never actually be
created.

`:BY`

`Value`

is a lemma-instance, `nil`

, or a new event name. If the value is
a lemma-instance (see lemma-instance), then it indicates that
the goal (when viewed as a clause) is subsumed by the proposition
denoted by the instance (when viewed as a clause). To view a
formula as a clause, union together the negations of the hypotheses
and add the conclusion. For example,

(IMPLIES (AND (h1 t1) (h2 t2)) (c t1))may be viewed as the clause

{~(h1 t1) ~(h2 t2) (c t1)}.Clause

`c1`

is ``subsumed'' by clause `c2`

iff some instance of `c2`

is a
subset of `c1`

. For example, the clause above is subsumed by
`{~(h1 x) (c x)}`

, which when viewed as a formula is
`(implies (h1 x) (c x))`

.
If the value is `nil`

or a new name, the prover does not even
attempt to prove the goal to which this hint is attached. Instead
the goal is given a ``bye'', i.e., it is skipped and the proof
attempt continues as though the goal had been proved. If the prover
terminates without error then it reports that the proof would have
succeeded had the indicated goals been proved and it prints an
appropriate defthm form to define each of the `:by`

names. The
``name'' `nil`

means ``make up a name.''

The system does not attempt to check the uniqueness of the `:by`

names
(supplied or made up), since by the time those goals are proved the
namespace will be cluttered still further. Therefore, the final
list of ``appropriate'' `defthm`

forms may be impossible to admit
without some renaming by the user. If you must invent new names,
remember to substitute the new ones for the old ones in the `:by`

hints themselves.

`:RESTRICT`

(Warning: This is a sophisticated hint, intended for advanced
users. This hint was suggested by Bishop Brock.)

`Value`

is an association list. Its members are of the form
`(x subst1 subst2 ...)`

, where: `x`

is either (1) a rune whose `car`

is
`:`

`rewrite`

or (2) an event name corresponding to one or more such
runes; and `(subst1 subst2 ...)`

is a non-empty list of substitutions,
i.e., of association lists pairing variables with terms. First
consider the case that `x`

is a `:`

`rewrite`

rune. First recall that
without this hint, the rewrite rule named `x`

is used by matching its
left-hand side (call it `lhs`

) against the term currently being
considered by the rewriter, that is, by attempting to find a
substitution `s`

such that the instantiation of `lhs`

using `s`

is equal
to that term. If however the `:restrict`

hint contains
`(x subst1 subst2 ...)`

, then this behavior will be modified by
restricting `s`

so that it must extend `subst1`

; and if there is no such
`s`

, then `s`

is restricted so that it must extend `subst2`

; and so on,
until the list of substitutions is exhausted. If no such `s`

is
found, then the rewrite rule named `x`

is not applied to that term.
Finally, if `x`

is an event name corresponding to one or more `:`

`rewrite`

runes (that is, `x`

is the ``base symbol'' of such runes;
see rune), say runes `r1`

, ... `rn`

, then the meaning is the same
except that `(x subst1 subst2 ...)`

is replaced by
`(ri subst1 subst2 ...)`

for each `i`

. Once this replacement is
complete, the hint may not contain two members whose `car`

is the same
rune.

Note that the substitutions in `:restrict`

hints refer to the
variables actually appearing in the goals, not to the variables
appearing in the `:`

`rewrite`

rule being restricted.

Here is an example, supplied by Bishop Brock. Suppose that the database includes the following rewrite rule, which is probably kept disabled. (We ignore the question of how to prove this rule.)

cancel-<-*$free: (implies (and (rationalp x) (rationalp y) (rationalp z)) (equal (< y z) (if (< x 0) (> (* x y) (* x z)) (if (> x 0) (< (* x y) (* x z)) (hide (< y z))))))Then ACL2 can prove the following theorem (unless other rules get in the way), essentially by multiplying both sides by

`x`

.
(thm (implies (and (rationalp x) (< 1 x)) (< (/ x) 1)) :hints (("Goal" :in-theory (enable cancel-<-*$free) :restrict ((cancel-<-*$free ((x x) (y (/ x)) (z 1)))))))The

`:restrict`

hint above says that the variables `x`

, `y`

, and `z`

in the
rewrite rule `cancel-<-*$free`

above should be instantiated
respectively by `x`

, `(/ x)`

, and `1`

. Thus `(< y z)`

becomes `(< (/ x) 1)`

,
and this inequality is replaced by the corresponding instance of the
right-hand-side of `cancel-<-*$free`

. Since the current conjecture
assumes `(< 1 x)`

, that instance of the right-hand side simplifies to
(< (* x (/ x)) (* x 1))which in turn simplifies to

`(< 1 x)`

, a hypothesis in the present
theorem.