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 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 REV is
described by the theorem (OR (CONSP (REV X)) (EQUAL (REV X) NIL)).
We used primitive type reasoning and the :type-prescription rule BINARY-
APPEND.

Summary
Form:  ( DEFUN REV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BINARY-APPEND))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.01, 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 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 REV3 is
described by the theorem (OR (CONSP (REV3 X)) (EQUAL (REV3 X) NIL)).
We used primitive type reasoning.

Summary
Form:  ( DEFUN REV3 ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
 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).


Name the formula above *1.

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).  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,
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 three nontautological subgoals.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X))))
         (EQUAL (REV X) (REV3 X))).

This simplifies, using the :definitions REV and REV3, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

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

This simplifies, using the :definition BINARY-APPEND, to the following
two conjectures.

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

This simplifies, using primitive type reasoning and the :rewrite rule
CONS-EQUAL, to


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, in this case destructor eliminiation. The documentation topic PROOF-TREE shows how to use an Emacs-based tool to locate simplification checkpoints automatically.

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


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

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.


You are welcome to continue scrolling through ACL2's vain attempt to prove the theorem. We recommend that you skip to the end of the proof attempt either now, or soon. (We will give you some more chances.)
Subgoal *1/3.2''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (CONSP X2)
              (EQUAL (REV X2) (REV3 X2))
              (CONSP (REV X2)))
         (EQUAL (APPEND (CDR (REV X2)) (LIST X1))
                (APPEND (REV (REV (CDR (REV X2))))
                        (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/3.2'''
(IMPLIES (AND (CONSP X2)
              (EQUAL (REV X2) (REV3 X2))
              (CONSP (REV X2)))
         (EQUAL (APPEND (CDR (REV X2)) (LIST X1))
                (APPEND (REV (REV (CDR (REV X2))))
                        (LIST X1)))).

We now use the second hypothesis by cross-fertilizing (REV3 X2) for
(REV X2) and throwing away the hypothesis.  This produces

Subgoal *1/3.2'4'
(IMPLIES (AND (CONSP X2) (CONSP (REV X2)))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV (CDR (REV X2))))
                        (LIST X1)))).

We generalize this conjecture, replacing (REV X2) by L.  This produces

Subgoal *1/3.2'5'
(IMPLIES (AND (CONSP X2) (CONSP L))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV (CDR L)))
                        (LIST X1)))).

The destructor terms (CAR L) and (CDR L) can be eliminated by using
CAR-CDR-ELIM to replace L by (CONS L1 L2), generalizing (CAR L) to
L1 and (CDR L) to L2.  This produces the following goal.

Subgoal *1/3.2'6'
(IMPLIES (AND (CONSP (CONS L1 L2)) (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/3.2'7'
(IMPLIES (CONSP X2)
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

Name the formula above *1.1.

Subgoal *1/3.1
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X)))
              (NOT (CONSP (REV (CDR X)))))
         (EQUAL (LIST (CAR X))
                (CONS (CAR (REV (CDR X)))
                      (APPEND (REV (REV (CDR (REV (CDR X)))))
                              (LIST (CAR X)))))).

This simplifies, using the :definition BINARY-APPEND, the :executable-
counterparts of CAR, CDR, CONSP and REV, primitive type reasoning,
the :rewrite rule CDR-CONS and the :type-prescription rule REV, to

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

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/3.1''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/3.1'''
(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
         (CONSP (REV X2))).

Name the formula above *1.2.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))))
         (EQUAL (REV X) (REV3 X))).

This simplifies, using the :definitions REV and REV3, to

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

But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterpart of CONSP and primitive
type reasoning.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV X) (REV3 X))).

But simplification reduces this to T, using the :definitions REV and
REV3 and the :executable-counterpart of EQUAL.

So we now return to *1.2, which is

(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
         (CONSP (REV X2))).

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


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
We will induct according to a scheme suggested by (REV3 X2).  If we
let  (:P X2) denote *1.2 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X2))
                   (NOT (ENDP (CDR X2)))
                   (:P (CDR X2)))
              (:P X2))
     (IMPLIES (AND (NOT (ENDP X2)) (ENDP (CDR X2)))
              (:P X2))
     (IMPLIES (ENDP X2) (:P X2))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X2) 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 five nontautological subgoals.

Subgoal *1.2/5
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (CONSP (REV (CDR X2)))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/5'
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (CONSP (REV (CDR X2)))
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

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

Subgoal *1.2/4
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (REV3 (CDR X2))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/4'
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (REV3 (CDR X2))
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

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


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
Subgoal *1.2/3
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (NOT (CONSP (CDR X2)))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But we reduce the conjecture to T, by case analysis.

Subgoal *1.2/2
(IMPLIES (AND (NOT (ENDP X2))
              (ENDP (CDR X2))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/2'
(IMPLIES (AND (CONSP X2)
              (NOT (CONSP (CDR X2)))
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But simplification reduces this to T, using the :definition REV3 and
primitive type reasoning.

Subgoal *1.2/1
(IMPLIES (AND (ENDP X2)
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But we reduce the conjecture to T, by case analysis.

That completes the proof of *1.2.

We therefore turn our attention to *1.1, which is

(IMPLIES (CONSP X2)
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

Perhaps we can prove *1.1 by induction.  Two induction schemes are
suggested by this conjecture.  We will choose arbitrarily among these.


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
We will induct according to a scheme suggested by (REV3 X2).  If we
let  (:P L2 X1 X2) denote *1.1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X2))
                   (NOT (ENDP (CDR X2)))
                   (:P L2 X1 (CDR X2)))
              (:P L2 X1 X2))
     (IMPLIES (AND (NOT (ENDP X2)) (ENDP (CDR X2)))
              (:P L2 X1 X2))
     (IMPLIES (ENDP X2) (:P L2 X1 X2))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X2) 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 four nontautological subgoals.

Subgoal *1.1/4
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (EQUAL (APPEND (CDR (REV3 (CDR X2))) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1)))
              (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/4'
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (EQUAL (APPEND (CDR (REV3 (CDR X2))) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1))))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using the :definitions REV and REV3, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

