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

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, toBelow 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, toHad 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, toHad 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 toFinally 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`

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

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.

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

`[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]ACL2 !>(defthm rev-append (equal (rev (append x y)) (append (rev y) (rev x))))

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.[top] [prev] [next]ACL2 !>(defthm rev-append (equal (rev (append x y)) (append (rev y) (rev x)))) 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) 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]ACL2 !>(defthm append-assoc (equal (append (append x y) z) (append x (append y z))))

[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]ACL2 !>(defthm rev-append (equal (rev (append x y)) (append (rev y) (rev x))))

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.[top] [prev] [next]ACL2 !>(defthm rev-append (equal (rev (append x y)) (append (rev y) (rev x)))) 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) 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]ACL2 !>(defthm append-nil (implies (true-listp x) (equal (append x nil) x)))

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

The proof succeeds, so we can pop this lemma off our to do list, leaving us with:[top] [prev] [next]ACL2 !>(defthm true-listp-rev (true-listp (rev x))) Name the formula above *1.

`(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]ACL2 !>(defthm rev-append (equal (rev (append x y)) (append (rev y) (rev x))))

The proof succeeds, so we can pop this lemma off our to do list, leaving us with:[top] [prev] [next]ACL2 !>(defthm rev-append (equal (rev (append x y)) (append (rev y) (rev x)))) Name the formula above *1.

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

`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]ACL2 !>(thm (equal (rev (rev 3)) nil))

Well, this use of[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 !>

`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))) 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]ACL2 !>(defthm rev-is-rev3 (equal (rev x) (rev3 x)))

The proof fails. In fact we can look through the proof attempt below and see that the lemma[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.

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

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]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 ***** [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-BUILDER 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-BUILDER 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-BUILDER 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 ``->: 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-BUILDER 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-BUILDER 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-builder's
focus on the `(REV (REV ..))`

subterm.
->: (dv 2 1)The command

`p`

(`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-builder 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-builder and prove an appropriate lemma to help out ACL2.

->: exit Exiting.... NIL ACL2 !>

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

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.[top] [prev] [next]ACL2 !>(defthm true-listp-cdr-rev (true-listp (cdr (rev 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)) (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]ACL2 !>:u

We choose to undo the last event,

`true-listp-cdr-rev`

, using the
`: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]ACL2 !>:u 7:x(DEFTHM REV-REV ...) ACL2 !>

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

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

OK, we are ready to try our main theorem again....

The proof succeeds! We might as well skip to the end now.[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.

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.

Below is a list of signatures:[top] [prev] [next]ACL2 !>(encapsulate

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

Go ahead and scroll quickly through a couple of screens or so of output.[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.

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

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

[top] [prev] [next]ACL2 !>:pbt 0

The command above means:printbackthrough 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`

(printcommandblock). Many other keyword commands are available for browsing the current ACL2 database (also called the ACL2world); 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]

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

- See the ACL2 home page for more information about ACL2.
- In particular, see the ACL2 documentation for more information. You can get more introductory information at ACL2-TUTORIAL.
- There are two books on ACL2: a textbook and an edited collection of case studies. You can get information on them here.
- More realistic ACL2 examples typically require both more high-level strategy in constructing the proof and more low-level hints. The latter are explained in the ACL2 documentation topic, HINTS. See also the Flying Demo.
- The ACL2 distribution comes with an organized collection of
*books*, which contain functions and proved theorems. It can be very helpful to start proof efforts by including these books. For example, suppose that there had been a book available with all the lemmas about`rev`

that precede`rev-append`

in our development, where`true-listp-rev`

was stored as a`:type-prescription`

rule. Then our proof effort would likely have avoided the need to prove the lemma`rev-append`

:`rev-rev`

is proved without the need for`rev-append`

. Specifically: without`rev-append`

, the following ``weakening'' of`rev-append`

is proved in the course of proving`rev-rev`

.(EQUAL (REV (APPEND RV (LIST X1))) (CONS X1 (REV RV))).

On the other hand, it is not a bad thing that we proved`rev-append`

. A useful by-product of proof development is a collection of useful lemmas. - ACL2 is increasingly used as a programming language, even without doing any proofs. This demo does not really touch on that aspect of ACL2.

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