Many of these hints affect the how the prover operates not only on the goal
to which they are applied but also on its subgoals (and its subgoals'
subgoals, etc.; for a deeper explanation see hints-and-the-waterfall).
The following hints, however, have a specific effect only on the goal to which
they are applied: :bdd, :by, :cases, :clause-processor,
:error, :induct, :or, and :use. For example, suppose that
you specify both a :cases hint and an :expand hint for
"Goal". Then the :cases hint will immediately result in subgoals,
without calling the ACL2 rewriter; the :expand hint will be used by the
rewriter in subsequent goals.
- :backchain-limit-rw
Value is a natural number or nil, indicating the level of
backchaining for rewrite, meta, and linear rules. This
overrides, for the current goal and (as with :in-theory hints)
descendant goals, the default backchain-limit
(see set-backchain-limit).
- :backtrack
This is an advanced hint. You can probably accomplish its effect by
the use of ordinary computed hints; see computed-hints. But if you are
an expert, read on. (See hints-and-the-waterfall for some relevant
background.)
Value is a computed hint, which is an expression that evaluates either
to nil — indicating that the :backtrack hint is to have no
effect — or to a non-empty alternating list of :keyi vali pairs,
as expected for a hint. However, unlike ordinary computed hints,
:backtrack hints are evaluated after a goal has been processed to
yield zero or more subgoals, not before. Moreover, variables PROCESSOR
and CLAUSE-LIST are allowed, but variable
STABLE-UNDER-SIMPLIFICATIONP is not. We explain in more detail below,
but first consider the following simple example. First we define a standard
list reversal function:
(defun rev (x)
(if (consp x)
(append (rev (cdr x)) (cons (car x) nil))
nil))
Now we prove:
(thm (true-listp (rev x)))
The successful proof includes the following output.
Subgoal *1/1'
(IMPLIES
(AND (CONSP X)
(TRUE-LISTP (REV (CDR X))))
(TRUE-LISTP (APPEND (REV (CDR X)) (LIST (CAR X))))).
The destructor terms (CAR X) and (CDR X) can be
eliminated by using CAR-CDR-ELIM to replace X
by (CONS X1 X2), (CAR X) by X1 and (CDR X) by
X2. This produces the following goal.
Subgoal *1/1''
(IMPLIES (AND (CONSP (CONS X1 X2))
(TRUE-LISTP (REV X2)))
(TRUE-LISTP (APPEND (REV X2) (LIST X1)))).
But suppose that we attach a :backtrack hint to the goal above at
which destructor elimination was applied:
(thm (true-listp (rev x))
:hints (("Subgoal *1/1'"
:backtrack
(quote (:do-not '(eliminate-destructors))))))
Then when ACL2 applies destructor elimination as displayed above, this time
the :backtrack hint applies, evaluating to (:do-not
'(eliminate-destructors)). Since this list is not nil, the prover
decides not to keep the new subgoal, and instead supplies this :do-not
hint before attacking the goal again. In this example, ACL2 happens to use a
technique later in its ``waterfall'' arsenal than destructor elimination,
namely, generalization:
Subgoal *1/1'
(IMPLIES
(AND (CONSP X)
(TRUE-LISTP (REV (CDR X))))
(TRUE-LISTP (APPEND (REV (CDR X)) (LIST (CAR X))))).
[Note: A hint was supplied for the goal above,
because of a :backtrack hint that is preventing
destructor elimination. Thanks!]
We generalize this conjecture, replacing
(REV (CDR X)) by RV. This produces
Subgoal *1/1''
(IMPLIES (AND (CONSP X) (TRUE-LISTP RV))
(TRUE-LISTP (APPEND RV (LIST (CAR X))))).
We now provide a careful explanation of how :backtrack hints work, but
we suggest that you keep the example above in mind. If ``:backtrack
form'' is part of the hint that has been selected for a goal, then form
is evaluated when one of ACL2's clause processors successfully applies
to the current goal to produce a list of subgoals. This evaluation takes
place in an environment just like that for any computed hint (see computed-hints), with the following exceptions. First, the variable
STABLE-UNDER-SIMPLIFICATIONP is not allowed to occur free in form,
but instead the following new variables are allowed to occur free and are
bound for this evaluation as follows: PROCESSOR is bound to the processor
in the list *preprocess-clause-ledge* that has applied to the goal, and
CLAUSE-LIST is bound to the list of clauses (each a list of literals that
is implicitly disjoined) returned by that clause processor. Second, the
variables HIST and PSPV are bound to the history and pspv returned
by the clause processor, not the ones that were passed to the clause
processor. If this evaluation returns an error, then the proof aborts, as for
any computed hint whose evaluation returns an error. If this evaluation
returns nil, then the :backtrack hint has no effect, and the goal is
replaced by the list of goals (the value of CLAUSE-LIST described above),
as usual. Otherwise, the clause processor is deemed to have failed, and the
goal clause is tried again starting at the top of the waterfall after
selecting the hint returned by the above evaluation. That hint will normally
be an alternating list of hint keywords and their values, but if it is a
custom keyword hint (see custom-keyword-hints), then it will be handled
in the usual manner but with the first three variables above bound to the
symbol :OMITTED. Of course, if the new hint includes a value for
:BACKTRACK then this process can loop; care should be taken to keep that
from happening.
A final note about :BACKTRACK hints: since these are a form of
computed hints, override-hints (if any) are applied to their evaluation
result just as with any computed hint. That is, the backtrack hint is
successively modified with each override-hint, to produce a final hint that is
actually used (or, ignored if that final hint is nil). See override-hints.
- :bdd
This hint indicates that ACL2's built-in 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 type-reasoning, 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.
- :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 either equal to
the proposition denoted by the instance, or is subsumed by that proposition
when both are viewed as clauses. 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)).
Note that if the value is the name of a function symbol introduced by
defun, then the original form of the body of that definition is used.
This behavior differs from that provided by a :use hint, which uses the
normalized (simplified) body; see normalize.
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.'' Here is an example
(admittedly contrived for illustration purposes).
ACL2 !>(thm (equal (append (append x y) z)
(append x y z))
:hints (("Subgoal *1/2'" :by nil)))
Name the formula above *1.
[[... output omitted here ...]]
[Note: A hint was supplied for the goal below. Thanks!]
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (APPEND (APPEND (CDR X) Y) Z)
(APPEND (CDR X) Y Z)))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X Y Z))).
But we have been asked to pretend that this goal is subsumed by the
yet-to-be-proved |THM Subgoal *1/2'|.
Subgoal *1/1
[[... proof goes on; further output omitted here ...]]
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.
- :case-split-limitations
Value is the same as for set-case-split-limitations. The
simplifier will behave as though the value had instead been supplied to
set-case-split-limitations; see set-case-split-limitations. This
behavior will persist through subgoals unless overridden by another
:CASE-SPLIT-LIMITATIONS hint.
- :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.
- :clause-processor
Value specifies the application of a user-defined simplifier to
the current goal. See clause-processor, which provides necessary
background and hint syntax. Also see define-trusted-clause-processor
for a discussion of ``trusted clause-processors'': goal-level simplifiers that
may be external to ACL2 and do not need to be proved correct in ACL2.
You can see all current :clause-processor rules by issuing the command
(print-clause-processor-rules), and you can see the names of all trusted
clause-processors by issuing the command (table
trusted-cl-proc-table).
- :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).
See also do-not-hint for a way to automatically provide
:do-not hints across several theorems.
- :do-not-induct
Value indicates whether induction is permitted under the
specified goal. The legal values are t, :otf-flg-override,
:otf, nil, or a non-keyword symbol other than t or nil.
The default is nil, meaning that induction is permitted as usual. A
non-nil value prohibits the use of induction to prove the indicated goal
or any of its subgoals, as described below.
If value is t or :otf-flg-override, 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, except that if :otf-flg t is specified (see otf-flg) and
value is t, then the proof will continue until the time at which the
goal pushed for induction is finally encountered and causes failure. The
latter behavior is also what occurs if value is :otf. See however
the :induct hint below. If value is a non-keyword symbol other than
t or nil, the theorem prover will skip every subgoal under the
indicated goal (giving it a ``bye'', as with a ``:by'' hint) that would
otherwise be attacked with induction. This will cause the theorem prover to
fail eventually, printing every subgoal thus skipped in the form of an event
to prove, each with a name based on the value of the :do-not-induct hint
that caused that subgoal to be skipped.
Remarks.
(1) An :induct hint is applied to a goal even if a :do-not-induct
hint is in effect for that goal. Consider the following examples.
(thm (equal (append (append x y) z) (append x y z))
:hints (("Goal" :induct t :do-not-induct t)))
(thm (and (equal (append (append x y) z) (append x y z))
(equal (append (append u v) w) (append u v w)))
:hints (("Goal" :do-not-induct t)
("Subgoal 2" :induct t)))
In the first of these, the :do-not-induct hint has no effect on the
proof; instead, the :induct hint forces an induction that allows the
proof to succeed (without any sub-inductions). The second of these
illustrates that even though :do-not-induct can stop sub-inductions, its
effect is overridden by :induct. For the proof of that second example,
ACL2 immediately splits into two subgoals. Then in spite of the top-level
:do-not-induct hint, the proof is allowed to proceed past Subgoal 2,
which requires induction, because of the hint :induct t. However, the
proof halts after Subgoal 1 because of the :do-not-induct hint that has
been established ``above'' it, at "Goal". (For more about the way
hints are processed, see hints-and-the-waterfall.)
(2) For an advanced example of the use of value :otf for
:do-not-induct combined with override-hints, see community book
books/hints/basic-tests.lisp.
- :error
Value is typically a ``fmt message'' to be printed by the fmt tilde-directive ~@ but may be any object. The effect of this hint is to
cause an error when the hint is translated. There is no reason to include an
:ERROR hint in any user-typein, since it will only cause an error when
the form is evaluated. :ERROR hints are useful in the definition of
functions that generate custom keyword hints (see custom-keyword-hints)
and computed hints (see computed-hints). For example, if you wish to
define a custom keyword hint :my-hint val and you wish the hint to signal
an error if there is something inappropriate about val in the context of
the hint, use the following code to generate the hint
(list :ERROR (cons "Your specified value, ~x0, is inappropriate"
(list (cons #0 val))))
which is equivalent to
(list :ERROR (msg "Your specified value, ~x0, is inappropriate"
val))
which, if val has the value 123, would evaluate to the hint
(:ERROR ("Your specified value, ~x0, is inappropriate" (#0 . 123))).
Note that any time an :ERROR keyword is produced during hint
processing, including iterations of the expansions of custom keyword hints or
of override-hints, an error will occur.
- :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. (There is no
separate ``expand'' process.) We permit value to be a single such term
instead of a singleton list. Remarks: (0) Note that in the event that
a :definition rule has been admitted for fn, then by default, the
body b is determined by the (most recently admitted such) rule rather
than the original definition of fn; see definition. (1) 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. (2) Also allowed are ``terms'' of the
form (:with name term), where name is a function symbol, a macro
name that denotes a function symbol (see macro-aliases-table), or a
rune. The corresponding definition rule or (less often) rewrite rule is then used in place of the current body for the function
symbol of term; see show-bodies and see set-body. If the
rule is of the form (implies hyp (equiv lhs rhs)), then after matching
lhs to the current term in a context that is maintaining equivalence
relation equiv, ACL2 will replace the current term with (if hyp rhs
(hide term)), or just rhs if the rule is just (equal lhs rhs).
(3) A combination of both :free and :with, as described above, is
legal. (4) The term :LAMBDAS is treated specially. It denotes the list
of all lambda applications (i.e., let expressions) encountered during
the proof. Conceptually, this use of :LAMBDAS tells ACL2 to treat lambda
applications as a notation for substitutions, rather than as function calls
whose opening is subject to the ACL2 rewriter's heuristics (specifically, not
allowing lambda applications to open when they introduce ``too many'' if
terms).
- :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. Note however that subterms will still be rewritten; see
hide if that is not what is intended. (The community book
books/clause-processors/autohide.lisp from Jared Davis may also be
helpful in that case.) 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.
Note that an :in-theory hint will always be evaluated relative
to the current ACL2 logical world, not relative to the theory of a
previous goal. Consider the following example.
(defthm prop
(p (f (g x)))
:hints (("Goal" :in-theory (disable f))
("Subgoal 3" :in-theory (enable g))))
Consider in particular the theory in effect at Subgoal 3. This call
of the enable macro enables g relative to the current-theory of the current logical world, not relative to
the theory produced by the hint at Goal. Thus, the disable of
f on behalf of the hint at Goal will be lost at Subgoal 3, and
f will be enabled at Subgoal 3 if was enabled globally when
prop was submitted.
- :induct
Value is either t or a term that is not an atom or a quoted
constant. The value t indicates that the system use induction
immediately by applying its induction heuristic to the specified goal
(without trying simplification, etc.). Otherwise, the system should apply
induction immediately, but it should analyze value rather than the goal
to generate its induction scheme. Either way (i.e., for value t
or not), 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.
- :instructions
Value is a list of interactive proof-builder instructions;
see instructions. Unlike other hint keywords described here, this one
is actually a custom keyword hint (see custom-keyword-hints) that
generates a suitable :clause-processor hint.
- :no-op
Value is any object and is irrelevant. This hint has no effect,
although unlike an empty hint such as ("Goal"), it is not dropped.
Thus, ("Goal" :no-op t) will shadow any later (or default) hint on
"Goal", but ("Goal") will not. Unlike other hint keywords,
multiple occurrences of the keyword :no-op are tolerated.
- :no-thanks
Value is any object. This hint does nothing, except that if
value is non-nil then the usual ``[Note: A hint was
supplied... Thanks!]'' is not printed.
- :nonlinearp
Value is t or nil, indicating whether non-linear-arithmetic is active. The default value is nil. See non-linear-arithmetic.
- :or
Value is a list (kwd-val-listp-1 ... kwd-val-listp-k), where
each kwd-val-listp-i is a list satisfying keyword-value-listp,
i.e., an alternating list of keywords and values. This hint causes an attempt
to prove the specified goal using hints kwd-val-listp-i in
sequence (first kwd-val-listp-1, then kwd-val-listp-2, and so on),
until the first of these succeeds. If none succeeds, then the prover proceeds
after heuristically choosing the ``best'' result, taking into account the
goals pushed in each case for proof by induction.
The following (contrived but illustrative example illustrates how :or
hints work.
ACL2 !>(thm (f x)
:hints
(("Goal"
:expand ((nth x 3))
:or ((:in-theory (disable car-cons))
(:use cdr-cons :in-theory (enable append)))
:do-not '(generalize))))
[Note: A hint was supplied for the goal above. Thanks!]
The :OR hint for Goal gives rise to two disjunctive branches. Proving
any one of these branches would suffice to prove Goal. We explore
them in turn, describing their derivations as we go.
---
Subgoal D2
( same formula as Goal ).
The first disjunctive branch (of 2) for Goal can be created by applying
the hint:
("Subgoal D2" :EXPAND ((NTH X 3))
:IN-THEORY (DISABLE CAR-CONS)
:DO-NOT '(GENERALIZE)).
[Note: A hint was supplied for the goal above. Thanks!]
Normally we would attempt to prove this formula by induction. However,
we prefer in this instance to focus on the original input conjecture
rather than this simplified special case. We therefore abandon our
previous work on this conjecture and reassign the name *1 to the original
conjecture. (See :DOC otf-flg.) [Note: Thanks again for the hint.]
---
Subgoal D1
( same formula as Goal ).
The second disjunctive branch (of 2) for Goal can be created by applying
the hint:
("Subgoal D1" :EXPAND ((NTH X 3))
:USE CDR-CONS
:IN-THEORY (ENABLE APPEND)
:DO-NOT '(GENERALIZE)).
[Note: A hint was supplied for the goal above. Thanks!]
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE the formula
of an enabled :REWRITE or :DEFINITION rule, so you may want to consider
disabling (:REWRITE CDR-CONS) in the hint provided for Subgoal D1.
See :DOC using-enabled-rules.
We augment the goal with the hypothesis provided by the :USE hint.
The hypothesis can be obtained from CDR-CONS. We are left with the
following subgoal.
Subgoal D1'
(IMPLIES (EQUAL (CDR (CONS X Y)) Y)
(F X)).
By the simple :rewrite rule CDR-CONS we reduce the conjecture to
Subgoal D1''
(F X).
... and so on. This example illustrates how ACL2 processes :or hints
in general. For each i from 1 to k, a so-called ``disjunctive''
subgoal is created by splicing kwd-val-listp-i into the other hint values
(if any) supplied for the given goal, in order. A corresponding subgoal is
created for each i, numbered in the usual manner (hence, counting down)
except that the ``D'' is prefixed to each resulting goal.
- :reorder
Value is a list of positive integers without duplicates,
corresponding to the numbering of subgoals generated for the goal-spec
"G", say "G.k" down to "G.1". Those subgoals are
reordered so that if value is (n1 n2 ... nk), then the goal now
numbered "G.k" will be the goal originally numbered "G.n1"; the
goal now numbered "G.k-1" will be the goal formerly numbered
"G.n2"; and so on, down the list of ni, after which the goals not
yet printed are printed in their original order. Note that reordering for
subgoals of a goal to be proved by induction, such as *1, is not
supported.
- :restrict
This hint, originally suggested by Bishop Brock, sometimes allows rules
with free variables (see free-variables) to be applied successfully by
the rewriter, thus avoiding the clutter, case-splitting, and theory management
(disabling) that can occur with :use hints.
Warning: This is a sophisticated hint that may be most appropriate for
experienced ACL2 users. In particular, :restrict hints are ignored by
the preprocessor, so you might find it useful to give the hint :do-not
'(preprocess) when using any :restrict hints, at least if the rules in
question are abbreviations (see simple).
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 :definition 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 or :definition rune. Recall that without this
hint, the 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 or definition rule named x is not applied to that
term. Finally, if x is an event name corresponding to one or more
:rewrite or :definition 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 rule
being restricted.
The following example, supplied by Mihir Mehta, illustrates the use of
:restrict to handle free variables (in this case, a single free variable
y). The call of thm below fails without the indicated
:restrict hint.
(defthm subsetp-trans
(implies (and (subsetp x y) (subsetp y z)) (subsetp x z)))
(defthm subsetp-evens (subsetp-equal (evens l) l))
(thm (subsetp (evens (evens l)) l)
:hints (("Goal" :restrict ((subsetp-trans ((y (evens l))))))))
Here is another example, this one 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.
- :rw-cache-state
Value is an element of the list constant
*legal-rw-cache-states*: :atom (the default), nil, t, or
:disabled. This hint applies to the indicated goal and all its
descendants, to set the so-called ``rw-cache-state'' to the indicated value;
see set-rw-cache-state.
- :use
Examples of :USE hints are shown near the top of this
documentation topic.
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: that is, the :use hint
replaces a goal, G, by the new goal, (IMPLIES P G), where P is
the theorem specified by the (conjunction of the) lemma instances provided.
The :instance form of a lemma-instance permits you to instantiate
the free variables of previously proved theorems any way you wish, even
allowing for differences in packages; see lemma-instance for
details. 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 (documented above). Sometimes theories are helpful when employing :use hints; see minimal-theory.
If the value is the name of a function symbol introduced by defun,
then the normalized (simplified) body of that definition is used; see normalize. This behavior differs from that provided by a :by hint,
where the original body of the definition is used.