Subgoal *1.1/4''
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (EQUAL (APPEND (CDR (REV3 (CDR X2))) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1))))
         (EQUAL (APPEND (APPEND (REV (REV (CDR (REV3 (CDR X2)))))
                                (LIST (CAR X2)))
                        (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

The destructor terms (CAR X2) and (CDR X2) can be eliminated by using
CAR-CDR-ELIM to replace X2 by (CONS X3 X4), generalizing (CAR X2) to
X3 and (CDR X2) to X4.  This produces the following goal.

Subgoal *1.1/4'''
(IMPLIES (AND (CONSP (CONS X3 X4))
              (CONSP X4)
              (EQUAL (APPEND (CDR (REV3 X4)) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1))))
         (EQUAL (APPEND (APPEND (REV (REV (CDR (REV3 X4))))
                                (LIST X3))
                        (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using primitive type reasoning, to


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
Subgoal *1.1/4'4'
(IMPLIES (AND (CONSP X4)
              (EQUAL (APPEND (CDR (REV3 X4)) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1))))
         (EQUAL (APPEND (APPEND (REV (REV (CDR (REV3 X4))))
                                (LIST X3))
                        (LIST X1))
                (APPEND (CDR (REV3 X4)) (LIST X1)))).

We now use the second hypothesis by substituting 
(APPEND (REV (REV L2)) (LIST X1)) for (APPEND (CDR (REV3 X4)) (LIST X1))
and throwing away the hypothesis.  This produces

Subgoal *1.1/4'5'
(IMPLIES (CONSP X4)
         (EQUAL (APPEND (APPEND (REV (REV (CDR (REV3 X4))))
                                (LIST X3))
                        (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

Name the formula above *1.1.1.

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (NOT (CONSP (CDR X2)))
              (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

But we reduce the conjecture to T, by case analysis.

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP X2))
              (ENDP (CDR X2))
              (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP X2) (NOT (CONSP (CDR X2))))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using the :definitions BINARY-APPEND and REV3, the
:executable-counterpart of CONSP and the :rewrite rule CDR-CONS, to


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
Subgoal *1.1/2''
(IMPLIES (AND (CONSP X2) (NOT (CONSP (CDR X2))))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

The destructor terms (CAR X2) and (CDR X2) can be eliminated by using
CAR-CDR-ELIM to replace X2 by (CONS X3 X4), generalizing (CAR X2) to
X3 and (CDR X2) to X4.  This produces the following goal.

Subgoal *1.1/2'''
(IMPLIES (AND (CONSP (CONS X3 X4))
              (NOT (CONSP X4)))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1.1/2'4'
(IMPLIES (NOT (CONSP X4))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

We suspect that the term (NOT (CONSP X4)) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1.1/2'5'
(EQUAL (LIST X1)
       (APPEND (REV (REV L2)) (LIST X1))).

Name the formula above *1.1.2.

Subgoal *1.1/1
(IMPLIES (AND (ENDP X2) (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

But we reduce the conjecture to T, by case analysis.

So we now return to *1.1.2, which is

(EQUAL (LIST X1)
       (APPEND (REV (REV L2)) (LIST X1))).

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


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
We will induct according to a scheme suggested by (REV L2).  If we
let  (:P L2 X1) denote *1.1.2 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP L2)) (:P (CDR L2) X1))
              (:P L2 X1))
     (IMPLIES (ENDP L2) (:P L2 X1))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT L2) 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.1.2/2
(IMPLIES (AND (NOT (ENDP L2))
              (EQUAL (LIST X1)
                     (APPEND (REV (REV (CDR L2)))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1.2/2'
(IMPLIES (AND (CONSP L2)
              (EQUAL (LIST X1)
                     (APPEND (REV (REV (CDR L2)))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using the :definition REV, to

Subgoal *1.1.2/2''
(IMPLIES (AND (CONSP L2)
              (EQUAL (LIST X1)
                     (APPEND (REV (REV (CDR L2)))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND (REV (CDR L2)) (LIST (CAR L2))))
                        (LIST X1)))).

The destructor terms (CAR L2) and (CDR L2) can be eliminated by using
CAR-CDR-ELIM to replace L2 by (CONS L3 L4), generalizing (CAR L2) to
L3 and (CDR L2) to L4.  This produces the following goal.

Subgoal *1.1.2/2'''
(IMPLIES (AND (CONSP (CONS L3 L4))
              (EQUAL (LIST X1)
                     (APPEND (REV (REV L4)) (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND (REV L4) (LIST L3)))
                        (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1.1.2/2'4'
(IMPLIES (EQUAL (LIST X1)
                (APPEND (REV (REV L4)) (LIST X1)))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND (REV L4) (LIST L3)))
                        (LIST X1)))).

We generalize this conjecture, replacing (REV L4) by RV.  This produces

Subgoal *1.1.2/2'5'
(IMPLIES (EQUAL (LIST X1)
                (APPEND (REV RV) (LIST X1)))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND RV (LIST L3)))
                        (LIST X1)))).

Name the formula above *1.1.2.1.


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
Subgoal *1.1.2/1
(IMPLIES (ENDP L2)
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1.2/1'
(IMPLIES (NOT (CONSP L2))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterparts of CONSP and REV and primitive
type reasoning.

So we now return to *1.1.2.1, which is

(IMPLIES (EQUAL (LIST X1)
                (APPEND (REV RV) (LIST X1)))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND RV (LIST L3)))
                        (LIST X1)))).

Perhaps we can prove *1.1.2.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 
(BINARY-APPEND RV (CONS L3 'NIL)).  If we let  (:P L3 RV X1) denote
*1.1.2.1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP RV))
                   (:P L3 (CDR RV) X1))
              (:P L3 RV X1))
     (IMPLIES (ENDP RV) (:P L3 RV X1))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT RV) 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 three nontautological
subgoals.

Subgoal *1.1.2.1/3
(IMPLIES (AND (NOT (ENDP RV))
              (EQUAL (LIST X1)
                     (APPEND (REV (APPEND (CDR RV) (LIST L3)))
                             (LIST X1)))
              (EQUAL (LIST X1)
                     (APPEND (REV RV) (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND RV (LIST L3)))
                        (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1.2.1/3'
(IMPLIES (AND (CONSP RV)
              (EQUAL (LIST X1)
                     (APPEND (REV (APPEND (CDR RV) (LIST L3)))
                             (LIST X1)))
              (EQUAL (LIST X1)
                     (APPEND (REV RV) (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND RV (LIST L3)))
                        (LIST X1)))).

This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

Subgoal *1.1.2.1/3''
(IMPLIES (AND (CONSP RV)
              (EQUAL (LIST X1)
                     (APPEND (REV (APPEND (CDR RV) (LIST L3)))
                             (LIST X1)))
              (EQUAL (LIST X1)
                     (APPEND (APPEND (REV (CDR RV)) (LIST (CAR RV)))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND (REV (APPEND (CDR RV) (LIST L3)))
                                (LIST (CAR RV)))
                        (LIST X1)))).

The destructor terms (CAR RV) and (CDR RV) can be eliminated by using
CAR-CDR-ELIM to replace RV by (CONS RV1 RV2), generalizing (CAR RV)
to RV1 and (CDR RV) to RV2.  This produces the following goal.


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
Subgoal *1.1.2.1/3'''
(IMPLIES (AND (CONSP (CONS RV1 RV2))
              (EQUAL (LIST X1)
                     (APPEND (REV (APPEND RV2 (LIST L3)))
                             (LIST X1)))
              (EQUAL (LIST X1)
                     (APPEND (APPEND (REV RV2) (LIST RV1))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
                                (LIST RV1))
                        (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1.1.2.1/3'4'
(IMPLIES (AND (EQUAL (LIST X1)
                     (APPEND (REV (APPEND RV2 (LIST L3)))
                             (LIST X1)))
              (EQUAL (LIST X1)
                     (APPEND (APPEND (REV RV2) (LIST RV1))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
                                (LIST RV1))
                        (LIST X1)))).

We generalize this conjecture, replacing (APPEND RV2 (LIST L3)) by
L and restricting the type of the new variable L to be that of the
term it replaces, as established by primitive type reasoning and BINARY-
APPEND.  This produces

Subgoal *1.1.2.1/3'5'
(IMPLIES (AND (CONSP L)
              (EQUAL (LIST X1)
                     (APPEND (REV L) (LIST X1)))
              (EQUAL (LIST X1)
                     (APPEND (APPEND (REV RV2) (LIST RV1))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND (REV L) (LIST RV1))
                        (LIST X1)))).

We generalize this conjecture, replacing (REV L) by RV.  This produces

Subgoal *1.1.2.1/3'6'
(IMPLIES (AND (CONSP L)
              (EQUAL (LIST X1) (APPEND RV (LIST X1)))
              (EQUAL (LIST X1)
                     (APPEND (APPEND (REV RV2) (LIST RV1))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND RV (LIST RV1))
                        (LIST X1)))).

We suspect that the term (CONSP L) is irrelevant to the truth of this
conjecture and throw it out.  We will thus try to prove

Subgoal *1.1.2.1/3'7'
(IMPLIES (AND (EQUAL (LIST X1) (APPEND RV (LIST X1)))
              (EQUAL (LIST X1)
                     (APPEND (APPEND (REV RV2) (LIST RV1))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND RV (LIST RV1))
                        (LIST X1)))).

Name the formula above *1.1.2.1.1.


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
Subgoal *1.1.2.1/2
(IMPLIES (AND (NOT (ENDP RV))
              (NOT (EQUAL (LIST X1)
                          (APPEND (REV (CDR RV)) (LIST X1))))
              (EQUAL (LIST X1)
                     (APPEND (REV RV) (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND RV (LIST L3)))
                        (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1.2.1/2'
(IMPLIES (AND (CONSP RV)
              (NOT (EQUAL (LIST X1)
                          (APPEND (REV (CDR RV)) (LIST X1))))
              (EQUAL (LIST X1)
                     (APPEND (REV RV) (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND RV (LIST L3)))
                        (LIST X1)))).

This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

Subgoal *1.1.2.1/2''
(IMPLIES (AND (CONSP RV)
              (NOT (EQUAL (LIST X1)
                          (APPEND (REV (CDR RV)) (LIST X1))))
              (EQUAL (LIST X1)
                     (APPEND (APPEND (REV (CDR RV)) (LIST (CAR RV)))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND (REV (APPEND (CDR RV) (LIST L3)))
                                (LIST (CAR RV)))
                        (LIST X1)))).

The destructor terms (CAR RV) and (CDR RV) can be eliminated by using
CAR-CDR-ELIM to replace RV by (CONS RV1 RV2), generalizing (CAR RV)
to RV1 and (CDR RV) to RV2.  This produces the following goal.

Subgoal *1.1.2.1/2'''
(IMPLIES (AND (CONSP (CONS RV1 RV2))
              (NOT (EQUAL (LIST X1)
                          (APPEND (REV RV2) (LIST X1))))
              (EQUAL (LIST X1)
                     (APPEND (APPEND (REV RV2) (LIST RV1))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
                                (LIST RV1))
                        (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1.1.2.1/2'4'
(IMPLIES (AND (NOT (EQUAL (LIST X1)
                          (APPEND (REV RV2) (LIST X1))))
              (EQUAL (LIST X1)
                     (APPEND (APPEND (REV RV2) (LIST RV1))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
                                (LIST RV1))
                        (LIST X1)))).

We generalize this conjecture, replacing (REV RV2) by RV.  This produces

Subgoal *1.1.2.1/2'5'
(IMPLIES (AND (NOT (EQUAL (LIST X1) (APPEND RV (LIST X1))))
              (EQUAL (LIST X1)
                     (APPEND (APPEND RV (LIST RV1))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
                                (LIST RV1))
                        (LIST X1)))).

Name the formula above *1.1.2.1.2.


Had enough yet? If so, skip to the end of the proof attempt. (We will give you some more chances.)
Subgoal *1.1.2.1/1
(IMPLIES (AND (ENDP RV)
              (EQUAL (LIST X1)
                     (APPEND (REV RV) (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND RV (LIST L3)))
                        (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to


Finally we are near the end of the proof attempt!. Scroll down a screen or two 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.1/1'
(IMPLIES (AND (NOT (CONSP RV))
              (EQUAL (LIST X1)
                     (APPEND (REV RV) (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (APPEND RV (LIST L3)))
                        (LIST X1)))).

This simplifies, using the :definitions BINARY-APPEND and REV, the
:executable-counterparts of CONSP and REV, primitive type reasoning
and the :rewrite rules CAR-CONS and CDR-CONS, to

Subgoal *1.1.2.1/1''
(CONSP RV).

We suspect that this conjecture is not a theorem.  We might as well
be trying to prove

Subgoal *1.1.2.1/1'''
NIL.

Obviously, the proof attempt has failed.

Summary
Form:  ( DEFTHM REV-IS-REV3 ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION REV3)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION REV))
Warnings:  None
Time:  1.36 seconds (prove: 1.02, print: 0.33, other: 0.01)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>

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.
Name the formula above *1.

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).  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,
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 (AND (NOT (ENDP X))
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (REV X)) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (REV X)) X)).

This simplifies, using the :definition REV, to

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

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (EQUAL (REV (REV X2)) X2))
         (EQUAL (REV (APPEND (REV X2) (LIST X1)))
                (CONS X1 X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (REV X2)) X2)
         (EQUAL (REV (APPEND (REV X2) (LIST X1)))
                (CONS X1 X2))).

We now use the hypothesis by cross-fertilizing (REV (REV X2)) for X2
and throwing away the hypothesis.  This produces

Subgoal *1/2'5'
(EQUAL (REV (APPEND (REV X2) (LIST X1)))
       (CONS X1 (REV (REV X2)))).

We generalize this conjecture, replacing (REV X2) by RV.  This produces

Subgoal *1/2'6'
(EQUAL (REV (APPEND RV (LIST X1)))
       (CONS X1 (REV RV))).

Name the formula above *1.1.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV (REV X)) X)).

This simplifies, using the :definition REV, the :executable-counterpart
of REV and primitive type reasoning, to

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

Name the formula above *1.2.

No induction schemes are suggested by *1.2.  Consequently, 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))
Warnings:  None
Time:  0.13 seconds (prove: 0.08, print: 0.03, other: 0.02)

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

Name the formula above *1.

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).  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,
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 (AND (NOT (ENDP X))
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (REV X)) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (REV X)) X)).

This simplifies, using the :definition REV, to

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


The goal just above is the first simplification checkpoint. (Notice the use of destructor elimination below.) 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, on to the next slide by scrolling down to the [next] link or clicking here.
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (EQUAL (REV (REV X2)) X2))
         (EQUAL (REV (APPEND (REV X2) (LIST X1)))
                (CONS X1 X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (REV X2)) X2)
         (EQUAL (REV (APPEND (REV X2) (LIST X1)))
                (CONS X1 X2))).

