INTRODUCTION

introduction to ACL2
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.

ACL2 !>

If not, you should type (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):

(defun my-app (x y) (if (atom x) y (cons (car x) (my-app x y))))

The system responds with the following message:

ACL2 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.

This means that the system could not find an expression involving the formal parameters 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):

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

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.)

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 of my-app get smaller in recursion. Actually, the theorem prover proved several theorems to admit my-app. The main one was that when (atom x) is false the acl2-count of (cdr x) is less than (in the e0-ord-< sense) the acl2-count of x. Acl2-count is 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-app will 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,

ACL2 !>:pe my-app L 73:x(DEFUN MY-APP (X Y) (IF (ATOM X) Y (CONS (CAR X) (MY-APP (CDR X) Y))))

This displays the definition along with some other relevant information. In this case, we know that this definition was processed in :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.

(defthm my-app-length (equal (len (my-app x y)) (+ (len x) (len y))))

First of all, how did we know about the functions 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?

(defthm my-app-length2 (equal (+ (len x) (len y)) (len (my-app x y)))).

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 (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

(in-theory (disable my-app-length)),

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 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.













































































STARTUP

How to start using ACL2; the ACL2 command loop
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.

ACL2 !>

If not, you should type (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.)

ACL2 !>(defun my-cons (x y) (cons x y))

An easy theorem may then be proved: the car of (my-cons a b) is A.

ACL2 !>(defthm car-my-cons (equal (car (my-cons a b)) a))

Notice that unlike Nqthm, the theorem command is 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.

ACL2 !>:pe my-cons

Also see pe. We may also view all the lemmas that rewrite terms whose top function symbol is car by using the following command, whose output will refer to the lemma car-my-cons proved above.

ACL2 !>:pl car

Also see pl. Finally, we may print all the commands back through the initial world as follows.

ACL2 !>:pbt 0

See history for a list of commands, including these, for viewing the current ACL2 world.

Continue with the documentation for tutorial-examples to see a simple but illustrative example in the use of ACL2 for reasoning about functions.













































































TIDBITS

some basic hints for using ACL2
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:

: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

See documentation to learn how to print documentation to the terminal. There are also versions of the documentation for Mosaic, Emacs Info, and hardcopy.

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.













































































TIPS

some hints for using the ACL2 prover
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 Basics

B. 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).

(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))))

One might think that (+ 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

(declare (xargs :measure (nfix (+ 1 i))))

in order to guarantee that the measure will always be an ordinal (in fact, a positive integer).

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:

(defaxiom commutativity-of-+ (equal (+ x y) (+ y x))).

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.

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

(implies p (equal term1 term2))

and

(implies (not p) (equal term1 term3))

consider:

(equal term1 (if p term2 term3))

However, sometimes this strategy can lead to case explosions: 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.













































































TUTORIAL-EXAMPLES

examples of ACL2 usage
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-Examples
You may also wish to visit the other introductory sections, startup and tidbits. These contain further information related to the use of ACL2.

When you feel you have read enough examples, you might want to try the following very simple example on your own. First define the notion of the ``fringe'' of a tree, where we identify trees simply as cons structures, with atoms at the leaves. For example:

ACL2 !>(fringe '((a . b) c . d)) (A B C D)

Next, define the notion of a ``leaf'' of a tree, i.e., a predicate 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).

(defthm leaf-p-iff-member-fringe (iff (leaf-p atm x) (member-equal atm (fringe x))))

For a solution, see solution-to-simple-example.













































































SOLUTION-TO-SIMPLE-EXAMPLE

solution to a simple example
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.

(defun fringe (x) (if (consp x) (append (fringe (car x)) (fringe (cdr x))) (list x)))

Now that 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.

(defun leaf-p (atm x) (if (consp x) (or (leaf-p atm (car x)) (leaf-p atm (cdr x))) (equal atm x)))

The main theorem is now as follows. Note that the rewrite rule below uses the equivalence relation 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))))















































































TUTORIAL1-TOWERS-OF-HANOI

The Towers of Hanoi Example
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.

(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)))))))

Notice that we give 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:

ACL2 !>(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))

From the algorithm it is clear that if it takes 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:

Disks 0 1 2 3 4 5 6 7 ... Moves 0 1 3 7 15 31 63 127 ...

The pattern is fairly clear. To move 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.

(defthm hanoi-moves-required-first-try (equal (len (hanoi a b c n)) (1- (expt 2 n))))

When we submit this to ACL2, the proof attempt fails. Along the way we notice subgoals such as:

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:

(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)))))

and submit it to ACL2 again.

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.)

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))))))

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.

(LEN (APPEND ... ...))

We conjecture that the length of the 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:

(defthm len-append (equal (len (append x y)) (+ (len x) (len y))))

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.

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:

(and (integerp n) (<= 0 n)).

This is an awkward way of saying that 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:

