Major Section: MISCELLANEOUS
Examples: "Goal" "goal" "Subgoal *1/3''" "subgoal *1/3''" "[2]Subgoal *1/3''"
When hints are given to the theorem prover, a goal-spec is provided to specify the goal to which the hints are to be applied. The hints provided are carried along innocuously until the named goal arises. When it arises, the hints are ``activated'' for that goal and its descendents.
A legal goal specification may be extracted from the theorem prover's output. Certain lines clearly label formulas, as in
Subgoal *1/3.2' (IMPLIES ... ...)and these lines all give rise to goal specifications. In general, these lines all start either with ``Goal'' or ``Subgoal'' or else with those words preceded by a number in square brackets, as in
[1]Subgoal *1/3.2' (IMPLIES ... ...).A goal specification may be obtained by deleting any surrounding whitespace from such a line and embedding the text in string quotation marks. Thus
"[1]Subgoal *1/3.2'"is the goal specifier for the goal above.
As noted, a hint is applied to a goal when the hint's goal
specification matches the name ACL2 assigns to the goal. The
matching algorithm is case-insensitive. Thus, alternative goal
specifications for the goal above are "[1]subgoal *1/3.2'" and
"[1]SUBGOAL *1/3.2'". The matching algorithm does not tolerate
non-case discrepancies. Thus, "[1]Subgoal*1/3.2'" and
" [1]Subgoal *1/3.2'" are unacceptable.
Sometimes a formula is given two names, e.g.,
Subgoal *1/14.2'
(IMPLIES ...
...)
Name the formula above *1.1.
It is the first name (the one that starts with ``Goal'' or
``Subgoal'') and not the second which constitutes a legal goal-spec.
Roughly speaking, when the system prints the line containing the
goal specification, it activates any hints that are attached to that
goal-spec. Consider the example above. Suppose Subgoal *1/14.2'
could be proved by using a certain lemma instance. Then the
appropriate entry in the hints would be:
("Subgoal *1/14.2'" :use ...)
This might surprise you because the system appears to do nothing
to *1/14.2' besides push it for a subsequent induction. But
actually between the time the system printed the goal-spec line and
the time it decides to push the goal, you can think of the system as
trying everything it has. So a use hint activated when
Subgoal *1/14.2' arises is just what you want.
But what if you want to give an :induct hint? By the time induction
is tried, the formula has been given the name *1.1. Well, this is
one you just have to remember:
("Subgoal *1/14.2'" :induct ...).
When the above hint is activated the :induct directive
short-circuits the rest of the processing and sends immediately the
formula into the pool of goals to prove by induction. The induct
hint is attached to the formula in the pool and when the time comes
to turn our attention to that goal, the induct advice is
followed.
Major Section: MISCELLANEOUS
The ACL2 system provides a mechanism for restricting a function
definition to a particular domain. Although such restrictions,
which are called ``guards,'' are actually ignored by the ACL2
logic, they can be useful as a specification device or as a
means of causing the execution of definitions directly in Common
Lisp. To make such a restriction, use the :guard xarg to
defun. See xargs for a discussion of how to use :guard.
The general issue of guards and guard verification is discussed
in the topics listed below.
Major Section: GUARD
Most users can probably profit by avoiding dealing with guards most
of the time. If they seem to get in the way, they can be ``turned
off'' using the command :set-guard-checking nil; for more
about this, see set-guard-checking. For more about guards in
general, see guard.
The guard on a function symbol is a formula about the formals of the
function. To see the guard on a function, use the keyword command
:args. See args. To specify the guard on a function at
defun-time, use the :guard xarg. See xargs.
Guards can be seen as having either of two roles: (a) they are a specification device allowing you to characterize the kinds of inputs a function ``should'' have, or (b) they are an efficiency device allowing logically defined functions to be executed directly in Common Lisp. Briefly: If the guards of a function definition are ``verified'' (see verify-guards), then the evaluation of a call of that function on arguments satisfying its guard will have the following property:
All subsequent function calls during that evaluation will be on arguments satisfying the guard of the called function.The consequence of this fact for (a) is that your specification function is well-formed, in the sense that the values returned by this function on appropriate arguments only depend on the restrictions of the called functions to their intended domains. The consequence of this fact for (b) is that in the ACL2 system, when a function whose guards have been verified is called on arguments that satisfy its guard, then the raw lisp function defined by this functions's
defun event is used to evaluate the call. Note
however that even when the user-supplied defun is not used, ACL2
uses a corresponding ``executable counterpart'' that generally
performs, we expect, nearly as well as the raw lisp function.
See comp to see how compilation can speed up both kinds of
execution.
Let us turn next to the issue of the relationship between guards and
evaluation. See guards-and-evaluation.
Major Section: GUARD
The discussion of guards concludes here with a few miscellaneous
remarks. (Presumably you found this documentation by following a
link; see guards-for-specification.) For further information
related to guards other than what you find under ``guard,'' see
any of the following documentation topics: guard-example,
set-verify-guards-eagerness, set-guard-checking, and
verify-guards.
Defun can be made to try to verify the guards on a function.
This is controlled by the ``defun-mode'' of the defun;
see defun-mode. The defun-mode is either as specified with the
:mode xarg of the defun or else defaults to the default
defun-mode. See default-defun-mode. If the defun-mode of the
defun is :logic and either a :guard is specified or
:verify-guards t is specified in the xargs, then we attempt to
verify the guards of the function. Otherwise we do not.
It is sometimes impossible for the system to verify the guards of a
recursive function at definition time. For example, the guard
conjectures might require the invention and proof of some
inductively derived property of the function (as often happens when
the value of a recursive call is fed to a guarded subroutine). So
sometimes it is necessary to define the function using
:verify-guards nil then to state and prove key theorems about the
function, and only then have the system attempt guard verification.
Post-defun guard verification is achieved via the event
verify-guards. See verify-guards.
It should be emphasized that guard verification affects only two things: how fast ACL2 can evaluate the function and whether the function is executed correctly by raw Common Lisp, without guard violations. Since ACL2 does not use the raw Common Lisp definition of a function to evaluate its calls unless that function's guards have been verified, the latter effect is felt only if you run functions in raw Common Lisp rather than via ACL2's command loop.
Guard verification does not otherwise affect the theorem prover or the semantics of a definition. If you are not planning on running your function on ``big'' inputs and you don't care if your function runs correctly in raw Common Lisp (e.g., you have formalized some abstract mathematical property and just happened to use ACL2 as your language), there is no need to suffer through guard verification. Often users start by not doing guard verification and address that problem later. Sometimes you are driven to it, even in mathematical projects, because you find that you want to run your functions particularly fast or in raw Common Lisp.
If certify-book is used to compile a file, and the file contains
functions with unverified guard conjectures, then you will be warned
that the compiled file cannot be loaded into raw Common Lisp with
the expectation that the functions will run correctly. This is just
the same point we have been making: ACL2 and Common Lisp agree only
on the restricted domains specified by our guards. When guards are
violated, Common Lisp can do anything. When you call a compiled
function on arguments violating its guards, the chances are only
increased that Common Lisp will go berserk, because compiled
functions generally check fewer things at runtime and tend to be
more fragile than interpreted ones.
Major Section: GUARD
For a careful introduction to guards, see guard.
I. GUARD CHECKING DURING EXECUTION
Effect
Guards on definitions are checked at execution time (except for guards on subsidiary calls of recursive or mutually recursive functions).
When does it happen
By default, guards are checked for all forms submitted at the top level.
To disable
:set-guard-checking nil
To (re-)enable
:set-guard-checking t
II. GUARD VERIFICATION
Effect
A proof is attempted of the obligations arising from the guards of
subsidiary functions in a defun, defthm, or defaxiom event.
When does it happen
Only names of defined functions, defthms, and defaxioms are
subject to guard verification. Guard verification may occur when
functions are defined (using defun), but it requires an explicit
call of verify-guards in order to verify guards for defthms
and defaxioms. Constrained functions (see encapsulate) may
not have their guards verified.
(verify-guards foo ...)
causes guard verification for the defun, defthm, or defaxiom named
by foo, if it has not already been successfully done. The default
defun-mode (see default-defun-mode) must be :logic, or else
this event is ignored.
(defun foo ...)
causes guard verification of foo if and only if the following
conditions are both met. (However,
see set-verify-guards-eagerness for how to change this
behavior.)
1. Foo is processed in:logicmode (either by setting mode:logicglobally, or by including:mode :logicin thexargsdeclaration).2. The
xargsdeclaration (see xargs) either specifies:guardor specifies:verify-guardst(or both).
(verify-termination foo ...)
causes guard verification of foo if foo is a function currently
defined in :program mode and the appropriate xargs are supplied, as
discussed for the case of defun above. The default defun-mode
(see default-defun-mode) must be :logic, or else this event is
ignored.
Major Section: GUARD
The guard has no effect on the logical axiom added by the definition of a function. It does, however, have consequences for how calls of that function are evaluated in ACL2. We begin by explaining those consequences, when ACL2 is in its default ``mode,'' i.e., as originally brought up. In subsequent discussion we'll consider other ways that guards can interact with evaluation. For more about guards in general, see guard. Also see generalized-booleans for discussion about a subtle issue in the evaluation of certain Common Lisp functions.
Guards and evaluation I: the default
Consider the following very simple definition.
(defun foo (x) (cons 1 (cdr x)))First consider how raw Common Lisp behaves when evaluating calls of this function. To evaluate
(foo x) for some expression x, first
x is evaluated to some value v, and then (cons 1 (cdr x)) is
evaluated with x bound to v. For example, if v is (cons 'a 3), then
Common Lisp computes (cons 1 3). But if (for example) v is a
number, e.g., 7, then there is no way to predict what Common
Lisp might do. Some implementations would cause ``sensible''
errors, others might return nonsense, still others might crash the
host machine. The results tend toward the catastrophic if the call
of foo in question is in compiled code.
Now by default, ACL2 evaluates calls of foo exactly as Common
Lisp does, except that it uses guards to check the ``legality'' of
each function call. So for example, since (cdr x) has a guard
of (or (consp x) (equal x nil)), the call (foo 7) would cause a
``guard violation,'' as illustrated below.
ACL2 !>(foo 7)Thus, the relation between evaluation in ACL2 and evaluation in Common Lisp is that the two produce the very same results, provided there is no guard violation.ACL2 Error in TOP-LEVEL: The guard for the function symbol CDR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CDR 7).
ACL2 !>
Guards and evaluation II: :set-guard-checking.
The ACL2 logic is a logic of total functions. That is, every application of a function defined has a completely specified result. See the documentation for each individual primitive for the specification of what it returns when its guard is violated; for example, see cdr.
The presence of guards thus introduces a choice in the sense of
evaluation. When you type a form for evaluation do you mean for
guards to be checked or not? Put another way, do you mean for the
form to be evaluated in Common Lisp (if possible) or in the ACL2
logic? Note: If Common Lisp delivers an answer, it will be the
same as in the logic, but it might be erroneous to execute the form
in Common Lisp. For example, the ACL2 logic definition of cdr
implies that the cdr of an atom is nil; see cdr. So:
should (cdr 7) cause a guard violation error or return nil?
The top-level ACL2 loop has a variable which controls which sense of
execution is provided. By default, ``guard checking'' is on, by
which we mean that guards are checked at runtime, in the sense
already described. To turn it off, do :set-guard-checking nil.
To turn ``guard checking'' back on, execute the top-level form
:set-guard-checking t. The status of this variable is reflected
in the prompt; guard-checking is ``on'' when the prompt contains an
exclamation mark (also see default-print-prompt). For example,
ACL2 !>means guard checking is on and
ACL2 >means guard checking is off. The exclamation mark can be thought of as ``barring'' certain computations. The absence of the mark suggests the absence of error messages or unbarred access to the logical axioms. Thus, for example
ACL2 !>(car 'abc)will signal an error, while
ACL2 >(car 'abc)will return
nil. To return to our previous example: with guard
checking off, (foo 7) evaluates to (cons 1 nil).Guards and evaluation III: guard verification
Consider the defininition of foo given above, but modified so
that a reasonable guard of (consp x) is specified, as shown below.
(defun foo (x) (declare (xargs :guard (consp x))) (cons 1 (cdr x)))We say ``reasonable guard'' above because if
x is such that
(consp x) holds, then the call of cdr in the evaluation of
(foo x) will not cause a guard violation. Thus, it ``should'' be
legal to evaluate (foo x), for any such x, simply by
evaluating this form in raw Common Lisp.
The verify-guards event has been provided for this purpose.
Details may be found elsewhere; see verify-guards. Briefly,
for any defined function fn, the event (verify-guards fn)
attempts to check the condition discussed above, that whenever fn
is called on arguments that satisfy its guard, the evaluation of
this call will proceed without any guard violation. If this check
is successful, then future calls of this sort will be evaluated in
raw Common Lisp.
Returning to our example above, the (verify-guards foo) will
succeed because the guard (consp x) of foo implies the guard
generated from the call (cdr x) in the body of the definition,
namely, (or (consp x) (equal x nil)) (see cdr). Then the
evaluation of (foo (cons 'a 3)) will take place in raw Common
Lisp, because (cons 'a 3) satisfies the guard of foo.
This ability to dive into raw Common Lisp hinges on the proof that the guards you attach to your own functions are sufficient to insure that the guards encountered in the body are satisfied. This is called ``guard verification.'' Once a function has had its guards verified, then ACL2 can evaluate the function somewhat faster (but see ``Guards and evaluation V: efficiency issues'' below). Perhaps more importantly, ACL2 can also guarantee that the function will be evaluated correctly by any implementation of Common Lisp (provided the guard of the function is satisfied on the input). That is, if you have verified the guards of a system of functions and you have determined that they work as you wish in your host ACL2 (perhaps by proving it, perhaps by testing), then they will work identically in any Common Lisp.
There is a subtlety to our treatment of evaluation of calls of functions whose guards have been verified. If the function's guard is not satisfied by such a call, then no further attempt is made to evaluate any call of that function in raw lisp during the course of evaluation of that call. This is obvious if guard checking is on, because an error is signalled the first time its guard is violated; but in fact it is also true when guard checking is off. See guard-example for an example.
Guards and evaluation IV: functions having :program mode
Strictly speaking, functions in :program mode (see defun-mode)
do not have definitions in the ACL2 logic. So what does it mean to
evaluate calls of such functions in ACL2? Our decision is to treat
:program functions exactly as we treat :logic functions whose guards
have been verified, except that when there is a guard violation we
signal an error regardless of whether guard checking is currently on
or off. Note that when the guard of a function in :logic mode is
violated, there is still a value that the ACL2 logic proves is equal
to the given call. But the same cannot be said for a function in
:program mode, so we really have no choice but to signal an error
when there is a guard violation for such a function.
To summarize: as with :logic functions, when a guard has been
satisfied on a call of a function with :program mode, no subsidiary
guard checking will be done.
Consider the same example foo as above, but where foo is
submitted in :program mode. Then even with guard checking off,
top-level calls of foo will signal a guard violation when the
arguments do not satisfy the guard of foo, e.g., (foo 7).
Notice that by treating functions in :program mode like functions
whose guards have been verified, we are using raw lisp to compute
their values when their guards are met. We do not check guards any
further once raw lisp is invoked. This can lead to hard lisp errors
if the guards are not appropriate, as illustrated below.
ACL2 >:program
ACL2 p>(defun foo (x)
(declare (xargs :guard t))
(cons 1 (cdr x)))
Summary
Form: ( DEFUN FOO ...)
Rules: NIL
Warnings: None
Time: 0.02 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.02)
FOO
ACL2 p>(foo 3)
Error: 3 is not of type LIST.
Fast links are on: do (use-fast-links nil) for debugging
Error signalled by CDR.
Broken at COND. Type :H for Help.
ACL2>>
See defun-mode-caveat.Guards and evaluation V: efficiency issues
We have seen that by verifying the guards for a :logic function, we
arrange that raw lisp is used for evaluation of calls of such
functions when the arguments satisfy its guard.
This has several apparent advantages over the checking of guards as
we go. First, the savings is magnified as your system of functions
gets deeper: the guard is checked upon the top-level entry to your
system and then raw Common Lisp does all the computing. Second, if
the raw Common Lisp is compiled, enormous speed-ups are possible.
Third, if your Common Lisp or its compiler does such optimizations
as tail-recursion removal, raw Common Lisp may be able to
compute your functions on input much ``bigger'' than ACL2 can.
The first of these advantages is quite important if you have complicated guards. However, the other two advantages are probably not very important, as we now explain.
When a function is defined in :logic mode, its defun is
executed in raw Common Lisp. (We might call this the ``primary''
raw lisp definition of the function.) However, a corresponding
``logic definition'' is also executed. The ``logic definition'' is
a defun in raw lisp that checks guards at runtime and escapes to
the primary raw lisp definition if the guard holds of the arguments
and the function has already had its guards verified. Otherwise the
logic definition executes the body of the function by calling the
logic definitions of each subroutine. Now it is true that
compilation generally speeds up execution enormously. However, the
:comp command (see comp) compiles both of the raw lisp
definitions associated with a :logic function. Also, we have
attempted to arrange that for every tail recursion removal done on
the actual defun, a corresonding tail recursion removal is done
on the ``logic definition.''
We believe that in most cases, the logic definition executes almost as fast as the primary raw lisp definition, at least if the evaluation of the guards is fast. So, the main advantage of guard verification is probably that it lets you know that the function may be executed safely in raw lisp, returning the value predicted by the ACL2 logic, whenever its arguments satisfy its guard. We envision the development of systems of applicative lisp functions that have been developed and reasoned about using ACL2 but which are intended for evaluation in raw Common Lisp (perhaps with only a small ``core'' of ACL2 loaded), so this advantage of guard verification is important.
Nevertheless, guard verification might be important for optimal
efficiency when the functions make use of type declarations. For
example, at this writing, the GCL implementation of Common Lisp can
often take great advantage of declare forms that assign small
integer types to formal parameters.
To continue the discussion of guards,
see guards-for-specification to read about the use of guards as
a specification device.
Major Section: GUARD
A use of guard verification that has nothing to do with efficiency is as a way to gain confidence in specifications. This use has the feel of ``types'' in many traditional programming languages, though guards allow much greater expressiveness than most systems of types (and unfortunately, as a result they are not syntactically checkable).
For more discussion of guards in general, see guard.
Suppose you have written a collection of function definitions that are intended to specify the behavior of some system. Perhaps certain functions are only intended to be called on certain sorts of inputs, so you attach guards to those functions in order to ``enforce'' that requirement. And then, you verify the guards for all those functions.
Then what have you gained, other than somewhat increased efficiency of execution (as explained above), which quite possibly isn't your main concern? You have gained the confidence that when evaluating any call of a (specification) function whose arguments satisfy that function's guard, all subsequent function calls during the course of evaluation will have this same property, that the arguments satisfy the guard of the calling function. In logical terms, we can say that the equality of the original call with the returned value is provable from weakened versions of the definitions, where each definitional axiom is replaced by an implication whose antecedent is the requirement that the arguments satisfy the guard and whose consequent is the original axiom. For example,
(defun foo (x) (declare (xargs :guard (consp x))) (cons 1 (cdr x)))originally generates the axiom
(equal (foo x)
(cons 1 (cdr x)))
but in fact, when evaluation involves no guard violation then the
following weaker axiom suffices in the justification of the
evaluation.
(implies (consp x)
(equal (foo x)
(cons 1 (cdr x))))
If you are following links to read this documentation as a hypertext
style document, then please see guard-miscellany. This
concludes our discussion of guards with miscellaneous remarks, and
also contains pointers to related topics.
Major Section: MISCELLANEOUS
Hide is actually the identity function: (hide x) = x for
all x. However, terms of the form (hide x) are ignored by the
ACL2 rewriter, except when explicit :expand hints are given
for such terms (see hints) or when rewrite rules explicitly
about hide are available. Hide terms are also ignored by the
induction heuristics.
Sometimes the ACL2 simplifier inserts hide terms into a proof
attempt out of the blue, as it were. Why and what can you do about
it? Suppose you have a constrained function, say constrained-fn, and
you define another function, say another-fn, in terms of it, as in:
(defun another-fn (x y z)
(if (big-hairy-test x y z)
(constrained-fn x y z)
t))
Suppose the term (another-fn 'a 'b 'c) arises in a proof. Since
the arguments are all constants, ACL2 will try to reduce such a term
to a constant by executing the definition of another-fn.
However, after a possibly extensive computation (because of
big-hairy-test) the execution fails because of the unevaluable
call of constrained-fn. To avoid subsequent attempts to evaluate
the term, ACL2 embeds it in a hide expression, i.e., rewrites it
to (hide (another-fn 'a 'b 'c)).
You might think this rarely occurs since all the arguments of
another-fn must be constants. You would be right except for one
special case: if another-fn takes no arguments, i.e., is a
constant function, then every call of it fits this case. Thus, if
you define a function of no arguments in terms of a constrained
function, you will often see (another-fn) rewrite to
(hide (another-fn)).
We do not hide the term if the executable counterpart of the
function is disabled -- because we do not try to evaluate it in the
first place. Thus, to prevent the insertion of a hide term into
the proof attempt, you can globally disable the executable
counterpart of the offending defined function, e.g.,
(in-theory (disable (:executable-counterpart another-fn))).
It is conceivable that you cannot afford to do this: perhaps some
calls of the offending function must be computed while others cannot
be. One way to handle this situation is to leave the executable
counterpart enabled, so that hide terms are introduced on the
calls that cannot be computed, but prove explicit :rewrite
rules for each of those hide terms. For example, suppose that in
the proof of some theorem, thm, it is necessary to leave the
executable counterpart of another-fn enabled but that the call
(another-fn 1 2 3) arises in the proof and cannot be computed.
Thus the proof attempt will introduce the term
(hide (another-fn 1 2 3)). Suppose that you can show that
(another-fn 1 2 3) is (contrained-fn 1 2 3) and that such
a step is necessary to the proof. Unfortunately, proving the rewrite
rule
(defthm thm-helper (equal (another-fn 1 2 3) (constrained-fn 1 2 3)))would not help the proof of thm because the target term is hidden inside the
hide. However,
(defthm thm-helper (equal (hide (another-fn 1 2 3)) (constrained-fn 1 2 3)))would be applied in the proof of thm and is the rule you should prove.
Now to prove thm-helper you need to use the two ``tricks'' which
have already been discussed. First, to eliminate the hide term
in the proof of thm-helper you should include the hint
:expand (hide (another-fn 1 2 3)). Second, to prevent the
hide term from being reintroduced when the system tries and fails
to evaluate (another-fn 1 2 3) you should include the hint
:in-theory (disable (:executable-counterpart another-fn)).
Thus, thm-helper will actually be:
(defthm thm-helper
(equal (hide (another-fn 1 2 3)) (constrained-fn 1 2 3))
:hints
(("Goal" :expand (hide (another-fn 1 2 3))
:in-theory (disable (:executable-counterpart another-fn)))))
See eviscerate-hide-terms for how to affect the printing of hide
terms.
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.