A Brief ACL2 Tutorial

Matt Kaufmann, Advanced Micro Devices, Inc.
J Strother Moore, Department of Computer Sciences, University of Texas at Austin

Email: kaufmann@cs.utexas.edu and moore@cs.utexas.edu

Abstract

ACL2 is an interactive mechanical theorem prover designed for use in modeling hardware and software and proving properties about those models. This demo is intended to help in getting you started using ACL2. We recommend that you first take at least the beginning of the Flying Demo in order to familiarize yourself with the basics of ACL2, including its Lisp syntax. See also the ACL2 home page for more about ACL2.

Here are the essentials for clicking your way through this demo.

This demo simulates an interactive session with the ACL2 read-eval-print loop. Colors will be used to distinguish user input (red), system output (black), and commentary added for the demo (blue).

We recommend that you navigate by clicking on our links, using your navigator's back and forward buttons, or using your navigator's scroll up and scroll down buttons. Navigation with the slide bar is usually confusing. The demo is best if you size your browser's window so that you can see everything on the row of x's below. The row ends with an exclamation mark; widen your window so you can see it without horizontal scrolling.

The full script for this demo on the Web and you may replay it with your local copy of ACL2.

xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx!

Introduction

Our goal in this demo is to illustrate how to interact with ACL2. This demo therefore differs somewhat from the Flying Demo, which covers a lot more ground by proving a much more diverse and interesting collection of theorems, but does not give much instruction in the use of ACL2. The present demo focuses in considerable detail on a simple problem that is not quite trivial, in order to help the ACL2 beginner get up to speed on using this theorem prover effectively.

The problem. Suppose that for whatever reason, we wish to investigate properties of a reverse function that is defined only using a recursive call and built-in functions endp, cons, car, cdr. The algorithm coded in rev3 below is due to Landin (we believe). The natural encoding of that algorithm is not, however, admissible in the ACL2 logic, because the second and third recursive calls of rev3 (see below) need information about the result of the first recursive call, and at definition time we do not yet have available any properties of rev3.

However, we can get around that problem by defining a more straightforward reverse function, rev, which we use for the second and third recursive calls in rev3. If we can then prove that rev and rev3 agree, we should be able to use rev3 as a ``witness'' to the desired algorithm. Our efforts culiminate in the encapsulate event at the end of this demo, where we show how to introduce into ACL2 a function, triple-rev, whose axiom encodes the desired algorithm.

But first there is a surprising amount of reasoning to do in order to show that rev and rev3 agree. That suits the primary purpose of this demo, which is to illustrate how to interact with the ACL2 prover.

Throughout this demo we use the term ``simplification checkpoint'' to refer to an unproved goal in the proof transcript printed out by ACL2, when that goal is not further simplified. See the ACL2 documentation, topic PROOF-TREE, for information about a tool that takes the user directly to simplification checkpoints.

The slides come in pairs (mostly). The first slide in each pair shows just the input, in red, which the second shows both the input in red and ACL2's response in black. We freely add our own comments, in blue.

Before we start, here is a brief word about an important aspect of our approach to proving theorems with ACL2. The ACL2 documentation topic THE-METHOD describes a process that we illustrate in this demo. As described there, we keep an informal running ``to do list'' of theorems to be proved. Typically there is a main theorem that one has in mind, and initially the to do list consist of just that theorem. Typically ACL2 cannot prove the main theorem by itself, so by thinking about the proof or by observing unproved simplification checkpoints in the prover's output, one comes up with lemmas to prove in support of the proof of the main theorem. These lemmas are pushed onto the to do list (which perhaps would be better termed a ``to do stack.'' The lemma on the top of this stack then gets our attention. We may need to push more lemmas on the stack in order to prove a given lemma, but ultimately the hope is to get ACL2 to prove that lemma. At times some lemmas on the stack need to be modified. Anyhow, we illustrate the use of this stack, or ``to do list,'' during the demo that follows.

Without further ado, let us start:

CLICK HERE TO START.


[top] [prev] [next]

ACL2 !>(in-package "ACL2")

The first form in a certified book must always be an in-package form. Usually the package is "ACL2", but users can define their own packages.


[top] [prev] [next]

ACL2 !>(in-package "ACL2")
 "ACL2"
ACL2 !>


[top] [prev] [next]

ACL2 !>(defun rev (x)
         (if (endp x)
             nil
           (append (rev (cdr x))
                   (list (car x)))))

