A Walking Tour of ACL2

COMMENT: This notebook is written in ACL2 Kernel by TANIGUCHI Masaya, and copied from A Walking Tour of ACL2. The license of original text is described at the end of this note book.

On this tour you will learn a little more about the ACL2 logic, the theorem prover, and the user interface.

This time we will stick with really simple things, such as the associativity of list concatenation.

We assume you have taken the Flying Tour but that you did not necessarily follow all the “off-tour” links because we encouraged you not to. With the Walking Tour we encourage you to visit off-tour links — provided they are not marked with the tiny warning sign (*). But they are “branches” in the tour that lead to “dead ends.” When you reach a dead end, remember to use your browser’s Back Button to return to the Walking Tour to continue.

When you get to the end of the tour we’ll give you a chance to repeat quickly both the Flying and the Walking Tours to visit any off-tour links still of interest.

Common Lisp

Common Lisp

The logic of ACL2 is based on Common Lisp.

Common Lisp is the standard list processing programming language. It is documented in: Guy L. Steele, Common Lisp The Language, Digital Press, 12 Crosby Drive, Bedford, MA 01730, 1990.

ACL2 formalizes only a subset of Common Lisp. It includes such familiar Lisp functions as cons, car and cdr for creating and manipulating list structures, various arithmetic primitives such as +, *, expt and <=, and intern and symbol-name for creating and manipulating symbols. Control primitives include cond, case and if, as well as function call, including recursion. New functions are defined with defun and macros with defmacro. See programming* for a list of the Common Lisp primitives supported by ACL2.

ACL2 supports five of Common Lisp’s datatypes:

  • the precisely represented, unbounded numbers (integers, rationals, and the complex numbers with rational components, called the “complex rationals” here),

  • the characters with ASCII codes between 0 and 255

  • strings of such characters

  • symbols (including packages)

  • conses

ACL2 is a very small subset of full Common Lisp. ACL2 does not include the Common Lisp Object System (CLOS), higher order functions, circular structures, and other aspects of Common Lisp that are non-applicative. Roughly speaking, a language is applicative if it follows the rules of function application. For example, f(x) must be equal to f(x), which means, among other things, that the value of f must not be affected by “global variables” and the object x must not change over time.

An Example Common Lisp Function Definition

Consider the binary trees x and y below.

In Lisp, x is written as the list '(A B) or, equivalently, as '(A B . NIL). Similarly, y may be written '(C D E). Suppose we wish to replace the right-most tip of x by the entire tree y. This is denoted (app x y), where app stands for "append".

We can define app with:

(defun app (x y)                           ; Concatenate x and y. 
  (declare (type (satisfies true-listp) x)); We expect x to end in NIL. 
  (cond ((endp x) y)                       ; If x is empty, return y. 
        (t (cons (car x)                   ; Else, copy first node 
                 (app (cdr x) y)))))       ;  and recur into next.

If you defined this function in some Common Lisp, then to run app the x and y above you could then type

(app '(A B) '(C D E))

and Common Lisp will print the (A B C D E).

An Example of ACL2 in Use

To introduce you to ACL2 we will consider the app function discussed in the Common Lisp page, except we will omit for the moment the declare form, which in ACL2 is called a guard.

Guards are arbitrary ACL2 terms that express the “intended domain” of functions. In that sense, guards are akin to type signatures. However, Common Lisp and ACL2 are untyped programming languages: while the language supports several different data types and the types of objects can be determined by predicates at runtime, any type of object may be passed to any function. Thus, guards are “extra-logical.” Recognizing both the practical and intellectual value of knowing that your functions are applied to the kinds of objects you intend, ACL2 imposes guards on Common Lisp and provides a means of proving that functions are used as intended. But the story is necessarily complicated and we do not recommend it to the new user. Get used to the fact that any ACL2 function may be applied to any objects and program accordingly. Read about guards later.

Here is the definition again

(defun app (x y) 
  (cond ((endp x) y) 
        (t (cons (car x)  
                 (app (cdr x) y)))))

