Major Section: MISCELLANEOUS
The ACL2 state object is used extensively in programming the ACL2 system, and has been used in other ACL2 programs as well. However, most users, especially those interested in specification and verification (as opposed to programming per se), need not be aware of the role of the state object in ACL2, and will not write functions that use it explicitly. We say more about this point at the end of this documentation topic.
The ACL2 state object is an example of a single-threaded object or
stobj. ACL2 allows the user to define new single-threaded objects.
Generally, the ACL2 may need to access the ACL2 state but should not
(cannot) change it except via a certain set of approved functions
defthm. If you need a state-like object
to which you have complete rights, you may want a stobj.
Key to the idea of our
state is the notion of single-threadedness.
This is explained in see stobj. The upshot of it is that
is a variable symbol with severe restrictions on its use, so that it
can be passed into only certain functions in certain slots, and must be
returned by those functions that ``modify'' it. Henceforth, we do not
discuss single-threaded objects in general (which the user can introduce
defstobj) but one in particular, namely ACL2's
The global table is perhaps the most visible portion of the state
object. Using the interface functions
assign, a user
may bind global variables to the results of function evaluations
(much as an Nqthm user exploits the Nqthm utility
See @, and see assign.
ACL2 supports several facilities of a truly von Neumannesque state
machine character, including file io and global variables.
Logically speaking, the state is a true list of the 14 components
described below. There is a ``current'' state object at the
top-level of the ACL2 command loop. This object is understood to be
the value of what would otherwise be the free variable
appearing in top-level input. When any command returns a state
object as one of its values, that object becomes the new current
state. But ACL2 provides von Neumann style speed for state
operations by maintaining only one physical (as opposed to logical)
state object. Operations on the state are in fact destructive.
This implementation does not violate the applicative semantics
because we enforce certain draconian syntactic rules regarding the
use of state objects. For example, one cannot ``hold on'' to an old
state, access the components of a state arbitrarily, or ``modify'' a
state object without passing it on to subsequent state-sensitive
Every routine that uses the state facilities (e.g. does io, or calls
a routine that does io), must be passed a ``state object.'' And a
routine must return a state object if the routine modifies the state
in any way. Rigid syntactic rules governing the use of state
objects are enforced by the function
translate, through which all
ACL2 user input first passes. State objects can only be ``held'' in
the formal parameter
state, never in any other formal parameter and
never in any structure (excepting a multiple-values return list
field which is always a state object). State objects can only be
accessed with the primitives we specifically permit. Thus, for
example, one cannot ask, in code to be executed, for the length of
state or the
state. In the statement and proof of theorems,
there are no syntactic rules prohibiting arbitrary treatment of
Logically speaking, a state object is a true list whose members are as follows:
Open-input-channels, an alist with keys that are symbols in package
"ACL2-INPUT-CHANNEL". The value (
cdr) of each pair has the form
((:header type file-name open-time) . elements), where
typeis one of
elementsis a list of things of the corresponding
type, i.e. characters, integers of type
(mod 255), or lisp objects in our theory.
File-nameis a string.
Open-timeis an integer. See io.
Open-output-channels, an alist with keys that are symbols in package
"ACL2-OUTPUT-CHANNEL". The value of a pair has the form
((:header type file-name open-time) . current-contents). See io.
Global-table, an alist associating symbols (to be used as ``global variables'') with values. See @, and see assign.
T-stack, a list of arbitrary objects accessed and changed by the functions
32-bit-integer-stack, a list of arbitrary 32-bit-integers accessed and changed by the functions
Big-clock-entry, an integer, that is used logically to bound the amount of effort spent to evaluate a quoted form.
Idates, a list of dates and times, used to implement the function
print-current-idate, which prints the date and time.
Run-times, a list of integers, used to implement the functions that let ACL2 report how much time was used, but inaccessible to the user.
File-clock, an integer that is increased on every file opening and closing and used to maintain the consistency of the
Readable-files, an alist whose keys have the form
(string type time), where
stringis a file name and
timeis an integer. The value associated with such a key is a list of characters, bytes, or objects, according to
timefield is used in the following way: when it comes time to open a file for input, we will only look for a file of the specified name and
typewhose time field is that of
file-clock. This permits us to have a ``probe-file'' aspect to
open-file: one can ask for a file, find it does not exist, but come back later and find that it does now exist.
Written-files, an alist whose keys have the form
(string type time1 time2), where
stringis a file name,
typeis one of
time2correspond to the
file-clocktime at which the channel for the file was opened and closed. This field is write-only; the only operation that affects this field is
conses a new entry on the front.
Read-files, a list of the form
(string type time1 time2), where
stringis a file name and
time2were the times at which the file was opened for reading and closed. This field is write only.
Writeable-files, an alist whose keys have the form
(string type time). To open a file for output, we require that the name, type, and time be on this list.
List-all-package-names-lst, a list of
true-listps. Roughly speaking, the
carof this list is the list of all package names known to this Common Lisp right now and the
cdrof this list is the value of this
statevariable after you look at its
car. The function,
list-all-package-names, which takes the state as an argument, returns the
cdrs the list (returning a new state too). This essentially gives ACL2 access to what is provided by CLTL's
Defpkguses this feature to insure that the about-to-be-created package is new in this lisp. Thus, for example, in
akclit is impossible to create the package
defpkgbecause it is on the list, while in Lucid that package name is not initially on the list.
We recommend avoiding the use of the state object when writing ACL2 code intended to be used as a formal model of some system, for several reasons. First, the state object is complicated and contains many components that are oriented toward implementation and are likely to be irrelevant to the model in question. Second, there is currently not much support for reasoning about ACL2 functions that manipulate the state object, beyond their logical definitions. Third, the documentation about state is not as complete as one might wish.
User-defined single-threaded objects offer the speed of
giving the user complete access to all the fields. See stobj.
Major Section: MISCELLANEOUS
Major Section: MISCELLANEOUS
Subtleties arise when one of the ``constrained'' functions,
introduced in the signature of an
encapsulate event, is
involved in the termination argument for a non-local recursively
g, in that
encapsulate. During the
processing of the encapsulated events,
f is locally defined to
be some witness function,
f'. Properties of
explicitly proved and exported from the encapsulate as the
constraints on the undefined function
f. But if
f is used
in a recursive
g defined within the encapsulate, then the
termination proof for
g may use properties of
f' -- the
witness -- that are not explicitly set forth in the constraints
g are said be ``subversive'' because if naively
treated they give rise to unsound induction schemes or (via
functional instantiation) recurrence equations that are impossible
to satisfy. We illustrate what could go wrong below.
Subversive recursions are not banned outright. Instead, they are
treated as part of the constraint. That is, in the case above, the
definitional equation for
g becomes one of the constraints on
f. This is generally a severe restriction on future functional
f. In addition, ACL2 removes from its knowledge
g any suggestions about legal inductions to ``unwind'' its
What should you do? Often, the simplest response is to move the
offending recursive definition, e.g.,
g, out of the encapsulate.
That is, introduce
f by constraint and then define
g as an
``independent'' event. You may need to constrain ``additional''
f in order to admit
g, e.g., constrain it to
reduce some ordinal measure. However, by separating the
f from the admission of
g you will clearly
identify the necessary constraints on
f will be simpler, and
g will be a useful
function which suggests inductions to the theorem prover.
Note that the functions introduced in the signature should not even occur ancestrally in the termination proofs for non-local recursive functions in the encapsulate. That is, the constrained functions of an encapsulate should not be reachable in the dependency graph of the functions used in the termination arguments of recursive functions in encapsulate. If they are reachable, their definitions become part of the constraints.
The following event illustrates the problem posed by subversive recursions.
(encapsulate (((f *) => *)) (local (defun f (x) (cdr x))) (defun g (x) (if (consp x) (not (g (f x))) t)))Suppose, contrary to how ACL2 works, that the encapsulate above were to introduce no constraints on
fon the bogus grounds that the only use of
fin the encapsulate is in an admissible function. We discuss the plausibility of this bogus argument in a moment.
Then it would be possible to prove the theorem:
(defthm f-not-identity (not (equal (f '(a . b)) '(a . b))) :rule-classes nil :hints (("Goal" :use (:instance g (x '(a . b))))))simply by observing that if
(f '(a . b))were
'(a . b), then
(g '(a . b))would be
(not (g '(a . b))), which is impossible.
But then we could functionally instantiate
f by the identity function, to prove
nil! This is bad.
(defthm bad nil :rule-classes nil :hints (("Goal" :use (:functional-instance f-not-identity (f identity)))))This sequence of events was legal in versions of ACL2 prior to Version 1.5. When we realized the problem we took steps to make it illegal. However, our steps were insufficient and it was possible to sneak in a subversive function (via mutual recursion) as late as Version 2.3.
We now turn to the plausibility of the bogus argument above. Why might
one even be tempted to think that the definition of
g above poses
no constraint on
f? Here is a very similar encapsulate.
(encapsulate (((f *) => *)) (local (defun f (x) (cdr x))) (defun map (x) (if (consp x) (cons (f x) (map (cdr x))) nil)))Here
mapplays the role of
mapcalls the constrained function
maptruly does not constrain
f. In particular, the definition of
mapcould be moved ``out'' of the encapsulate so that
mapis introduced afterwards. The difference between
gis that the constrained function plays no role in the termination argument for the one but does for the other.
As a ``user-friendly'' gesture, ACL2 implicitly moves
functions out of encapsulations; logically speaking, they are
introduced after the encapsulation. This simplifies the constraint.
This is done only for ``top-level'' encapsulations. When an
encapsulate containing a non-empty signature list is
embedded in another
encapsulate with a non-empty signature list,
no attempt is made to move
map-like functions out. The user is
advised, via the ``infected'' warning, to phrase the encapsulation
in the simplest way possible.
The lingering bug between Versions 1.5 and 2.3 mentioned above was
due to our failure to detect the
g-like nature of some functions
when they were defined in mutually recursively cliques with other
functions. The singly recursive case was recognized. The bug arose
because our detection ``algorithm'' was based on the ``suggested
inductions'' left behind by successful definitions. We failed to
recall that mutually-recursive definitions do not, as of this
writing, make any suggestions about inductions and so did not leave
any traces of their subversive natures.
Major Section: MISCELLANEOUS
For the details of ACL2 syntax, see CLTL. For examples of ACL2
pe to print some of the ACL2 system code. For example:
:pe assoc-equal :pe dumb-occur :pe fn-var-count :pe add-linear-variable-to-alist
There is no comprehensive description of the ACL2 syntax yet, except
that found in CLTL. Also see term.
Major Section: MISCELLANEOUS
Example: Consider the :REWRITE rule created fromThe
(IMPLIES (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))) (EQUAL (LXD X) (LXD (NORM X)))).
syntaxphypothesis in this rule will allow the rule to be applied to
(lxd (trn a b))but will not allow it to be applied to
(lxd (norm a)).
General Form: (SYNTAXP test)may be used as the nth hypothesis in a
(implies (and hyp1 ... hypn ... hypk) (equiv lhs rhs))provided
testis a term,
testcontains at least one variable, and every variable occuring freely in
testoccurs freely in
lhsor in some
syntaxpis a function of one argument;
tand so may be added as a vacuous hypothesis. However, the test ``inside'' the
syntaxpform is actually treated as a meta-level proposition about the proposed instantiation of the rule's variables and that proposition must evaluate to true (non-
nil) to ``establish'' the
We illustrate this by slightly elaborating the example given above.
rewrite rule whose
(IMPLIES (AND (RATIONALP X) (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM))))) (EQUAL (LXD X) (LXD (NORM X))))How is this rule applied to
(lxd (trn a b))? First, we form a substitution that instantiates the left-hand side of the conclusion of the rule so that it is identical to the target term. In the present case, the substitution replaces
(trn a b). Then we backchain to establish the hypotheses, in order. Ordinarily this means that we instantiate each hypothesis with our substitution and then attempt to rewrite the resulting instance to true. Of course, most users are aware of some exceptions to this general rule. For example, if a hypothesis contains a ``free-variable'' -- one not bound by the current substitution -- we attempt to extend the substitution by searching for an instance of the hypothesis among known truths.
Forced hypotheses are another exception to the general rule of how hypotheses are relieved. Hypotheses marked with
syntaxp, as in
(syntaxp test), are also exceptions. Instead of instantiating the hypothesis and trying to establish it, we evaluate
testin an environment in which its variable symbols are bound to the quotations of the terms to which those variables are bound in the instantiating substitution. In the case in point, we evaluate the test
(NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))in an environment where
xis bound to
'(trn a b), i.e., the list of length three whose
caris the symbol
'trn. Thus, the test returns
caris not the symbol
'norm. When the
syntaxptest evaluates to
t, we consider the
syntaxphypothesis to have been established; this is sound because
test. If the test evaluates to
nil(or fails to evaluate because of guard violations) we act as though we cannot establish the hypothesis and abandon the attempt to apply the rule; it is always sound to give up.
Note that the test of a
syntaxp hypothesis does not deal with the
meaning or semantics or values of the terms but with their syntactic
forms. In the example above, the
syntaxp hypothesis allows the rule
to be applied to every target of the form
(lxd u), provided
(rationalp u) can be established and
u is not of the form
Observe that without this syntactic restriction the rule above could
loop producing a sequence of increasingly complex targets
(lxd (norm a)),
(lxd (norm (norm a))), etc. An intuitive reading of
the rule might be ``
norm the argument of
lxd (when it is
unless it has already been
Another common syntactic restriction is
(SYNTAXP (AND (CONSP X) (EQ (CAR X) 'QUOTE))).A rule with such a hypothesis can be applied only if
xis bound to a specific constant. Thus, if
23(which is actually represented internally as
(quote 23)), the test evaluates to
t; but if
(+ 11 12)it evaluates to
(car x)is the symbol
+). It is often desirable to delay the application of a rule until certain subterms are in some kind of normal form so that the application doesn't produce excessive case splits.
Major Section: MISCELLANEOUS
Examples of Terms: (cond ((caar x) (cons t x)) (t 0)) ; an untranslated term
(if (car (car x)) (cons 't x) '0) ; a translated term
(car (cons x y) 'nil v) ; a pseudo-term
In traditional first-order predicate calculus a ``term'' is a syntactic entity denoting some object in the universe of individuals. Often, for example, the syntactic characterization of a term is that it is either a variable symbol or the application of a function symbol to the appropriate number of argument terms. Traditionally, ``atomic formulas'' are built from terms with predicate symbols such as ``equal'' and ``member;'' ``formulas'' are then built from atomic formulas with propositional ``operators'' like ``not,'' ``and,'' and ``implies.'' Theorems are formulas. Theorems are ``valid'' in the sense that the value of a theorem is true, in any model of the axioms and under all possible assignments of individuals to variables.
However, in ACL2, terms are used in place of both atomic formulas
and formulas. ACL2 does not have predicate symbols or propositional
operators as distinguished syntactic entities. The ACL2 universe of
individuals includes a ``true'' object (denoted by
t) and a
``false'' object (denoted by
nil), predicates and propositional
operators are functions that return these objects. Theorems in ACL2
are terms and the ``validity'' of a term means that, under no
assignment to the variables does the term evaluate to
We use the word ``term'' in ACL2 in three distinct senses. We will speak of ``translated'' terms, ``untranslated'' terms, and ``pseudo-'' terms.
Translated Terms: The Strict Sense and Internal Form
In its most strict sense, a ``term'' is either a legal variable
symbol, a quoted constant, or the application of an n-ary function
symbol or closed
lambda expression to a true list of n terms.
The legal variable symbols are symbols other than
which are not in the keyword package, do not start with ampersand,
do not start and end with asterisks, and if in the main Lisp
package, do not violate an appropriate restriction (see name).
Quoted constants are expressions of the form
(quote x), where
any ACL2 object. Such expressions may also be written
lambda expressions are expressions of the form
(lambda (v1 ... vn) body) where the
vi are distinct legal
body is a term, and the only free variables in
body are among the
termp, which takes two arguments, an alleged term
a logical world
w (see world), recognizes terms of a given
extension of the logic.
Termp is defined in
Its definition may be inspected with
termp for a complete
specification of what we mean by ``term'' in the most strict sense.
Most ACL2 term-processing functions deal with terms in this strict
sense and use
termp as a guard. That is, the ``internal form''
of a term satisfies
termp, the strict sense of the word ``term.''
Untranslated Terms: What the User Types
While terms in the strict sense are easy to explore (because their structure is so regular and simple) they can be cumbersome to type. Thus, ACL2 supports a more sugary syntax that includes uses of macros and constant symbols. Very roughly speaking, macros are functions that produce terms as their results. Constants are symbols that are associated with quoted objects. Terms in this sugary syntax are ``translated'' to terms in the strict sense; the sugary syntax is more often called ``untranslated.'' Roughly speaking, translation just implements macroexpansion, the replacement of constant symbols by their quoted values, and the checking of all the rules governing the strict sense of ``term.''
More precisely, macro symbols are as described in the documentation
defmacro. A macro,
mac, can be thought of as a function,
mac-fn, from ACL2 objects to an ACL2 object to be treated as an
untranslated term. For example,
caar is defined as a macro symbol;
the associated macro function maps the object
x into the object
(car (car x)). A macro form is a ``call'' of a macro symbol,
i.e., a list whose
car is the macro symbol and whose
cdr is an
arbitrary true list of objects, used as a term. Macroexpansion is
the process of replacing in an untranslated term every occurrence of
a macro form by the result of applying the macro function to the
appropriate arguments. The ``appropriate'' arguments are determined
by the exact form of the definition of the macro; macros support
positional, keyword, optional and other kinds of arguments.
In addition to macroexpansion and constant symbol dereferencing,
translation implements the mapping of
let* forms into
lambda expressions and closes
containing free variables. Thus, the translation of
(let ((x (1+ i))) (cons x k))can be seen as a two-step process that first produces
((lambda (x) (cons x k)) (1+ i))and then
((lambda (x k) (cons x k)) (1+ i) k) .Observe that the body of the
letand of the first
lambdaexpression contains a free
kwhich is finally bound and passed into the second
When we say, of an event-level function such as
that some argument ``must be a term'' we mean an untranslated term.
The event functions translate their term-like arguments.
To better understand the mapping between untranslated terms and
translated terms it is convenient to use the keyword command
to see examples of translations. See trans and also
Pseudo-Terms: A Common Guard for Metafunctions
termp is defined in
program mode, it cannot be used
effectively in conjectures to be proved. Furthermore, from the
perspective of merely guarding a term processing function,
often checks more than is required. Finally, because
requires the logical world as one of its arguments it is impossible
termp as a guard in places where the logical world is not
itself one of the arguments.
For these reasons we support the idea of ``pseudo-terms.'' A
pseudo-term is either a symbol (but not necessarily one having the
syntax of a legal variable symbol), a true list beginning with
(but not necessarily well-formed), or the ``application of'' a
symbol or pseudo
lambda expression to a true list of
pseudo-terms. A pseudo
lambda expression is an expression of the
(lambda (v1 ... vn) body) where the
vi are all symbols
body is a pseudo-term.
Pseudo-terms are recognized by the unary function
(termp x w) is true, then
(pseudo-termp x) is true. However, if
fails to be a (strict) term it may nevertheless still be a
pseudo-term. For example,
(car a b) is not a term, because
applied to the wrong number of arguments, but it is a pseudo-term.
The structures recognized by
pseudo-termp can be recursively
explored with the same simplicity that terms can be. In particular,
x is not a
variablep or an
(ffn-symb x) is the
lambda expression) and
(fargs x) is the list of
argument pseudo-terms. A metafunction may use
pseudo-termp as the
Major Section: MISCELLANEOUS
ACL2 must occasionally choose which of two terms is syntactically smaller. The need for such a choice arises, for example, when using equality hypotheses in conjectures (the smaller term is substituted for the larger elsewhere in the formula), in stopping loops in permutative rewrite rules (see loop-stopper), and in choosing the order in which to try to cancel the addends in linear arithmetic inequalities. When this notion of syntactic size is needed, ACL2 uses ``term order.'' Popularly speaking, term order is just a lexicographic ordering on terms. But the situation is actually more complicated.
We define term order only with respect to terms in translated form. See trans.
Term1 comes before
term2 in the term order iff
(a) the number of variable occurrences in
term1is less than that in
(b) the numbers of variable occurrences in the two terms are equal but the number of function applications in
term1is less than that in
(c) the numbers of variable occurrences in the two terms are equal, the numbers of functions applications in the two terms are equal, and
term2in a certain lexicographic ordering based their structure as Lisp objects.
term-order, when applied to the translations of two ACL2 terms, returns
tiff the first is ``less than or equal'' to the second in the term order.
By ``number of variable occurrences'' we do not mean ``number of
distinct variables'' but ``number of times a variable symbol is
(cons x x) has two variable occurrences, not one.
Thus, perhaps counterintuitively, a large term that contains only
one variable occurrence, e.g.,
(standard-char-p (car (reverse x)))
(cons x x) in the term order.
Since constants contain no variable occurrences and non-constant expressions must contain at least one variable occurrence, constants come before non-constants in the term order, no matter how large the constants. For example, the list constant
'(monday tuesday wednesday thursday friday)comes before
xin the term order. Because term order is involved in the control of permutative rewrite rules and used to shift smaller terms to the left, a set of permutative rules designed to allow the permutation of any two tips in a tree representing the nested application of some function will always move the constants into the left-most tips. Thus,
(+ x 3 (car (reverse klst)) (dx i j)) ,which in translated form is
(binary-+ x (binary-+ '3 (binary-+ (dx i j) (car (reverse klst))))),will be permuted under the built-in commutativity rules to
(binary-+ '3 (binary-+ x (binary-+ (car (reverse klst)) (dx i j))))or
(+ 3 x (car (reverse klst)) (dx i j)).Clearly, two constants are ordered using cases (b) and (c) of term order, since they each contain 0 variable occurrences. This raises the question ``How many function applications are in a constant?'' Because we regard the number of function applications as a more fundamental measure of the size of a constant than lexicographic considerations, we decided that for the purposes of term order, constants would be seen as being built by primitive constructor functions. These constructor functions are not actually defined in ACL2 but merely imagined for the purposes of term order. We here use suggestive names for these imagined functions, ignoring entirely the prior use of these names within ACL2.
The constant function
0. Positive integers are
(z) by the successor function,
(s (s (z))) and contains three function applications.
contains one hundred and one applications. Negative integers are
constructed from their positive counterparts by
(- (s (s (z)))) and has four applications. Ratios are
constructed by the dyadic function
(/ (- (s (z))) (s (s (z))))and contains seven applications. Complex rationals are similarly constructed from rationals. All character objects are considered primitive and are constructed by constant functions of the same name. Thus
#\bboth contain one application. Strings are built from the empty string,
(o)by the ``string-cons'' function written
(cs (#\a) (cs (#\b) (o)))and contains five applications. Symbols are obtained from strings by ``packing'' the
symbol-namewith the unary function
(p (cs (#\a) (cs (#\b) (o))))and has six applications. Note that packages are here ignored and thus
'my-package::abeach contain just six applications. Finally, conses are built with
cons, as usual. So
'(1 . 2)is
(cons '1 '2)and contains six applications, since
'1contains two and
'2contains three. This, for better or worse, answers the question ``How many function applications are in a constant?''
Two terms with the same numbers of variable occurrences and function
applications are ordered by lexicographic means, based on their
structures. In the lexicographic ordering, two atoms are ordered
``alphabetically'' as described below, an atom and a cons are
ordered so that the atom comes first, and two conses are ordered so
that the one with the recursively smaller
car comes first, with the
cdrs being compared only if the
cars are equal. Thus, if two terms
(member ...) and
(reverse ...) contain the same numbers of variable
occurrences and function applications, then the
member term is first
in the term order because
member comes before
reverse in the term
order (which is here reduced to alphabetic ordering).
It remains only to define what we mean by the alphabetic ordering on
Lisp atoms. Within a single type, numbers are compared
arithmetically, characters are compared via their (char) codes, and
strings and symbols are compared with the conventional alphabetic
ordering on sequences of characters. Across types, numbers come
before characters, characters before strings, and strings before
Major Section: MISCELLANEOUS
Many users develop proof scripts in an Emacs buffer and submit one
event at a time to the theorem prover running in a
The script buffer is logically divided into two regions: the events
that have been accepted by the theorem prover and those that have
not yet been accepted. An imaginary ``barrier'' divides these two
regions. The region above the barrier describes the state of the
*shell* buffer (and ACL2's logical world). The region below the
barrier is the ``to do'' list.
We usually start a proof project by typing the key lemmas, and main goal into the to do list. Definitions are here just regarded as theorems to prove (i.e., the measure conjectures). Then we follow ``The Method.''
(1) Think about the proof of the first theorem in the to do list. Structure the proof either as an induction followed by simplification or just simplification. Have the necessary lemmas been proved? That is, are the necessary lemmas in the done list already? If so, proceed to Step 2. Otherwise, add the necessary lemmas at the front of the to do list and repeat Step 1.
(2) Call the theorem prover on the first theorem in the to do list and let the output stream into the *shell* buffer. Abort the proof if it runs more than a few seconds.
(3) If the theorem prover succeeded, advance the barrier past the successful command and go to Step 1.
(4) Otherwise, inspect the failed proof attempt, starting from the beginning, not the end. Basically you should look for the first place the proof attempt deviates from your imagined proof. If your imagined proof was inductive, inspect the induction scheme used by ACL2. If that is ok, then find the first subsequent subgoal that is stable under simplification and think about why it was not proved by the simplifier. If your imagined proof was not inductive, then think about the first subgoal stable under simplification, as above. Modify the script appropriately. It usually means adding lemmas to the to do list, just in front of the theorem just tried. It could mean adding hints to the current theorem. In any case, after the modifications go to Step 1.
We do not seriously suggest that this or any rotely applied algorithm will let you drive ACL2 to difficult proofs. Indeed, to remind you of this we call this ``The Method'' rather than ``the method.'' That is, we are aware of the somewhat pretentious nature of any such advice. But these remarks have helped many users approach ACL2 in a constructive and disciplined way.
We say much more about The Method in the ACL2 book. See the home page.
Learning to read failed proofs is a useful skill. There are several kinds of ``checkpoints'' in a proof: (1) a formula to which induction is being (or would be) applied, (2) the first formula stable under simplification, (3) a formula that is possibly generalized, either by cross-fertilizing with and throwing away an equivalence hypothesis or by explicit generalization of a term with a new variable.
At the induction checkpoint, confirm that you believe the formula being proved is a theorem and that it is appropriately strong for an inductive proof. Read the selected induction scheme and make sure it agrees with your idea of how the proof should go.
At the post-simplification checkpoint, which is probably the most
commonly seen, consider whether there are additional rewrite rules
you could prove to make the formula simplify still further. Look
for compositions of function symbols you could rewrite. Look for
contradictions among hypotheses and prove the appropriate
implications: for example, the checkpoint might contain the two
(P (F A)) and
(NOT (Q (G (F A)))) and you might
(implies (p x) (q (g x))) is a theorem. Look for
signs that your existing rules did not apply, e.g., for terms that
should have been rewritten, and figure out why they were not.
Possible causes include that they do not exactly match your old
rules, that your old rules have hypotheses that cannot be relieved
here -- perhaps because some other rules are missing, or perhaps
your old rules are disabled. If you cannot find any further
simplifications to make in the formula, ask yourself whether it is
valid. If so, sketch a proof. Perhaps the proof is by appeal to a
combination of lemmas you should now prove?
At the two generalization checkpoints --- where hypotheses are discarded or terms are replaced by variables --- ask yourself whether the result is a theorem. It often is not. Think about rewrite rules that would prove the formula. These are often restricted versions of the overly-general formulas created by the system's heuristics.
See proof-tree for a discussion of a tool to help you navigate through