We begin with the usual definition of a function that reverses a list. As throughout the demo, the slides come in pairs (mostly). This slide shows just input to ACL2, in red. The next slide shows the same input in red, but followed by the resulting ACL2 output, in black. Our comments are added to the session in blue (such as this one).

Again, we recommend that you navigate between slides using the [prev] and [next] links.

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defun rev (x)
         (if (endp x)
             nil
           (append (rev (cdr x))
                   (list (car x)))))

Recursive definitions, such as the one above, carry a proof obligation. Roughly speaking, the obligation is to show that an appropriate measure of the arguments decreases (in an appropriate sense) for each recursive call. Thus, in the present function, ACL2 must prove that the argument (cdr x) of the recursive call is smaller, in an appropriate sense, than is x. The paragraph below is ACL2's way of informing the user that it has carried out such an argument. Experienced ACL2 users rarely find any reason to read that particular commentary.

The admission of REV 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 REV is described by the
theorem (TRUE-LISTP (REV X)).  We used primitive type reasoning and
the :type-prescription rules BINARY-APPEND and TRUE-LISTP-APPEND.

Summary
Form:  ( DEFUN REV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 REV

Next, we set ourselves to the task of definining the function rev3 discussed in the introduction. The comments in blue below the definition are intended to help make sense of it!

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defun rev3 (x)
         (cond
          ((endp x)
           nil)
          ((endp (cdr x))
           (list (car x)))
          (t
           (let* ((b@c (cdr x))
                  (c@rev-b (rev3 b@c)) ; note recursive call of rev3
                  (rev-b (cdr c@rev-b))
                  (b (rev rev-b))      ; note call of rev
                  (a (car x))
                  (a@b (cons a b))
                  (rev-b@a (rev a@b))  ; note call of rev
                  (c (car c@rev-b))
                  (c@rev-b@a (cons c rev-b@a)))
             c@rev-b@a))))

Above, we use variable names that contain the character @ to suggest concatenation, for improved readability. For example, we write c@rev-b to suggest the result of concatenating c to the front of the reverse of b.

In the let* form above, think of x as a@b@c where a and c are single elements. Let* sequentially binds variables. For example, we assign b@c to (cdr x), c@rev-b to the concatenation of c with the reverse of b, and so on.

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defun rev3 (x)
         (cond
          ((endp x)
           nil)
          ((endp (cdr x))
           (list (car x)))
          (t
           (let* ((b@c (cdr x))
                  (c@rev-b (rev3 b@c)) ; note recursive call of rev3
                  (rev-b (cdr c@rev-b))
                  (b (rev rev-b))      ; note call of rev
                  (a (car x))
                  (a@b (cons a b))
                  (rev-b@a (rev a@b))  ; note call of rev
                  (c (car c@rev-b))
                  (c@rev-b@a (cons c rev-b@a)))
             c@rev-b@a))))

The admission of REV3 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 REV3 is described by the
theorem (TRUE-LISTP (REV3 X)).  We used primitive type reasoning and
the :type-prescription rule REV.

Summary
Form:  ( DEFUN REV3 ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION REV))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 REV3
ACL2 !>

We next assign ourselves the following goal: prove that (rev x) equals (rev3 x). Later we will see how that theorem enables us to introduce a function like rev3 that does not ``cheat'' by calling the function rev.

What the heck, why don't we just try letting ACL2 do all the work to prove this theorem, by submitting it now.

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-is-rev3
         (equal (rev x)
                (rev3 x)))

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-is-rev3
         (equal (rev x)
                (rev3 x)))

The theorem prover chooses to prove this theorem by induction, because no other proof technique applies.