The next few stops along the Walking Tour will show you

The next few stops along the Walking Tour will show you

  • how to use the ACL2 documentation,
  • what happens when the above definition is submitted to ACL2,
  • what happens when you evaluate calls of app,
  • what one simple theorem about app looks like,
  • how ACL2 proves the theorem, and
  • how that theorem can be used in another proof.

Along the way we will talk about the definitional principle, types, the ACL2 read-eval-print loop, and how the theorem prover works.

When we complete this part of the tour we will return briefly to the notion of guard and revisit several of the topics above in that context.

How To Find Out about ACL2 Functions

Most ACL2 primitives are documented. Here is the definition of app again, with the documented topics higlighted. * All of the links below lead into the ACL2 User's Manual. So follow these links if you with, but use your Back Button to return here!

(defun app (x y) 
  (cond ((endp x) y) 
        (t (cons (car x)  
                 (app (cdr x) y)))))

By following the link on endp* we see that it is a Common Lisp function and is defined to be the same as atom*, which recognizes non-conses. But endp has a guard. Since we are ignoring guards for now, we'll ignore the guard issue on endp.

So this definition reads "to app x and y: if x is an atom, return y; otherwise, app (cdr x) and y and then cons (car x) onto that."

How To Find Out about ACL2 Functions (cont)

The ACL2 documentation is also available in Emacs, via the ACL2-Doc browser (see ACL2-Doc)* , allowing you to explore the hyperlinked documentation in the comfort of a text editor that can also interact with ACL2.

In addition, runtime images of ACL2 have the hyperlinked text as a large ACL2 data structure that can be explored with ACL2’s :doc command. If you have ACL2 running, try the command :doc endp.

Another way to find out about ACL2 functions, if you have an ACL2 image available, is to use the command :args* which prints the formals, type, and guard of a function symbol.

Of course, the ACL2 documentation can also be printed out as a very long book but we do not recommend that! See the ACL2 Home Page to download the Postscript.

The admission of App

Now let’s continue with app.

In [1]:
(defun app (x y) 
  (cond ((endp x) y) 
        (t (cons (car x)  
                 (app (cdr x) y))))) 
The admission of APP is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of APP is described by the
theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).  We used primitive
type reasoning.

Summary
Form:  ( DEFUN APP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 APP

The text between the lines above is one interaction with the ACL2 command loop. Interacting with the latest version of ACL2 may not produce the very same output, but we trust you’ll recognize the basics.

Above you see the user’s input and how the system responds. This little example shows you what the syntax looks like and is a very typical successful interaction with the definitional principle.

Let’s look at it a little more closely.

Revisiting the Admission of App

Here is the definition of app again with certain parts highlighted. If you are taking the Walking Tour, please read the text carefully and click on each of the links below, except those marked*. Then come back here.

ACL2 !> (defun app (x y) 
  (cond ((endp x) y) 
        (t (cons (car x)  
                 (app (cdr x) y))))) 

The admission of APP is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  We observe that the type of APP is described by the
theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).  We used primitive
type reasoning.