(defmacro naturalp (x) (list 'and (list 'integerp x) (list '<= 0 x)))

Subsequently, we can use (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:

(defthm hanoi-moves-required (implies (naturalp n) (equal (len (hanoi a b c n)) (1- (expt 2 n))))).

Another interesting (but much harder) theorem asserts that the list of moves generated by our 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:

ACL2 !>(1- (expt 2 64)) 18446744073709551615 ACL2 !>

We're guessing they won't finish any time soon.













































































TUTORIAL2-EIGHTS-PROBLEM

The Eights Problem Example
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:

for all n > 7, there exist naturals i and j such that: n = 3i + 5j.

In ACL2, we could phrase this theorem using quantification. However we will start with a constructive approach, i.e., we will show that values of 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:

(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)))))

That is, assuming that 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:

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; ...

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:

(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))))))))

Notice that we explicitly compute the values of 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:

ACL2 !>(split 28) (6 . 2)

ACL2 !>(split 45) (15 . 0)

ACL2 !>(split 335) (110 . 1)

Finally, we submit our theorem 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.

(defun-sk split-able (n) (exists (i j) (equal n (+ (* 3 i) (* 5 j)))))

Then our theorem is given below. Notice that we prove it by observing that our previous function split delivers just such an i and j (as we proved above).

(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)))))))

Unfortunately, understanding the mechanics of the proof requires knowing something about the way defun-sk works. See defun-sk or see Tutorial4-Defun-Sk-Example for more on that subject.













































































TUTORIAL3-PHONEBOOK-EXAMPLE

A Phonebook Specification
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:

(include-book "/slocal/src/acl2/v1-9/books/public/alist-defthms")

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.)

Including this book makes available a collection of functions including the following:

(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

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,

(defthm bound?-bind (equal (bound? x (bind y v a)) (or (equal x y) (bound? x a))))

asserts that x will be bound in (bind y v a) if and only if: either x = y or x was already bound in a. Also,

(defthm binding-bind (equal (binding x (bind y v a)) (if (equal x y) v (binding x a))))

asserts that the resulting binding will be 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:

the 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.

For example, what is the value of 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:

(include-book (:relative "books" "public" "alist-defthms"))

Then, you can use :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:

(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)))).

This introduces a Boolean-valued recognizer 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:

(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)))))

Thus, a phone book is really a list of pairs (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?.)

(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))

Notice that we don't have to check whether a name is in the book before deleting, because 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:

(defthm add-in-book (in-book? nm (add-phone nm pnum bk))).

You may wonder why we didn't need any hypotheses about the ``types'' of the arguments. In fact, 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:

(defthm add-in-book (implies (and (namep nm) (pnump pnum) (phonebookp bk)) (in-book? nm (add-phone nm pnum bk)))),

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.

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:

(in-book? nm (add-phone nm pnum bk)).

Since we've already proved 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:

Warnings: Non-rec Time: 0.18 seconds (prove: 0.05, print: 0.00, other: 0.13) ADD-IN-BOOK

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 that 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:

(defthm find-add-first-cut (equal (find-phone nm (add-phone nm pnum bk)) pnum))

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 nm is already in the book. We can remedy this situation by reformulating our lemma in at least two different ways:

(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)))

For technical reasons, lemmas such as 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.

(defthm find-change (equal (find-phone nm (change-phone nm pnum bk)) (if (in-book? nm bk) pnum (find-phone nm bk))))

Property 4 says: changing and then deleting a number is the same as just deleting. We can model this as follows.

(defthm del-change (equal (del-phone nm (change-phone nm pnum bk)) (del-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: endp holds of lists that are empty.)

Subgoal *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))).

Our intuition about rembind and bind tells us that this goal should be true even without the hypotheses. We attempt to prove the following lemma.

(defthm rembind-bind (equal (rembind nm (bind nm pnum bk)) (rembind nm bk)))

The prover proves this by induction, and stores it as a rewrite rule. After that, the prover has no difficulty in proving 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:

(defthm in-book-del (not (in-book? nm (del-phone nm bk))))

This proves easily. But notice that it's only true because 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).

(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))))

Now, we want to show under what conditions our operations preserve the property of being a 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.

(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))))

Note the ``: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-phone and change-phone necessarily 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 range and notice that it is defined in terms of the function strip-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-cdrs analogous to the lemma member-equal-strip-cars-bind above.

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))))















































































TUTORIAL4-DEFUN-SK-EXAMPLE

example of quantified notions
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))))















































































TUTORIAL5-MISCELLANEOUS-EXAMPLES

miscellaneous ACL2 examples
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.















































































FILE-READING-EXAMPLE

example of reading files in ACL2
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.

(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)))))

The function 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)))))















































































GUARD-EXAMPLE

a brief transcript illustrating guards in ACL2
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.

ACL2 !> ; 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

Here are some examples with 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.















































































MUTUAL-RECURSION-PROOF-EXAMPLE

a small proof about mutually recursive functions
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-recursion

(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)))))

)

The idea of the following function is that it suggests a proof by induction in two cases, according to the top-level 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)

(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))))))

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 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)))))