J Strother Moore, Department of Computer Sciences, University of Texas at Austin

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

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!
```

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

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

Recursive definitions, such as the one above, carry a proof obligation. Roughly speaking, the obligation is to show that an appropriate[top] [prev] [next]ACL2 !>(defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x)))))

`(cdr x)`

of the recursive call is smaller, in an
appropriate sense, than is `x`

. The paragraph below is ACL2's way
of informing the user that it has carried out such an argument. Experienced
ACL2 users rarely find any reason to read that particular commentary.
The admission of REV is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of REV is described by the theorem (TRUE-LISTP (REV X)). We used primitive type reasoning and the :type-prescription rules BINARY-APPEND and TRUE-LISTP-APPEND. Summary Form: ( DEFUN REV ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION BINARY-APPEND) (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) REV

Next, we set ourselves to the task of definining the function

`rev3`

discussed in the introduction. The comments in blue below
the definition are intended to help make sense of it!
[top] [prev] [next]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]ACL2 !>(defun rev3 (x) (cond ((endp x) nil) ((endp (cdr x)) (list (car x))) (t (let* ((b@c (cdr x)) (c@rev-b (rev3 b@c)) ; note recursive call of rev3 (rev-b (cdr c@rev-b)) (b (rev rev-b)) ; note call of rev (a (car x)) (a@b (cons a b)) (rev-b@a (rev a@b)) ; note call of rev (c (car c@rev-b)) (c@rev-b@a (cons c rev-b@a))) c@rev-b@a)))) The admission of REV3 is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of REV3 is described by the theorem (TRUE-LISTP (REV3 X)). We used primitive type reasoning and the :type-prescription rule REV. Summary Form: ( DEFUN REV3 ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION REV)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) REV3 ACL2 !>

We next assign ourselves the following goal: prove that

`(rev x)`

equals `(rev3 x)`

. Later we will see how that
theorem enables us to introduce a function like `rev3`

that does not
``cheat'' by calling the function `rev`

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

[top] [prev] [next]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.[top] [prev] [next]ACL2 !>(defthm rev-is-rev3 (equal (rev x) (rev3 x)))

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

*1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (REV3 X). This suggestion was produced using the :induction rules REV and REV3. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (ENDP (CDR X))) (:P (CDR X))) (:P X)) (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit REV3. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Splitter note (see :DOC splitter) for Subgoal *1/3'' (2 subgoals). if-intro: ((:DEFINITION BINARY-APPEND)) Subgoal *1/3.2 Subgoal *1/3.2' Subgoal *1/3.2'' Subgoal *1/3.2''' Subgoal *1/3.2'4' Subgoal *1/3.2'5' Subgoal *1/3.2'6' Subgoal *1/3.2'7' Subgoal *1/3.2'8'Below is the first simplification checkpoint, that is, the first goal that cannot be simplified (other than the original theorem, actually). You can tell that it cannot be simplified because some other technique is being used on it.

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

([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/3.2' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (EQUAL (REV (CDR X)) (REV3 (CDR X))) (CONSP (REV (CDR X)))) (EQUAL (APPEND (CDR (REV (CDR X))) (LIST (CAR X))) (APPEND (REV (REV (CDR (REV (CDR X))))) (LIST (CAR X))))) *1.1 (Subgoal *1/3.2'8') is pushed for proof by induction. ])You are welcome to continue scrolling through ACL2's attempt to prove the theorem, which ultimately fails. We recommend that you skip to near the end of the proof attempt.

Subgoal *1/3.1 Subgoal *1/3.1' Subgoal *1/3.1'' Subgoal *1/3.1''' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/3.1' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (REV3 (CDR X)))) (CONSP (REV (CDR X)))) *1.2 (Subgoal *1/3.1''') is pushed for proof by induction. ]) Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/1 Subgoal *1/1' So we now return to *1.2, which is (IMPLIES (AND (CONSP X2) (NOT (REV3 X2))) (CONSP (REV X2))). Subgoal *1.2/5 Subgoal *1.2/5' Subgoal *1.2/4 Subgoal *1.2/4' Subgoal *1.2/3 Subgoal *1.2/2 Subgoal *1.2/2' Subgoal *1.2/1 *1.2 is COMPLETED! Thus key checkpoint Subgoal *1/3.1' is COMPLETED! We therefore turn our attention to *1.1, which is (IMPLIES (AND (TRUE-LISTP L2) (CONSP X2)) (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1)) (APPEND (REV (REV L2)) (LIST X1)))). Subgoal *1.1/3 Subgoal *1.1/3' Subgoal *1.1/3'' Subgoal *1.1/3''' Subgoal *1.1/3'4' Subgoal *1.1/3'5' Subgoal *1.1/3'6' Subgoal *1.1/3'7' *1.1.1 (Subgoal *1.1/3'7') is pushed for proof by induction. Subgoal *1.1/2 Subgoal *1.1/1 Subgoal *1.1/1' Subgoal *1.1/1'' Subgoal *1.1/1''' *1.1.2 (Subgoal *1.1/1''') is pushed for proof by induction. So we now return to *1.1.2, which is (IMPLIES (CONSP X2) (EQUAL (APPEND (CDR (REV3 X2)) (LIST X1)) (LIST X1))). Subgoal *1.1.2/4 Subgoal *1.1.2/4' Subgoal *1.1.2/4'' Subgoal *1.1.2/4''' Subgoal *1.1.2/4'4' Subgoal *1.1.2/4'5' Splitter note (see :DOC splitter) for Subgoal *1.1.2/4'5' (2 subgoals). if-intro: ((:DEFINITION TRUE-LISTP)) Subgoal *1.1.2/4.2 Subgoal *1.1.2/4.2' Subgoal *1.1.2/4.2'' Subgoal *1.1.2/4.2''' *1.1.2.1 (Subgoal *1.1.2/4.2''') is pushed for proof by induction.Finally we are near the end of the proof attempt!. Scroll down and you will see ACL2 give up, because somehow it has produced the goal of proving

`nil`

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

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

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

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

[top] [prev] [next]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)
```