Summary
Form:  ( DEFUN APP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 APP

COMMENT: As I could not add link to code blocks, I listed links you need to visit.

Evaluating App on Sample Input

In [2]:
(app nil '(x y z))
(X Y Z)
In [3]:
(app '(1 2 3) '(4 5 6 7)) 
(1 2 3 4 5 6 7)
In [4]:
(app '(a b c d e f g) '(x y z)) 
; click http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Conversion for an explanation
(A B C D E F G X Y Z)
In [5]:
(app (app '(1 2) '(3 4)) '(5 6))
(1 2 3 4 5 6)
In [6]:
(app '(1 2) (app '(3 4) '(5 6))) 
(1 2 3 4 5 6)
In [7]:
(let ((a '(1 2)) 
      (b '(3 4)) 
      (c '(5 6))) 
  (equal (app (app a b) c) 
         (app a (app b c)))) 
T

As we can see from these examples, ACL2 functions can be executed more or less as Common Lisp.

The last three examples suggest an interesting property of app

The Associativity of App

Observe that, for the particular a, b, and c above, (app (app a b) c) returns the same thing as (app a (app b c)). Perhaps app is associative. Of course, to be associative means that the above property must hold for all values of a, b, and c, not just the ones tested above.

Wouldn't it be cool if you could type

In [9]:
(equal (app (app a b) c) 
       (app a (app b c))) 
ACL2 Error in TOP-LEVEL:  Global variables, such as A, B and C, are
not allowed. See :DOC ASSIGN and :DOC @.

and have ACL2 compute the value T? Well, you can’t! If you try it, you’ll get an error message! The message says we can’t evaluate that form because it contains free variables, i.e., variables not given values. Click here to see the message.

We cannot evaluate a form on an infinite number of cases. But we can prove that a form is a theorem and hence know that it will always evaluate to true.

The Theorem that App is Associative

In [10]:
(defthm associativity-of-app 
   (equal (app (app a b) c) 
          (app a (app b c))))
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.

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.  

We will induct according to a scheme suggested by (APP A B).  This
suggestion was produced using the :induction rule APP.  If we let (:P A B C)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) B C))
              (:P A B C))
     (IMPLIES (ENDP A) (:P A B C))).
This induction is justified by the same argument used to admit APP.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM ASSOCIATIVITY-OF-APP ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  435
 ASSOCIATIVITY-OF-APP

The formula above says app is associative. The defthm* command instructs ACL2 to prove the formula and to name it associativity-of-app. Actually, the defthm command also builds the formula into the database as a rewrite* rule, but we won’t go into that just yet.

What we will consider is how the ACL2 theorem prover proves this formula.

If you proceed you will find the actual output of ACL2 in response to the command above. Some of the text is highlighted for the purposes of the tour. ACL2 does not highlight its output.

You will note that we sometimes highlight a single open parenthesis. This is our way of drawing your attention to the subformula that begins with that parenthesis. By clicking on the parenthesis you will get an explanation of the subformula or its processing.

The Proof of the Associativity of App

Here is the theorem prover’s output when it processes the defthm command for the associativity of app. We have highlighted text for which we offer some explanation, and broken the presentation into several pages. (The most recent version of ACL2 may print slightly different output but the basics are the same.) Just follow the Walking Tour after exploring the explanations.

However, before exploring this (defthm associativity-of-app (equal (app (app a b) c) (app a (app b c))))(defthm associativity-of-app (equal (app (app a b) c) (app a (app b c))))output you should understand that ACL2 users rarely read successful proofs! Instead, they look at certain subgoals printed in failed proofs, figure whether and how those subgoals can be proved, and give ACL2 directions for proving them, usually by simply proving other lemmas. Furthermore, to be a good user of ACL2 you do not have to understand how the theorem prover works. You just have to understand how to interact with it. We explain this in great detail later. But basically all new users are curious to know how ACL2 works and this little tour attempts to give some answers, just to satisfy your curiosity.

ACL2 !> (defthm associativity-of-app 
   (equal (app (app a b) c) 
          (app a (app b c))))

*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.

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.  

We will induct according to a scheme suggested by (APP A B).  This
suggestion was produced using the :induction rule APP.  If we let (:P A B C)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) B C))
              (:P A B C))
     (IMPLIES (ENDP A) (:P A B C))).
This induction is justified by the same argument used to admit APP.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.

Subgoal *1/2 
(IMPLIES (AND (NOT (ENDP A)) 
              (EQUAL (APP (APP (CDR A) B) C) 
                     (APP (CDR A) (APP B C)))) 
         (EQUAL (APP (APP A B) C) 
                (APP A (APP B C)))). 

By the simple :definition ENDP we reduce the conjecture to 

Subgoal *1/2' 
(IMPLIES (AND (CONSP A) 
              (EQUAL (APP (APP (CDR A) B) C) 
                     (APP (CDR A) (APP B C)))) 
         (EQUAL (APP (APP A B) C) 
                (APP A (APP B C)))). 