The proof eventually fails. Scroll down a few screens, just glancing briefly at the output, until you see some added commentary (in blue).

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

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (REV3 X).  This suggestion
was produced using the :induction rules REV and REV3.  If we let (:P X)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (ENDP (CDR X)))
                   (:P (CDR X)))
              (:P X))
     (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV3.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''

Splitter note (see :DOC splitter) for Subgoal *1/3'' (2 subgoals).
  if-intro: ((:DEFINITION BINARY-APPEND))

Subgoal *1/3.2
Subgoal *1/3.2'
Subgoal *1/3.2''
Subgoal *1/3.2'''
Subgoal *1/3.2'4'
Subgoal *1/3.2'5'
Subgoal *1/3.2'6'
Subgoal *1/3.2'7'
Subgoal *1/3.2'8'

Below is the first simplification checkpoint, that is, the first goal that cannot be simplified (other than the original theorem, actually). You can tell that it cannot be simplified because some other technique is being used on it.

Look carefully at the simplification checkpoint below. Does any term suggest a rewrite rule that would simplify it?


([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/3.2'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X)))
              (CONSP (REV (CDR X))))
         (EQUAL (APPEND (CDR (REV (CDR X)))
                        (LIST (CAR X)))
                (APPEND (REV (REV (CDR (REV (CDR X)))))
                        (LIST (CAR X)))))

*1.1 (Subgoal *1/3.2'8') is pushed for proof by induction.

])

You are welcome to continue scrolling through ACL2's attempt to prove the theorem, which ultimately fails. We recommend that you skip to near the end of the proof attempt.


Subgoal *1/3.1
Subgoal *1/3.1'
Subgoal *1/3.1''
Subgoal *1/3.1'''

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/3.1'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (NOT (REV3 (CDR X))))
         (CONSP (REV (CDR X))))

*1.2 (Subgoal *1/3.1''') is pushed for proof by induction.

])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.2, which is

(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
         (CONSP (REV X2))).
Subgoal *1.2/5
Subgoal *1.2/5'
Subgoal *1.2/4
Subgoal *1.2/4'
Subgoal *1.2/3
Subgoal *1.2/2
Subgoal *1.2/2'
Subgoal *1.2/1

*1.2 is COMPLETED!
Thus key checkpoint Subgoal *1/3.1' is COMPLETED!

We therefore turn our attention to *1.1, which is

(IMPLIES (AND (TRUE-LISTP L2) (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/3''
Subgoal *1.1/3'''
Subgoal *1.1/3'4'
Subgoal *1.1/3'5'
Subgoal *1.1/3'6'
Subgoal *1.1/3'7'

*1.1.1 (Subgoal *1.1/3'7') is pushed for proof by induction.
Subgoal *1.1/2
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
Subgoal *1.1/1'''

*1.1.2 (Subgoal *1.1/1''') is pushed for proof by induction.

So we now return to *1.1.2, which is

(IMPLIES (CONSP X2)
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (LIST X1))).
Subgoal *1.1.2/4
Subgoal *1.1.2/4'
Subgoal *1.1.2/4''
Subgoal *1.1.2/4'''
Subgoal *1.1.2/4'4'
Subgoal *1.1.2/4'5'

Splitter note (see :DOC splitter) for Subgoal *1.1.2/4'5' (2 subgoals).
  if-intro: ((:DEFINITION TRUE-LISTP))

Subgoal *1.1.2/4.2
Subgoal *1.1.2/4.2'
Subgoal *1.1.2/4.2''
Subgoal *1.1.2/4.2'''

*1.1.2.1 (Subgoal *1.1.2/4.2''') is pushed for proof by induction.

Finally we are near the end of the proof attempt!. Scroll down and you will see ACL2 give up, because somehow it has produced the goal of proving nil (false), which is impossible.


Subgoal *1.1.2/4.1
Subgoal *1.1.2/4.1'
Subgoal *1.1.2/4.1''

A goal of NIL, Subgoal *1.1.2/4.1'', has been generated!  Obviously,
the proof attempt has failed.

At this point we do not know whether the theorem we just tried to prove is not a theorem, or whether ACL2 simply needs help in proving it. Did you answer the question above, about whether the first simplification checkpoint suggests a possible rewrite rule? The term


     (REV (REV (CDR (REV (CDR X)))))

from that simplification checkpoint may suggest the rewrite rule on the next slide, which would simplify this term to:

     (CDR (REV (CDR X)))

A large part of the process of using ACL2 successfully is to identify rewrite rules, by inspecting simplification checkpoints of failed proof attempts, that appear simple enough to be provable without too much effort. (How simple the rule is to prove is not always an easy thing to determine, but is sometimes not hard to guess, with experience.) An example is on the next slide,

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-rev
         (equal (rev (rev x))
                x))

As described above, we maintain a stack or ``to do list'' of goals to be proved. Initially the list contained just our main goal, rev-is-rev3, but an analysis of a simplification checkpoint from the preceding proof attempt led us to decide to prove the theorem above. The proof will fail, leading us to a to do list of

(rev-rev
rev-is-rev3)

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-rev
         (equal (rev (rev x))
                x))

The proof below fails, but it is not terribly long. Scroll down through it and see if you can find the first simplification checkpoint.

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

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

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

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X))))
                X))

*1.1 (Subgoal *1/2'7') is pushed for proof by induction.

])
Subgoal *1/1
Subgoal *1/1'
Subgoal *1/1''
Subgoal *1/1'''

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X))