We now use the hypothesis by cross-fertilizing (REV (REV X2)) for X2
and throwing away the hypothesis.  This produces

Subgoal *1/2'5'
(EQUAL (REV (APPEND (REV X2) (LIST X1)))
       (CONS X1 (REV (REV X2)))).

We generalize this conjecture, replacing (REV X2) by RV.  This produces

Subgoal *1/2'6'
(EQUAL (REV (APPEND RV (LIST X1)))
       (CONS X1 (REV RV))).

Name the formula above *1.1.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV (REV X)) X)).

This simplifies, using the :definition REV, the :executable-counterpart
of REV and primitive type reasoning, to

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

Name the formula above *1.2.

No induction schemes are suggested by *1.2.  Consequently, 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))
Warnings:  None
Time:  0.13 seconds (prove: 0.08, print: 0.03, other: 0.02)

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

Name the formula above *1.


This proof fails. This failure is a bit unusual in that we find that some simplification checkpoint other than the first suggests a particularly useful lemma. Scroll down through the proof and look for the blue comments.
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 (BINARY-APPEND X Y).
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, 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 (AND (NOT (ENDP X))
              (EQUAL (REV (APPEND (CDR X) Y))
                     (APPEND (REV Y) (REV (CDR X)))))
         (EQUAL (REV (APPEND X Y))
                (APPEND (REV Y) (REV X)))).

By the simple :definition ENDP we reduce the conjecture to

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

This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

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


The mention of destructor terms below suggests that the goal above is a simplification checkpoint. Although you may find a rewrite rule suggested by this checkpoint, let us scroll further down and look for more simplification checkpoints.
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (EQUAL (REV (APPEND X2 Y))
                     (APPEND (REV Y) (REV X2))))
         (EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
                (APPEND (REV Y) (REV X2) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (APPEND X2 Y))
                (APPEND (REV Y) (REV X2)))
         (EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
                (APPEND (REV Y) (REV X2) (LIST X1)))).


Just above is another simplification checkpoint (as the description below points to equality substitution rather than further simplification). But we do not yet see a term that suggests a really nice rewrite rule.
We now use the hypothesis by substituting (APPEND (REV Y) (REV X2))
for (REV (APPEND X2 Y)) and throwing away the hypothesis.  This produces

Subgoal *1/2'5'
(EQUAL (APPEND (APPEND (REV Y) (REV X2))
               (LIST X1))
       (APPEND (REV Y) (REV X2) (LIST X1))).


AHA! The simplification checkpoint just above does clearly suggest that we prove the associativity of the append operator. We push such a lemma onto our exsting to do list, (rev-append rev-rev rev-is-rev3). You are welcome to scroll to the end of this failed proof, but we suggest that you take the action of an experienced ACL2 user, which is to ignore the rest of the proof now that we have discovered a suitable rewrite rule to prove and go do it! So click here.
We generalize this conjecture, replacing (REV X2) by RV and (REV Y)
by RV0.  This produces

Subgoal *1/2'6'
(EQUAL (APPEND (APPEND RV0 RV) (LIST X1))
       (APPEND RV0 RV (LIST X1))).

Name the formula above *1.1.

Subgoal *1/1
(IMPLIES (ENDP X)
         (EQUAL (REV (APPEND X Y))
                (APPEND (REV Y) (REV X)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV (APPEND X Y))
                (APPEND (REV Y) (REV X)))).

This simplifies, using the :definitions BINARY-APPEND and REV, to

Subgoal *1/1''
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV Y) (APPEND (REV Y) NIL))).

We generalize this conjecture, replacing (REV Y) by RV.  This produces

Subgoal *1/1'''
(IMPLIES (NOT (CONSP X))
         (EQUAL RV (APPEND RV NIL))).

We suspect that the term (NOT (CONSP X)) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1/1'4'
(EQUAL RV (APPEND RV NIL)).

Name the formula above *1.2.

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

We will induct according to a scheme suggested by (BINARY-APPEND RV 'NIL).
If we let  (:P RV) denote *1.2 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP RV)) (:P (CDR RV)))
              (:P RV))
     (IMPLIES (ENDP RV) (:P RV))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT RV) 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/2
(IMPLIES (AND (NOT (ENDP RV))
              (EQUAL (CDR RV) (APPEND (CDR RV) NIL)))
         (EQUAL RV (APPEND RV NIL))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/2'
(IMPLIES (AND (CONSP RV)
              (EQUAL (CDR RV) (APPEND (CDR RV) NIL)))
         (EQUAL RV (APPEND RV NIL))).

But simplification reduces this to T, using the :definition BINARY-
APPEND, primitive type reasoning and the :rewrite rule CAR-CDR-ELIM.

Subgoal *1.2/1
(IMPLIES (ENDP RV)
         (EQUAL RV (APPEND RV NIL))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/1'
(IMPLIES (NOT (CONSP RV))
         (EQUAL RV (APPEND RV NIL))).

This simplifies, using the :definition BINARY-APPEND and primitive
type reasoning, to

Subgoal *1.2/1''
(IMPLIES (NOT (CONSP RV)) (NOT RV)).

Name the formula above *1.2.1.

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

Summary
Form:  ( DEFTHM REV-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.25 seconds (prove: 0.13, print: 0.10, other: 0.02)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(defthm append-assoc
         (equal (append (append x y) z)
                (append x (append y z))))
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(defthm append-assoc
         (equal (append (append x y) z)
                (append x (append y z))))

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.  

We will induct according to a scheme suggested by (BINARY-APPEND X Y).
If we let  (:P X Y Z) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y Z))
              (:P X Y Z))
     (IMPLIES (ENDP X) (:P X Y Z))).
This induction is justified by the same argument used to admit BINARY-
APPEND, 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 (AND (NOT (ENDP X))
              (EQUAL (APPEND (APPEND (CDR X) Y) Z)
                     (APPEND (CDR X) Y Z)))
         (EQUAL (APPEND (APPEND X Y) Z)
                (APPEND X Y Z))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (EQUAL (APPEND (APPEND (CDR X) Y) Z)
                     (APPEND (CDR X) Y Z)))
         (EQUAL (APPEND (APPEND X Y) Z)
                (APPEND X Y Z))).

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

Subgoal *1/1
(IMPLIES (ENDP X)
         (EQUAL (APPEND (APPEND X Y) Z)
                (APPEND X Y Z))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (APPEND (APPEND X Y) Z)
                (APPEND X Y Z))).

But simplification reduces this to T, using the :definition BINARY-
APPEND and primitive type reasoning.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM APPEND-ASSOC ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.07 seconds (prove: 0.03, print: 0.02, other: 0.02)
 APPEND-ASSOC
ACL2 !>

Notice the time for the proof above. This was an easy lemma for ACL2! We can pop our to do list back down to (rev-append rev-rev rev-is-rev3). So the next thing to do is retry the proof of the top of this stack, rev-append.
[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))))

Name the formula above *1.


The proof fails once again. You are welcome to scroll through the proof. However, we are happy to give you a shortcut by directing you to the simplification checkpoint that we think most clearly suggests some useful lemmas. Click here if you would like that shortcut.
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 (BINARY-APPEND X Y).
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, 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 (AND (NOT (ENDP X))
              (EQUAL (REV (APPEND (CDR X) Y))
                     (APPEND (REV Y) (REV (CDR X)))))
         (EQUAL (REV (APPEND X Y))
                (APPEND (REV Y) (REV X)))).

By the simple :definition ENDP we reduce the conjecture to

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

This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

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

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (EQUAL (REV (APPEND X2 Y))
                     (APPEND (REV Y) (REV X2))))
         (EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
                (APPEND (REV Y) (REV X2) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (APPEND X2 Y))
                (APPEND (REV Y) (REV X2)))
         (EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
                (APPEND (REV Y) (REV X2) (LIST X1)))).

We now use the hypothesis by substituting (APPEND (REV Y) (REV X2))
for (REV (APPEND X2 Y)) and throwing away the hypothesis.  This produces

Subgoal *1/2'5'
(EQUAL (APPEND (APPEND (REV Y) (REV X2))
               (LIST X1))
       (APPEND (REV Y) (REV X2) (LIST X1))).

By the simple :rewrite rule APPEND-ASSOC we reduce the conjecture to

Subgoal *1/2'6'
(EQUAL (APPEND (REV Y) (REV X2) (LIST X1))
       (APPEND (REV Y) (REV X2) (LIST X1))).

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

Subgoal *1/1
(IMPLIES (ENDP X)
         (EQUAL (REV (APPEND X Y))
                (APPEND (REV Y) (REV X)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV (APPEND X Y))
                (APPEND (REV Y) (REV X)))).

This simplifies, using the :definitions BINARY-APPEND and REV, to

Subgoal *1/1''
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV Y) (APPEND (REV Y) NIL))).


The simplification checkpoint above suggests two rewrite rules. One, which we call append-nil, says that (append x nil) is equal to x under suitable hypotheses. What are those hypotheses? We need to know that the last cdr of x is nil. (Note: This kind of thinking is sometimes annoying to beginning users of ACL2, but with a little practice one gets used to the need for hypotheses of the form (true-listp ...), where the function true-listp recognizes lists whose last cdr is nil.) Here are some examples related to this notion of true list.

ACL2 !>(cons 1 nil)
(1)
ACL2 !>(cons 2 (cons 1 nil))
(2 1)
ACL2 !>(true-listp (cons 1 nil))
T
ACL2 !>(true-listp (cons 2 (cons 1 nil)))
T
ACL2 !>(true-listp (cons 2 (cons 1 7)))
NIL
ACL2 !>
Now in order to apply this rewrite rule, rewriting
(EQUAL (REV Y) (APPEND (REV Y) NIL))
to nil, we need to know that (REV Y) is a true list. This observation leads us to prove a second lemma, true-listp-rev. So at the moment our to do stack is:
(append-nil true-listp-rev rev-append rev-rev rev-is-rev3)

We recommend that you click here to move to the next slide.


We generalize this conjecture, replacing (REV Y) by RV.  This produces

Subgoal *1/1'''
(IMPLIES (NOT (CONSP X))
         (EQUAL RV (APPEND RV NIL))).