.
The proof below fails, but it is not terribly long. Scroll down through it and see if you can find the first simplification checkpoint.[top] [prev] [next]ACL2 !>(defthm rev-rev (equal (rev (rev x)) x))

*1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (REV X). This suggestion was produced using the :induction rule REV. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit REV. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/2''' Subgoal *1/2'4' Subgoal *1/2'5' Subgoal *1/2'6' Subgoal *1/2'7' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2'' (IMPLIES (AND (CONSP X) (EQUAL (REV (REV (CDR X))) (CDR X))) (EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X)))) X)) *1.1 (Subgoal *1/2'7') is pushed for proof by induction. ]) Subgoal *1/1 Subgoal *1/1' Subgoal *1/1'' Subgoal *1/1''' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/1'' (IMPLIES (NOT (CONSP X)) (NOT X)) A goal of NIL, Subgoal *1/1''', has been generated! Obviously, the proof attempt has failed. ]) Summary Form: ( DEFTHM REV-REV ...) Rules: ((:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION REV) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART REV) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION REV) (:TYPE-PRESCRIPTION REV)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 1351 --- The key checkpoint goals, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Goal (EQUAL (REV (REV X)) X) *** Key checkpoints under a top-level induction before generating a goal of NIL (see :DOC nil-goal): *** Subgoal *1/2'' (IMPLIES (AND (CONSP X) (EQUAL (REV (REV (CDR X))) (CDR X))) (EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X)))) X)) Subgoal *1/1'' (IMPLIES (NOT (CONSP X)) (NOT X)) ACL2 Error in ( DEFTHM REV-REV ...): See :DOC failure. ******** FAILED ******** ACL2 !>Did you find the first simplification checkpoint above? The next slide reproduces the ACL2 input and output shown on this slide, but contains a comment analyzing that checkpoint.

The goal just above is the first simplification checkpoint. Can you think of a lemma that might lead to a useful simplification of some subterm of the goal above? After thinking about that question, move on to the next slide by scrolling down to the[top] [prev] [next]ACL2 !>(defthm rev-rev (equal (rev (rev x)) x)) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (REV X). This suggestion was produced using the :induction rule REV. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit REV. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/2''' Subgoal *1/2'4' Subgoal *1/2'5' Subgoal *1/2'6' Subgoal *1/2'7' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2'' (IMPLIES (AND (CONSP X) (EQUAL (REV (REV (CDR X))) (CDR X))) (EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X)))) X)) *1.1 (Subgoal *1/2'7') is pushed for proof by induction. ])