A goal of NIL, Subgoal *1/1''', has been generated!  Obviously, the
proof attempt has failed.

])

Summary
Form:  ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:TYPE-PRESCRIPTION REV))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1351

---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(EQUAL (REV (REV X)) X)

*** Key checkpoints under a top-level induction
    before generating a goal of NIL (see :DOC nil-goal): ***

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X))))
                X))

Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X))

ACL2 Error in ( DEFTHM REV-REV ...):  See :DOC failure.

******** FAILED ********
ACL2 !>

Did you find the first simplification checkpoint above? The next slide reproduces the ACL2 input and output shown on this slide, but contains a comment analyzing that checkpoint.

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-rev
         (equal (rev (rev x))
                x))

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

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

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

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X))))
                X))

*1.1 (Subgoal *1/2'7') is pushed for proof by induction.

])

The goal just above is the first simplification checkpoint. Can you think of a lemma that might lead to a useful simplification of some subterm of the goal above? After thinking about that question, move on to the next slide by scrolling down to the [next] link or clicking here.

Subgoal *1/1
Subgoal *1/1'
Subgoal *1/1''
Subgoal *1/1'''

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X))

A goal of NIL, Subgoal *1/1''', has been generated!  Obviously, the
proof attempt has failed.

])

Summary
Form:  ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:TYPE-PRESCRIPTION REV))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1351

---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(EQUAL (REV (REV X)) X)

*** Key checkpoints under a top-level induction
    before generating a goal of NIL (see :DOC nil-goal): ***

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X))))
                X))

Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X))

ACL2 Error in ( DEFTHM REV-REV ...):  See :DOC failure.

******** FAILED ********
ACL2 !>

The simplification checkpoint above suggests the theorem on the next slide. Our current to do list is (rev-rev rev-is-rev3), and if the next lemma (rev-append) fails then it will be

(rev-append rev-rev
rev-is-rev3)

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-append
         (equal (rev (append x y))
                (append (rev y) (rev x))))

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-append
         (equal (rev (append x y))
                (append (rev y) (rev x))))

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

This proof succeeds!

*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 (APPEND X Y).  This
suggestion was produced using the :induction rules BINARY-APPEND and
REV.  If we let (:P X Y) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
              (:P X Y))
     (IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-APPEND.
When applied to the goal at hand the above induction scheme produces
two nontautological subgoals.
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/2'''
Subgoal *1/2'4'
Subgoal *1/2'5'
Subgoal *1/2'6'

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (APPEND (CDR X) Y))
                     (APPEND (REV Y) (REV (CDR X)))))
         (EQUAL (APPEND (REV (APPEND (CDR X) Y))
                        (LIST (CAR X)))
                (APPEND (REV Y)
                        (REV (CDR X))
                        (LIST (CAR X)))))

*1.1 (Subgoal *1/2'6') is pushed for proof by induction.

])
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.1, which is

(IMPLIES (AND (TRUE-LISTP RV) (TRUE-LISTP RV0))
         (EQUAL (APPEND (APPEND RV0 RV) (LIST X1))
                (APPEND RV0 RV (LIST X1)))).
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/1
Subgoal *1.1/1'

*1.1 and *1 are COMPLETED!
Thus key checkpoints Subgoal *1/2'' and Goal are COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM REV-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION TRUE-LISTP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:INDUCTION REV)
        (:INDUCTION TRUE-LISTP)
        (:REWRITE APPEND-TO-NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION REV)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  2624
 REV-APPEND
ACL2 !>

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-rev
         (equal (rev (rev x))
                x))

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-rev
         (equal (rev (rev x))
                x))

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

Perhaps we can prove *1 by induction.  One induction scheme is suggested
by this conjecture.  