We suspect that the term (NOT (CONSP X)) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1/1'4'
(EQUAL RV (APPEND RV NIL)).

Name the formula above *1.1.

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

We will induct according to a scheme suggested by (BINARY-APPEND RV 'NIL).
If we let  (:P RV) denote *1.1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP RV)) (:P (CDR RV)))
              (:P RV))
     (IMPLIES (ENDP RV) (:P RV))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT RV) 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.1/2
(IMPLIES (AND (NOT (ENDP RV))
              (EQUAL (CDR RV) (APPEND (CDR RV) NIL)))
         (EQUAL RV (APPEND RV NIL))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP RV)
              (EQUAL (CDR RV) (APPEND (CDR RV) NIL)))
         (EQUAL RV (APPEND RV NIL))).

But simplification reduces this to T, using the :definition BINARY-
APPEND, primitive type reasoning and the :rewrite rule CAR-CDR-ELIM.

Subgoal *1.1/1
(IMPLIES (ENDP RV)
         (EQUAL RV (APPEND RV NIL))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/1'
(IMPLIES (NOT (CONSP RV))
         (EQUAL RV (APPEND RV NIL))).

This simplifies, using the :definition BINARY-APPEND and primitive
type reasoning, to

Subgoal *1.1/1''
(IMPLIES (NOT (CONSP RV)) (NOT RV)).

Name the formula above *1.1.1.

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

Summary
Form:  ( DEFTHM REV-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE APPEND-ASSOC)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.23 seconds (prove: 0.15, print: 0.06, other: 0.02)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(defthm append-nil
         (implies (true-listp x)
                  (equal (append x nil) x)))
[top] [prev] [next]




























































[top] [prev] [next]

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

Name the formula above *1.

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 (BINARY-APPEND X 'NIL).
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 BINARY-
APPEND, 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 three nontautological
subgoals.

Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
              (EQUAL (APPEND (CDR X) NIL) (CDR X))
              (TRUE-LISTP X))
         (EQUAL (APPEND X NIL) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (CONSP X)
              (EQUAL (APPEND (CDR X) NIL) (CDR X))
              (TRUE-LISTP X))
         (EQUAL (APPEND X NIL) X)).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, primitive type reasoning and the :rewrite rule
CAR-CDR-ELIM.

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (NOT (TRUE-LISTP (CDR X)))
              (TRUE-LISTP X))
         (EQUAL (APPEND X NIL) X)).

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

Subgoal *1/1
(IMPLIES (AND (ENDP X) (TRUE-LISTP X))
         (EQUAL (APPEND X NIL) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X))
         (EQUAL (APPEND X NIL) X)).

But simplification reduces this to T, using the :definition TRUE-LISTP,
the :executable-counterparts of BINARY-APPEND, CONSP and EQUAL and
primitive type reasoning.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM APPEND-NIL ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION IMPLIES)
        (:DEFINITION NOT)
        (:DEFINITION TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART BINARY-APPEND)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CDR-ELIM))
Warnings:  None
Time:  0.07 seconds (prove: 0.03, print: 0.02, other: 0.02)
 APPEND-NIL
ACL2 !>

Since the proof succeeded, we pop append-nil off our to do list, which leads us to the next goal.
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(defthm true-listp-rev
         (true-listp (rev x)))
[top] [prev] [next]




























































[top] [prev] [next]

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

Name the formula above *1.


The proof succeeds, so we can pop this lemma off our to do list, leaving us with:
(rev-append rev-rev rev-is-rev3)
By now you may have picked up on the idea that when a proof succeeds, an ACL2 user will probably be happy not to spend time and effort analyzing the successful proof. Instead, that user will see that the proof succeeded and move on. Click here to move on.

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).  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,
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 (AND (NOT (ENDP X))
              (TRUE-LISTP (REV (CDR X))))
         (TRUE-LISTP (REV X))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (TRUE-LISTP (REV (CDR X))))
         (TRUE-LISTP (REV X))).

This simplifies, using the :definition REV, to

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (TRUE-LISTP (REV (CDR X))))
         (TRUE-LISTP (APPEND (REV (CDR X)) (LIST (CAR X))))).

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (TRUE-LISTP (REV X2)))
         (TRUE-LISTP (APPEND (REV X2) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (TRUE-LISTP (REV X2))
         (TRUE-LISTP (APPEND (REV X2) (LIST X1)))).

We generalize this conjecture, replacing (REV X2) by RV.  This produces

Subgoal *1/2'5'
(IMPLIES (TRUE-LISTP RV)
         (TRUE-LISTP (APPEND RV (LIST X1)))).

Name the formula above *1.1.

Subgoal *1/1
(IMPLIES (ENDP X) (TRUE-LISTP (REV X))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (TRUE-LISTP (REV X))).

But simplification reduces this to T, using the :definition REV and
the :executable-counterpart of TRUE-LISTP.

So we now return to *1.1, which is

(IMPLIES (TRUE-LISTP RV)
         (TRUE-LISTP (APPEND RV (LIST X1)))).

Perhaps we can prove *1.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 
(BINARY-APPEND RV (CONS X1 'NIL)).  If we let  (:P RV X1) denote *1.1
above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP RV)) (:P (CDR RV) X1))
              (:P RV X1))
     (IMPLIES (ENDP RV) (:P RV X1))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT RV) 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 three nontautological
subgoals.

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP RV))
              (TRUE-LISTP (APPEND (CDR RV) (LIST X1)))
              (TRUE-LISTP RV))
         (TRUE-LISTP (APPEND RV (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/3'
(IMPLIES (AND (CONSP RV)
              (TRUE-LISTP (APPEND (CDR RV) (LIST X1)))
              (TRUE-LISTP RV))
         (TRUE-LISTP (APPEND RV (LIST X1)))).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, primitive type reasoning and the :type-prescription
rule BINARY-APPEND.

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP RV))
              (NOT (TRUE-LISTP (CDR RV)))
              (TRUE-LISTP RV))
         (TRUE-LISTP (APPEND RV (LIST X1)))).

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

Subgoal *1.1/1
(IMPLIES (AND (ENDP RV) (TRUE-LISTP RV))
         (TRUE-LISTP (APPEND RV (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/1'
(IMPLIES (AND (NOT (CONSP RV)) (TRUE-LISTP RV))
         (TRUE-LISTP (APPEND RV (LIST X1)))).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, the :executable-counterpart of CONSP and primitive
type reasoning.

That completes the proofs of *1.1 and *1.

Q.E.D.

The storage of TRUE-LISTP-REV depends upon the :type-prescription rule
TRUE-LISTP.

Summary
Form:  ( DEFTHM TRUE-LISTP-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION TRUE-LISTP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION TRUE-LISTP))
Warnings:  None
Time:  0.12 seconds (prove: 0.04, print: 0.06, other: 0.02)
 TRUE-LISTP-REV
ACL2 !>
[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))))

Name the formula above *1.


The proof succeeds, so we can pop this lemma off our to do list, leaving us with:
(rev-rev rev-is-rev3)
Click here to move on.

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 (BINARY-APPEND X Y).
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, 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 (AND (NOT (ENDP X))
              (EQUAL (REV (APPEND (CDR X) Y))
                     (APPEND (REV Y) (REV (CDR X)))))
         (EQUAL (REV (APPEND X Y))
                (APPEND (REV Y) (REV X)))).

By the simple :definition ENDP we reduce the conjecture to

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

This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

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

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (EQUAL (REV (APPEND X2 Y))
                     (APPEND (REV Y) (REV X2))))
         (EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
                (APPEND (REV Y) (REV X2) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (APPEND X2 Y))
                (APPEND (REV Y) (REV X2)))
         (EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
                (APPEND (REV Y) (REV X2) (LIST X1)))).

We now use the hypothesis by substituting (APPEND (REV Y) (REV X2))
for (REV (APPEND X2 Y)) and throwing away the hypothesis.  This produces

Subgoal *1/2'5'
(EQUAL (APPEND (APPEND (REV Y) (REV X2))
               (LIST X1))
       (APPEND (REV Y) (REV X2) (LIST X1))).

By the simple :rewrite rule APPEND-ASSOC we reduce the conjecture to

Subgoal *1/2'6'
(EQUAL (APPEND (REV Y) (REV X2) (LIST X1))
       (APPEND (REV Y) (REV X2) (LIST X1))).

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

Subgoal *1/1
(IMPLIES (ENDP X)
         (EQUAL (REV (APPEND X Y))
                (APPEND (REV Y) (REV X)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV (APPEND X Y))
                (APPEND (REV Y) (REV X)))).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, primitive type reasoning and the :rewrite rules APPEND-
NIL and TRUE-LISTP-REV.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM REV-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE APPEND-ASSOC)
        (:REWRITE APPEND-NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE TRUE-LISTP-REV))
Warnings:  None
Time:  0.17 seconds (prove: 0.11, print: 0.04, other: 0.02)
 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))

Name the formula above *1.

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).  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,
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 (AND (NOT (ENDP X))
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (REV X)) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X)))
         (EQUAL (REV (REV X)) X)).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterparts of CONSP and REV, primitive
type reasoning and the :rewrite rules CAR-CDR-ELIM, CAR-CONS, CDR-CONS
and REV-APPEND.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV (REV X)) X)).

This simplifies, using the :definition REV, the :executable-counterpart
of REV and primitive type reasoning, to


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.

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

Name the formula above *1.1.

No induction schemes are suggested by *1.1.  Consequently, 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)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE REV-APPEND))
Warnings:  None
Time:  0.05 seconds (prove: 0.02, print: 0.01, other: 0.02)

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

But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL and REV.

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART REV))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)

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

Name the formula above *1.

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).  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,
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 three nontautological subgoals.

Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
              (EQUAL (REV (REV (CDR X))) (CDR X))
              (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (CONSP X)
              (EQUAL (REV (REV (CDR X))) (CDR X))
              (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

But simplification reduces this to T, using the :definitions BINARY-
APPEND, REV and TRUE-LISTP, the :executable-counterparts of CONSP and
REV, primitive type reasoning and the :rewrite rules CAR-CDR-ELIM,
CAR-CONS, CDR-CONS and REV-APPEND.

Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
              (NOT (TRUE-LISTP (CDR X)))
              (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

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

Subgoal *1/1
(IMPLIES (AND (ENDP X) (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X))
         (EQUAL (REV (REV X)) X)).

But simplification reduces this to T, using the :definition TRUE-LISTP,
the :executable-counterparts of CONSP, EQUAL and REV and primitive
type reasoning.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION IMPLIES)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION TRUE-LISTP)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE REV-APPEND))
Warnings:  None
Time:  0.07 seconds (prove: 0.01, print: 0.04, other: 0.02)
 REV-REV