But simplification reduces this to T, using the :definition APP, the 
:rewrite rules CDR-CONS and CAR-CONS and primitive type reasoning. 

Subgoal *1/1 
(IMPLIES (ENDP A) 
         (EQUAL (APP (APP A B) C) 
                (APP A (APP B C)))). 

By the simple :definition ENDP we reduce the conjecture to 

Subgoal *1/1' 
(IMPLIES (NOT (CONSP A)) 
         (EQUAL (APP (APP A B) C) 
                (APP A (APP B C)))). 

But simplification reduces this to T, using the :definition APP and 
primitive type reasoning. 
*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM ASSOCIATIVITY-OF-APP ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  435
 ASSOCIATIVITY-OF-APP

COMMENT: As I could not add link to code blocks, I listed links you need to visit.

Guiding the ACL2 Theorem Prover

Now that you have seen the theorem prover in action you might be curious as to how you guide it.

Look at the picture above. It is meant to suggest that Q is an important lemma needed for the proof P. Note that to lead the prover to the proof of P the user first proves Q. In a way, the formulation and proof of Q is a hint to the prover about how to prove P.

The user usually doesn't think of Q or recognize the need to prove it separately until he or she sees the theorem prover fail to prove P wihout it "knowing" Q.

The way the user typically discovers the need for Q is to look at failed proofs.

ACL2 as an Interactive Theorem Prover (cont)

When ACL2 proves a lemma, it is converted into one or more rules and stored in a database. The theorem prover is rule-driven. By proving lemmas you can configure ACL2 to behave in certain ways when it is trying to prove formulas in a certain problem domain. The expert user can make ACL2 do amazingly "smart" looking things.

But it would be wrong to think that ACL2 knows the mathematical content of formula just because it has proved it. What ACL2 knows — all ACL2 knows — is what is encoded in its rules. There are many types of rules (see rule-classes*)

Many formuals can be effectively coded as rules. But by the same token, it is possible to encode a formula as a rule that is so ineffective it cannot even prove itself!

The way a formula is stored as a rule is entirely up to the user. That is, you determine how ACL2 should use each formula that it proves.

The most common kind of rule is the rewrite rule. It is so common that if you don't tell ACL2 how to store a formula, it stores it as a rewrite rule.

ACL2 System Archtecture

The user interacts with the theorem prover by giving it definitions, theorems and advice. Most often the advice is about how to store each proved theorem as a rule. Sometimes the advice is about how to prove a specific theorem.

The databese consists of all the rules ACL2 "knows." It is possible to include in the database all of the rules in some certified file of other events. Such certified files are called books*.

Interesting proofs are usually built on top of many boks, some of which are written especially for that problem domain and others of which are about oft--used domains, like arithmetic or list processing. ACL2's distribution includes many books written by users. See the "books" link under the Lemma Libraries and Utilities* link tof the ACL2 home page.

Rewrite Rules are Generated from DEFTHM Events

By reading the documentation of defthm* (and especially of its :rule-classes* argument) you would lean that when we submitted the command

(defthm associativity-of-app 
  (equal (app (app a b) c) 
         (app a (app b c))))

We not only command the system to prove that app is an associative function but

* we commanded it to use that fact as a rewrite rule.

That means that every time the system encounters a term of the form

(app (app x y) z)

it will replace it with

(app x (app y z))

You Must Think about the Use of a Formula as a Rule

This is good and bad.

The good news is that you can program ACL2's simplifier.

The bad news is that when you command ACL2 to prove a theorem you must give some thought to how that theorem is to be used as a rule!

For example, if after proving associativity-of-app as previously shown, you engaged in the mathematically trivial act of proving it again but with the equality reversed, you would have programmed ACL2's rewriter to loop forever.

You can avoid adding any rule by using the command;

In [11]:
(defthm associativity-of-app 
  (equal (app (app a b) c) 
         (app a (app b c))) 
  :rule-classes nil) 
ACL2 Error in ( DEFTHM ASSOCIATIVITY-OF-APP ...):  The name 
ASSOCIATIVITY-OF-APP is in use as a theorem.  The redefinition feature
is currently off.  See :DOC ld-redefinition-action.