We will induct according to a scheme suggested by (REV X).  This suggestion
was produced using the :induction rule REV.  If we let (:P X) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV.
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'
Subgoal *1/1''
Subgoal *1/1'''

Below is the only simplification checkpoint. It says that every non-cons is nil. Well, 3 (for example) is a non-cons that is not nil. You can see clearly that 3 is a counterexample to the following conjecture by executing the following form, which ACL2 proves:
(thm (IMPLIES (NOT (CONSP 3)) (NOT 3)))
(thm (not (equal (rev (rev 3)) 3)))
So we will add the hypothesis that X is a true list. But first, a question: To what value is (rev (rev 3)) provably equal? How can we check our conjecture with ACL2? One way to do this is shown on the next slide.


([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X))

A goal of NIL, Subgoal *1/1''', has been generated!  Obviously, the
proof attempt has failed.

])

Summary
Form:  ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-CAR-CDR)
        (:REWRITE REV-APPEND))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  375

---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(EQUAL (REV (REV X)) X)

*** Key checkpoint under a top-level induction
    before generating a goal of NIL (see :DOC nil-goal): ***

Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X))

ACL2 Error in ( DEFTHM REV-REV ...):  See :DOC failure.

******** FAILED ********
ACL2 !>

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(thm (equal (rev (rev 3)) nil))

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(thm (equal (rev (rev 3)) nil))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART REV))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  5

Proof succeeded.
ACL2 !>

Well, this use of THM has been a fun diversion, but let us return to our proof. Our to do list at this point is

(rev-rev
rev-is-rev3)

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-rev
         (implies (true-listp x)
                  (equal (rev (rev x))
                         x)))

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-rev
         (implies (true-listp x)
                  (equal (rev (rev x))
                         x)))

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

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  These merge into one derived induction scheme.

We will induct according to a scheme suggested by (REV X).  This suggestion
was produced using the :induction rules REV and TRUE-LISTP.  If we
let (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/1
Subgoal *1/1'

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

Q.E.D.

Summary
Form:  ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:INDUCTION TRUE-LISTP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-CAR-CDR)
        (:REWRITE REV-APPEND))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  447
 REV-REV
ACL2 !>

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(defthm rev-is-rev3
         (equal (rev x)
                (rev3 x)))

[top] [prev] [next]

The proof succeeds! But we got a bit lucky; for example, with the :hints shown below, we can turn off a proof technique used in that proof in order to make the proof fail.