ACL2 !>
[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)))

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


Name the formula above *1.


The proof fails. In fact we can look through the proof attempt below and see that the lemma rev-rev, which we proved for the specific purpose of simplifying a checkpoint produced by an earlier proof attempt, was never applied to any goal. Why not? This time, rather than looking over the failed proof, let us try another technique, using the so-called proof-checker.. (See also the ACL2 documentation page on PROOF-CHECKER.) Click here to go to the next slide, where we illustrate the use of the proof-checker.
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).  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,
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 three nontautological subgoals.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X))))
         (EQUAL (REV X) (REV3 X))).

This simplifies, using the :definitions REV and REV3, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

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

This simplifies, using the :definition BINARY-APPEND, to the following
two conjectures.

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

This simplifies, using primitive type reasoning and the :rewrite rule
CONS-EQUAL, to

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

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.


Getting tired yet? We'll make the offer again: Click here to go to the next slide, where we illustrate the use of the proof-checker.
Subgoal *1/3.2''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (CONSP X2)
              (EQUAL (REV X2) (REV3 X2))
              (CONSP (REV X2)))
         (EQUAL (APPEND (CDR (REV X2)) (LIST X1))
                (APPEND (REV (REV (CDR (REV X2))))
                        (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/3.2'''
(IMPLIES (AND (CONSP X2)
              (EQUAL (REV X2) (REV3 X2))
              (CONSP (REV X2)))
         (EQUAL (APPEND (CDR (REV X2)) (LIST X1))
                (APPEND (REV (REV (CDR (REV X2))))
                        (LIST X1)))).

We now use the second hypothesis by cross-fertilizing (REV3 X2) for
(REV X2) and throwing away the hypothesis.  This produces

Subgoal *1/3.2'4'
(IMPLIES (AND (CONSP X2) (CONSP (REV X2)))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV (CDR (REV X2))))
                        (LIST X1)))).

We generalize this conjecture, replacing (REV X2) by L.  This produces

Subgoal *1/3.2'5'
(IMPLIES (AND (CONSP X2) (CONSP L))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV (CDR L)))
                        (LIST X1)))).

The destructor terms (CAR L) and (CDR L) can be eliminated by using
CAR-CDR-ELIM to replace L by (CONS L1 L2), generalizing (CAR L) to
L1 and (CDR L) to L2.  This produces the following goal.

Subgoal *1/3.2'6'
(IMPLIES (AND (CONSP (CONS L1 L2)) (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/3.2'7'
(IMPLIES (CONSP X2)
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

Name the formula above *1.1.

Subgoal *1/3.1
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X)))
              (NOT (CONSP (REV (CDR X)))))
         (EQUAL (LIST (CAR X))
                (CONS (CAR (REV (CDR X)))
                      (APPEND (REV (REV (CDR (REV (CDR X)))))
                              (LIST (CAR X)))))).

This simplifies, using the :definition BINARY-APPEND, the :executable-
counterparts of CAR, CDR, CONSP and REV, primitive type reasoning,
the :rewrite rule CDR-CONS and the :type-prescription rule REV, to

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

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/3.1''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/3.1'''
(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
         (CONSP (REV X2))).

Name the formula above *1.2.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))))
         (EQUAL (REV X) (REV3 X))).

This simplifies, using the :definitions REV and REV3, to

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

But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterpart of CONSP and primitive
type reasoning.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV X) (REV3 X))).

But simplification reduces this to T, using the :definitions REV and
REV3 and the :executable-counterpart of EQUAL.

So we now return to *1.2, which is

(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
         (CONSP (REV X2))).

Perhaps we can prove *1.2 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 X2).  If we
let  (:P X2) denote *1.2 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X2))
                   (NOT (ENDP (CDR X2)))
                   (:P (CDR X2)))
              (:P X2))
     (IMPLIES (AND (NOT (ENDP X2)) (ENDP (CDR X2)))
              (:P X2))
     (IMPLIES (ENDP X2) (:P X2))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X2) 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 five nontautological subgoals.

Subgoal *1.2/5
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (CONSP (REV (CDR X2)))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/5'
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (CONSP (REV (CDR X2)))
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

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

Subgoal *1.2/4
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (REV3 (CDR X2))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

By the simple :definition ENDP we reduce the conjecture to
[SGC for 1113 CONS pages..(3589 writable)..(T=17).GC finished]

Subgoal *1.2/4'
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (REV3 (CDR X2))
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

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

Subgoal *1.2/3
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (NOT (CONSP (CDR X2)))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But we reduce the conjecture to T, by case analysis.

Subgoal *1.2/2
(IMPLIES (AND (NOT (ENDP X2))
              (ENDP (CDR X2))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.2/2'
(IMPLIES (AND (CONSP X2)
              (NOT (CONSP (CDR X2)))
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But simplification reduces this to T, using the :definition REV3 and
primitive type reasoning.

Subgoal *1.2/1
(IMPLIES (AND (ENDP X2)
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But we reduce the conjecture to T, by case analysis.

That completes the proof of *1.2.

We therefore turn our attention to *1.1, which is

(IMPLIES (CONSP X2)
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

Perhaps we can prove *1.1 by induction.  Two induction schemes are
suggested by this conjecture.  We will choose arbitrarily among these.

We will induct according to a scheme suggested by (REV3 X2).  If we
let  (:P L2 X1 X2) denote *1.1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X2))
                   (NOT (ENDP (CDR X2)))
                   (:P L2 X1 (CDR X2)))
              (:P L2 X1 X2))
     (IMPLIES (AND (NOT (ENDP X2)) (ENDP (CDR X2)))
              (:P L2 X1 X2))
     (IMPLIES (ENDP X2) (:P L2 X1 X2))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X2) 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 four nontautological subgoals.

Subgoal *1.1/4
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (EQUAL (APPEND (CDR (REV3 (CDR X2))) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1)))
              (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/4'
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (EQUAL (APPEND (CDR (REV3 (CDR X2))) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1))))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using the :definitions BINARY-APPEND, REV and REV3,
the :executable-counterpart of CONSP, primitive type reasoning and
the :rewrite rules APPEND-ASSOC, CAR-CONS and CDR-CONS, to

Subgoal *1.1/4''
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (EQUAL (APPEND (CDR (REV3 (CDR X2))) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1))))
         (EQUAL (APPEND (REV (REV (CDR (REV3 (CDR X2)))))
                        (LIST (CAR X2) X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

The destructor terms (CAR X2) and (CDR X2) can be eliminated by using
CAR-CDR-ELIM to replace X2 by (CONS X3 X4), generalizing (CAR X2) to
X3 and (CDR X2) to X4.  This produces the following goal.

Subgoal *1.1/4'''
(IMPLIES (AND (CONSP (CONS X3 X4))
              (CONSP X4)
              (EQUAL (APPEND (CDR (REV3 X4)) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1))))
         (EQUAL (APPEND (REV (REV (CDR (REV3 X4))))
                        (LIST X3 X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1.1/4'4'
(IMPLIES (AND (CONSP X4)
              (EQUAL (APPEND (CDR (REV3 X4)) (LIST X1))
                     (APPEND (REV (REV L2)) (LIST X1))))
         (EQUAL (APPEND (REV (REV (CDR (REV3 X4))))
                        (LIST X3 X1))
                (APPEND (CDR (REV3 X4)) (LIST X1)))).

We now use the second hypothesis by substituting 
(APPEND (REV (REV L2)) (LIST X1)) for (APPEND (CDR (REV3 X4)) (LIST X1))
and throwing away the hypothesis.  This produces

Subgoal *1.1/4'5'
(IMPLIES (CONSP X4)
         (EQUAL (APPEND (REV (REV (CDR (REV3 X4))))
                        (LIST X3 X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

Name the formula above *1.1.1.

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (NOT (CONSP (CDR X2)))
              (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

But we reduce the conjecture to T, by case analysis.

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP X2))
              (ENDP (CDR X2))
              (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP X2) (NOT (CONSP (CDR X2))))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using the :definitions BINARY-APPEND and REV3, the
:executable-counterpart of CONSP and the :rewrite rule CDR-CONS, to

Subgoal *1.1/2''
(IMPLIES (AND (CONSP X2) (NOT (CONSP (CDR X2))))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

The destructor terms (CAR X2) and (CDR X2) can be eliminated by using
CAR-CDR-ELIM to replace X2 by (CONS X3 X4), generalizing (CAR X2) to
X3 and (CDR X2) to X4.  This produces the following goal.

Subgoal *1.1/2'''
(IMPLIES (AND (CONSP (CONS X3 X4))
              (NOT (CONSP X4)))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1.1/2'4'
(IMPLIES (NOT (CONSP X4))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

We suspect that the term (NOT (CONSP X4)) is irrelevant to the truth
of this conjecture and throw it out.  We will thus try to prove

Subgoal *1.1/2'5'
(EQUAL (LIST X1)
       (APPEND (REV (REV L2)) (LIST X1))).

Name the formula above *1.1.2.

Subgoal *1.1/1
(IMPLIES (AND (ENDP X2) (CONSP X2))
         (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
                (APPEND (REV (REV L2)) (LIST X1)))).

But we reduce the conjecture to T, by case analysis.

So we now return to *1.1.2, which is

(EQUAL (LIST X1)
       (APPEND (REV (REV L2)) (LIST X1))).

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

We will induct according to a scheme suggested by (REV L2).  If we
let  (:P L2 X1) denote *1.1.2 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP L2)) (:P (CDR L2) X1))
              (:P L2 X1))
     (IMPLIES (ENDP L2) (:P L2 X1))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT L2) 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.1.2/2
