hide a term from the rewriter
Parent topic: MISCELLANEOUS Home
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). They are also ignored by the induction
heuristics.
See eviscerate-hide-terms for how to affect the printing of such terms.
advice to the theorem proving process
Parent topic: MISCELLANEOUS Home
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))
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 :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.
: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.
a convenient marker for use with rebuild
Parent topic: MISCELLANEOUS Home
Example Input File for Rebuild: (defun fn1 (x y) ...) (defthm lemma1 ...) (defthm lemma2 ...) (i-am-here) The following lemma won't go through. I started typing the hint but realized I need to prove a lemma first. See the failed proof attempt in foo.bar. I'm going to quit for the night now and resume tomorrow from home.(defthm lemma3 ... :hints (("Goal" :use (:instance ??? ...
By putting an (i-am-here) form at the ``frontier'' of an evolving
file of commands, you can use rebuild to load the file up to the
(i-am-here). I-am-here simply returns an ld error triple and any
form that ``causes an error'' will do the same job. Note that the
text of the file after the (i-am-here) need not be machine
readable.
when executable counterpart is enabled,
forced hypotheses are attacked immediately
Parent topic: MISCELLANEOUS Home
This function symbol is defined simply to provide a rune which can be enabled and disabled. Enabling
(:executable-counterpart immediate-force-modep)causes ACL2 to attack forced hypotheses immediately instead of delaying them to the next forcing round.
Example Hints
:in-theory (disable (:executable-counterpart immediate-force-modep))
; delay forced hyps to forcing round
:in-theory (enable (:executable-counterpart immediate-force-modep))
; split on forced hyps immediately
See force for background information. When a forced
hypothesis cannot be established a record is made of that fact and
the proof continues. When the proof succeeds a ``forcing round'' is
undertaken in which the system attempts to prove each of the forced
hypotheses explicitly. However, if the rune
(:executable-counterpart immediate-force-modep) is enabled at the
time the hypothesis is forced, then ACL2 does not delay the attempt
to prove that hypothesis but undertakes the attempt more or less
immediately.
select current package
Parent topic: MISCELLANEOUS Home
Example: (in-package "MY-PKG")whereGeneral Form: (in-package str)
str is a string that names an existing ACL2 package, i.e.,
one of the initial packages such as "KEYWORD" or "ACL2" or a
package introduced with defpkg. For a complete list of the known
packages created with defpkg, evaluate
(strip-cars (known-package-alist state)).See defpkg.
In-package forms can only be typed at the
top-level of the ACL2 loop and as the first form in a file being
loaded or compiled.
functions that are invisible to the loop-stopper algorithm
Parent topic: MISCELLANEOUS Home
Examples: ACL2 !>(invisible-fns-alist (w state)) ((binary-+ unary--) (binary-* unary-/) (unary-- unary--) (unary-/ unary-/))Among other things, the setting above has the effect of making
unary-- ``invisible'' for the purposes of applying permutative
:rewrite rules to binary-+ trees.
See set-invisible-fns-alist.
The notion of ``invisible functions'' has to do with the control
mechanism on permutative :rewrite rules. See loop-stopper for
a detailed discussion of the control mechanism.
See set-invisible-fns-alist for a discussion of how to set the
invisible functions alist.
how keyword commands are processed
Parent topic: MISCELLANEOUS Home
Examples: user type-in form evaluated :pc 5 (ACL2::PC '5) :pcs app rev (ACL2::PCS 'app 'rev) :length (1 2 3) (ACL2::LENGTH '(1 2 3))
When a keyword, :key, is read as a command, ACL2 determines whether
the symbol with the same name in the "ACL2" package, acl2::key, is
a function or simple macro of n arguments. If so, ACL2 reads n more
objects, obj1, ..., objn, and then acts as though it had read the
following form (for a given key):
(ACL2::key 'obj1 ... 'objn)Thus, by using the keyword command hack you avoid typing the parentheses, the
"ACL2" package name, and the quotation marks.
Note the generality of this hack. Almost any function or macro in
the "ACL2" package can be so invoked, not just ``commands.''
Indeed, there is no such thing as a distinguished class of commands.
The one caveat is that the keyword hack can be used to invoke a
macro only if that macro has a simple argument list -- one
containing no lambda keywords (such as &rest), since they complicate
or render impossible the task of deciding how many objects to read.
Users may take advantage of the keyword command hack by defining
functions and macros in the "ACL2" package.
determines ld's response to an error
Parent topic: MISCELLANEOUS Home
Ld-error-action is an ld special (see ld). The accessor is
(ld-error-action state) and the updater is
(set-ld-error-action val state). Ld-error-action must be
:continue, :return, or :error. The initial value of
ld-error-action is :continue, which means that the top-level
ACL2 command loop will not exit when an error is caused by
user-typein. But the default value for ld-error-action on
calls of ld is :return.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-error-action is one of them. If, while ld-error-triples is t, a
form evaluates to three results, the first of which is non-nil and
the third of which is state, an error is said to have occurred. If
an error occurs, ld's action depends on ld-error-action. If it is
:continue, ld just continues processing the forms in standard-oi.
If it is :return, ld stops and returns as though it had emptied the
channel. If it is :error, ld stops and returns, signalling an error
to its caller.
determines whether a form caused an error during ld
Parent topic: MISCELLANEOUS Home
Ld-error-triples is an ld special (see ld). The accessor is
(ld-error-triples state) and the updater is
(set-ld-error-triples val state). Ld-error-triples must be
either t or nil. The initial value of ld-error-triples is
t.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-error-triples is one of them. If this variable has the value t
then when a form evaluates to 3 values, the first of which is
non-nil and the third of which is state, an error is deemed to have
occurred. When an error occurs in evaluating a form, ld rolls back
the ACL2 world to the configuration it had at the conclusion of the
last error-free form. Then ld takes the action determined by
ld-error-action.
determines whether ld suppresses details when printing
Parent topic: MISCELLANEOUS Home
Ld-evisc-tuple is an ld special (see ld). The accessor is
(ld-evisc-tuple state) and the updater is
(set-ld-evisc-tuple val state). Ld-evisc-tuple must be either
nil or a list of the form
(alist nil nil print-level print-length hiding-cars)where
alist is an alist that pairs objects to strings, print-level
and print-length are either nil or non-negative integers, and
hiding-cars is a list of symbols. The initial value of
ld-evisc-tuple is nil.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-evisc-tuple is one of them. Ld may print the forms it is
evaluating and/or the results of evaluation. If the value of
ld-evisc-tuple is a list as shown above, then ld ``eviscerates'' the
objects it prints before printing them. To ``eviscerate'' an object
we replace certain substructures within it by strings which are
printed in their stead. Print-level and print-length, above, are
used as described in CLTL (pp 372) to replace those substructures
deeper than print-level by ``#'' and those longer than print-length
by ``...''. Alist is used to replace any substructure occuring as a
key in alist by the corresponding string. Finally, any consp x
that starts with one of the symbols in hiding-cars is printed as
<hidden>.
allows the abbreviation of some keyword commands
Parent topic: MISCELLANEOUS Home
Example:
(set-ld-keyword-aliases '((:q 0 q-fn)
(:e 0 exit-acl2-macro))
state)
Ld-keyword-aliases is an ld special (see ld). The accessor
is (ld-keyword-aliases state) and the updater is
(set-ld-keyword-aliases val state). Ld-keyword-aliases must be an
alist, each element of which is of the form (:keyword n fn), where
:keyword is a keyword, n is a nonnegative integer, and fn is a
function symbol of arity n, a macro symbol, or a lambda expression
of arity n. When keyword is typed as an ld command, n more forms
are read, x1, ..., xn, and the form (fn 'x1 ... 'xn) is then
evaluated. The initial value of ld-keyword-aliases is nil.
In the example above, :q has been redefined to have the effect of
executing (q-fn), so for example if you define
(defmacro q-fn () '(er soft 'q "You un-bound :q and now we have a soft error."))then
:q will cause an error, and if you define
(defmacro exit-acl2-macro () '(exit-ld state))then
:e will cause the effect (it so happens) that :q normally
has. If you prefer :e to :q for exiting the ACL2 loop, you might
even want to put such definitions of q-fn and exit-acl2-macro
together with the set-ld-keyword-aliases form above in your
"acl2-customization.lisp" file; see acl2-customization.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-keyword-aliases is one of them. Ld-keyword-aliases affects how
keyword commands are parsed. Generally speaking, ld's command
interpreter reads ``:fn x1 ... xn'' as ``(fn 'x1 ... 'xn)'' when :fn
is a keyword and fn is the name of an n-ary function. But this
parse is overridden, as described above, for the keywords bound in
ld-keyword-aliases.
determines whether and how ld prints the result of evaluation
Parent topic: MISCELLANEOUS Home
Ld-post-eval-print is an ld special (see ld). The accessor is
(ld-post-eval-print state) and the updater is
(set-ld-post-eval-print val state). Ld-post-eval-print must be
either t, nil, or :command-conventions. The initial value of
ld-post-eval-print is :command-conventions.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-post-eval-print is one of them. If this global variable is t, ld
prints the result. In the case of a form that produces multiple
values, ld prints the list containing them all (which, logically
speaking, is what the form returned). If ld-post-eval-print is nil,
ld does not print the values. This is most useful when ld is used
to load a previously processed file.
Finally, if ld-post-eval-print is :command-conventions then ld
prints the result but treats ``error triples'' specially. An
``error triple'' is a result, (mv erp val state), that consists of
three values, the third of which is state. Many ACL2 functions use
such triples to signal errors. The convention is that if erp (the
first value) is nil, then the function is returning val (the second
value) as its conventional single result and possibly side-effecting
state (as with some output). If erp is t, then an error has been
caused, val is irrelevant and the error message has been printed in
the returned state. Example ACL2 functions that follow this
convention include defun and in-package. If such ``error
producing'' functions are evaluated while ld-post-eval-print is
set to t, then you would see them producing lists of length 3. This
is disconcerting to users accustomed to Common Lisp (where these
functions produce single results but sometimes cause errors or
side-effect state).
When ld-post-eval-print is :command-conventions and a form produces
an error triple (mv erp val state) as its value, ld prints nothing
if erp is non-nil and otherwise ld prints just val. Because it is a
misrepresentation to suggest that just one result was returned, ld
prints the value of the global variable 'triple-print-prefix before
printing val. 'triple-print-prefix is initially " ", which means
that when non-erroneous error triples are being abbreviated to val,
val appears one space off the left margin instead of on the margin.
In addition, when ld-post-eval-print is :command-conventions and the
value component of an error triple is the keyword :invisible then ld
prints nothing. This is the way certain commands (e.g., :pc) appear
to return no value.
By printing nothing when an error has been signalled, ld makes it
appear that the error (whose message has already appeared in state)
has ``thrown'' the computation back to load without returning a
value. By printing just val otherwise, we suppress the fact that
state has possibly been changed.