`[next]`

link or clicking here.
Subgoal *1/1 Subgoal *1/1' Subgoal *1/1'' Subgoal *1/1''' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/1'' (IMPLIES (NOT (CONSP X)) (NOT X)) A goal of NIL, Subgoal *1/1''', has been generated! Obviously, the proof attempt has failed. ]) Summary Form: ( DEFTHM REV-REV ...) Rules: ((:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION REV) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART REV) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION REV) (:TYPE-PRESCRIPTION REV)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 1351 --- The key checkpoint goals, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Goal (EQUAL (REV (REV X)) X) *** Key checkpoints under a top-level induction before generating a goal of NIL (see :DOC nil-goal): *** Subgoal *1/2'' (IMPLIES (AND (CONSP X) (EQUAL (REV (REV (CDR X))) (CDR X))) (EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X)))) X)) Subgoal *1/1'' (IMPLIES (NOT (CONSP X)) (NOT X)) ACL2 Error in ( DEFTHM REV-REV ...): See :DOC failure. ******** FAILED ******** ACL2 !>

The simplification checkpoint above suggests the theorem on the next slide. Our current to do list is

`(rev-rev rev-is-rev3)`

, and if the next lemma
(`rev-append`

) fails then it will be ```
(rev-append rev-rev
rev-is-rev3)
```

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

This proof succeeds![top] [prev] [next]ACL2 !>(defthm rev-append (equal (rev (append x y)) (append (rev y) (rev x)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction.

*1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (APPEND X Y). This suggestion was produced using the :induction rules BINARY-APPEND and REV. If we let (:P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y)) (:P X Y)) (IMPLIES (ENDP X) (:P X Y))). This induction is justified by the same argument used to admit BINARY-APPEND. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/2''' Subgoal *1/2'4' Subgoal *1/2'5' Subgoal *1/2'6' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2'' (IMPLIES (AND (CONSP X) (EQUAL (REV (APPEND (CDR X) Y)) (APPEND (REV Y) (REV (CDR X))))) (EQUAL (APPEND (REV (APPEND (CDR X) Y)) (LIST (CAR X))) (APPEND (REV Y) (REV (CDR X)) (LIST (CAR X))))) *1.1 (Subgoal *1/2'6') is pushed for proof by induction. ]) Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (AND (TRUE-LISTP RV) (TRUE-LISTP RV0)) (EQUAL (APPEND (APPEND RV0 RV) (LIST X1)) (APPEND RV0 RV (LIST X1)))). Subgoal *1.1/3 Subgoal *1.1/3' Subgoal *1.1/2 Subgoal *1.1/1 Subgoal *1.1/1' *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/2'' and Goal are COMPLETED! Q.E.D. Summary Form: ( DEFTHM REV-APPEND ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION REV) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION BINARY-APPEND) (:INDUCTION REV) (:INDUCTION TRUE-LISTP) (:REWRITE APPEND-TO-NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION REV) (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 2624 REV-APPEND ACL2 !>

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

Below is the only simplification checkpoint. It says that every non-cons is[top] [prev] [next]ACL2 !>(defthm rev-rev (equal (rev (rev x)) x)) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (REV X). This suggestion was produced using the :induction rule REV. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit REV. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' Subgoal *1/1'' Subgoal *1/1'''

`nil`

. Well, 3 (for example)
is a non-cons that is not `nil`

. You can see clearly that 3 is a
counterexample to the following conjecture by executing the following form,
which ACL2 proves:`(thm (IMPLIES (NOT (CONSP 3)) (NOT 3)))`

`(thm (not (equal (rev (rev 3)) 3)))`

So we will add the hypothesis that

`X`

is a true list. But first, a question: To what value is
`(rev (rev 3))`

provably equal? How can we check our conjecture
with ACL2? One way to do this is shown on the next
slide.
([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/1'' (IMPLIES (NOT (CONSP X)) (NOT X)) A goal of NIL, Subgoal *1/1''', has been generated! Obviously, the proof attempt has failed. ]) Summary Form: ( DEFTHM REV-REV ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION REV) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART REV) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION REV) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR) (:REWRITE REV-APPEND)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 375 --- The key checkpoint goals, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Goal (EQUAL (REV (REV X)) X) *** Key checkpoint under a top-level induction before generating a goal of NIL (see :DOC nil-goal): *** Subgoal *1/1'' (IMPLIES (NOT (CONSP X)) (NOT X)) ACL2 Error in ( DEFTHM REV-REV ...): See :DOC failure. ******** FAILED ******** ACL2 !>

[top] [prev] [next]ACL2 !>(thm (equal (rev (rev 3)) nil))

Well, this use of[top] [prev] [next]ACL2 !>(thm (equal (rev (rev 3)) nil)) Q.E.D. Summary Form: ( THM ...) Rules: ((:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART REV)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 5 Proof succeeded. ACL2 !>

`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]ACL2 !>(defthm rev-rev (implies (true-listp x) (equal (rev (rev x)) x)))

[top] [prev] [next]ACL2 !>(defthm rev-rev (implies (true-listp x) (equal (rev (rev x)) x))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (REV X). This suggestion was produced using the :induction rules REV and TRUE-LISTP. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit REV. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/2 Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM REV-REV ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION REV) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART REV) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION REV) (:INDUCTION TRUE-LISTP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR) (:REWRITE REV-APPEND)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 447 REV-REV ACL2 !>

[top] [prev] [next]ACL2 !>(defthm rev-is-rev3 (equal (rev x) (rev3 x)))

The proof succeeds! But we got a bit lucky; for example, with the
`:hints`

shown below, we can turn off a proof technique
used in that proof in order to make the proof fail.

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

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

[top] [prev] [next]ACL2 !>(defthm rev-is-rev3 (equal (rev x) (rev3 x)) :hints (("Goal" :do-not '(eliminate-destructors)))) ACL2 Warning [Subsume] in ( DEFTHM REV-IS-REV3 ...): A newly proposed :REWRITE rule generated from REV-IS-REV3 probably subsumes the previously added :REWRITE rules REV-REV and REV-APPEND, in the sense that the new rule will now probably be applied whenever the old rules would have been. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (REV3 X). This suggestion was produced using the :induction rules REV and REV3. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (ENDP (CDR X))) (:P (CDR X))) (:P X)) (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit REV3. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/3'4' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/3'4' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (REV3 (CDR X)))) (CONSP (REV (CDR X)))) *1.1 (Subgoal *1/3'4') is pushed for proof by induction. ]) Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (REV3 (CDR X)))) (CONSP (REV (CDR X)))). No induction schemes are suggested by *1.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM REV-IS-REV3 ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION REV) (:DEFINITION REV3) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION REV) (:INDUCTION REV3) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE REV-REV) (:TYPE-PRESCRIPTION REV)) Warnings: Subsume Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 1787 --- The key checkpoint goals, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Goal (EQUAL (REV X) (REV3 X)) *** Key checkpoint under a top-level induction: *** Subgoal *1/3'4' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (REV3 (CDR X)))) (CONSP (REV (CDR X)))) ACL2 Error in ( DEFTHM REV-IS-REV3 ...): See :DOC failure. ******** FAILED ******** ACL2 !>

[top] [prev] [next]ACL2 !>(verify (equal (rev x) (rev3 x)))

The above use of

`verify`

puts us into an interactive loop, where we
can issue commands at a lower level than we have seen above. We will precede
each proof-builder command on the next slide by a comment (in blue) that
explains what it does.
Experience suggests that this sort of lemma, the equivalence of two recursively defined functions, will require a proof by induction. So we instruct the proof-builder to replace the goal by base and induction steps.[top] [prev] [next]ACL2 !>(verify (equal (rev x) (rev3 x)))

->: induct ***** Now entering the theorem prover ***** *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. We have been told to use induction. Two induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (REV3 X). This suggestion was produced using the :induction rules REV and REV3. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (ENDP (CDR X))) (:P (CDR X))) (:P X)) (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit REV3. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/3 (IMPLIES (AND (NOT (ENDP X)) (NOT (ENDP (CDR X))) (EQUAL (REV (CDR X)) (REV3 (CDR X)))) (EQUAL (REV X) (REV3 X))) Subgoal *1/3 is subsumed by a goal yet to be proved. ]) Subgoal *1/2 ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X))) (EQUAL (REV X) (REV3 X))) Subgoal *1/2 is subsumed by a goal yet to be proved. ]) Subgoal *1/1 ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/1 (IMPLIES (ENDP X) (EQUAL (REV X) (REV3 X))) Subgoal *1/1 is subsumed by a goal yet to be proved. ]) *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Creating three new goals: (MAIN . 1), (MAIN . 2) and (MAIN . 3). The proof of the current goal, MAIN, has been completed. However, the following subgoals remain to be proved: (MAIN . 1), (MAIN . 2) and (MAIN . 3). Now proving (MAIN . 1).The proof-builder has just told us that we have three goals to prove. Let us use the

`th`

command (for ``->: th *** Top-level hypotheses: 1. (NOT (ENDP X)) 2. (NOT (ENDP (CDR X))) 3. (EQUAL (REV (CDR X)) (REV3 (CDR X))) The current subterm is: (EQUAL (REV X) (REV3 X))No particular idea comes to mind for how to proceed (we are willing to forge ahead at this point without a great deal of thought). So we issue a command,

`bash`

, to simplify the current goal using the full power
of the ACL2 simplifier.
->: bash ***** Now entering the theorem prover ***** Goal' Goal'' Goal''' Goal'4' ([ A key checkpoint: Goal'4' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (REV3 (CDR X)))) (CONSP (REV (CDR X)))) Goal'4' is subsumed by a goal yet to be proved. ]) Q.E.D. Creating one new goal: ((MAIN . 1) . 1). The proof of the current goal, (MAIN . 1), has been completed. However, the following subgoals remain to be proved: ((MAIN . 1) . 1). Now proving ((MAIN . 1) . 1).What did bash leave us with? Let's take a look at the goal left on top of the goal stack, again using the

