Major Section: ACL2-TUTORIAL
This section contains introductory material on ACL2 including what ACL2 is, how to get started using the system, how to read the output, and other introductory topics. It was written almost entirely by Bill Young of Computational Logic, Inc.
You might also find CLI Technical Report 101 helpful, especially if you are familiar with Nqthm. If you would like more familiarity with Nqthm, we suggest CLI Technical Report 100.
OVERVIEW
ACL2 is an automated reasoning system under development at Computational Logic, Inc. It is the successor to the Nqthm (or Boyer-Moore) logic and proof system and its Pc-Nqthm interactive enhancement. The acronym ACL2 actually stands for ``A Computational Logic for Applicative Common Lisp''. This title suggests several distinct but related aspects of ACL2.
We assume that readers of the ACL2 documentation have at least a very slight familiarity with some Lisp-like language. We will address the issue of prerequisites further, in ``ABOUT THIS TUTORIAL'' below.
As a logic, ACL2 is a formal system with rigorously defined syntax and semantics. In mathematical parlance, the ACL2 logic is a first-order logic of total recursive functions providing mathematical induction on the ordinals up to epsilon-0 and two extension principles: one for recursive definition and one for constrained introduction of new function symbols, here called encapsulation. The syntax of ACL2 is that of Common Lisp; ACL2 specifications are ``also'' Common Lisp programs in a way that we will make clear later. In less formal language, the ACL2 logic is an integrated collection of rules for defining (or axiomatizing) recursive functions, stating properties of those functions, and rigorously establishing those properties. Each of these activities is mechanically supported.
As a specification language, ACL2 supports modeling of systems of various kinds. An ACL2 function can equally be used to express purely formal relationships among mathematical entities, to describe algorithms, or to capture the intended behavior of digital systems. For digital systems, an ACL2 specification is a mathematical model that is intended to formalize relevant aspects of system behavior. Just as physics allows us to model the behavior of continuous physical systems, ACL2 allows us to model digital systems, including many with physical realizations such as computer hardware. As early as the 1930's Church, Kleene, Turing and others established that recursive functions provide an expressive formalism for modeling digital computation. Digital computation should be understood in a broad sense, covering a wide variety of activities including almost any systematic or algorithmic activity, or activity that can be reasonably approximated in that way. This ranges from the behavior of a digital circuit to the behavior of a programming language compiler to the behavior of a controller for a physical system (as long as the system can be adequately modeled discretely). All of these have been modeled using ACL2 or its predecessor Nqthm.
ACL2 is a computational logic in at least three distinct senses. First, the theory of recursive functions is often considered the mathematics of computation. Church conjectured that any ``effective computation'' can be modeled as a recursive function. Thus, ACL2 provides an expressive language for modeling digital systems. Second, many ACL2 specifications are executable. In fact, recursive functions written in ACL2 are Common Lisp functions that can be submitted to any compliant Common Lisp compiler and executed (in an environment where suitable ACL2-specific macros and functions are defined). Third, ACL2 is computational in the sense that calculation is heavily integrated into the reasoning process. Thus, an expression with explicit constant values but no free variables can be simplified by calculation rather than by complex logical manipulations.
ACL2 is a powerful, automated theorem prover or proof checker. This means that a competent user can utilize the ACL2 system to discover proofs of theorems stated in the ACL2 logic or to check previously discovered proofs. The basic deductive steps in an ACL2-checked proof are often quite large, due to the sophisticated combination of decision procedures, conditional rewriting, mathematical and structural induction, propositional simplification, and complex heuristics to orchestrate the interactions of these capabilities. Unlike some automated proof systems, ACL2 does not produce a formal proof. However, we believe that if ACL2 certifies the ``theoremhood'' of a given conjecture, then such a formal proof exists and, therefore, the theorem is valid. The ultimate result of an ACL2 proof session is a collection of ``events,'' possibly grouped into ``books,'' that can be replayed in ACL2. Therefore, a proof can be independently validated by any ACL2 user.
ACL2 may be used in purely automated mode in the shallow sense that conjectures are submitted to the prover and the user does not interact with the proof attempt (except possibly to stop it) until the proof succeeds or fails. However, any non-trivial proof attempt is actually interactive, since successful proof ``events'' influence the subsequent behavior of the prover. For example, proving a lemma may introduce a rule that subsequently is used automatically by the prover. Thus, any realistic proof attempt, even in ``automatic'' mode, is really an interactive dialogue with the prover to craft a sequence of events building an appropriate theory and proof rules leading up to the proof of the desired result. Also, ACL2 supports annotating a theorem with ``hints'' designed to guide the proof attempt. By supplying appropriate hints, the user can suggest proof strategies that the prover would not discover automatically. There is a ``proof-tree'' facility (see proof-tree) that allows the user to monitor the progress and structure of a proof attempt in real-time. Exploring failed proof attempts is actually where heavy-duty ACL2 users spend most of their time.
ACL2 can also be used in a more explicitly interactive mode. The ``proof-checker'' subsystem of ACL2 allows exploration of a proof on a fairly low level including expanding calls of selected function symbols, invoking specific rewrite rules, and selectively navigating around the proof. This facility can be used to gain sufficient insight into the proof to construct an automatic version, or to generate a detailed interactive-style proof that can be replayed in batch mode.
Because ACL2 is all of these things -- computational logic, specification language, programming system, and theorem prover -- it is more than the sum of its parts. The careful integration of these diverse aspects has produced a versatile automated reasoning system suitable for building highly reliable digital systems. In the remainder of this tutorial, we will illustrate some simple uses of this automated reasoning system.
ABOUT THIS TUTORIAL
ACL2 is a complex system with a vast array of features, bells and whistles. However, it is possible to perform productive work with the system using only a small portion of the available functionality. The goals of this tutorial are to:
familiarize the new user with the most basic features of and modes of interaction with ACL2;
familiarize her with the form of output of the system; and
work through a graduated series of examples.
The more knowledge the user brings to this system, the easier it will be to become proficient. On one extreme: the ideal user of ACL2 is an expert Common Lisp programmer, has deep understanding of automated reasoning, and is intimately familiar with the earlier Nqthm system. Such ideal users are unlikely to need this tutorial. However, without some background knowledge, the beginning user is likely to become extremely confused and frustrated by this system. We suggest that a new user of ACL2 should:
(a) have a little familiarity with Lisp, including basic Lisp programming and prefix notation (a Lisp reference manual such as Guy Steele's ``Common Lisp: The Language'' is also helpful);
(b) be convinced of the utility of formal modeling; and
(c) be willing to gain familiarity with basic automated theorem proving topics such as rewriting and algebraic simplification.
We will not assume any deep familiarity with Nqthm (the so-called ``Boyer-Moore Theorem Prover''), though the book ``A Computational Logic Handbook'' by Boyer and Moore (Academic Press, 1988) is an extremely useful reference for many of the topics required to become a competent ACL2 user. We'll refer to it as ACLH below.
As we said in the introduction, ACL2 has various facets. For example, it can be used as a Common Lisp programming system to construct application programs. In fact, the ACL2 system itself is a large Common Lisp program constructed almost entirely within ACL2. Another use of ACL2 is as a specification and modeling tool. That is the aspect we will concentrate on in the remainder of this tutorial.
GETTING STARTED
This section is an abridged version of what's available elsewhere; feel free to see startup for more details.
How you start ACL2 will be system dependent, but you'll probably type something like ``acl2'' at your operating system prompt. Consult your system administrator for details.
When you start up ACL2, you'll probably find yourself inside the ACL2 command loop, as indicated by the following prompt.
If not, you should typeACL2 !>
(LP). See lp, which has a lot more
information about the ACL2 command loop.
There are two ``modes'' for using ACL2, :logic and
:program. When you begin ACL2, you will ordinarily be in the
:logic mode. This means that any new function defined is not
only executable but also is axiomatically defined in the ACL2 logic.
(See defun-mode and see default-defun-mode.) Roughly
speaking, :program mode is available for using ACL2 as a
programming language without some of the logical burdens
necessary for formal reasoning. In this tutorial we will assume
that we always remain in :logic mode and that our purpose is
to write formal models of digital systems and to reason about them.
Now, within the ACL2 command loop you can carry out various kinds of activities, including the folllowing. (We'll see examples later of many of these.)
define new functions (see defun);
execute functions on concrete data;
pose and attempt to prove conjectures about previously defined functions (see defthm);
query the ACL2 ``world'' or database (e.g., see pe); and
numerous other things.
In addition, there is extensive on-line documentation, of which this tutorial introduction is a part.
INTERACTING WITH ACL2
The standard means of interacting with ACL2 is to submit a sequence
of forms for processing by the ACL2 system. These forms are checked
for syntactic and semantic acceptability and appropriately processed
by the system. These forms can be typed directly at the ACL2
prompt. However, most successful ACL2 users prefer to do their work
using the Emacs text editor, maintaining an Emacs ``working'' buffer
in which forms are edited. Those forms are then copied to the ACL2
interaction buffer, which is often the "*shell*" buffer.
In some cases, processing succeeds and makes some change to the ACL2 ``logical world,'' which affects the processing of subsequent forms. How can this processing fail? For example, a proposed theorem will be rejected unless all function symbols mentioned have been previously defined. Also the ability of ACL2 to discover the proof of a theorem may depend on the user previously having proved other theorems. Thus, the order in which forms are submitted to ACL2 is quite important. Maintaining forms in an appropriate order in your working buffer will be helpful for re-playing the proof later.
One of the most common events in constructing a model is
introducing new functions. New functions are usually introduced
using the defun form; we'll encounter some exceptions later.
Proposed function definitions are checked to make sure that they are
syntactically and semantically acceptable (e.g., that all mentioned
functions have been previously defined) and, for recursive
functions, that their recursive calls terminate. A recursive
function definition is guaranteed to terminate if there is some some
``measure'' of the arguments and a ``well-founded'' ordering such
that the arguments to the function get smaller in each recursive
call. See well-founded-relation.
For example, suppose that we need a function that will append two
lists together. (We already have one in the ACL2 append
function; but suppose perversely that we decide to define our own.)
Suppose we submit the following definition (you should do so as well
and study the system output):
The system responds with the following message:(defun my-app (x y) (if (atom x) y (cons (car x) (my-app x y))))
This means that the system could not find an expression involving the formal parametersACL2 Error in ( DEFUN MY-APP ...): No :MEASURE was supplied with the definition of MY-APP. Our heuristics for guessing one have not made any suggestions. No argument of the function is tested along every branch and occurs as a proper subterm at the same argument position in every recursive call. You must specify a :MEASURE. See :DOC defun.
x and y that decreases under some
well-founded order in every recursive call (there is only one such
call). It should be clear that there is no such measure in this
case because the only recursive call doesn't change the arguments at
all. The definition is obviously flawed; if it were accepted and
executed it would loop forever. Notice that a definition that is
rejected is not stored in the system database; there is no need to
take any action to have it ``thrown away.'' Let's try again with
the correct definition. The interaction now looks like (we're also
putting in the ACL2 prompt; you don't type that):
Notice that this time the function definition was accepted. We didn't have to supply a measure explicitly; the system inferred one from the form of the definition. On complex functions it may be necessary to supply a measure explicitly. (See xargs.)ACL2 !>(defun my-app (x y) (if (atom x) y (cons (car x) (my-app (cdr x) y))))
The admission of MY-APP is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of MY-APP is described by the theorem (OR (CONSP (MY-APP X Y)) (EQUAL (MY-APP X Y) Y)). We used primitive type reasoning.
Summary Form: ( DEFUN MY-APP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.07 seconds (prove: 0.00, print: 0.00, other: 0.07) MY-APP
The system output provides several pieces of information.
The revised definition is acceptable. The system realized that there is a particular measure (namely,
(acl2-count x)) and a well-founded relation (e0-ord-<) under which the arguments ofmy-appget smaller in recursion. Actually, the theorem prover proved several theorems to admitmy-app. The main one was that when(atom x)is false theacl2-countof(cdr x)is less than (in thee0-ord-<sense) theacl2-countofx.Acl2-countis the most commonly used measure of the ``size`` of an ACL2 object.E0-ord-<is the ordering relation on ordinals less than epsilon-0. On the natural numbers it is just ordinary ``<''.The observation printed about ``the type of MY-APP'' means that calls of the function
my-appwill always return a value that is either a cons pair or is equal to the second parameter.The summary provides information about which previously introduced definitions and lemmas were used in this proof, about some notable things to watch out for (the Warnings), and about how long this event took to process.
Usually, it's not important to read this information. However, it is a good habit to scan it briefly to see if the type information is surprising to you or if there are Warnings. We'll see an example of them later.
After a function is accepted, it is stored in the database and
available for use in other function definitions or lemmas. To see
the definition of any function use the :pe command
(see pe). For example,
This displays the definition along with some other relevant information. In this case, we know that this definition was processed inACL2 !>:pe my-app L 73:x(DEFUN MY-APP (X Y) (IF (ATOM X) Y (CONS (CAR X) (MY-APP (CDR X) Y))))
:logic mode (the ``L'') and was the 73rd command
processed in the current session.We can also try out our newly defined function on some sample data. To do that, just submit a form to be evaluated to ACL2. For example,
ACL2 !>(my-app '(0 1 2) '(3 4 5)) (0 1 2 3 4 5) ACL2 !>(my-app nil nil) NIL ACL2 !>
Now suppose we want to prove something about the function just
introduced. We conjecture, for example, that the length of the
append of two lists is the sum of their lengths. We can formulate
this conjecture in the form of the following ACL2 defthm form.
First of all, how did we know about the functions(defthm my-app-length (equal (len (my-app x y)) (+ (len x) (len y))))
len and +, etc.?
The answer to that is somewhat unsatisfying -- we know them from our
past experience in using Common Lisp and ACL2. It's hard to know
that a function such as len exists without first knowing some Common
Lisp. If we'd guessed that the appropriate function was called
length (say, from our knowledge of Lisp) and tried :pe length, we
would have seen that length is defined in terms of len, and we
could have explored from there. Luckily, you can write a lot of
ACL2 functions without knowing too many of the primitive functions.
Secondly, why don't we need some ``type'' hypotheses? Does it make
sense to append things that are not lists? Well, yes. ACL2 and
Lisp are both quite weakly typed. For example, inspection of the
definition of my-app shows that if x is not a cons pair, then
(my-app x y) always returns y, no matter what y is.
Thirdly, would it matter if we rewrote the lemma with the equality reversed, as follows?
The two are logically equivalent, but...yes, it would make a big difference. Recall our remark that a lemma is not only a ``fact'' to be proved; it also is used by the system to prove other later lemmas. The current lemma would be stored as a rewrite rule. (See rule-classes.) For a rewrite rule, a conclusion of the form(defthm my-app-length2 (equal (+ (len x) (len y)) (len (my-app x y)))).
(EQUAL LHS RHS) means to replace instances of the LHS by the
appropriate instance of the RHS. Presumably, it's better to rewrite
(len (my-app x y)) to (+ (len x) (len y)) than the other way around.
The reason is that the system ``knows'' more about + than it does
about the new function symbol my-app.
So let's see if we can prove this lemma. Submitting our preferred
defthm to ACL2 (do it!), we get the following interaction:
--------------------------------------------------
ACL2 !>(defthm my-app-length
(equal (len (my-app x y))
(+ (len x) (len y))))
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. These merge into two derived
induction schemes. However, one of these is flawed and so we are
left with one viable candidate.
We will induct according to a scheme suggested by (LEN X), but
modified to accommodate (MY-APP X Y). If we let (:P X Y) denote *1
above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X Y))
(IMPLIES (AND (CONSP X) (:P (CDR X) Y))
(:P X Y))).
This induction is justified by the same argument used to admit LEN,
namely, the measure (ACL2-COUNT X) is decreasing according to the
relation E0-ORD-< (which is known to be well-founded on the domain
recognized by E0-ORDINALP). When applied to the goal at hand the
above induction scheme produces the following two nontautological
subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(EQUAL (LEN (MY-APP X Y))
(+ (LEN X) (LEN Y)))).
But simplification reduces this to T, using the :definitions of FIX,
LEN and MY-APP, the :type-prescription rule LEN, the :rewrite rule
UNICITY-OF-0 and primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(EQUAL (LEN (MY-APP (CDR X) Y))
(+ (LEN (CDR X)) (LEN Y))))
(EQUAL (LEN (MY-APP X Y))
(+ (LEN X) (LEN Y)))).
This simplifies, using the :definitions of LEN and MY-APP, primitive
type reasoning and the :rewrite rules COMMUTATIVITY-OF-+ and
CDR-CONS, to
Subgoal *1/1'
(IMPLIES (AND (CONSP X)
(EQUAL (LEN (MY-APP (CDR X) Y))
(+ (LEN Y) (LEN (CDR X)))))
(EQUAL (+ 1 (LEN (MY-APP (CDR X) Y)))
(+ (LEN Y) 1 (LEN (CDR X))))).
But simplification reduces this to T, using linear arithmetic,
primitive type reasoning and the :type-prescription rule LEN.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MY-APP-LENGTH ...)
Rules: ((:REWRITE UNICITY-OF-0)
(:DEFINITION FIX)
(:REWRITE COMMUTATIVITY-OF-+)
(:DEFINITION LEN)
(:REWRITE CDR-CONS)
(:DEFINITION MY-APP)
(:TYPE-PRESCRIPTION LEN)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:FAKE-RUNE-FOR-LINEAR NIL))
Warnings: None
Time: 0.30 seconds (prove: 0.13, print: 0.05, other: 0.12)
MY-APP-LENGTH
--------------------------------------------------
Wow, it worked! In brief, the system first tried to rewrite and simplify as much as possible. Nothing changed; we know that because it said ``Name the formula above *1.'' Whenever the system decides to name a formula in this way, we know that it has run out of techniques to use other than proof by induction.
The induction performed by ACL2 is structural or ``Noetherian''
induction. You don't need to know much about that except that it is
induction based on the structure of some object. The heuristics
infer the structure of the object from the way the object is
recursively decomposed by the functions used in the conjecture. The
heuristics of ACL2 are reasonably good at selecting an induction
scheme in simple cases. It is possible to override the heuristic
choice by providing an :induction hint (see hints). In the
case of the theorem above, the system inducts on the structure of
x as suggested by the decomposition of x in both (my-app x y)
and (len x). In the base case, we assume that x is not a
consp. In the inductive case, we assume that it is a consp
and assume that the conjecture holds for (cdr x).
There is a close connection between the analysis that goes on when a
function like my-app is accepted and when we try to prove
something inductively about it. That connection is spelled out well
in Boyer and Moore's book ``A Computational Logic,'' if you'd like to
look it up. But it's pretty intuitive. We accepted my-app
because the ``size'' of the first argument x decreases in the
recursive call. That tells us that when we need to prove something
inductively about my-app, it's a good idea to try an induction on
the size of the first argument. Of course, when you have a theorem
involving several functions, it may be necessary to concoct a more
complicated induction schema, taking several of them into account.
That's what's meant by ``merging'' the induction schemas.
The proof involves two cases: the base case, and the inductive case.
You'll notice that the subgoal numbers go down rather than up,
so you always know how many subgoals are left to process. The base
case (Subgoal *1/2) is handled by opening up the function
definitions, simplifying, doing a little rewriting, and performing
some reasoning based on the types of the arguments. You'll often
encounter references to system defined lemmas (like
unicity-of-0). You can always look at those with :pe; but,
in general, assume that there's a lot of simplification power under
the hood that's not too important to understand fully.
The inductive case (Subgoal *1/1) is also dispatched pretty
easily. Here we assume the conjecture true for the cdr of the
list and try to prove it for the entire list. Notice that the
prover does some simplification and then prints out an updated
version of the goal (Subgoal *1/1'). Examining these gives you a
pretty good idea of what's going on in the proof.
Sometimes one goal is split into a number of subgoals, as happened with the induction above. Sometimes after some initial processing the prover decides it needs to prove a subgoal by induction; this subgoal is given a name and pushed onto a stack of goals. Some steps, like generalization (see ACLH), are not necessarily validity preserving; that is, the system may adopt a false subgoal while trying to prove a true one. (Note that this is ok in the sense that it is not ``unsound.'' The system will fail in its attempt to establish the false subgoal and the main proof attempt will fail.) As you gain facility with using the prover, you'll get pretty good at recognizing what to look for when reading a proof script. The prover's proof-tree utility helps with monitoring an ongoing proof and jumping to designated locations in the proof (see proof-tree). See tips for a number of useful pointers on using the theorem prover effectively.
When the prover has successfully proved all subgoals, the proof is
finished. As with a defun, a summary of the proof is printed.
This was an extremely simple proof, needing no additional guidance.
More realistic examples typically require the user to look carefully
at the failed proof log to find ways to influence the prover to do
better on its next attempt. This means either: proving some rules
that will then be available to the prover, changing the global state
in ways that will affect the proof, or providing some hints
locally that will influence the prover's behavior. Proving this
lemma (my-app-length) is an example of the first. Since this is
a rewrite rule, whenever in a later proof an instance of the
form (LEN (MY-APP X Y)) is encountered, it will be rewritten to
the corresponding instance of (+ (LEN X) (LEN Y)). Disabling the
rule by executing the command
is an example of a global change to the behavior of the prover since this rewrite will not be performed subsequently (unless the rule is again enabled). Finally, we can add a (local) disable ``hint'' to a(in-theory (disable my-app-length)),
defthm, meaning to disable the lemma only in the proof of one
or more subgoals. For example:
(defthm my-app-length-commutativity
(equal (len (my-app x y))
(len (my-app y x)))
:hints (("Goal" :in-theory (disable my-app-length))))
In this case, the hint supplied is a bad idea since the proof is much
harder with the hint than without it. Try it both ways.
By the way, to undo the previous event use :u (see u). To
undo back to some earlier event use :ubt (see ubt). To view
the current event use :pe :here. To list several events use
:pbt (see pbt).
Notice the form of the hint in the previous example
(see hints). It specifies a goal to which the hint applies.
"Goal" refers to the top-level goal of the theorem. Subgoals
are given unique names as they are generated. It may be useful to
suggest that a function symbol be disabled only for Subgoal
1.3.9, say, and a different function enabled only on Subgoal
5.2.8. Overuse of such hints often suggests a poor global
proof strategy.
We now recommend that you visit documentation on additional
examples. See tutorial-examples.
Major Section: ACL2-TUTORIAL
When you start up ACL2, you'll probably find yourself inside the ACL2 command loop, as indicated by the following prompt.
If not, you should typeACL2 !>
(LP). See lp, which has a lot more
information about the ACL2 command loop.
You should now be in ACL2. The current ``default-defun-mode'' is
:logic; the other mode is :program, which would cause the letter p
to be printed in the prompt. :Logic means that any function we
define is not only executable but also is axiomatically defined in
the ACL2 logic. See defun-mode and
see default-defun-mode. For example we can define a function
my-cons as follows. (You may find it useful to start up ACL2 and
submit this and other commands below to the ACL2 command loop, as we
won't include output below.)
An easy theorem may then be proved: theACL2 !>(defun my-cons (x y) (cons x y))
car of (my-cons a b) is
A.
Notice that unlike Nqthm, the theorem command isACL2 !>(defthm car-my-cons (equal (car (my-cons a b)) a))
defthm rather than
prove-lemma. See defthm, which explains (among other things)
that the default is to turn theorems into rewrite rules.
Various keyword commands are available to query the ACL2 ``world'',
or database. For example, we may view the definition of my-cons by
invoking a command to print events, as follows.
Also see pe. We may also view all the lemmas that rewrite terms whose top function symbol isACL2 !>:pe my-cons
car by using the following
command, whose output will refer to the lemma car-my-cons proved
above.
Also see pl. Finally, we may print all the commands back through the initial world as follows.ACL2 !>:pl car
See history for a list of commands, including these, for viewing the current ACL2 world.ACL2 !>:pbt 0
Continue with the documentation for tutorial-examples to
see a simple but illustrative example in the use of ACL2 for
reasoning about functions.
Major Section: ACL2-TUTORIAL
See books for a discussion of books. Briefly, a book is a file whose name ends in ``.lisp'' that contains ACL2 events; see events.
See history for a list of useful commands. Some examples:
See documentation to learn how to print documentation to the terminal. There are also versions of the documentation for Mosaic, Emacs Info, and hardcopy.:pbt :here ; print the current event :pbt (:here -3) ; print the last four events :u ; undo the last event :pe append ; print the definition of append
There are quite a few kinds of rules allowed in ACL2 besides
:rewrite rules, though we hope that beginners won't usually need
to be aware of them. See rule-classes for details. In
particular, there is support for congruence rewriting.
See rune (``RUle NamE'') for a description of the various kinds
of rules in the system. Also see theories for a description of
how to build theories of runes, which are often used in hints;
see hints.
A ``programming mode'' is supported; see program,
see defun-mode, and see default-defun-mode. It can be
useful to prototype functions after executing the command :program,
which will cause definitions to be syntaxed-checked only.
ACL2 supports mutual recursion, though this feature is not tied into the automatic discovery of induction schemas and is often not the best way to proceed when you expect to be reasoning about the functions. See defuns; also see mutual-recursion.
See ld for discussion of how to load files of events. There
are many options to ld, including ones to suppress proofs and to
control output.
The :otf-flg (Onward Thru the Fog FLaG) is a useful feature that
Nqthm users have often wished for. It prevents the prover from
aborting a proof attempt and inducting on the original conjecture.
See otf-flg.
ACL2 supports redefinition and redundancy in events; see ld-redefinition-action and see redundant-events.
A proof-tree display feature is available for use with Emacs. This feature provides a view of ACL2 proofs that can be much more useful than reading the stream of characters output by the theorem prover as its ``proof.'' See proof-tree.
An interactive feature similar to Pc-Nqthm is supported in ACL2. See verify and see proof-checker.
ACL2 allows you to monitor the use of rewrite rules. See break-rewrite.
See arrays to read about applicative, fast arrays in ACL2.
To quit the ACL2 command loop, or (in akcl) to return to the ACL2
command loop after an interrupt, type :q. To continue (resume)
after an interrupt (in akcl), type :r. To cause an interrupt (in
akcl under Unix (trademark of AT&T)), hit control-C (twice, if
inside Emacs). To exit ACL2 altogether, first type :q to exit
the ACL2 command loop, and then exit Lisp (by typing
(user::bye) in akcl).
See state to read about the von Neumannesque ACL2 state object.
Also see @, and see assign, to learn about reading and
setting global state variables.
Major Section: ACL2-TUTORIAL
We present here some tips for using ACL2 effectively. Though this collection is somewhat ad hoc, we try to provide some organization, albeit somewhat artificial: for example, the sections overlap, and no particular order is intended. This material has been adapted by Bill Young from a very similar list for Nqthm that appeared in the conclusion of: ``Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem,'' by Matt Kaufmann and Paolo Pecchiari, CLI Technical Report 100, June, 1995. We also draw from a similar list in Chapter 13 of ``A Computational Logic Handbook'' by R.S. Boyer and J S. Moore (Academic Press, 1988). We'll refer to this as ``ACLH'' below.
These tips are organized roughly as follows.
A. ACL2 BasicsB. Strategies for creating events
C. Dealing with failed proofs
D. Performance tips
E. Miscellaneous tips and knowledge
F. Some things you DON'T need to know
ACL2 BASICS
A1. The ACL2 logic.
This is a logic of total functions. For example, if A and B
are less than or equal to each other, then we need to know something
more in order to conclude that they are equal (e.g., that they are
numbers). This kind of twist is important in writing definitions;
for example, if you expect a function to return a number, you may
want to apply the function fix or some variant (e.g., nfix or
ifix) in case one of the formals is to be returned as the value.
ACL2's notion of ordinals is important on occasion in supplying ``measure hints'' for the acceptance of recursive definitions. Be sure that your measure is really an ordinal. Consider the following example, which ACL2 fails to admit (as explained below).
One might think that(defun cnt (name a i x) (declare (xargs :measure (+ 1 i))) (cond ((zp (+ 1 i)) 0) ((equal x (aref1 name a i)) (1+ (cnt name a (1- i) x))) (t (cnt name a (1- i) x))))
(+ 1 i) is a reasonable measure, since we
know that (+ 1 i) is a positive integer in any recursive call of
cnt, and positive integers are ACL2 ordinals
(see e0-ordinalp). However, the ACL2 logic requires that the
measure be an ordinal unconditionally, not just under the governing
assumptions that lead to recursive calls. An appropriate fix is to
apply nfix to (+ 1 i), i.e., to use
in order to guarantee that the measure will always be an ordinal (in fact, a positive integer).(declare (xargs :measure (nfix (+ 1 i))))
A2. Simplification.
The ACL2 simplifier is basically a rewriter, with some ``linear
arithmetic'' thrown in. One needs to understand the notion of
conditional rewriting. See rewrite.
A3. Parsing of rewrite rules.
ACL2 parses rewrite rules roughly as explained in ACLH, except
that it never creates ``unusual'' rule classes. In ACL2, if you
want a :linear rule, for example, you must specify :linear in
the :rule-classes. See rule-classes, and also
see rewrite and see linear.
A4. Linear arithmetic.
On this subject, it should suffice to know that the prover can
handle truths about + and -, and that linear rules (see above)
are somehow ``thrown in the pot'' when the prover is doing such
reasoning. Perhaps it's also useful to know that linear rules can
have hypotheses, and that conditional rewriting is used to relieve
those hypotheses.
A5. Events.
Over time, the expert ACL2 user will know some subtleties of its
events. For example, in-theory events and hints are
important, and they distinguish between a function and its
executable counterpart.
B. STRATEGIES FOR CREATING EVENTS
In this section, we concentrate on the use of definitions and rewrite rules. There are quite a few kinds of rules allowed in ACL2 besides rewrite rules, though most beginning users probably won't usually need to be aware of them. See rule-classes for details. In particular, there is support for congruence rewriting. Also see rune (``RUle NamE'') for a description of the various kinds of rules in the system.
B1. Use high-level strategy.
Decompose theorems into ``manageable'' lemmas (admittedly,
experience helps here) that yield the main result ``easily.'' It's
important to be able to outline non-trivial proofs by hand (or in
your head). In particular, avoid submitting goals to the prover
when there's no reason to believe that the goal will be proved and
there's no ``sense'' of how an induction argument would apply. It
is often a good idea to avoid induction in complicated theorems
unless you have a reason to believe that it is appropriate.
B2. Write elegant definitions.
Try to write definitions in a reasonably modular style, especially
recursive ones. Think of ACL2 as a programming language whose
procedures are definitions and lemmas, hence we are really
suggesting that one follow good programming style (in order to avoid
duplication of ``code,'' for example).
When possible, complex functions are best written as compositions of simpler functions. The theorem prover generally performs better on primitive recursive functions than on more complicated recursions (such as those using accumulating parameters).
Avoid large non-recursive definitions which tend to lead to large case explosions. If such definitions are necessary, try to prove all relevant facts about the definitions and then disable them.
Whenever possible, avoid mutual recursion if you care to prove anything about your functions. The induction heuristics provide essentially no help with reasoning about mutually defined functions. Mutually recursive functions can usually be combined into a single function with a ``flag'' argument. (However, see mutual-recursion-proof-example for a small example of proof involving mutually recursive functions.)
B3. Look for analogies.
Sometimes you can easily edit sequences of lemmas into sequences of
lemmas about analogous functions.
B4. Write useful rewrite rules.
As explained in A3 above, every rewrite rule is a directive to the
theorem prover, usually to replace one term by another. The
directive generated is determined by the syntax of the defthm
submitted. Never submit a rewrite rule unless you have considered
its interpretation as a proof directive.
B4a. Rewrite rules should simplify.
Try to write rewrite rules whose right-hand sides are in some sense
``simpler than'' (or at worst, are variants of) the left-hand sides.
This will help to avoid infinite loops in the rewriter.
B4b. Avoid needlessly expensive rules.
Consider a rule whose conclusion's left-hand side (or, the entire
conclusion) is a term such as (consp x) that matches many terms
encountered by the prover. If in addition the rule has complicated
hypotheses, this rule could slow down the prover greatly. Consider
switching the conclusion and a complicated hypothesis (negating
each) in that case.
B4c. The ``Knuth-Bendix problem''.
Be aware that left sides of rewrite rules should match the
``normalized forms'', where ``normalization'' (rewriting) is inside
out. Be sure to avoid the use of nonrecursive function symbols on
left sides of rewrite rules, except when those function symbols are
disabled, because they tend to be expanded away before the rewriter
would encounter an instance of the left side of the rule. Also
assure that subexpressions on the left hand side of a rule are in
simplified form.
B4d. Avoid proving useless rules.
Sometimes it's tempting to prove a rewrite rule even before you see
how it might find application. If the rule seems clean and
important, and not unduly expensive, that's probably fine,
especially if it's not too hard to prove. But unless it's either
part of the high-level strategy or, on the other hand, intended to
get the prover past a particular unproved goal, it may simply waste
your time to prove the rule, and then clutter the database of rules
if you are successful.
B4e. State rules as strongly as possible, usually.
It's usually a good idea to state a rule in the strongest way
possible, both by eliminating unnecessary hypotheses and by
generalizing subexpressions to variables.
Advanced users may choose to violate this policy on occasion, for example in order to avoid slowing down the prover by excessive attempted application of the rule. However, it's a good rule of thumb to make the strongest rule possible, not only because it will then apply more often, but also because the rule will often be easier to prove (see also B6 below). New users are sometimes tempted to put in extra hypotheses that have a ``type restriction'' appearance, without realizing that the way ACL2 handles (total) functions generally lets it handle trivial cases easily.
B4f. Avoid circularity.
A stack overflow in a proof attempt almost always results from
circular rewriting. Use brr to investigate the stack;
see break-lemma. Because of the complex heuristics, it is not
always easy to define just when a rewrite will cause circularity.
See the very good discussion of this topic in ACLH.
See break-lemma for a trick involving use of the forms brr t
and (cw-gstack *deep-gstack* state) for inspecting loops in the
rewriter.
B4g. Remember restrictions on permutative rules.
Any rule that permutes the variables in its left hand side could
cause circularity. For example, the following axiom is
automatically supplied by the system:
This would obviously lead to dangerous circular rewriting if such ``permutative'' rules were not governed by a further restriction. The restriction is that such rules will not produce a term that is ``lexicographically larger than'' the original term (see loop-stopper). However, this sometimes prevents intended rewrites. See Chapter 13 of ACLH for a discussion of this problem.(defaxiom commutativity-of-+ (equal (+ x y) (+ y x))).
B5. Conditional vs. unconditional rewrite rules.
It's generally preferable to form unconditional rewrite rules unless
there is a danger of case explosion. That is, rather than pairs of
rules such as
and(implies p (equal term1 term2))
consider:(implies (not p) (equal term1 term3))
However, sometimes this strategy can lead to case explosions:(equal term1 (if p term2 term3))
IF
terms introduce cases in ACL2. Use your judgment. (On the subject
of IF: COND, CASE, AND, and OR are macros that
abbreviate IF forms, and propositional functions such as
IMPLIES quickly expand into IF terms.)
B6. Create elegant theorems.
Try to formulate lemmas that are as simple and general as possible.
For example, sometimes properties about several functions can be
``factored'' into lemmas about one function at a time. Sometimes
the elimination of unnecessary hypotheses makes the theorem easier
to prove, as does generalizing first by hand.
B7. Use defaxioms temporarily to explore possibilities.
When there is a difficult goal that seems to follow immediately (by
a :use hint or by rewriting) from some other lemmas, you can
create those lemmas as defaxiom events (or, the application of
skip-proofs to defthm events) and then double-check that the
difficult goal really does follow from them. Then you can go back
and try to turn each defaxiom into a defthm. When you do
that, it's often useful to disable any additional rewrite rules that
you prove in the process, so that the ``difficult goal'' will still
be proved from its lemmas when the process is complete.
Better yet, rather than disabling rewrite rules, use the local
mechanism offered by encapsulate to make temporary rules
completely local to the problem at hand. See encapsulate and
see local.
B9. Use books.
Consider using previously certified books, especially for arithmetic
reasoning. This cuts down the duplication of effort and starts your
specification and proof effort from a richer foundation. See the
file "doc/README" in the ACL2 distribution for information on books
that come with the system.
C. DEALING WITH FAILED PROOFS
C1. Look in proof output for goals that can't be further simplified.
Use the ``proof-tree'' utility to explore the proof space.
However, you don't need to use that tool to use the ``checkpoint''
strategy. The idea is to think of ACL2 as a ``simplifier'' that
either proves the theorem or generates some goal to consider. That
goal is the first ``checkpoint,'' i.e., the first goal that does not
further simplify. Exception: it's also important to look at the
induction scheme in a proof by induction, and if induction seems
appropriate, then look at the first checkpoint after the
induction has begun.
Consider whether the goal on which you focus is even a theorem. Sometimes you can execute it for particular values to find a counterexample.
When looking at checkpoints, remember that you are looking for any reason at all to believe the goal is a theorem. So for example, sometimes there may be a contradiction in the hypotheses.
Don't be afraid to skip the first checkpoint if it doesn't seem very helpful. Also, be willing to look a few lines up or down from the checkpoint if you are stuck, bearing in mind however that this practice can be more distracting than helpful.
C2. Use the ``break rewrite'' facility.
Brr and related utilities let you inspect the ``rewrite stack.''
These can be valuable tools in large proof efforts.
See break-lemma for an introduction to these tools, and
see break-rewrite for more complete information.
The break facility is especially helpful in showing you why a particular rewrite rule is not being applied.
C3. Use induction hints when necessary.
Of course, if you can define your functions so that they suggest the
correct inductions to ACL2, so much the better! But for complicated
inductions, induction hints are crucial. See hints for a
description of :induct hints.
C4. Use the ``Proof Checker'' to explore.
The verify command supplied by ACL2 allows one to explore problem
areas ``by hand.'' However, even if you succeed in proving a
conjecture with verify, it is useful to prove it without using
it, an activity that will often require the discovery of rewrite
rules that will be useful in later proofs as well.
C5. Don't have too much patience.
Interrupt the prover fairly quickly when simplification isn't
succeeding.
C6. Simplify rewrite rules.
When it looks difficult to relieve the hypotheses of an existing
rewrite rule that ``should'' apply in a given setting, ask yourself
if you can eliminate a hypothesis from the existing rewrite rule.
If so, it may be easier to prove the new version from the old
version (and some additional lemmas), rather than to start from
scratch.
C7. Deal with base cases first.
Try getting past the base case(s) first in a difficult proof by
induction. Usually they're easier than the inductive step(s), and
rules developed in proving them can be useful in the inductive
step(s) too. Moreover, it's pretty common that mistakes in the
statement of a theorem show up in the base case(s) of its proof by
induction.
C8. Use :expand hints.
Consider giving :expand hints. These are especially useful when a
proof by induction is failing. It's almost always helpful to open
up a recursively defined function that is supplying the induction
scheme, but sometimes ACL2 is too timid to do so; or perhaps the
function in question is disabled.
D. PERFORMANCE TIPS
D1. Disable rules.
There are a number of instances when it is crucial to disable rules,
including (often) those named explicitly in :use hints. Also,
disable recursively defined functions for which you can prove what
seem to be all the relevant properties. The prover can spend
significant time ``behind the scenes'' trying to open up recursively
defined functions, where the only visible effect is slowness.
D2. Turn off the ``break rewrite'' facility.
Remember to execute :brr nil after you've finished with the
``break rewrite'' utility (see break-rewrite), in order to
bring the prover back up to full speed.
E. MISCELLANEOUS TIPS AND KNOWLEDGE
E1. Order of application of rewrite rules.
Keep in mind that the most recent rewrite rules in the history
are tried first.
E2. Relieving hypotheses is not full-blown theorem proving.
Relieving hypotheses on rewrite rules is done by rewriting and linear
arithmetic alone, not by case splitting or by other prover processes
``below'' simplification.
E3. ``Free variables'' in rewrite rules.
The set of ``free
variables'' of a rewrite rule is defined to contain those
variables occurring in the rule that do not occur in the left-hand
side of the rule. It's often a good idea to avoid rules containing
free variables because they are ``weak,'' in the sense that
hypotheses containing such variables can generally only be proved
when they are ``obviously'' present in the current context. This
weakness suggests that it's important to put the most
``interesting'' (specific) hypotheses about free variables first, so
that the right instances are considered. For example, suppose you
put a very general hypothesis such as (consp x) first. If the
context has several terms around that are known to be
consps, then x may be bound to the wrong one of them.
E4. Obtaining information
Use :pl foo to inspect rewrite rules whose left hand sides are
applications of the function foo. Another approach to seeing
which rewrite rules apply is to enter the proof-checker with
verify, and use the show-rewrites or sr command.
E5. Consider esoteric rules with care.
If you care to see rule-classes and peruse the list of
subtopics (which will be listed right there in most versions of this
documentation), you'll see that ACL2 supports a wide variety of
rules in addition to :rewrite rules. Should you use them?
This is a complex question that we are not ready to answer with any
generality. Our general advice is to avoid relying on such rules as
long as you doubt their utility. More specifically: be careful not
to use conditional type prescription rules, as these have been known
to bring ACL2 to its knees, unless you are conscious that you are
doing so and have reason to believe that they are working well.
F. SOME THINGS YOU DON'T NEED TO KNOW
Most generally: you shouldn't usually need to be able to predict too much about ACL2's behavior. You should mainly just need to be able to react to it.
F1. Induction heuristics.
Although it is often important to read the part of the prover's
output that gives the induction scheme chosen by the prover, it is
not necessary to understand how the prover made that choice.
(Granted, advanced users may occasionally gain minor insight from
such knowledge. But it's truly minor in many cases.) What is
important is to be able to tell it an appropriate induction when it
doesn't pick the right one (after noticing that it doesn't). See C3
above.
F2. Heuristics for expanding calls of recursively defined functions.
As with the previous topic, the important thing isn't to understand
these heuristics but, rather, to deal with cases where they don't
seem to be working. That amounts to supplying :expand hints for
those calls that you want opened up, which aren't. See also C8
above.
F3. The ``waterfall''.
As discussed many times already, a good strategy for using ACL2 is
to look for checkpoints (goals stable under simplification) when a
proof fails, perhaps using the proof-tree facility. Thus, it
is reasonable to ignore almost all the prover output, and to avoid
pondering the meaning of the other ``processes'' that ACL2 uses
besides simplification (such as elimination, cross-fertilization,
generalization, and elimination of irrelevance). For example, you
don't need to worry about prover output that mentions ``type
reasoning'' or ``abbreviations,'' for example.
Major Section: ACL2-TUTORIAL
Beginning users may find these examples at least as useful as the extensive documentation on particular topics. We suggest that you read these in the following order:
Tutorial1-Towers-of-Hanoi Tutorial2-Eights-Problem Tutorial3-Phonebook-Example Tutorial4-Defun-Sk-Example Tutorial5-Miscellaneous-ExamplesYou may also wish to visit the other introductory sections, startup and tidbits. These contain further information related to the use of ACL2.
Next, define the notion of a ``leaf'' of a tree, i.e., a predicateACL2 !>(fringe '((a . b) c . d)) (A B C D)
leaf-p that is true of an atom if and only if that atom appears
at the tip of the tree. Define this notion without referencing the
function fringe. Finally, prove the following theorem, whose
proof may well be automatic (i.e., not require any lemmas).
For a solution, see solution-to-simple-example.(defthm leaf-p-iff-member-fringe (iff (leaf-p atm x) (member-equal atm (fringe x))))
Major Section: TUTORIAL-EXAMPLES
To see a statement of the problem solved below, see tutorial-examples.
Here is a sequence of ACL2 events that illustrates the use of ACL2 to make definitions and prove theorems. We will introduce the notion of the fringe of a tree, as well as the notion of a leaf of a tree, and then prove that the members of the fringe are exactly the leaves.
We begin by defining the fringe of a tree, where we identify
trees simply as cons structures, with atoms at the leaves. The
definition is recursive, breaking into two cases. If x is a cons,
then the fringe of x is obtained by appending together the fringes
of the car and cdr (left and right child) of x. Otherwise, x is an
atom and its fringe is the one-element list containing only x.
Now that(defun fringe (x) (if (consp x) (append (fringe (car x)) (fringe (cdr x))) (list x)))
fringe has been defined, let us proceed by defining the
notion of an atom appearing as a ``leaf'', with the goal of proving
that the leaves of a tree are exactly the members of its fringe.
The main theorem is now as follows. Note that the rewrite rule below uses the equivalence relation(defun leaf-p (atm x) (if (consp x) (or (leaf-p atm (car x)) (leaf-p atm (cdr x))) (equal atm x)))
iff (see equivalence)
rather than equal, since member returns the tail of the given
list that begins with the indicated member, rather than returning a
Boolean. (Use :pe member to see the definition of member.)
(defthm leaf-p-iff-member-fringe (iff (leaf-p atm x) (member-equal atm (fringe x))))
Major Section: TUTORIAL-EXAMPLES
This example was written almost entirely by Bill Young of Computational Logic, Inc.
We will tackle the famous ``Towers of Hanoi'' problem. This problem is illustrated by the following picture.
| | |
| | |
--- | |
----- | |
------- | |
A B C
We have three pegs -- a, b, and c -- and n disks of
different sizes. The disks are all initially on peg a. The goal
is to move all disks to peg c while observing the following two
rules.1. Only one disk may be moved at a time, and it must start and finish the move as the topmost disk on some peg;
2. A disk can never be placed on top of a smaller disk.
Let's consider some simple instances of this problem. If n = 1,
i.e., only one disk is to be moved, simply move it from a to
c. If n = 2, i.e., two disks are to be moved, the following
sequence of moves suffices: move from a to b, move from a
to c, move from b to c.
In general, this problem has a straightforward recursive solution.
Suppose that we desire to move n disks from a to c, using
b as the intermediate peg. For the basis, we saw above that we
can always move a single disk from a to c. Now if we have
n disks and assume that we can solve the problem for n-1
disks, we can move n disks as follows. First, move n-1 disks
from a to b using c as the intermediate peg; move the
single disk from a to c; then move n-1 disks from b to
c using a as the intermediate peg.
In ACL2, we can write a function that will return the sequence of
moves. One such function is as follows. Notice that we have two
base cases. If (zp n) then n is not a positive integer; we
treat that case as if n were 0 and return an empty list of moves.
If n is 1, then we return a list containing the single
appropriate move. Otherwise, we return the list containing exactly
the moves dictated by our recursive analysis above.
Notice that we give(defun move (a b) (list 'move a 'to b))
(defun hanoi (a b c n) (if (zp n) nil (if (equal n 1) (list (move a c)) (append (hanoi a c b (1- n)) (cons (move a c) (hanoi b a c (1- n)))))))
hanoi four arguments: the three pegs, and
the number of disks to move. It is necessary to supply the pegs
because, in recursive calls, the roles of the pegs differ. In any
execution of the algorithm, a given peg will sometimes be the source
of a move, sometimes the destination, and sometimes the intermediate
peg.
After submitting these functions to ACL2, we can execute the hanoi
function on various specific arguments. For example:
From the algorithm it is clear that if it takesACL2 !>(hanoi 'a 'b 'c 1) ((MOVE A TO C))
ACL2 !>(hanoi 'a 'b 'c 2) ((MOVE A TO B) (MOVE A TO C) (MOVE B TO C))
ACL2 !>(hanoi 'a 'b 'c 3) ((MOVE A TO C) (MOVE A TO B) (MOVE C TO B) (MOVE A TO C) (MOVE B TO A) (MOVE B TO C) (MOVE A TO C))
m moves to
transfer n disks, it will take (m + 1 + m) = 2m + 1 moves for
n+1 disks. From some simple calculations, we see that we need
the following number of moves in specific cases:
The pattern is fairly clear. To moveDisks 0 1 2 3 4 5 6 7 ... Moves 0 1 3 7 15 31 63 127 ...
n disks requires (2^n - 1)
moves. Let's attempt to use ACL2 to prove that fact.
First of all, how do we state our conjecture? Recall that hanoi
returns a list of moves. The length of the list (given by the
function len) is the number of moves required. Thus, we can state
the following conjecture.
When we submit this to ACL2, the proof attempt fails. Along the way we notice subgoals such as:(defthm hanoi-moves-required-first-try (equal (len (hanoi a b c n)) (1- (expt 2 n))))
Subgoal *1/1' (IMPLIES (NOT (< 0 N)) (EQUAL 0 (+ -1 (EXPT 2 N)))).
This tells us that the prover is considering cases that are
uninteresting to us, namely, cases in which n might be negative.
The only cases that are really of interest are those in which n
is a non-negative natural number. Therefore, we revise our theorem
as follows:
and submit it to ACL2 again.(defthm hanoi-moves-required (implies (and (integerp n) (<= 0 n)) ;; n is at least 0 (equal (len (hanoi a b c n)) (1- (expt 2 n)))))
Again the proof fails. Examining the proof script we encounter the following text. (How did we decide to focus on this goal? Some information is provided in ACLH, and the ACL2 documentation on tips may be helpful. But the simplest answer is: this was the first goal suggested by the ``proof-tree'' tool below the start of the proof by induction. See proof-tree.)
It is difficult to make much sense of such a complicated goal. However, we do notice something interesting. In the conclusion is a term of the following shape.Subgoal *1/5'' (IMPLIES (AND (INTEGERP N) (< 0 N) (NOT (EQUAL N 1)) (EQUAL (LEN (HANOI A C B (+ -1 N))) (+ -1 (EXPT 2 (+ -1 N)))) (EQUAL (LEN (HANOI B A C (+ -1 N))) (+ -1 (EXPT 2 (+ -1 N))))) (EQUAL (LEN (APPEND (HANOI A C B (+ -1 N)) (CONS (LIST 'MOVE A 'TO C) (HANOI B A C (+ -1 N))))) (+ -1 (* 2 (EXPT 2 (+ -1 N))))))
We conjecture that the length of the(LEN (APPEND ... ...))
append of two lists should
be the sum of the lengths of the lists. If the prover knew that, it
could possibly have simplified this term earlier and made more
progress in the proof. Therefore, we need a rewrite rule that
will suggest such a simplification to the prover. The appropriate
rule is:
We submit this to the prover, which proves it by a straightforward induction. The prover stores this lemma as a rewrite rule and will subsequently (unless we disable the rule) replace terms matching the left hand side of the rule with the appropriate instance of the term on the right hand side.(defthm len-append (equal (len (append x y)) (+ (len x) (len y))))
We now resubmit our lemma hanoi-moves-required to ACL2. On this
attempt, the proof succeeds and we are done.
One bit of cleaning up is useful. We needed the hypotheses that:
This is an awkward way of saying that(and (integerp n) (<= 0 n)).
n is a natural number;
natural is not a primitive data type in ACL2. We could define a
function naturalp, but it is somewhat more convenient to define a
macro as follows:
Subsequently, we can use(defmacro naturalp (x) (list 'and (list 'integerp x) (list '<= 0 x)))
(naturalp n) wherever we need to note
that a quantity is a natural number. See defmacro for more
information about ACL2 macros. With this macro, we can reformulate
our theorem as follows:
Another interesting (but much harder) theorem asserts that the list of moves generated by our(defthm hanoi-moves-required (implies (naturalp n) (equal (len (hanoi a b c n)) (1- (expt 2 n))))).
hanoi function actually accomplishes
the desired goal while following the rules. When you can state and
prove that theorem, you'll be a very competent ACL2 user.By the way, the name ``Towers of Hanoi'' derives from a legend that a group of Vietnamese monks works day and night to move a stack of 64 gold disks from one diamond peg to another, following the rules set out above. We're told that the world will end when they complete this task. From the theorem above, we know that this requires 18,446,744,073,709,551,615 moves:
We're guessing they won't finish any time soon.ACL2 !>(1- (expt 2 64)) 18446744073709551615 ACL2 !>
Major Section: TUTORIAL-EXAMPLES
This example was written almost entirely by Bill Young of Computational Logic, Inc.
This simple example was brought to our attention as one that Paul Jackson has solved using the NuPrl system. The challenge is to prove the theorem:
In ACL2, we could phrase this theorem using quantification. However we will start with a constructive approach, i.e., we will show that values offor all n > 7, there exist naturals i and j such that: n = 3i + 5j.
i and j exist by writing a function that will
construct such values for given n. Suppose we had a function
(split n) that returns an appropriate pair (i . j). Our
theorem would be as follows:
That is, assuming that(defthm split-splits (let ((i (car (split n))) (j (cdr (split n)))) (implies (and (integerp n) (< 7 n)) (and (integerp i) (<= 0 i) (integerp j) (<= 0 j) (equal (+ (* 3 i) (* 5 j)) n)))))
n is a natural number greater than 7,
(split n) returns values i and j that are in the
appropriate relation to n.Let's look at a few cases:
Maybe you will have observed a pattern here; any natural number larger than 10 can be obtained by adding some multiple of 3 to 8, 9, or 10. This gives us the clue to constructing a proof. It is clear that we can write split as follows:8 = 3x1 + 5x1; 11 = 3x2 + 5x1; 14 = 3x3 + 5x1; ... 9 = 3x3 + 5x0; 12 = 3x4 + 5x0; 15 = 3x5 + 5x0; ... 10 = 3x0 + 5x2; 13 = 3x1 + 5x2; 16 = 3x2 + 5x2; ...
Notice that we explicitly compute the values of(defun bump-i (x) ;; Bump the i component of the pair ;; (i . j) by 1. (cons (1+ (car x)) (cdr x)))
(defun split (n) ;; Find a pair (i . j) such that ;; n = 3i + 5j. (if (or (zp n) (< n 8)) nil ;; any value is really reasonable here (if (equal n 8) (cons 1 1) (if (equal n 9) (cons 3 0) (if (equal n 10) (cons 0 2) (bump-i (split (- n 3))))))))
i and j for
the cases of 8, 9, and 10, and for the degenerate case when n is
not a natural or is less than 8. For all naturals greater than
n, we decrement n by 3 and bump the number of 3's (the value
of i) by 1. We know that the recursion must terminate because any
integer value greater than 10 can eventually be reduced to 8, 9, or
10 by successively subtracting 3.Let's try it on some examples:
Finally, we submit our theoremACL2 !>(split 28) (6 . 2)
ACL2 !>(split 45) (15 . 0)
ACL2 !>(split 335) (110 . 1)
split-splits, and the proof
succeeds. In this case, the prover is ``smart'' enough to induct
according to the pattern indicated by the function split.
For completeness, we'll note that we can state and prove a quantified
version of this theorem. We introduce the notion split-able to mean
that appropriate i and j exist for n.
Then our theorem is given below. Notice that we prove it by observing that our previous function(defun-sk split-able (n) (exists (i j) (equal n (+ (* 3 i) (* 5 j)))))
split delivers just such an
i and j (as we proved above).
Unfortunately, understanding the mechanics of the proof requires knowing something about the way(defthm split-splits2 (implies (and (integerp n) (< 7 n)) (split-able n)) :hints (("Goal" :use (:instance split-able-suff (i (car (split n))) (j (cdr (split n)))))))
defun-sk works.
See defun-sk or see Tutorial4-Defun-Sk-Example for more on
that subject.
Major Section: TUTORIAL-EXAMPLES
The other tutorial examples are rather small and entirely self contained. The present example is rather more elaborate, and makes use of a feature that really adds great power and versatility to ACL2, namely: the use of previously defined collections of lemmas, in the form of ``books.''
This example was written almost entirely by Bill Young of Computational Logic, Inc.
This example is based on one developed by Ricky Butler and Sally Johnson of NASA Langley for the PVS system, and subsequently revised by Judy Crow, et al, at SRI. It is a simple phone book specification. We will not bother to follow their versions closely, but will instead present a style of specification natural for ACL2.
The idea is to model an electronic phone book with the following properties.
Our phone book will store the phone numbers of a city.
It must be possible to retrieve a phone number, given a name.
It must be possible to add and delete entries.
Of course, there are numerous ways to construct such a model. A
natural approach within the Lisp/ACL2 context is to use
``association lists'' or ``alists.'' Briefly, an alist is a list of
pairs (key . value) associating a value with a key. A phone
book could be an alist of pairs (name . pnum). To find the phone
number associated with a given name, we merely search the alist
until we find the appropriate pair. For a large city, such a linear
list would not be efficient, but at this point we are interested
only in modeling the problem, not in deriving an efficient
implementation. We could address that question later by proving our
alist model equivalent, in some desired sense, to a more efficient
data structure.
We could build a theory of alists from scratch, or we can use a
previously constructed theory (book) of alist definitions and facts.
By using an existing book, we build upon the work of others, start
our specification and proof effort from a much richer foundation,
and hopefully devote more of our time to the problem at hand.
Unfortunately, it is not completely simple for the new user to know
what books are available and what they contain. We hope later
to improve the documentation of the growing collection of books
available with the ACL2 distribution; for now, the reader is
encouraged to look in the README file in the books subdirectory.
For present purposes, the beginning user can simply take our word
that a book exists containing useful alist definitions and facts.
On our local machine, these definitions and lemmas can be introduced
into the current theory using the command:
This book has been ``certified,'' which means that the definitions and lemmas have been mechanically checked and stored in a safe manner. (See books and see include-book for details.)(include-book "/slocal/src/acl2/v1-9/books/public/alist-defthms")
Including this book makes available a collection of functions including the following:
Along with these function definitions, the book also provides a number of proved lemmas that aid in simplifying expressions involving these functions. (See rule-classes for the way in which lemmas are used in simplification and rewriting.) For example,(ALISTP A) ; is A an alist (actually a primitive ACL2 function)
(BIND X V A) ; associate the key X with value V in alist A
(BINDING X A) ; return the value associated with key X in alist A
(BOUND? X A) ; is key X associated with any value in alist A
(DOMAIN A) ; return the list of keys bound in alist A
(RANGE A) ; return the list of values bound to keys in alist A
(REMBIND X A) ; remove the binding of key X in alist A
asserts that(defthm bound?-bind (equal (bound? x (bind y v a)) (or (equal x y) (bound? x a))))
x will be bound in (bind y v a) if and only if:
either x = y or x was already bound in a. Also,
asserts that the resulting binding will be(defthm binding-bind (equal (binding x (bind y v a)) (if (equal x y) v (binding x a))))
v, if x = y, or the
binding that x had in a already, if not.Thus, the inclusion of this book essentially extends our specification and reasoning capabilities by the addition of new operations and facts about these operations that allow us to build further specifications on a richer and possibly more intuitive foundation.
However, it must be admitted that the use of a book such as this has two potential limitations:
For example, what is the value ofthe definitions available in a book may not be ideal for your particular problem;
it is (extremely) likely that some useful facts (especially, rewrite rules) are not available in the book and will have to be proved.
binding when given a key that
is not bound in the alist? We can find out by examining the
function definition. Look at the definition of the binding
function (or any other defined function), using the :pe command:
ACL2 !>:pe binding d 33 (INCLUDE-BOOK "/slocal/src/acl2/v1-9/books/public/alist-defthms") >V d (DEFUN BINDING (X A) "The value bound to X in alist A." (DECLARE (XARGS :GUARD (ALISTP A))) (CDR (ASSOC-EQUAL X A)))
This tells us that binding was introduced by the given
include-book form, is currently disabled in the current
theory, and has the definition given by the displayed defun form.
We see that binding is actually defined in terms of the primitive
assoc-equal function. If we look at the definition of
assoc-equal:
ACL2 !>:pe assoc-equal V -489 (DEFUN ASSOC-EQUAL (X ALIST) (DECLARE (XARGS :GUARD (ALISTP ALIST))) (COND ((ENDP ALIST) NIL) ((EQUAL X (CAR (CAR ALIST))) (CAR ALIST)) (T (ASSOC-EQUAL X (CDR ALIST)))))
we can see that assoc-equal returns nil upon reaching the end
of an unsuccessful search down the alist. So binding returns
(cdr nil) in that case, which is nil. Notice that we could also
have investigated this question by trying some simple examples.
ACL2 !>(binding 'a nil) NIL
ACL2 !>(binding 'a (list (cons 'b 2))) NIL
These definitions aren't ideal for all purposes. For one thing,
there's nothing that keeps us from having nil as a value bound to
some key in the alist. Thus, if binding returns nil we don't
always know if that is the value associated with the key in the
alist, or if that key is not bound. We'll have to keep that
ambiguity in mind whenever we use binding in our specification.
Suppose instead that we wanted binding to return some error
string on unbound keys. Well, then we'd just have to write our own
version of binding. But then we'd lose much of the value of
using a previously defined book. As with any specification
technique, certain tradeoffs are necessary.
Why not take a look at the definitions of other alist functions and see how they work together to provide the ability to construct and search alists? We'll be using them rather heavily in what follows so it will be good if you understand basically how they work. Simply start up ACL2 and execute the form shown earlier, but substituting our directory name for the top-level ACL2 directory with yours. Alternatively, the following should work if you start up ACL2 in the directory of the ACL2 sources:
Then, you can use(include-book (:relative "books" "public" "alist-defthms"))
:pe to look at function definitions.
You'll soon discover that almost all of the definitions are built on
definitions of other, more primitive functions, as binding is
built on assoc-equal. You can look at those as well, of course,
or in many cases visit their documentation.
The other problem with using a predefined book is that it will
seldom be ``sufficiently complete,'' in the sense that the
collection of rewrite rules supplied won't be adequate to prove
everything we'd like to know about the interactions of the various
functions. If it were, there'd be no real reason to know that
binding is built on top of assoc-equal, because everything
we'd need to know about binding would be nicely expressed in the
collection of theorems supplied with the book. However, that's very
seldom the case. Developing such a collection of rules is currently
more art than science and requires considerable experience. We'll
encounter examples later of ``missing'' facts about binding and
our other alist functions. So, let's get on with the example.
Notice that alists are mappings of keys to values; but, there is no
notion of a ``type'' associated with the keys or with the values.
Our phone book example, however, does have such a notion of types;
we map names to phone numbers. We can introduce these ``types'' by
explicitly defining them, e.g., names are strings and phone numbers
are integers. Alternatively, we can partially define or
axiomatize a recognizer for names without giving a full definition.
A way to safely introduce such ``constrained'' function symbols in
ACL2 is with the encapsulate form. For example, consider the
following form.
(encapsulate ;; Introduce a recognizer for names with a ``type'' lemma. ((namep (x) t)) ;; (local (defun namep (x) ;; This declare is needed to tell ;; ACL2 that we're aware that the ;; argument x is not used in the body ;; of the function. (declare (ignore x)) t)) ;; (defthm namep-booleanp (booleanp (namep x))))
This encapsulate form introduces the new function namep of one
argument and one result and constrains (namep x) to be Boolean,
for all inputs x. More generally, an encapsulation establishes
an environment in which functions can be defined and theorems and
rules added without necessarily introducing those functions,
theorems, and rules into the environment outside the encapsulation.
To be admissible, all the events in the body of an encapsulate must be
admissible. But the effect of an encapsulate is to assume only the
non-local events.
The first ``argument'' to encapsulate, ((namep (x) t)) above,
declares the intended signatures of new function symbols that
will be ``exported'' from the encapsulation without definition. The
local defun of name defines name within the encapsulation
always to return t. The defthm event establishes that
namep is Boolean. By making the defun local but the defthm
non-local this encapsulate constrains the undefined function
namep to be Boolean; the admissibility of the encapsulation
establishes that there exists a Boolean function (namely the
constant function returning t).
We can subsequently use namep as we use any other Boolean
function, with the proviso that we know nothing about it except that
it always returns either t or nil. We use namep to
``recognize'' legal keys for our phonebook alist.
We wish to do something similar to define what it means to be a legal phone number. We submit the following form to ACL2:
This introduces a Boolean-valued recognizer(encapsulate ;; Introduce a recognizer for phone numbers. ((pnump (x) t)) ;; (local (defun pnump (x) (not (equal x nil)))) ;; (defthm pnump-booleanp (booleanp (pnump x))) ;; (defthm nil-not-pnump (not (pnump nil)))).
pnump, with the
additional proviso that the constant nil is not a pnump. We
impose this restriction to guarantee that we'll never bind a name to
nil in our phone book and thereby introduce the kind of ambiguity
described above regarding the use of binding.
Now a legal phone book is an alist mapping from nameps to
pnumps. We can define this as follows:
Thus, a phone book is really a list of pairs(defun name-phonenum-pairp (x) ;; Recognizes a pair of (name . pnum). (and (consp x) (namep (car x)) (pnump (cdr x))))
(defun phonebookp (l) ;; Recognizes a list of such pairs. (if (not (consp l)) (null l) (and (name-phonenum-pairp (car l)) (phonebookp (cdr l)))))
(name . pnum).
Notice that we have not assumed that the keys of the phone book are
distinct. We'll worry about that question later. (It is not always
desirable to insist that the keys of an alist be distinct. But it
may be a useful requirement for our specific example.)Now we are ready to define some of the functions necessary for our phonebook example. The functions we need are:
(IN-BOOK? NM BK) ; does NM have a phone number in BK
(FIND-PHONE NM BK) ; find NM's phone number in phonebook BK
(ADD-PHONE NM PNUM BK) ; give NM the phone number PNUM in BK
(CHANGE-PHONE NM PNUM BK) ; change NM's phone number to PNUM in BK
(DEL-PHONE NM PNUM) ; remove NM's phone number from BK
Given our underlying theory of alists, it is easy to write these functions. But we must take care to specify appropriate ``boundary'' behavior. Thus, what behavior do we want when, say, we try to change the phone number of a client who is not currently in the book? As usual, there are numerous possibilities; here we'll assume that we return the phone book unchanged if we try anything ``illegal.''
Possible definitions of our phone book functions are as follows.
(Remember, an include-book form such as the ones shown earlier
must be executed in order to provide definitions for functions such
as bound?.)
Notice that we don't have to check whether a name is in the book before deleting, because(defun in-book? (nm bk) (bound? nm bk))
(defun find-phone (nm bk) (binding nm bk))
(defun add-phone (nm pnum bk) ;; If nm already in-book?, make no change. (if (in-book? nm bk) bk (bind nm pnum bk)))
(defun change-phone (nm pnum bk) ;; Make a change only if nm already has a phone number. (if (in-book? nm bk) (bind nm pnum bk) bk))
(defun del-phone (nm bk) ;; Remove the binding from bk, if there is one. (rembind nm bk))
rembind is essentially a no-op if nm
is not bound in bk.In some sense, this completes our specification. But we can't have any real confidence in its correctness without validating our specification in some way. One way to do so is by proving some properties of our specification. Some candidate properties are:
1. A name will be in the book after we add it.
2. We will find the most recently added phone number for a client.
3. If we change a number, we'll find the change.
4. Changing and then deleting a number is the same as just deleting.
5. A name will not be in the book after we delete it.
Let's formulate some of these properties. The first one, for example, is:
You may wonder why we didn't need any hypotheses about the ``types'' of the arguments. In fact,(defthm add-in-book (in-book? nm (add-phone nm pnum bk))).
add-in-book is really expressing a
property that is true of alists in general, not just of the
particular variety of alists we are dealing with. Of course, we
could have added some extraneous hypotheses and proved:
but that would have yielded a weaker and less useful lemma because it would apply to fewer situations. In general, it is best to state lemmas in the most general form possible and to eliminate unnecessary hypotheses whenever possible. The reason for that is simple: lemmas are usually stored as rules and used in later proofs. For a lemma to be used, its hypotheses must be relieved (proved to hold in that instance); extra hypotheses require extra work. So we avoid them whenever possible.(defthm add-in-book (implies (and (namep nm) (pnump pnum) (phonebookp bk)) (in-book? nm (add-phone nm pnum bk)))),
There is another, more important observation to make about our
lemma. Even in its simpler form (without the extraneous
hypotheses), the lemma add-in-book may be useless as a
rewrite rule. Notice that it is stated in terms of the
non-recursive functions in-book? and add-phone. If such
functions appear in the left hand side of the conclusion of a lemma,
the lemma may not ever be used. Suppose in a later proof, the
theorem prover encountered a term of the form:
Since we've already proved(in-book? nm (add-phone nm pnum bk)).
add-in-book, you'd expect that this
would be immediately reduced to true. However, the theorem prover
will often ``expand'' the non-recursive definitions of in-book?
and add-phone using their definitions before it attempts
rewriting with lemmas. After this expansion, lemma add-in-book
won't ``match'' the term and so won't be applied. Look back at
the proof script for add-in-proof and you'll notice that at the
very end the prover warned you of this potential difficulty when it
printed:
The ``Warnings'' line notifies you that there are non-recursive function calls in the left hand side of the conclusion and that this problem might arise. Of course, it may be that you don't ever plan to use the lemma for rewriting or that your intention is to disable these functions. Disabled functions are not expanded and the lemma should apply. However, you should always take note of such warnings and consider an appropriate response. By the way, we noted above thatWarnings: Non-rec Time: 0.18 seconds (prove: 0.05, print: 0.00, other: 0.13) ADD-IN-BOOK
binding is disabled. If it
were not, none of the lemmas about binding in the book we
included would likely be of much use for exactly the reason we just
gave.
For our current example, let's assume that we're just investigating
the properties of our specifications and not concerned about using
our lemmas for rewriting. So let's go on. If we really want to
avoid the warnings, we can add :rule-classes nil to each
defthm event; see rule-classes.
Property 2 is: we always find the most recently added phone number for a client. Try the following formalization:
and you'll find that the proof attempt fails. Examining the proof attempt and our function definitions, we see that the lemma is false if(defthm find-add-first-cut (equal (find-phone nm (add-phone nm pnum bk)) pnum))
nm is already in the book. We can remedy this situation by
reformulating our lemma in at least two different ways:
For technical reasons, lemmas such as(defthm find-add1 (implies (not (in-book? nm bk)) (equal (find-phone nm (add-phone nm pnum bk)) pnum)))
(defthm find-add2 (equal (find-phone nm (add-phone nm pnum bk)) (if (in-book? nm bk) (find-phone nm bk) pnum)))
find-add2, i.e., which do
not have hypotheses, are usually slightly preferable. This lemma is
stored as an ``unconditional'' rewrite rule (i.e., has no
hypotheses) and, therefore, will apply more often than find-add1.
However, for our current purposes either version is all right.Property 3 says: If we change a number, we'll find the change. This is very similar to the previous example. The formalization is as follows.
Property 4 says: changing and then deleting a number is the same as just deleting. We can model this as follows.(defthm find-change (equal (find-phone nm (change-phone nm pnum bk)) (if (in-book? nm bk) pnum (find-phone nm bk))))
Unfortunately, when we try to prove this, we encounter subgoals that seem to be true, but for which the prover is stumped. For example, consider the following goal. (Note:(defthm del-change (equal (del-phone nm (change-phone nm pnum bk)) (del-phone nm bk)))
endp holds of lists that
are empty.)
Our intuition aboutSubgoal *1/4 (IMPLIES (AND (NOT (ENDP BK)) (NOT (EQUAL NM (CAAR BK))) (NOT (BOUND? NM (CDR BK))) (BOUND? NM BK)) (EQUAL (REMBIND NM (BIND NM PNUM BK)) (REMBIND NM BK))).
rembind and bind tells us that this goal
should be true even without the hypotheses. We attempt to prove the
following lemma.
The prover proves this by induction, and stores it as a rewrite rule. After that, the prover has no difficulty in proving(defthm rembind-bind (equal (rembind nm (bind nm pnum bk)) (rembind nm bk)))
del-change.
The need to prove lemma rembind-bind illustrates a point we made
early in this example: the collection of rewrite rules
supplied by a previously certified book will almost never be
everything you'll need. It would be nice if we could operate purely
in the realm of names, phone numbers, and phone books without ever
having to prove any new facts about alists. Unfortunately, we
needed a fact about the relation between rembind and bind that
wasn't supplied with the alists theory. Hopefully, such omissions
will be rare.
Finally, let's consider our property 5 above: a name will not be in the book after we delete it. We formalize this as follows:
This proves easily. But notice that it's only true because(defthm in-book-del (not (in-book? nm (del-phone nm bk))))
del-phone (actually rembind) removes all occurrences of a
name from the phone book. If it only removed, say, the first one it
encountered, we'd need a hypothesis that said that nm occurs at
most once in bk. Ah, maybe that's a property you hadn't
considered. Maybe you want to ensure that any name occurs at
most once in any valid phonebook.To complete this example, let's consider adding an invariant to our specification. In particular, suppose we want to assure that no client has more than one associated phone number. One way to ensure this is to require that the domain of the alist is a ``set'' (has no duplicates).
Now, we want to show under what conditions our operations preserve the property of being a(defun setp (l) (if (atom l) (null l) (and (not (member-equal (car l) (cdr l))) (setp (cdr l)))))
(defun valid-phonebookp (bk) (and (phonebookp bk) (setp (domain bk))))
valid-phonebookp. The operations
in-book? and find-phone don't return a phone book, so we
don't really need to worry about them. Since we're really
interested in the ``types'' of values preserved by our phonebook
functions, let's look at the types of those operations as well.
Note the ``(defthm in-book-booleanp (booleanp (in-book? nm bk)))
(defthm in-book-namep (implies (and (phonebookp bk) (in-book? nm bk)) (namep nm)) :hints (("Goal" :in-theory (enable bound?))))
(defthm find-phone-pnump (implies (and (phonebookp bk) (in-book? nm bk)) (pnump (find-phone nm bk))) :hints (("Goal" :in-theory (enable bound? binding))))
:hints'' on the last two lemmas. Neither of these
would prove without these hints, because once again there are
some facts about bound? and binding not available in our
current context. Now, we could figure out what those facts are and
try to prove them. Alternatively, we can enable bound? and
binding and hope that by opening up these functions, the
conjectures will reduce to versions that the prover does know enough
about or can prove by induction. In this case, this strategy works.
The hints tell the prover to enable the functions in question
when considering the designated goal.
Below we develop the theorems showing that add-phone,
change-phone, and del-phone preserve our proposed invariant.
Notice that along the way we have to prove some subsidiary facts,
some of which are pretty ugly. It would be a good idea for you to
try, say, add-phone-preserves-invariant without introducing the
following four lemmas first. See if you can develop the proof and
only add these lemmas as you need assistance. Then try
change-phone-preserves-invariant and del-phone-preserves-invariant.
They will be easier. It is illuminating to think about why
del-phone-preserves-invariant does not need any ``type''
hypotheses.
(defthm bind-preserves-phonebookp (implies (and (phonebookp bk) (namep nm) (pnump num)) (phonebookp (bind nm num bk)))) (defthm member-equal-strip-cars-bind (implies (and (not (equal x y)) (not (member-equal x (strip-cars a)))) (not (member-equal x (strip-cars (bind y z a)))))) (defthm bind-preserves-domain-setp (implies (and (alistp bk) (setp (domain bk))) (setp (domain (bind nm num bk)))) :hints (("Goal" :in-theory (enable domain)))) (defthm phonebookp-alistp (implies (phonebookp bk) (alistp bk))) (defthm ADD-PHONE-PRESERVES-INVARIANT (implies (and (valid-phonebookp bk) (namep nm) (pnump num)) (valid-phonebookp (add-phone nm num bk))) :hints (("Goal" :in-theory (disable domain-bind)))) (defthm CHANGE-PHONE-PRESERVES-INVARIANT (implies (and (valid-phonebookp bk) (namep nm) (pnump num)) (valid-phonebookp (change-phone nm num bk))) :hints (("Goal" :in-theory (disable domain-bind)))) (defthm remove-equal-preserves-setp (implies (setp l) (setp (remove-equal x l)))) (defthm rembind-preserves-phonebookp (implies (phonebookp bk) (phonebookp (rembind nm bk)))) (defthm DEL-PHONE-PRESERVES-INVARIANT (implies (valid-phonebookp bk) (valid-phonebookp (del-phone nm bk))))
As a final test of your understanding, try to formulate and prove an invariant that says that no phone number is assigned to more than one name. The following hints may help.
1. Define the appropriate invariant. (Hint: remember the function
range.)2. Do our current definitions of
add-phoneandchange-phonenecessarily preserve this property? If not, consider what hypotheses are necessary in order to guarantee that they do preserve this property.3. Study the definition of the function
rangeand notice that it is defined in terms of the functionstrip-cdrs. Understand how this defines the range of an alist.4. Formulate the correctness theorems and attempt to prove them. You'll probably benefit from studying the invariant proof above. In particular, you may need some fact about the function
strip-cdrsanalogous to the lemmamember-equal-strip-cars-bindabove.
Below is one solution to this exercise. Don't look at the solution,
however, until you've struggled a bit with it. Notice that we
didn't actually change the definitions of add-phone and
change-phone, but added a hypothesis saying that the number is
``new.'' We could have changed the definitions to check this and
return the phonebook unchanged if the number was already in use.
(defun pnums-in-use (bk) (range bk)) (defun phonenums-unique (bk) (setp (pnums-in-use bk))) (defun new-pnump (pnum bk) (not (member-equal pnum (pnums-in-use bk)))) (defthm member-equal-strip-cdrs-rembind (implies (not (member-equal x (strip-cdrs y))) (not (member-equal x (strip-cdrs (rembind z y)))))) (defthm DEL-PHONE-PRESERVES-PHONENUMS-UNIQUE (implies (phonenums-unique bk) (phonenums-unique (del-phone nm bk))) :hints (("Goal" :in-theory (enable range)))) (defthm strip-cdrs-bind-non-member (implies (and (not (bound? x a)) (alistp a)) (equal (strip-cdrs (bind x y a)) (append (strip-cdrs a) (list y)))) :hints (("Goal" :in-theory (enable bound?)))) (defthm setp-append-list (implies (setp l) (equal (setp (append l (list x))) (not (member-equal x l))))) (defthm ADD-PHONE-PRESERVES-PHONENUMS-UNIQUE (implies (and (phonenums-unique bk) (new-pnump pnum bk) (alistp bk)) (phonenums-unique (add-phone nm pnum bk))) :hints (("Goal" :in-theory (enable range)))) (defthm member-equal-strip-cdrs-bind (implies (and (not (member-equal z (strip-cdrs a))) (not (equal z y))) (not (member-equal z (strip-cdrs (bind x y a)))))) (defthm CHANGE-PHONE-PRESERVES-PHONENUMS-UNIQUE (implies (and (phonenums-unique bk) (new-pnump pnum bk) (alistp bk)) (phonenums-unique (change-phone nm pnum bk))) :hints (("Goal" :in-theory (enable range))))
Major Section: TUTORIAL-EXAMPLES
This example illustrates the use of defun-sk and defthm
events to reason about quantifiers. See defun-sk.
Many users prefer to avoid the use of quantifiers, since ACL2 provides only very limited support for reasoning about quantifiers.
Here is a list of events that proves that if there are arbitrarily
large numbers satisfying the disjunction (OR P R), then either
there are arbitrarily large numbers satisfying P or there are
arbitrarily large numbers satisfying R.
; Introduce undefined predicates p and r. (defstub p (x) t) (defstub r (x) t)
; Define the notion that something bigger than x satisfies p. (defun-sk some-bigger-p (x) (exists y (and (< x y) (p y))))
; Define the notion that something bigger than x satisfies r. (defun-sk some-bigger-r (x) (exists y (and (< x y) (r y))))
; Define the notion that arbitrarily large x satisfy p. (defun-sk arb-lg-p () (forall x (some-bigger-p x)))
; Define the notion that arbitrarily large x satisfy r. (defun-sk arb-lg-r () (forall x (some-bigger-r x)))
; Define the notion that something bigger than x satisfies p or r. (defun-sk some-bigger-p-or-r (x) (exists y (and (< x y) (or (p y) (r y)))))
; Define the notion that arbitrarily large x satisfy p or r. (defun-sk arb-lg-p-or-r () (forall x (some-bigger-p-or-r x)))
; Prove the theorem promised above. Notice that the functions open ; automatically, but that we have to provide help for some rewrite ; rules because they have free variables in the hypotheses. The ; ``witness functions'' mentioned below were introduced by DEFUN-SK.
(thm (implies (arb-lg-p-or-r) (or (arb-lg-p) (arb-lg-r))) :hints (("Goal" :use ((:instance some-bigger-p-suff (x (arb-lg-p-witness)) (y (some-bigger-p-or-r-witness (max (arb-lg-p-witness) (arb-lg-r-witness))))) (:instance some-bigger-r-suff (x (arb-lg-r-witness)) (y (some-bigger-p-or-r-witness (max (arb-lg-p-witness) (arb-lg-r-witness))))) (:instance arb-lg-p-or-r-necc (x (max (arb-lg-p-witness) (arb-lg-r-witness))))))))
; And finally, here's a cute little example. We have already ; defined above the notion (some-bigger-p x), which says that ; something bigger than x satisfies p. Let us introduce a notion ; that asserts that there exists both y and z bigger than x which ; satisfy p. On first glance this new notion may appear to be ; stronger than the old one, but careful inspection shows that y and ; z do not have to be distinct. In fact ACL2 realizes this, and ; proves the theorem below automatically.
(defun-sk two-bigger-p (x) (exists (y z) (and (< x y) (p y) (< x z) (p z))))
(thm (implies (some-bigger-p x) (two-bigger-p x)))
; A technical point: ACL2 fails to prove the theorem above ; automatically if we take its contrapositive, unless we disable ; two-bigger-p as shown below. That is because ACL2 needs to expand ; some-bigger-p before applying the rewrite rule introduced for ; two-bigger-p, which contains free variables. The moral of the ; story is: Don't expect too much automatic support from ACL2 for ; reasoning about quantified notions.
(thm (implies (not (two-bigger-p x)) (not (some-bigger-p x))) :hints (("Goal" :in-theory (disable two-bigger-p))))
Major Section: TUTORIAL-EXAMPLES
The following examples are more advanced examples of usage of ACL2. They are included largely for reference, in case someone finds them useful.
Major Section: TUTORIAL5-MISCELLANEOUS-EXAMPLES
This example illustrates the use of ACL2's IO primitives to read the forms in a file. See io.
This example provides a solution to the following problem. Let's
say that you have a file that contains s-expressions. Suppose that
you want to build a list by starting with nil, and updating it
``appropriately'' upon encountering each successive s-expression in
the file. That is, suppose that you have written a function
update-list such that (update-list obj current-list) returns
the list obtained by ``updating'' current-list with the next
object, obj, encountered in the file. The top-level function for
processing such a file, returning the final list, could be defined
as follows. Notice that because it opens a channel to the given
file, this function modifies state and hence must return state.
Thus it actually returns two values: the final list and the new
state.
The function(defun process-file (filename state) (mv-let (channel state) (open-input-channel filename :object state) (mv-let (result state) (process-file1 nil channel state) ;see below (let ((state (close-input-channel channel state))) (mv result state)))))
process-file1 referred to above takes the currently
constructed list (initially, nil), together with a channel to the
file being read and the state, and returns the final updated
list. Notice that this function is tail recursive. This is
important because many Lisp compilers will remove tail recursion,
thus avoiding the potential for stack overflows when the file
contains a large number of forms.
(defun process-file1 (current-list channel state) (mv-let (eofp obj state) (read-object channel state) (cond (eofp (mv current-list state)) (t (process-file1 (update-list obj current-list) channel state)))))
Major Section: TUTORIAL5-MISCELLANEOUS-EXAMPLES
This note addresses the question: what is the use of guards in ACL2? Although we recommend that beginners try to avoid guards for a while, we hope that the summary here is reasonably self-contained and will provide a reasonable introduction to guards in ACL2. For a more systematic discussion, see guard. For a summary of that topic, see guard-quick-reference.
Before we get into the issue of guards, let us note that there are two important ``modes'':
defun-mode -- ``Does this defun add an axiom (`:logic mode') or not
(`:program mode')?'' (See defun-mode.) Only :logic mode
functions can have their ``guards verified'' via mechanized proof;
see verify-guards.
set-guard-checking -- ``Should runtime guard violations signal an
error (t) or go undetected (nil)? Equivalently, are expressions
evaluated in Common Lisp or in the logic?''
(See set-guard-checking.)
Prompt examples
Here some examples of the relation between the ACL2 prompt and the
``modes'' discussed above. Also see default-print-prompt. The
first examples all have ld-skip-proofsp nil; that is, proofs are
not skipped.
Here are some examples withACL2 !> ; logic mode with guard checking on ACL2 > ; logic mode with guard checking off ACL2 p!> ; program mode with guard checking on ACL2 p> ; program mode with guard checking off
default-defun-mode of :logic.
ACL2 > ; guard checking off, ld-skip-proofsp nil ACL2 s> ; guard checking off, ld-skip-proofsp t ACL2 !> ; guard checking on, ld-skip-proofsp nil ACL2 !s> ; guard checking on, ld-skip-proofsp t
Sample session
ACL2 !>(+ 'abc 3)ACL2 Error in TOP-LEVEL: The guard for the function symbol BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)), is violated by the arguments in the call (+ 'ABC 3).
ACL2 !>:set-guard-checking nil ;;;; verbose output omitted here ACL2 >(+ 'abc 3) 3 ACL2 >(< 'abc 3) T ACL2 >(< 3 'abc) NIL ACL2 >(< -3 'abc) T ACL2 >:set-guard-checking t
Turning guard checking on.
ACL2 !>(defun sum-list (x) (declare (xargs :guard (integer-listp x) :verify-guards nil)) (cond ((endp x) 0) (t (+ (car x) (sum-list (cdr x))))))
The admission of SUM-LIST is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of SUM-LIST is described by the theorem (ACL2-NUMBERP (SUM-LIST X)). We used primitive type reasoning.
Summary Form: ( DEFUN SUM-LIST ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.03) SUM-LIST ACL2 !>(sum-list '(1 2 3)) 6 ACL2 !>(sum-list '(1 2 abc 3))
ACL2 Error in TOP-LEVEL: The guard for the function symbol BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)), is violated by the arguments in the call (+ 'ABC 3).
ACL2 !>:set-guard-checking nil ;;;; verbose output omitted here ACL2 >(sum-list '(1 2 abc 3)) 6 ACL2 >(defthm sum-list-append (equal (sum-list (append a b)) (+ (sum-list a) (sum-list b))))
<< Starting proof tree logging >>
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate.
...
That completes the proof of *1.
Q.E.D.
Guard verification vs. defun
Declare Form Guards Verified?
(declare (xargs :mode :program ...)) no (declare (xargs :guard g)) yes (declare (xargs :guard g :verify-guards nil)) no (declare (xargs ...<no :guard>...)) no
ACL2 >:pe sum-list l 8 (DEFUN SUM-LIST (X) (DECLARE (XARGS :GUARD (INTEGER-LISTP X) :VERIFY-GUARDS NIL)) (COND ((ENDP X) 0) (T (+ (CAR X) (SUM-LIST (CDR X)))))) ACL2 >(verify-guards sum-list) The non-trivial part of the guard conjecture for SUM-LIST, given the :type-prescription rule SUM-LIST, is
Goal (AND (IMPLIES (AND (INTEGER-LISTP X) (NOT (CONSP X))) (EQUAL X NIL)) (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X))) (INTEGER-LISTP (CDR X))) (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X))) (ACL2-NUMBERP (CAR X)))).
...
ACL2 >:pe sum-list lv 8 (DEFUN SUM-LIST (X) (DECLARE (XARGS :GUARD (INTEGER-LISTP X) :VERIFY-GUARDS NIL)) ACL2 >:set-guard-checking t
ACL2 !>(sum-list '(1 2 abc 3))
ACL2 Error in TOP-LEVEL: The guard for the function symbol SUM-LIST, which is (INTEGER-LISTP X), is violated by the arguments in the call (SUM-LIST '(1 2 ABC ...)).
ACL2 !>:set-guard-checking nil
ACL2 >(sum-list '(1 2 abc 3)) 6 ACL2 >:comp sum-list Compiling gazonk0.lsp. End of Pass 1. End of Pass 2. Finished compiling gazonk0.lsp. Loading gazonk0.o start address -T 1bbf0b4 Finished loading gazonk0.o Compiling gazonk0.lsp. End of Pass 1. End of Pass 2. Finished compiling gazonk0.lsp. Loading gazonk0.o start address -T 1bc4408 Finished loading gazonk0.o SUM-LIST ACL2 >:q
Exiting the ACL2 read-eval-print loop. ACL2>(trace sum-list) (SUM-LIST)
ACL2>(lp)
ACL2 Version 1.8. Level 1. Cbd "/slocal/src/acl2/v1-9/". Type :help for help. ACL2 >(sum-list '(1 2 abc 3)) 6 ACL2 >(sum-list '(1 2 3)) 1> (SUM-LIST (1 2 3))> 2> (SUM-LIST (2 3))> 3> (SUM-LIST (3))> 4> (SUM-LIST NIL)> <4 (SUM-LIST 0)> <3 (SUM-LIST 3)> <2 (SUM-LIST 5)> <1 (SUM-LIST 6)> 6 ACL2 >:pe sum-list-append 9 (DEFTHM SUM-LIST-APPEND (EQUAL (SUM-LIST (APPEND A B)) (+ (SUM-LIST A) (SUM-LIST B)))) ACL2 >(verify-guards sum-list-append)
The non-trivial part of the guard conjecture for SUM-LIST-APPEND, given the :type-prescription rule SUM-LIST, is
Goal (AND (TRUE-LISTP A) (INTEGER-LISTP (APPEND A B)) (INTEGER-LISTP A) (INTEGER-LISTP B)).
...
****** FAILED ******* See :DOC failure ****** FAILED ****** ACL2 >(defthm common-lisp-sum-list-append (if (and (integer-listp a) (integer-listp b)) (equal (sum-list (append a b)) (+ (sum-list a) (sum-list b))) t) :rule-classes nil)
<< Starting proof tree logging >>
By the simple :rewrite rule SUM-LIST-APPEND we reduce the conjecture to
Goal' (IMPLIES (AND (INTEGER-LISTP A) (INTEGER-LISTP B)) (EQUAL (+ (SUM-LIST A) (SUM-LIST B)) (+ (SUM-LIST A) (SUM-LIST B)))).
But we reduce the conjecture to T, by primitive type reasoning.
Q.E.D. ;;;; summary omitted here ACL2 >(verify-guards common-lisp-sum-list-append)
The non-trivial part of the guard conjecture for COMMON-LISP-SUM-LIST-APPEND, given the :type-prescription rule SUM-LIST, is
Goal (AND (IMPLIES (AND (INTEGER-LISTP A) (INTEGER-LISTP B)) (TRUE-LISTP A)) (IMPLIES (AND (INTEGER-LISTP A) (INTEGER-LISTP B)) (INTEGER-LISTP (APPEND A B)))).
...
Q.E.D.
That completes the proof of the guard theorem for COMMON-LISP-SUM-LIST-APPEND. COMMON-LISP-SUM-LIST-APPEND is compliant with Common Lisp. ;;;; Summary omitted here. ACL2 >(defthm foo (consp (mv x y)))
...
Q.E.D.
ACL2 >(verify-guards foo)ACL2 Error in (VERIFY-GUARDS FOO): The number of values we need to return is 1 but the number of values returned by the call (MV X Y) is 2.
> (CONSP (MV X Y))
ACL2 Error in (VERIFY-GUARDS FOO): The guards for FOO cannot be verified because the theorem has the wrong syntactic form. See :DOC verify-guards.
Major Section: TUTORIAL5-MISCELLANEOUS-EXAMPLES
Sometimes one wants to reason about mutually recursive functions. Although this is possible in ACL2, it can be a bit awkward. This example is intended to give some ideas about how one can go about such proofs.
For an introduction to mutual recursion in ACL2, see mutual-recursion.
We begin by defining two mutually recursive functions: one that
collects the variables from a term, the other that collects the
variables from a list of terms. We actually imagine the term
argument to be a pseudo-termp; see pseudo-termp.
(mutual-recursionThe idea of the following function is that it suggests a proof by induction in two cases, according to the top-level(defun free-vars1 (term ans) (cond ((atom term) (add-to-set-eq term ans)) ((fquotep term) ans) (t (free-vars1-lst (fargs term) ans))))
(defun free-vars1-lst (lst ans) (cond ((atom lst) ans) (t (free-vars1-lst (cdr lst) (free-vars1 (car lst) ans)))))
)
if structure of
the body. In one case, (atom x) is true, and the theorem to be
proved should be proved under no additional hypotheses except for
(atom x). In the other case, (not (atom x)) is assumed together
with three instances of the theorem to be proved, one for each
recursive call in this case. So, one instance substitutes (car x)
for x; one substitutes (cdr x) for x; and the third substitutes
(cdr x) for x and (free-vars1 (car x) ans) for ans. If you think
about how you would go about a hand proof of the theorem to follow,
you'll come up with a similar scheme.
(defun symbol-listp-free-vars1-induction (x ans)
(if (atom x)
; then we just make sure x and ans aren't considered irrelevant
(list x ans)
(list (symbol-listp-free-vars1-induction (car x) ans)
(symbol-listp-free-vars1-induction (cdr x) ans)
(symbol-listp-free-vars1-induction
(cdr x)
(free-vars1 (car x) ans)))))
We now prove the two theorems together as a conjunction, because the
inductive hypotheses for one are sometimes needed in the proof of
the other (even when you do this proof on paper!).
(defthm symbol-listp-free-vars1
(and (implies (and (pseudo-termp x)
(symbol-listp ans))
(symbol-listp (free-vars1 x ans)))
(implies (and (pseudo-term-listp x)
(symbol-listp ans))
(symbol-listp (free-vars1-lst x ans))))
:hints
(("Goal" :induct (symbol-listp-free-vars1-induction x ans))))
The above works, but let's try for a more efficient proof, which
avoids cluttering the proof with irrelevant (false) inductive
hypotheses.
(ubt 'symbol-listp-free-vars1-induction)We now state the theorem as a conditional, so that it can be proved nicely using the induction scheme that we have just coded. The prover will not store an(defun symbol-listp-free-vars1-induction (flg x ans)
; Flg is non-nil (or t) if we are ``thinking'' of a single term.
(if (atom x) (list x ans) (if flg (symbol-listp-free-vars1-induction nil (cdr x) ans) (list (symbol-listp-free-vars1-induction t (car x) ans) (symbol-listp-free-vars1-induction nil (cdr x) (free-vars1 (car x) ans))))))
if term as a rewrite rule, but that's OK
(as long as we tell it not to try), because we're going to derive
the corollaries of interest later and make them into rewrite
rules.
(defthm symbol-listp-free-vars1-flg
(if flg
(implies (and (pseudo-termp x)
(symbol-listp ans))
(symbol-listp (free-vars1 x ans)))
(implies (and (pseudo-term-listp x)
(symbol-listp ans))
(symbol-listp (free-vars1-lst x ans))))
:hints
(("Goal" :induct (symbol-listp-free-vars1-induction flg x ans)))
:rule-classes nil)
And finally, we may derive the theorems we are interested in as
immediate corollaries.
(defthm symbol-listp-free-vars1
(implies (and (pseudo-termp x)
(symbol-listp ans))
(symbol-listp (free-vars1 x ans)))
:hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
(flg t)))))
(defthm symbol-listp-free-vars1-lst
(implies (and (pseudo-term-listp x)
(symbol-listp ans))
(symbol-listp (free-vars1-lst x ans)))
:hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
(flg nil)))))