(IMPLIES (AND (NOT (ENDP L2))
              (EQUAL (LIST X1)
                     (APPEND (REV (REV (CDR L2)))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1.2/2'
(IMPLIES (AND (CONSP L2)
              (EQUAL (LIST X1)
                     (APPEND (REV (REV (CDR L2)))
                             (LIST X1))))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

This simplifies, using the :definitions BINARY-APPEND and REV, the
:executable-counterparts of CONSP and REV, primitive type reasoning
and the :rewrite rules CAR-CONS, CDR-CONS and REV-APPEND, to

Subgoal *1.1.2/2''
(IMPLIES (CONSP L2)
         (NOT (EQUAL (LIST X1)
                     (APPEND (REV (REV (CDR L2)))
                             (LIST X1))))).

The destructor terms (CAR L2) and (CDR L2) can be eliminated by using
CAR-CDR-ELIM to replace L2 by (CONS L3 L4), generalizing (CAR L2) to
L3 and (CDR L2) to L4.  This produces the following goal.

Subgoal *1.1.2/2'''
(IMPLIES (CONSP (CONS L3 L4))
         (NOT (EQUAL (LIST X1)
                     (APPEND (REV (REV L4)) (LIST X1))))).

This simplifies, using primitive type reasoning, to

Subgoal *1.1.2/2'4'
(NOT (EQUAL (LIST X1)
            (APPEND (REV (REV L4)) (LIST X1)))).

Name the formula above *1.1.2.1.

Subgoal *1.1.2/1
(IMPLIES (ENDP L2)
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1.2/1'
(IMPLIES (NOT (CONSP L2))
         (EQUAL (LIST X1)
                (APPEND (REV (REV L2)) (LIST X1)))).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterparts of CONSP and REV and primitive
type reasoning.

So we now return to *1.1.2.1, which is

(NOT (EQUAL (LIST X1)
            (APPEND (REV (REV L4)) (LIST X1)))).

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

We will induct according to a scheme suggested by (REV L4).  If we
let  (:P L4 X1) denote *1.1.2.1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP L4)) (:P (CDR L4) X1))
              (:P L4 X1))
     (IMPLIES (ENDP L4) (:P L4 X1))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT L4) 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.1.2.1/2
(IMPLIES (AND (NOT (ENDP L4))
              (NOT (EQUAL (LIST X1)
                          (APPEND (REV (REV (CDR L4)))
                                  (LIST X1)))))
         (NOT (EQUAL (LIST X1)
                     (APPEND (REV (REV L4)) (LIST X1))))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1.2.1/2'
(IMPLIES (AND (CONSP L4)
              (NOT (EQUAL (LIST X1)
                          (APPEND (REV (REV (CDR L4)))
                                  (LIST X1)))))
         (NOT (EQUAL (LIST X1)
                     (APPEND (REV (REV L4)) (LIST X1))))).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterparts of CONSP and REV, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and REV-APPEND
and the :type-prescription rule BINARY-APPEND.

Subgoal *1.1.2.1/1
(IMPLIES (ENDP L4)
         (NOT (EQUAL (LIST X1)
                     (APPEND (REV (REV L4)) (LIST X1))))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1.2.1/1'
(IMPLIES (NOT (CONSP L4))
         (NOT (EQUAL (LIST X1)
                     (APPEND (REV (REV L4)) (LIST X1))))).

This simplifies, using the :definitions BINARY-APPEND and REV, the
:executable-counterparts of CONSP and REV and primitive type reasoning,
to

Subgoal *1.1.2.1/1''
(CONSP L4).

We suspect that this conjecture is not a theorem.  We might as well
be trying to prove

Subgoal *1.1.2.1/1'''
NIL.

Obviously, the proof attempt has failed.

Summary
Form:  ( DEFTHM REV-IS-REV3 ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION REV3)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART REV)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE APPEND-ASSOC)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL)
        (:REWRITE REV-APPEND)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION REV))
Warnings:  Subsume
Time:  1.24 seconds (prove: 0.94, print: 0.28, other: 0.02)

******** FAILED ********  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-checker 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-checker to replace the goal by base and induction steps.
->: induct
***** Now entering the theorem prover *****

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

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).  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,
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 three nontautological subgoals.

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

But we have been asked to pretend that this goal is subsumed by the
as-yet-to-be-proved |PROOF-CHECKER Subgoal *1/3|.

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

But we have been asked to pretend that this goal is subsumed by the
as-yet-to-be-proved |PROOF-CHECKER Subgoal *1/2|.

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

But we have been asked to pretend that this goal is subsumed by the
as-yet-to-be-proved |PROOF-CHECKER Subgoal *1/1|.

That completes the proof of *1.

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-checer 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 *****

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

By the simple :definition ENDP we reduce the conjecture to

Goal'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X))))
         (EQUAL (REV X) (REV3 X))).

This simplifies, using the :definitions REV and REV3, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

Goal''
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X))))
         (EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
                (CONS (CAR (REV (CDR X)))
                      (APPEND (REV (REV (CDR (REV (CDR X)))))
                              (LIST (CAR X)))))).

This simplifies, using the :definition BINARY-APPEND, to the following
two conjectures.

Subgoal 2
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X)))
              (CONSP (REV (CDR X))))
         (EQUAL (CONS (CAR (REV (CDR X)))
                      (APPEND (CDR (REV (CDR X)))
                              (LIST (CAR X))))
                (CONS (CAR (REV (CDR X)))
                      (APPEND (REV (REV (CDR (REV (CDR X)))))
                              (LIST (CAR X)))))).

This simplifies, using primitive type reasoning and the :rewrite rule
CONS-EQUAL, to

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

But we have been asked to pretend that this goal is subsumed by the
as-yet-to-be-proved |PROOF-CHECKER Subgoal 2'|.

Subgoal 1
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X)))
              (NOT (CONSP (REV (CDR X)))))
         (EQUAL (LIST (CAR X))
                (CONS (CAR (REV (CDR X)))
                      (APPEND (REV (REV (CDR (REV (CDR X)))))
                              (LIST (CAR X)))))).

This simplifies, using the :definition BINARY-APPEND, the :executable-
counterparts of CAR, CDR, CONSP and REV, primitive type reasoning,
the :rewrite rule CDR-CONS and the :type-prescription rule REV, to

Subgoal 1'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (NOT (REV3 (CDR X))))
         (CONSP (REV (CDR X)))).

But we have been asked to pretend that this goal is subsumed by the
as-yet-to-be-proved |PROOF-CHECKER Subgoal 1'|.

Q.E.D.


Creating two new goals:  ((MAIN . 1) . 1) and ((MAIN . 1) . 2).

The proof of the current goal, (MAIN . 1), has been completed.  However,
the following subgoals remain to be proved:
  ((MAIN . 1) . 1) and ((MAIN . 1) . 2).
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. (EQUAL (REV (CDR X)) (REV3 (CDR X)))
4. (CONSP (REV (CDR X)))

The current subterm is:
(EQUAL (APPEND (CDR (REV (CDR X)))
               (LIST (CAR X)))
       (APPEND (REV (REV (CDR (REV (CDR X)))))
               (LIST (CAR X))))

AHA! We see a term of the form (REV (REV ..)), which is good since we had set out to discover why the theorem prover was not applying our lemma rev-rev. We want to dive to the second argument of the EQUAL call above, and then the first argument of that. So we use the dv to dive in that manner, i.e., to bring the proof-checker's focus on the (REV (REV ..)) subterm.
->: (dv 2 1)

The command p (Print) is like th, except that it prints only the current subterm, not the hypotheses. Notice that the preceding dv command has taken effect; the current subterm is now the (REV (REV ..)) subterm of the goal's conclusion.
->: p
(REV (REV (CDR (REV (CDR X)))))

We would like to apply the rewrite rule rev-rev to the above term. There is, in fact, a proof-checker command rewrite (or, r for short) that will do this, creating new goals for the nontrivial hypotheses that need to be relieved (proved). However, we choose first to issue the command show-rewrites (sr for short) to show all rewrite rules that may apply to the current subterm.
->: sr
1. REV-REV
  New term: (CDR (REV (CDR X)))
  Hypotheses: ((TRUE-LISTP (CDR (REV (CDR X)))))

We can now make a good guess of what the problem is. The above hypothesis was presumably not proved by ACL2. Let us leave the proof-checker and prove an appropriate lemma to help out ACL2.
->: exit
Exiting....
 NIL
ACL2 !>
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(defthm true-listp-cdr-rev
         (true-listp (cdr (rev x))))
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(defthm true-listp-cdr-rev
         (true-listp (cdr (rev x))))

Name the formula above *1.


The theorem prover has to work a bit harder than we might have guessed in order to prove this lemma, but it does succeed in doing so (in much less than a second). So click here to move on to the next slide; again, there is rarely significant value in looking over a successful proof.
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).  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,
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 (AND (NOT (ENDP X))
              (TRUE-LISTP (CDR (REV (CDR X)))))
         (TRUE-LISTP (CDR (REV X)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X)
              (TRUE-LISTP (CDR (REV (CDR X)))))
         (TRUE-LISTP (CDR (REV X)))).

This simplifies, using the :definition REV, to

Subgoal *1/2''
(IMPLIES (AND (CONSP X)
              (TRUE-LISTP (CDR (REV (CDR X)))))
         (TRUE-LISTP (CDR (APPEND (REV (CDR X))
                                  (LIST (CAR X)))))).

This simplifies, using the :definition BINARY-APPEND, to the following
two conjectures.

Subgoal *1/2.2
(IMPLIES (AND (CONSP X)
              (TRUE-LISTP (CDR (REV (CDR X))))
              (CONSP (REV (CDR X))))
         (TRUE-LISTP (CDR (CONS (CAR (REV (CDR X)))
                                (APPEND (CDR (REV (CDR X)))
                                        (LIST (CAR X))))))).

By the simple :rewrite rule CDR-CONS we reduce the conjecture to