(defthm rev-is-rev3
  (equal (rev x)
         (rev3 x))
	 :hints (("Goal" :do-not '(eliminate-destructors))))

So let's see if we can finish the proof without using destructor elimination.


[top] [prev] [next]

ACL2 !>(defthm rev-is-rev3
         (equal (rev x)
                (rev3 x))
	 :hints (("Goal" :do-not '(eliminate-destructors))))

ACL2 Warning [Subsume] in ( DEFTHM REV-IS-REV3 ...):  A newly proposed
:REWRITE rule generated from REV-IS-REV3 probably subsumes the previously
added :REWRITE rules REV-REV and REV-APPEND, in the sense that the
new rule will now probably be applied whenever the old rules would
have been.


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

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (REV3 X).  This suggestion
was produced using the :induction rules REV and REV3.  If we let (:P X)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (ENDP (CDR X)))
                   (:P (CDR X)))
              (:P X))
     (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV3.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/3'''
Subgoal *1/3'4'

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/3'4'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (NOT (REV3 (CDR X))))
         (CONSP (REV (CDR X))))

*1.1 (Subgoal *1/3'4') is pushed for proof by induction.

])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.1, which is

(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (NOT (REV3 (CDR X))))
         (CONSP (REV (CDR X)))).

No induction schemes are suggested by *1.1.  Consequently, the proof
attempt has failed.

Summary
Form:  ( DEFTHM REV-IS-REV3 ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION REV3)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:INDUCTION REV3)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE REV-REV)
        (:TYPE-PRESCRIPTION REV))
Warnings:  Subsume
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1787

---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(EQUAL (REV X) (REV3 X))

*** Key checkpoint under a top-level induction: ***

Subgoal *1/3'4'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (NOT (REV3 (CDR X))))
         (CONSP (REV (CDR X))))

ACL2 Error in ( DEFTHM REV-IS-REV3 ...):  See :DOC failure.

******** FAILED ********
ACL2 !>

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(verify (equal (rev x)
                      (rev3 x)))

The above use of verify puts us into an interactive loop, where we can issue commands at a lower level than we have seen above. We will precede each proof-builder command on the next slide by a comment (in blue) that explains what it does.

[top] [prev] [next]


[top] [prev] [next]

ACL2 !>(verify (equal (rev x)
                      (rev3 x)))

Experience suggests that this sort of lemma, the equivalence of two recursively defined functions, will require a proof by induction. So we instruct the proof-builder to replace the goal by base and induction steps.

->: induct
***** Now entering the theorem prover *****

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

We have been told to use induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (REV3 X).  This suggestion
was produced using the :induction rules REV and REV3.  If we let (:P X)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (ENDP (CDR X)))
                   (:P (CDR X)))
              (:P X))
     (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV3.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
              (NOT (ENDP (CDR X)))
              (EQUAL (REV (CDR X)) (REV3 (CDR X))))
         (EQUAL (REV X) (REV3 X)))

Subgoal *1/3 is subsumed by a goal yet to be proved.

])
Subgoal *1/2

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X)))
         (EQUAL (REV X) (REV3 X)))

Subgoal *1/2 is subsumed by a goal yet to be proved.

])
Subgoal *1/1

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/1
(IMPLIES (ENDP X)
         (EQUAL (REV X) (REV3 X)))

Subgoal *1/1 is subsumed by a goal yet to be proved.

])

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

Q.E.D.


Creating three new goals:  (MAIN . 1), (MAIN . 2) and (MAIN . 3).

The proof of the current goal, MAIN, has been completed.  However,
the following subgoals remain to be proved:
  (MAIN . 1), (MAIN . 2) and (MAIN . 3).
Now proving (MAIN . 1).

The proof-builder has just told us that we have three goals to prove. Let us use the th command (for ``THeorem'') to view the current goal.

->: th
*** Top-level hypotheses:
1. (NOT (ENDP X))
2. (NOT (ENDP (CDR X)))
3. (EQUAL (REV (CDR X)) (REV3 (CDR X)))

The current subterm is:
(EQUAL (REV X) (REV3 X))

No particular idea comes to mind for how to proceed (we are willing to forge ahead at this point without a great deal of thought). So we issue a command, bash, to simplify the current goal using the full power of the ACL2 simplifier.

->: bash
***** Now entering the theorem prover *****
Goal'
Goal''
Goal'''
Goal'4'

([ A key checkpoint:

Goal'4'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (NOT (REV3 (CDR X))))
         (CONSP (REV (CDR X))))

Goal'4' is subsumed by a goal yet to be proved.

])

Q.E.D.


Creating one new goal:  ((MAIN . 1) . 1).

The proof of the current goal, (MAIN . 1), has been completed.  However,
the following subgoals remain to be proved:
  ((MAIN . 1) . 1).
Now proving ((MAIN . 1) . 1).

What did bash leave us with? Let's take a look at the goal left on top of the goal stack, again using the th command.

->: th
*** Top-level hypotheses:
1. (CONSP X)
2. (CONSP (CDR X))
3. (NOT (REV3 (CDR X)))

The current subterm is:
(CONSP (REV (CDR X)))

AHA! It looks like hypotheses 2 and 3 are contradictory. It seems that ACL2 would know that if only it would expand the definition of REV3 on (CDR X). The proof finally succeeds with such a hint:

[top] [prev] [next]


[top] [prev]

ACL2 !>(defthm rev-is-rev3
         (equal (rev x)
                (rev3 x))
	 :hints (("Goal" :do-not '(eliminate-destructors)
		  :expand ((rev3 (cdr x))))))


ACL2 Warning [Subsume] in ( DEFTHM REV-IS-REV3 ...):  A newly proposed
:REWRITE rule generated from REV-IS-REV3 probably subsumes the previously
added :REWRITE rules REV-REV and REV-APPEND, in the sense that the
new rule will now probably be applied whenever the old rules would
have been.


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

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (REV3 X).  This suggestion
was produced using the :induction rules REV and REV3.  If we let (:P X)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
                   (NOT (ENDP (CDR X)))
                   (:P (CDR X)))
              (:P X))
     (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X)))
              (:P X))
     (IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV3.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/2
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 REV-IS-REV3 ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION REV3)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REV)
        (:INDUCTION REV3)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE REV-REV)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION REV)
        (:TYPE-PRESCRIPTION REV3)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Warnings:  Subsume
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1680
 REV-IS-REV3
ACL2 !>