`th`

command.
->: th *** Top-level hypotheses: 1. (CONSP X) 2. (CONSP (CDR X)) 3. (NOT (REV3 (CDR X))) The current subterm is: (CONSP (REV (CDR X)))AHA! It looks like hypotheses 2 and 3 are contradictory. It seems that ACL2 would know that if only it would expand the definition of

`REV3`

on `(CDR X)`

. The proof finally
succeeds with such a hint:
[top] [prev]ACL2 !>(defthm rev-is-rev3 (equal (rev x) (rev3 x)) :hints (("Goal" :do-not '(eliminate-destructors) :expand ((rev3 (cdr x))))))

ACL2 Warning [Subsume] in ( DEFTHM REV-IS-REV3 ...): A newly proposed :REWRITE rule generated from REV-IS-REV3 probably subsumes the previously added :REWRITE rules REV-REV and REV-APPEND, in the sense that the new rule will now probably be applied whenever the old rules would have been. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (REV3 X). This suggestion was produced using the :induction rules REV and REV3. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (ENDP (CDR X))) (:P (CDR X))) (:P X)) (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit REV3. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM REV-IS-REV3 ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION REV) (:DEFINITION REV3) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION REV) (:INDUCTION REV3) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE REV-REV) (:TYPE-PRESCRIPTION BINARY-APPEND) (:TYPE-PRESCRIPTION REV) (:TYPE-PRESCRIPTION REV3) (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND)) Warnings: Subsume Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 1680 REV-IS-REV3 ACL2 !>