Subgoal *1/2.2'
(IMPLIES (AND (CONSP X)
              (TRUE-LISTP (CDR (REV (CDR X))))
              (CONSP (REV (CDR X))))
         (TRUE-LISTP (APPEND (CDR (REV (CDR X)))
                             (LIST (CAR X))))).

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/2.2''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (TRUE-LISTP (CDR (REV X2)))
              (CONSP (REV X2)))
         (TRUE-LISTP (APPEND (CDR (REV X2)) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2.2'''
(IMPLIES (AND (TRUE-LISTP (CDR (REV X2)))
              (CONSP (REV X2)))
         (TRUE-LISTP (APPEND (CDR (REV X2)) (LIST X1)))).

We generalize this conjecture, replacing (REV X2) by L.  This produces

Subgoal *1/2.2'4'
(IMPLIES (AND (TRUE-LISTP (CDR L)) (CONSP L))
         (TRUE-LISTP (APPEND (CDR L) (LIST X1)))).

The destructor terms (CAR L) and (CDR L) can be eliminated by using
CAR-CDR-ELIM to replace L by (CONS L1 L2), generalizing (CAR L) to
L1 and (CDR L) to L2.  This produces the following goal.

Subgoal *1/2.2'5'
(IMPLIES (AND (CONSP (CONS L1 L2))
              (TRUE-LISTP L2))
         (TRUE-LISTP (APPEND L2 (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/2.2'6'
(IMPLIES (TRUE-LISTP L2)
         (TRUE-LISTP (APPEND L2 (LIST X1)))).

Name the formula above *1.1.

Subgoal *1/2.1
(IMPLIES (AND (CONSP X)
              (TRUE-LISTP (CDR (REV (CDR X))))
              (NOT (CONSP (REV (CDR X)))))
         (TRUE-LISTP (CDR (LIST (CAR X))))).

But we reduce the conjecture to T, by the :executable-counterpart of
TRUE-LISTP and the simple :rewrite rule CDR-CONS.

Subgoal *1/1
(IMPLIES (ENDP X)
         (TRUE-LISTP (CDR (REV X)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (TRUE-LISTP (CDR (REV X)))).

But simplification reduces this to T, using the :definition REV and
the :executable-counterparts of CDR and TRUE-LISTP.

So we now return to *1.1, which is

(IMPLIES (TRUE-LISTP L2)
         (TRUE-LISTP (APPEND L2 (LIST X1)))).

Perhaps we can prove *1.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 
(BINARY-APPEND L2 (CONS X1 'NIL)).  If we let  (:P L2 X1) denote *1.1
above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP L2)) (:P (CDR L2) X1))
              (:P L2 X1))
     (IMPLIES (ENDP L2) (:P L2 X1))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT L2) 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 three nontautological
subgoals.

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP L2))
              (TRUE-LISTP (APPEND (CDR L2) (LIST X1)))
              (TRUE-LISTP L2))
         (TRUE-LISTP (APPEND L2 (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/3'
(IMPLIES (AND (CONSP L2)
              (TRUE-LISTP (APPEND (CDR L2) (LIST X1)))
              (TRUE-LISTP L2))
         (TRUE-LISTP (APPEND L2 (LIST X1)))).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, primitive type reasoning and the :type-prescription
rule BINARY-APPEND.

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP L2))
              (NOT (TRUE-LISTP (CDR L2)))
              (TRUE-LISTP L2))
         (TRUE-LISTP (APPEND L2 (LIST X1)))).

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

Subgoal *1.1/1
(IMPLIES (AND (ENDP L2) (TRUE-LISTP L2))
         (TRUE-LISTP (APPEND L2 (LIST X1)))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/1'
(IMPLIES (AND (NOT (CONSP L2)) (TRUE-LISTP L2))
         (TRUE-LISTP (APPEND L2 (LIST X1)))).

But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, the :executable-counterpart of CONSP and primitive
type reasoning.

That completes the proofs of *1.1 and *1.

Q.E.D.

The storage of TRUE-LISTP-CDR-REV depends upon the :type-prescription
rule TRUE-LISTP.

Summary
Form:  ( DEFTHM TRUE-LISTP-CDR-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION TRUE-LISTP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION TRUE-LISTP))
Warnings:  None
Time:  0.20 seconds (prove: 0.07, print: 0.11, other: 0.02)
 TRUE-LISTP-CDR-REV
ACL2 !>
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>:u

We choose to undo the last event, true-listp-cdr-rev, using the keyword command shown: :u. We do not need to do so; the proof of rev-is-rev3 will succeed now. But true-listp-rev is a pretty ugly lemma, so here we show a way to avoid it.

Some experienced ACL2 users would have made true-listp-rev (above) a :type-prescription rule instead of (or in addition to) a :rewrite rule (the default). This would have made the immediately preceding lemma, true-listp-cdr-rev, unnecessary. Let us undo this lemma and replace it with a :type-prescription rule now. See the ACL2 documentation page RULE-CLASSES for other kinds of rules.


[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>:u
          7:x(DEFTHM REV-REV ...)
ACL2 !>
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(defthm true-listp-rev-type-prescription
         (true-listp (rev x))
         :rule-classes :type-prescription)
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(defthm true-listp-rev-type-prescription
         (true-listp (rev x))
         :rule-classes :type-prescription)

ACL2 Observation in ( DEFTHM TRUE-LISTP-REV-TYPE-PRESCRIPTION ...):
Our heuristics choose (REV X) as the :TYPED-TERM.

But we reduce the conjecture to T, by the simple :rewrite rule TRUE-
LISTP-REV.

Q.E.D.

Summary
Form:  ( DEFTHM TRUE-LISTP-REV-TYPE-PRESCRIPTION ...)
Rules: ((:REWRITE TRUE-LISTP-REV))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 TRUE-LISTP-REV-TYPE-PRESCRIPTION
ACL2 !>
[top] [prev] [next]




























































[top] [prev] [next]

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

OK, we are ready to try our main theorem again....
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(defthm rev-is-rev3 ; succeeds -> to do list is empty!
         (equal (rev x)
                (rev3 x)))

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


Name the formula above *1.


The proof succeeds! We might as well skip to the end now.
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).  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,
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 three nontautological subgoals.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/3'
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X))))
         (EQUAL (REV X) (REV3 X))).

This simplifies, using the :definitions REV and REV3, primitive type
reasoning, the :rewrite rules CAR-CONS, CDR-CONS and REV-REV and the
:type-prescription rule TRUE-LISTP-REV-TYPE-PRESCRIPTION, to

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

This simplifies, using the :definition BINARY-APPEND, to

Subgoal *1/3'''
(IMPLIES (AND (CONSP X)
              (CONSP (CDR X))
              (EQUAL (REV (CDR X)) (REV3 (CDR X)))
              (NOT (CONSP (REV (CDR X)))))
         (EQUAL (LIST (CAR X))
                (CONS (CAR (REV (CDR X)))
                      (APPEND (CDR (REV (CDR X)))
                              (LIST (CAR X)))))).

This simplifies, using the :definition BINARY-APPEND, the :executable-
counterparts of CAR, CDR and CONSP, primitive type reasoning, the :rewrite
rule CDR-CONS and the :type-prescription rule TRUE-LISTP-REV-TYPE-PRESCRIPTION\
, to

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

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2.  This produces the following goal.

Subgoal *1/3'5'
(IMPLIES (AND (CONSP (CONS X1 X2))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

This simplifies, using primitive type reasoning, to

Subgoal *1/3'6'
(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
         (CONSP (REV X2))).

Name the formula above *1.1.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/2'
(IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))))
         (EQUAL (REV X) (REV3 X))).

This simplifies, using the :definitions REV and REV3, to

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

But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterpart of CONSP and primitive
type reasoning.

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

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV X) (REV3 X))).

But simplification reduces this to T, using the :definitions REV and
REV3 and the :executable-counterpart of EQUAL.

So we now return to *1.1, which is

(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
         (CONSP (REV X2))).

Perhaps we can prove *1.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 X2).  If we
let  (:P X2) denote *1.1 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X2))
                   (NOT (ENDP (CDR X2)))
                   (:P (CDR X2)))
              (:P X2))
     (IMPLIES (AND (NOT (ENDP X2)) (ENDP (CDR X2)))
              (:P X2))
     (IMPLIES (ENDP X2) (:P X2))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X2) 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 five nontautological subgoals.

Subgoal *1.1/5
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (CONSP (REV (CDR X2)))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/5'
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (CONSP (REV (CDR X2)))
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But simplification reduces this to T, using the :definitions REV and
REV3, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rule TRUE-LISTP-REV-TYPE-PRESCRIPTION.

Subgoal *1.1/4
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (REV3 (CDR X2))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/4'
(IMPLIES (AND (CONSP X2)
              (CONSP (CDR X2))
              (REV3 (CDR X2))
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But simplification reduces this to T, using the :definitions REV and
REV3, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rule TRUE-LISTP-REV-TYPE-PRESCRIPTION.

Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP X2))
              (NOT (ENDP (CDR X2)))
              (NOT (CONSP (CDR X2)))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But we reduce the conjecture to T, by case analysis.

Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP X2))
              (ENDP (CDR X2))
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

By the simple :definition ENDP we reduce the conjecture to

Subgoal *1.1/2'
(IMPLIES (AND (CONSP X2)
              (NOT (CONSP (CDR X2)))
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But simplification reduces this to T, using the :definition REV3 and
primitive type reasoning.

Subgoal *1.1/1
(IMPLIES (AND (ENDP X2)
              (CONSP X2)
              (NOT (REV3 X2)))
         (CONSP (REV X2))).

But we reduce the conjecture to T, by case analysis.

That completes the proofs of *1.1 and *1.

Q.E.D.

Summary
Form:  ( DEFTHM REV-IS-REV3 ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REV)
        (:DEFINITION REV3)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE REV-REV)
        (:TYPE-PRESCRIPTION TRUE-LISTP-REV-TYPE-PRESCRIPTION))
Warnings:  Subsume
Time:  0.24 seconds (prove: 0.16, print: 0.06, other: 0.02)
 REV-IS-REV3
ACL2 !>

Having finally proved this lemma, we can now introduce a function that satisfies the recursion equation that we really had in mind, unlike rev3, where we had to substitute rev for rev3 in two of the three recursive calls.

We use an encapsulate event to introduce a new function, triple-rev (we have to pick a new name since "rev3" has already been used). The new function has the defining axiom we desire, and is ``witnessed'' by rev3. That is, this encapsulate directs ACL2 to check that rev3 satisfies the axiom introduced for triple-rev. The theorem rev-is-rev3 proved above is what allows ACL2 to make that deduction.