Note: ASSOCIATIVITY-OF-APP was previously defined at the top level.


Summary
Form:  ( DEFTHM ASSOCIATIVITY-OF-APP ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)

ACL2 Error in ( DEFTHM ASSOCIATIVITY-OF-APP ...):  See :DOC failure.

******** FAILED ********

Using the Associativity of App to Prove a Trivial Consequence

If we have proved the associativity-of-app rule, then the following theorem is trivial:

In [12]:
(defthm trivial-consequence
  (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
         (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7))))))
ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...):  The previously
added rule ASSOCIATIVITY-OF-APP subsumes a newly proposed :REWRITE
rule generated from TRIVIAL-CONSEQUENCE, in the sense that the old
rule rewrites a more general target.  Because the new rule will be
tried first, it may nonetheless find application.


Q.E.D.

Summary
Form:  ( DEFTHM TRIVIAL-CONSEQUENCE ...)
Rules: ((:REWRITE ASSOCIATIVITY-OF-APP))
Warnings:  Subsume
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  82
 TRIVIAL-CONSEQUENCE

Below we show the proof

ACL2 !>(defthm trivial-consequence 
         (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7) 
                (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7)))))) 

ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...):  The previously 
added rule ASSOCIATIVITY-OF-APP subsumes the newly proposed :REWRITE 
rule TRIVIAL-CONSEQUENCE, in the sense that the old rule rewrites a 
more general target.  Because the new rule will be tried first, it 
may nonetheless find application. 

By the simple :rewrite rule ASSOCIATIVITY-OF-APP we reduce the conjecture 
to 

Goal' 
(EQUAL (APP X1 
            (APP X2 
                 (APP X3 (APP X4 (APP X5 (APP X6 X7)))))) 
       (APP X1 
            (APP X2 
                 (APP X3 (APP X4 (APP X5 (APP X6 X7))))))). 

But we reduce the conjecture to T, by primitive type reasoning. 

Q.E.D. 

Summary 
Form:  ( DEFTHM TRIVIAL-CONSEQUENCE ...) 
Rules: ((:REWRITE ASSOCIATIVITY-OF-APP) 
        (:FAKE-RUNE-FOR-TYPE-SET NIL)) 
Warnings:  Subsume 
Time:  0.20 seconds (prove: 0.02, print: 0.00, other: 0.18) 
 TRIVIAL-CONSEQUENCE

COMMENT: As I could not add link to code blocks, I listed links you need to visit.

You might explore the links before moving on.

The End of the Walking Tour

The completes the Walking Tour.

We intend to document many other parts of the system this way, but we just haven't gotten around to it.

To start the two tours over again from the beginning, click on the icons below. If you are really interested in learning how to use ACL2, we recommend that you repeat each tour at least once more to explore branches of the tour that you might have missed.

If you want to learn how to use the theorem prover, we now recommend that you devote the time necessary to work your way through the extended introduction to how to use the prover.

See introduction-to-the-theorem-prover.

This will explain how to interact with ACL2 and has some sample problems for you to solve including some challenge proofs to make ACL2 find.

We hope you enjoy ACL2. We do.

Matt Kaufmann and J Strother Moore

Appendix: Playground

The Jupyter provides an interactive programming environment. You can run ACL2 code in below cells. Try to review this tour!

In [ ]:
 

License

[Note: The license below is based on the template found July 25, 2014
       at: http://opensource.org/licenses/BSD-3-Clause.  Except as
       otherwise noted, it applies to all files distributed from
       http://www.cs.utexas.edu/users/moore/acl2/current/,
       as well as to all files distributed from
       https://github.com/acl2/acl2 other than those in the
       ACL2 Community Books (the books/ subdirectory).

When a file in the ACL2 Community Books refers to this LICENSE, that file's specified copyright supersedes the copyright shown immediately below.]

Copyright (c) 2020, Regents of the University of Texas All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

  • Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

  • Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

  • Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.