[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(encapsulate

Below is a list of signatures:
triple-rev takes one argument and returns one value.

        (((triple-rev *) => *))

What follows is a local definition:
The properties that follow will to be proved using this definition of triple-rev.

        (local (defun triple-rev (x)
                 (rev3 x)))

What follows is essentially the definition we wanted to make when we defined rev3. Notice that triple-rev does not call rev or any other function other than itself and a few built-ins (endp, list, car, cdr, cons).
        (defthm triple-rev-def
          (equal (triple-rev x)
                 (cond
                  ((endp x)
                   nil)
                  ((endp (cdr x))
                   (list (car x)))
                  (t
                   (let* ((b@c (cdr x))
                          (c@rev-b (triple-rev b@c)) ; recursive call
                          (rev-b (cdr c@rev-b))
                          (b (triple-rev rev-b))     ; recursive call
                          (a (car x))
                          (a@b (cons a b))
                          (rev-b@a (triple-rev a@b)) ; recursive call
                          (c (car c@rev-b))
                          (c@rev-b@a (cons c rev-b@a)))
                     c@rev-b@a))))

Here we specify that the formula above be used like a definition. Details may be found on the ACL2 documentation page RULE-CLASSES. This is really optional.
          :rule-classes ((:definition :clique (triple-rev)
                           :controller-alist ((triple-rev t)))))

)
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>(encapsulate
        (((triple-rev *) => *))

        (local (defun triple-rev (x)
                 (rev3 x)))

        (defthm triple-rev-def
          (equal (triple-rev x)
                 (cond
                  ((endp x)
                   nil)
                  ((endp (cdr x))
                   (list (car x)))
                  (t
                   (let* ((b@c (cdr x))
                          (c@rev-b (triple-rev b@c)) ; recursive call
                          (rev-b (cdr c@rev-b))
                          (b (triple-rev rev-b))     ; recursive call
                          (a (car x))
                          (a@b (cons a b))
                          (rev-b@a (triple-rev a@b)) ; recursive call
                          (c (car c@rev-b))
                          (c@rev-b@a (cons c rev-b@a)))
                     c@rev-b@a))))
          :rule-classes ((:definition :clique (triple-rev)
                           :controller-alist ((triple-rev t)))))

)

To verify that the two encapsulated events correctly extend the current
theory we will evaluate them.  The theory thus constructed is only
ephemeral.


Go ahead and scroll quickly through a couple of screens or so of output.
Encapsulated Events:


ACL2 !>>(LOCAL (DEFUN TRIPLE-REV (X) (REV3 X)))

Since TRIPLE-REV is non-recursive, its admission is trivial.  We observe
that the type of TRIPLE-REV is described by the theorem 
(OR (CONSP (TRIPLE-REV X)) (EQUAL (TRIPLE-REV X) NIL)).  We used the
:type-prescription rule REV3.

Summary
Form:  ( DEFUN TRIPLE-REV ...)
Rules: ((:TYPE-PRESCRIPTION REV3))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
TRIPLE-REV


ACL2 !>>(DEFTHM TRIPLE-REV-DEF
                (EQUAL (TRIPLE-REV X)
                       (COND ((ENDP X) NIL)
                             ((ENDP (CDR X)) (LIST (CAR X)))
                             (T (LET* ((B@C (CDR X))
                                       (C@REV-B (TRIPLE-REV B@C))
                                       (REV-B (CDR C@REV-B))
                                       (B (TRIPLE-REV REV-B))
                                       (A (CAR X))
                                       (A@B (CONS A B))
                                       (REV-B@A (TRIPLE-REV A@B))
                                       (C (CAR C@REV-B))
                                       (C@REV-B@A (CONS C REV-B@A)))
                                      C@REV-B@A))))
                :RULE-CLASSES
                ((:DEFINITION :CLIQUE (TRIPLE-REV)
                              :CONTROLLER-ALIST ((TRIPLE-REV T)))))

ACL2 Warning [Non-rec] in ( DEFTHM TRIPLE-REV-DEF ...):  The :DEFINITION
rule generated from TRIPLE-REV-DEF will be triggered only by terms
containing the non-recursive function symbol TRIPLE-REV.  Unless this
function is disabled, TRIPLE-REV-DEF is unlikely ever to be used.


ACL2 Warning [Subsume] in ( DEFTHM TRIPLE-REV-DEF ...):  The newly
proposed :DEFINITION rule TRIPLE-REV-DEF probably subsumes the previously
added :REWRITE rule TRIPLE-REV, in the sense that TRIPLE-REV-DEF will
now probably be applied whenever the old rule would have been.


ACL2 Warning [Subsume] in ( DEFTHM TRIPLE-REV-DEF ...):  The previously
added rule TRIPLE-REV subsumes the newly proposed :DEFINITION rule
TRIPLE-REV-DEF, 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 :definition TRIPLE-REV we reduce the conjecture to

Goal'
(EQUAL (REV3 X)
       (AND (NOT (ENDP X))
            (IF (ENDP (CDR X))
                (LIST (CAR X))
                (LET ((C@REV-B (REV3 (CDR X))))
                     (CONS (CAR C@REV-B)
                           (REV3 (CONS (CAR X)
                                       (REV3 (CDR C@REV-B))))))))).

This simplifies, using the :definition ENDP, to the following three
conjectures.

Subgoal 3
(IMPLIES (NOT (CONSP X))
         (EQUAL (REV3 X) NIL)).

But simplification reduces this to T, using the :definition REV3 and
the :executable-counterpart of EQUAL.

Subgoal 2
(IMPLIES (AND (CONSP X) (CONSP (CDR X)))
         (EQUAL (REV3 X)
                (CONS (CAR (REV3 (CDR X)))
                      (REV3 (CONS (CAR X)
                                  (REV3 (CDR (REV3 (CDR X))))))))).

But simplification reduces this to T, using the :definition REV3, primitive
type reasoning and the :rewrite rule REV-IS-REV3.

Subgoal 1
(IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))))
         (EQUAL (REV3 X) (LIST (CAR X)))).

But simplification reduces this to T, using the :definition REV3 and
primitive type reasoning.

Q.E.D.

Summary
Form:  ( DEFTHM TRIPLE-REV-DEF ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION REV3)
        (:DEFINITION TRIPLE-REV)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE REV-IS-REV3))
Warnings:  Subsume and Non-rec
Time:  0.10 seconds (prove: 0.05, print: 0.02, other: 0.03)
TRIPLE-REV-DEF

End of Encapsulated Events.

Having verified that the encapsulated events validate the signatures
of the ENCAPSULATE event, we discard the ephemeral theory and extend
the original theory as directed by the signatures and the non-LOCAL
events.

The following constraint is associated with the function TRIPLE-REV:

(EQUAL
 (TRIPLE-REV X)
 (AND
  (NOT (ENDP X))
  (IF
   (ENDP (CDR X))
   (LIST (CAR X))
   (LET
       ((B@C (CDR X)))
       (LET ((C@REV-B (TRIPLE-REV B@C)))
            (LET ((REV-B (CDR C@REV-B)))
                 (LET ((B (TRIPLE-REV REV-B)))
                      (LET ((A (CAR X)))
                           (LET ((A@B (CONS A B)))
                                (LET ((REV-B@A (TRIPLE-REV A@B)))
                                     (LET ((C (CAR C@REV-B)))
                                          (LET ((C@REV-B@A (CONS C REV-B@A)))
                                               C@REV-B@A))))))))))))

Summary
Form:  ( ENCAPSULATE (((TRIPLE-REV * ...) ...) ...) ...)
Rules: NIL
Warnings:  Subsume and Non-rec
Time:  0.18 seconds (prove: 0.05, print: 0.02, other: 0.11)
 T
ACL2 !>
[top] [prev] [next]




























































[top] [prev] [next]
We are done! All that remains is to see just where we are, and to make a few remarks.






























































[top] [prev] [next]

ACL2 !>:pbt 0


The command above means: print back through command number 0 (the start of the session).
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>:pbt 0
          0  (EXIT-BOOT-STRAP-MODE)
 L        1  (DEFUN REV (X) ...)
 L        2  (DEFUN REV3 (X) ...)
          3  (DEFTHM APPEND-ASSOC ...)
          4  (DEFTHM APPEND-NIL ...)
          5  (DEFTHM TRUE-LISTP-REV ...)
          6  (DEFTHM REV-APPEND ...)
          7  (DEFTHM REV-REV ...)
          8  (DEFTHM TRUE-LISTP-REV-TYPE-PRESCRIPTION ...)
          9  (DEFTHM REV-IS-REV3 ...)
         10:x(ENCAPSULATE (((TRIPLE-REV *) ...)) ...)
ACL2 !>

The encapsulate above was printed in very abbreviated form. Let us take a look at it in more detail using the command :pcb (print command block). Many other keyword commands are available for browsing the current ACL2 database (also called the ACL2 world); see the ACL2 documentation topic HISTORY.
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>:pcb! :x
[top] [prev] [next]




























































[top] [prev] [next]

ACL2 !>:pcb! :x
         10:x(ENCAPSULATE
                 (((TRIPLE-REV *) => *))
                 (LOCAL (DEFUN TRIPLE-REV (X) (REV3 X)))
                 (DEFTHM TRIPLE-REV-DEF
                         (EQUAL (TRIPLE-REV X)
                                (COND ((ENDP X) NIL)
                                      ((ENDP (CDR X)) (LIST (CAR X)))
                                      (T (LET* ((B@C (CDR X))
                                                (C@REV-B (TRIPLE-REV B@C))
                                                (REV-B (CDR C@REV-B))
                                                (B (TRIPLE-REV REV-B))
                                                (A (CAR X))
                                                (A@B (CONS A B))
                                                (REV-B@A (TRIPLE-REV A@B))
                                                (C (CAR C@REV-B))
                                                (C@REV-B@A (CONS C REV-B@A)))
                                               C@REV-B@A))))
                         :RULE-CLASSES
                         ((:DEFINITION :CLIQUE (TRIPLE-REV)
                                       :CONTROLLER-ALIST ((TRIPLE-REV T))))))
              (DEFTHM TRIPLE-REV-DEF
                      (EQUAL (TRIPLE-REV X)
                             (COND ((ENDP X) NIL)
                                   ((ENDP (CDR X)) (LIST (CAR X)))
                                   (T (LET* ((B@C (CDR X))
                                             (C@REV-B (TRIPLE-REV B@C))
                                             (REV-B (CDR C@REV-B))
                                             (B (TRIPLE-REV REV-B))
                                             (A (CAR X))
                                             (A@B (CONS A B))
                                             (REV-B@A (TRIPLE-REV A@B))
                                             (C (CAR C@REV-B))
                                             (C@REV-B@A (CONS C REV-B@A)))
                                            C@REV-B@A))))
                      :RULE-CLASSES
                      ((:DEFINITION :CLIQUE (TRIPLE-REV)
                                    :CONTROLLER-ALIST ((TRIPLE-REV T)))))
ACL2 !>
[top] [prev] [next]




























































[top] [prev] [next]
Here are a few points that we have not yet made. [top] [prev] [next]




























































[top] [prev]
This concludes the tutorial. We thank Rob Sumners for useful comments on an earlier draft.

[top] [prev]