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")
"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)))))
Again, we recommend that you navigate between slides using the [prev] and [next] links.
[top] [prev] [next]
ACL2 !>(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x))
(list (car x)))))
Recursive definitions, such as the one above, carry a
proof obligation. Roughly speaking, the obligation is to show that an
appropriate measure of the arguments decreases (in an appropriate sense)
for each recursive call. Thus, in the present function, ACL2 must prove that
the argument (cdr x) of the recursive call is smaller, in an
appropriate sense, than is x. The paragraph below is ACL2's way
of informing the user that it has carried out such an argument. Experienced
ACL2 users rarely find any reason to read that particular commentary.
The admission of REV is trivial, using the relation E0-ORD-< (which
is known to be well-founded on the domain recognized by E0-ORDINALP)
and the measure (ACL2-COUNT X). We observe that the type of REV is
described by the theorem (OR (CONSP (REV X)) (EQUAL (REV X) NIL)).
We used primitive type reasoning and the :type-prescription rule BINARY-
APPEND.
Summary
Form: ( DEFUN REV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:TYPE-PRESCRIPTION BINARY-APPEND))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
REV
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))))
@ 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 !>
(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)))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-is-rev3
(equal (rev x)
(rev3 x)))
The theorem prover chooses to prove this theorem by induction, because no other
proof technique applies.
The proof eventually fails. Scroll down a few screens, just glancing briefly at the output, until you see some added commentary (in blue).
Name the formula above *1.
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. Subsumption reduces that number to one.
We will induct according to a scheme suggested by (REV3 X). If we
let (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (ENDP (CDR X)))
(:P (CDR X)))
(:P X))
(IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP). When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
(NOT (ENDP (CDR X)))
(EQUAL (REV (CDR X)) (REV3 (CDR X))))
(EQUAL (REV X) (REV3 X))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/3'
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X))))
(EQUAL (REV X) (REV3 X))).
This simplifies, using the :definitions REV and REV3, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to
Subgoal *1/3''
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X))))
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
(CONS (CAR (REV (CDR X)))
(APPEND (REV (REV (CDR (REV (CDR X)))))
(LIST (CAR X)))))).
This simplifies, using the :definition BINARY-APPEND, to the following
two conjectures.
Subgoal *1/3.2
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X)))
(CONSP (REV (CDR X))))
(EQUAL (CONS (CAR (REV (CDR X)))
(APPEND (CDR (REV (CDR X)))
(LIST (CAR X))))
(CONS (CAR (REV (CDR X)))
(APPEND (REV (REV (CDR (REV (CDR X)))))
(LIST (CAR X)))))).
This simplifies, using primitive type reasoning and the :rewrite rule
CONS-EQUAL, to
Below is the first simplification checkpoint, that is, the first goal that
cannot be simplified (other than the original theorem, actually). You can tell
that it cannot be simplified because some other technique is being used on it,
in this case destructor eliminiation. The documentation topic PROOF-TREE shows
how to use an Emacs-based tool to locate simplification checkpoints automatically.
Look carefully at the simplification checkpoint below. Does any term suggest a rewrite rule that would simplify it?
Subgoal *1/3.2'
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X)))
(CONSP (REV (CDR X))))
(EQUAL (APPEND (CDR (REV (CDR X)))
(LIST (CAR X)))
(APPEND (REV (REV (CDR (REV (CDR X)))))
(LIST (CAR X))))).
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
You are welcome to continue scrolling through ACL2's vain attempt to prove the
theorem. We recommend that you skip to the end of the proof
attempt either now, or soon. (We will give you some more chances.)
Subgoal *1/3.2''
(IMPLIES (AND (CONSP (CONS X1 X2))
(CONSP X2)
(EQUAL (REV X2) (REV3 X2))
(CONSP (REV X2)))
(EQUAL (APPEND (CDR (REV X2)) (LIST X1))
(APPEND (REV (REV (CDR (REV X2))))
(LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1/3.2'''
(IMPLIES (AND (CONSP X2)
(EQUAL (REV X2) (REV3 X2))
(CONSP (REV X2)))
(EQUAL (APPEND (CDR (REV X2)) (LIST X1))
(APPEND (REV (REV (CDR (REV X2))))
(LIST X1)))).
We now use the second hypothesis by cross-fertilizing (REV3 X2) for
(REV X2) and throwing away the hypothesis. This produces
Subgoal *1/3.2'4'
(IMPLIES (AND (CONSP X2) (CONSP (REV X2)))
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV (CDR (REV X2))))
(LIST X1)))).
We generalize this conjecture, replacing (REV X2) by L. This produces
Subgoal *1/3.2'5'
(IMPLIES (AND (CONSP X2) (CONSP L))
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV (CDR L)))
(LIST X1)))).
The destructor terms (CAR L) and (CDR L) can be eliminated by using
CAR-CDR-ELIM to replace L by (CONS L1 L2), generalizing (CAR L) to
L1 and (CDR L) to L2. This produces the following goal.
Subgoal *1/3.2'6'
(IMPLIES (AND (CONSP (CONS L1 L2)) (CONSP X2))
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1/3.2'7'
(IMPLIES (CONSP X2)
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
Name the formula above *1.1.
Subgoal *1/3.1
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X)))
(NOT (CONSP (REV (CDR X)))))
(EQUAL (LIST (CAR X))
(CONS (CAR (REV (CDR X)))
(APPEND (REV (REV (CDR (REV (CDR X)))))
(LIST (CAR X)))))).
This simplifies, using the :definition BINARY-APPEND, the :executable-
counterparts of CAR, CDR, CONSP and REV, primitive type reasoning,
the :rewrite rule CDR-CONS and the :type-prescription rule REV, to
Subgoal *1/3.1'
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(NOT (REV3 (CDR X))))
(CONSP (REV (CDR X)))).
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
Subgoal *1/3.1''
(IMPLIES (AND (CONSP (CONS X1 X2))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
This simplifies, using primitive type reasoning, to
Subgoal *1/3.1'''
(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
(CONSP (REV X2))).
Name the formula above *1.2.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X)))
(EQUAL (REV X) (REV3 X))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))))
(EQUAL (REV X) (REV3 X))).
This simplifies, using the :definitions REV and REV3, to
Subgoal *1/2''
(IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))))
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
(LIST (CAR X)))).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterpart of CONSP and primitive
type reasoning.
Subgoal *1/1
(IMPLIES (ENDP X)
(EQUAL (REV X) (REV3 X))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(EQUAL (REV X) (REV3 X))).
But simplification reduces this to T, using the :definitions REV and
REV3 and the :executable-counterpart of EQUAL.
So we now return to *1.2, which is
(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
(CONSP (REV X2))).
Perhaps we can prove *1.2 by induction. Two induction schemes are
suggested by this conjecture. Subsumption reduces that number to one.
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
We will induct according to a scheme suggested by (REV3 X2). If we
let (:P X2) denote *1.2 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(:P (CDR X2)))
(:P X2))
(IMPLIES (AND (NOT (ENDP X2)) (ENDP (CDR X2)))
(:P X2))
(IMPLIES (ENDP X2) (:P X2))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X2) is decreasing according to the
relation E0-ORD-< (which is known to be well-founded on the domain
recognized by E0-ORDINALP). When applied to the goal at hand the above
induction scheme produces the following five nontautological subgoals.
Subgoal *1.2/5
(IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(CONSP (REV (CDR X2)))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.2/5'
(IMPLIES (AND (CONSP X2)
(CONSP (CDR X2))
(CONSP (REV (CDR X2)))
(NOT (REV3 X2)))
(CONSP (REV X2))).
But simplification reduces this to T, using the :definitions REV and
REV3, primitive type reasoning and the :rewrite rules CAR-CONS and
CDR-CONS.
Subgoal *1.2/4
(IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(REV3 (CDR X2))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.2/4'
(IMPLIES (AND (CONSP X2)
(CONSP (CDR X2))
(REV3 (CDR X2))
(NOT (REV3 X2)))
(CONSP (REV X2))).
But simplification reduces this to T, using the :definitions REV and
REV3, primitive type reasoning and the :rewrite rules CAR-CONS and
CDR-CONS.
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
Subgoal *1.2/3
(IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(NOT (CONSP (CDR X2)))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
But we reduce the conjecture to T, by case analysis.
Subgoal *1.2/2
(IMPLIES (AND (NOT (ENDP X2))
(ENDP (CDR X2))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.2/2'
(IMPLIES (AND (CONSP X2)
(NOT (CONSP (CDR X2)))
(NOT (REV3 X2)))
(CONSP (REV X2))).
But simplification reduces this to T, using the :definition REV3 and
primitive type reasoning.
Subgoal *1.2/1
(IMPLIES (AND (ENDP X2)
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
But we reduce the conjecture to T, by case analysis.
That completes the proof of *1.2.
We therefore turn our attention to *1.1, which is
(IMPLIES (CONSP X2)
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
Perhaps we can prove *1.1 by induction. Two induction schemes are
suggested by this conjecture. We will choose arbitrarily among these.
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
We will induct according to a scheme suggested by (REV3 X2). If we
let (:P L2 X1 X2) denote *1.1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(:P L2 X1 (CDR X2)))
(:P L2 X1 X2))
(IMPLIES (AND (NOT (ENDP X2)) (ENDP (CDR X2)))
(:P L2 X1 X2))
(IMPLIES (ENDP X2) (:P L2 X1 X2))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X2) is decreasing according to the
relation E0-ORD-< (which is known to be well-founded on the domain
recognized by E0-ORDINALP). When applied to the goal at hand the above
induction scheme produces the following four nontautological subgoals.
Subgoal *1.1/4
(IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(EQUAL (APPEND (CDR (REV3 (CDR X2))) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))
(CONSP X2))
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/4'
(IMPLIES (AND (CONSP X2)
(CONSP (CDR X2))
(EQUAL (APPEND (CDR (REV3 (CDR X2))) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1))))
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
This simplifies, using the :definitions REV and REV3, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to
Subgoal *1.1/4''
(IMPLIES (AND (CONSP X2)
(CONSP (CDR X2))
(EQUAL (APPEND (CDR (REV3 (CDR X2))) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1))))
(EQUAL (APPEND (APPEND (REV (REV (CDR (REV3 (CDR X2)))))
(LIST (CAR X2)))
(LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
The destructor terms (CAR X2) and (CDR X2) can be eliminated by using
CAR-CDR-ELIM to replace X2 by (CONS X3 X4), generalizing (CAR X2) to
X3 and (CDR X2) to X4. This produces the following goal.
Subgoal *1.1/4'''
(IMPLIES (AND (CONSP (CONS X3 X4))
(CONSP X4)
(EQUAL (APPEND (CDR (REV3 X4)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1))))
(EQUAL (APPEND (APPEND (REV (REV (CDR (REV3 X4))))
(LIST X3))
(LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
This simplifies, using primitive type reasoning, to
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
Subgoal *1.1/4'4'
(IMPLIES (AND (CONSP X4)
(EQUAL (APPEND (CDR (REV3 X4)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1))))
(EQUAL (APPEND (APPEND (REV (REV (CDR (REV3 X4))))
(LIST X3))
(LIST X1))
(APPEND (CDR (REV3 X4)) (LIST X1)))).
We now use the second hypothesis by substituting
(APPEND (REV (REV L2)) (LIST X1)) for (APPEND (CDR (REV3 X4)) (LIST X1))
and throwing away the hypothesis. This produces
Subgoal *1.1/4'5'
(IMPLIES (CONSP X4)
(EQUAL (APPEND (APPEND (REV (REV (CDR (REV3 X4))))
(LIST X3))
(LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
Name the formula above *1.1.1.
Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(NOT (CONSP (CDR X2)))
(CONSP X2))
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
But we reduce the conjecture to T, by case analysis.
Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP X2))
(ENDP (CDR X2))
(CONSP X2))
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/2'
(IMPLIES (AND (CONSP X2) (NOT (CONSP (CDR X2))))
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
This simplifies, using the :definitions BINARY-APPEND and REV3, the
:executable-counterpart of CONSP and the :rewrite rule CDR-CONS, to
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
Subgoal *1.1/2''
(IMPLIES (AND (CONSP X2) (NOT (CONSP (CDR X2))))
(EQUAL (LIST X1)
(APPEND (REV (REV L2)) (LIST X1)))).
The destructor terms (CAR X2) and (CDR X2) can be eliminated by using
CAR-CDR-ELIM to replace X2 by (CONS X3 X4), generalizing (CAR X2) to
X3 and (CDR X2) to X4. This produces the following goal.
Subgoal *1.1/2'''
(IMPLIES (AND (CONSP (CONS X3 X4))
(NOT (CONSP X4)))
(EQUAL (LIST X1)
(APPEND (REV (REV L2)) (LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1.1/2'4'
(IMPLIES (NOT (CONSP X4))
(EQUAL (LIST X1)
(APPEND (REV (REV L2)) (LIST X1)))).
We suspect that the term (NOT (CONSP X4)) is irrelevant to the truth
of this conjecture and throw it out. We will thus try to prove
Subgoal *1.1/2'5'
(EQUAL (LIST X1)
(APPEND (REV (REV L2)) (LIST X1))).
Name the formula above *1.1.2.
Subgoal *1.1/1
(IMPLIES (AND (ENDP X2) (CONSP X2))
(EQUAL (APPEND (CDR (REV3 X2)) (LIST X1))
(APPEND (REV (REV L2)) (LIST X1)))).
But we reduce the conjecture to T, by case analysis.
So we now return to *1.1.2, which is
(EQUAL (LIST X1)
(APPEND (REV (REV L2)) (LIST X1))).
Perhaps we can prove *1.1.2 by induction. One induction scheme is
suggested by this conjecture.
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
We will induct according to a scheme suggested by (REV L2). If we
let (:P L2 X1) denote *1.1.2 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP L2)) (:P (CDR L2) X1))
(:P L2 X1))
(IMPLIES (ENDP L2) (:P L2 X1))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT L2) is decreasing according to the
relation E0-ORD-< (which is known to be well-founded on the domain
recognized by E0-ORDINALP). When applied to the goal at hand the above
induction scheme produces the following two nontautological subgoals.
Subgoal *1.1.2/2
(IMPLIES (AND (NOT (ENDP L2))
(EQUAL (LIST X1)
(APPEND (REV (REV (CDR L2)))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (REV L2)) (LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1.2/2'
(IMPLIES (AND (CONSP L2)
(EQUAL (LIST X1)
(APPEND (REV (REV (CDR L2)))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (REV L2)) (LIST X1)))).
This simplifies, using the :definition REV, to
Subgoal *1.1.2/2''
(IMPLIES (AND (CONSP L2)
(EQUAL (LIST X1)
(APPEND (REV (REV (CDR L2)))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (APPEND (REV (CDR L2)) (LIST (CAR L2))))
(LIST X1)))).
The destructor terms (CAR L2) and (CDR L2) can be eliminated by using
CAR-CDR-ELIM to replace L2 by (CONS L3 L4), generalizing (CAR L2) to
L3 and (CDR L2) to L4. This produces the following goal.
Subgoal *1.1.2/2'''
(IMPLIES (AND (CONSP (CONS L3 L4))
(EQUAL (LIST X1)
(APPEND (REV (REV L4)) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (APPEND (REV L4) (LIST L3)))
(LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1.1.2/2'4'
(IMPLIES (EQUAL (LIST X1)
(APPEND (REV (REV L4)) (LIST X1)))
(EQUAL (LIST X1)
(APPEND (REV (APPEND (REV L4) (LIST L3)))
(LIST X1)))).
We generalize this conjecture, replacing (REV L4) by RV. This produces
Subgoal *1.1.2/2'5'
(IMPLIES (EQUAL (LIST X1)
(APPEND (REV RV) (LIST X1)))
(EQUAL (LIST X1)
(APPEND (REV (APPEND RV (LIST L3)))
(LIST X1)))).
Name the formula above *1.1.2.1.
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
Subgoal *1.1.2/1
(IMPLIES (ENDP L2)
(EQUAL (LIST X1)
(APPEND (REV (REV L2)) (LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1.2/1'
(IMPLIES (NOT (CONSP L2))
(EQUAL (LIST X1)
(APPEND (REV (REV L2)) (LIST X1)))).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterparts of CONSP and REV and primitive
type reasoning.
So we now return to *1.1.2.1, which is
(IMPLIES (EQUAL (LIST X1)
(APPEND (REV RV) (LIST X1)))
(EQUAL (LIST X1)
(APPEND (REV (APPEND RV (LIST L3)))
(LIST X1)))).
Perhaps we can prove *1.1.2.1 by induction. Two induction schemes
are suggested by this conjecture. Subsumption reduces that number
to one.
We will induct according to a scheme suggested by
(BINARY-APPEND RV (CONS L3 'NIL)). If we let (:P L3 RV X1) denote
*1.1.2.1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP RV))
(:P L3 (CDR RV) X1))
(:P L3 RV X1))
(IMPLIES (ENDP RV) (:P L3 RV X1))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT RV) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following three nontautological
subgoals.
Subgoal *1.1.2.1/3
(IMPLIES (AND (NOT (ENDP RV))
(EQUAL (LIST X1)
(APPEND (REV (APPEND (CDR RV) (LIST L3)))
(LIST X1)))
(EQUAL (LIST X1)
(APPEND (REV RV) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (APPEND RV (LIST L3)))
(LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1.2.1/3'
(IMPLIES (AND (CONSP RV)
(EQUAL (LIST X1)
(APPEND (REV (APPEND (CDR RV) (LIST L3)))
(LIST X1)))
(EQUAL (LIST X1)
(APPEND (REV RV) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (APPEND RV (LIST L3)))
(LIST X1)))).
This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to
Subgoal *1.1.2.1/3''
(IMPLIES (AND (CONSP RV)
(EQUAL (LIST X1)
(APPEND (REV (APPEND (CDR RV) (LIST L3)))
(LIST X1)))
(EQUAL (LIST X1)
(APPEND (APPEND (REV (CDR RV)) (LIST (CAR RV)))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV (APPEND (CDR RV) (LIST L3)))
(LIST (CAR RV)))
(LIST X1)))).
The destructor terms (CAR RV) and (CDR RV) can be eliminated by using
CAR-CDR-ELIM to replace RV by (CONS RV1 RV2), generalizing (CAR RV)
to RV1 and (CDR RV) to RV2. This produces the following goal.
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
Subgoal *1.1.2.1/3'''
(IMPLIES (AND (CONSP (CONS RV1 RV2))
(EQUAL (LIST X1)
(APPEND (REV (APPEND RV2 (LIST L3)))
(LIST X1)))
(EQUAL (LIST X1)
(APPEND (APPEND (REV RV2) (LIST RV1))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
(LIST RV1))
(LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1.1.2.1/3'4'
(IMPLIES (AND (EQUAL (LIST X1)
(APPEND (REV (APPEND RV2 (LIST L3)))
(LIST X1)))
(EQUAL (LIST X1)
(APPEND (APPEND (REV RV2) (LIST RV1))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
(LIST RV1))
(LIST X1)))).
We generalize this conjecture, replacing (APPEND RV2 (LIST L3)) by
L and restricting the type of the new variable L to be that of the
term it replaces, as established by primitive type reasoning and BINARY-
APPEND. This produces
Subgoal *1.1.2.1/3'5'
(IMPLIES (AND (CONSP L)
(EQUAL (LIST X1)
(APPEND (REV L) (LIST X1)))
(EQUAL (LIST X1)
(APPEND (APPEND (REV RV2) (LIST RV1))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV L) (LIST RV1))
(LIST X1)))).
We generalize this conjecture, replacing (REV L) by RV. This produces
Subgoal *1.1.2.1/3'6'
(IMPLIES (AND (CONSP L)
(EQUAL (LIST X1) (APPEND RV (LIST X1)))
(EQUAL (LIST X1)
(APPEND (APPEND (REV RV2) (LIST RV1))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND RV (LIST RV1))
(LIST X1)))).
We suspect that the term (CONSP L) is irrelevant to the truth of this
conjecture and throw it out. We will thus try to prove
Subgoal *1.1.2.1/3'7'
(IMPLIES (AND (EQUAL (LIST X1) (APPEND RV (LIST X1)))
(EQUAL (LIST X1)
(APPEND (APPEND (REV RV2) (LIST RV1))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND RV (LIST RV1))
(LIST X1)))).
Name the formula above *1.1.2.1.1.
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
Subgoal *1.1.2.1/2
(IMPLIES (AND (NOT (ENDP RV))
(NOT (EQUAL (LIST X1)
(APPEND (REV (CDR RV)) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV RV) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (APPEND RV (LIST L3)))
(LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1.2.1/2'
(IMPLIES (AND (CONSP RV)
(NOT (EQUAL (LIST X1)
(APPEND (REV (CDR RV)) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV RV) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (APPEND RV (LIST L3)))
(LIST X1)))).
This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to
Subgoal *1.1.2.1/2''
(IMPLIES (AND (CONSP RV)
(NOT (EQUAL (LIST X1)
(APPEND (REV (CDR RV)) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV (CDR RV)) (LIST (CAR RV)))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV (APPEND (CDR RV) (LIST L3)))
(LIST (CAR RV)))
(LIST X1)))).
The destructor terms (CAR RV) and (CDR RV) can be eliminated by using
CAR-CDR-ELIM to replace RV by (CONS RV1 RV2), generalizing (CAR RV)
to RV1 and (CDR RV) to RV2. This produces the following goal.
Subgoal *1.1.2.1/2'''
(IMPLIES (AND (CONSP (CONS RV1 RV2))
(NOT (EQUAL (LIST X1)
(APPEND (REV RV2) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV RV2) (LIST RV1))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
(LIST RV1))
(LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1.1.2.1/2'4'
(IMPLIES (AND (NOT (EQUAL (LIST X1)
(APPEND (REV RV2) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV RV2) (LIST RV1))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
(LIST RV1))
(LIST X1)))).
We generalize this conjecture, replacing (REV RV2) by RV. This produces
Subgoal *1.1.2.1/2'5'
(IMPLIES (AND (NOT (EQUAL (LIST X1) (APPEND RV (LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND RV (LIST RV1))
(LIST X1))))
(EQUAL (LIST X1)
(APPEND (APPEND (REV (APPEND RV2 (LIST L3)))
(LIST RV1))
(LIST X1)))).
Name the formula above *1.1.2.1.2.
Had enough yet? If so, skip to the end of the proof
attempt. (We will give you some more chances.)
Subgoal *1.1.2.1/1
(IMPLIES (AND (ENDP RV)
(EQUAL (LIST X1)
(APPEND (REV RV) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (APPEND RV (LIST L3)))
(LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Finally we are near the end of the proof attempt!.
Scroll down a screen or two and you will see ACL2 give up, because somehow it
has produced the goal of proving nil (false), which is
impossible.
Subgoal *1.1.2.1/1'
(IMPLIES (AND (NOT (CONSP RV))
(EQUAL (LIST X1)
(APPEND (REV RV) (LIST X1))))
(EQUAL (LIST X1)
(APPEND (REV (APPEND RV (LIST L3)))
(LIST X1)))).
This simplifies, using the :definitions BINARY-APPEND and REV, the
:executable-counterparts of CONSP and REV, primitive type reasoning
and the :rewrite rules CAR-CONS and CDR-CONS, to
Subgoal *1.1.2.1/1''
(CONSP RV).
We suspect that this conjecture is not a theorem. We might as well
be trying to prove
Subgoal *1.1.2.1/1'''
NIL.
Obviously, the proof attempt has failed.
Summary
Form: ( DEFTHM REV-IS-REV3 ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION REV3)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART REV)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-EQUAL)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION REV))
Warnings: None
Time: 1.36 seconds (prove: 1.02, print: 0.33, other: 0.01)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>
(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))
rev-is-rev3, but an analysis of a simplification checkpoint
from the preceding proof attempt led us to decide to prove the theorem
above. The proof will fail, leading us to a to do list of (rev-rev
rev-is-rev3).
[top] [prev] [next]
ACL2 !>(defthm rev-rev
(equal (rev (rev x))
x))
The proof below fails, but it is not terribly long. Scroll down through it and
see if you can find the first simplification checkpoint.
Name the formula above *1.
Perhaps we can prove *1 by induction. One induction scheme is suggested
by this conjecture.
We will induct according to a scheme suggested by (REV X). If we let
(:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP). When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (REV (REV (CDR X))) (CDR X)))
(EQUAL (REV (REV X)) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (REV (REV (CDR X))) (CDR X)))
(EQUAL (REV (REV X)) X)).
This simplifies, using the :definition REV, to
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(EQUAL (REV (REV (CDR X))) (CDR X)))
(EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X))))
X)).
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
(EQUAL (REV (REV X2)) X2))
(EQUAL (REV (APPEND (REV X2) (LIST X1)))
(CONS X1 X2))).
This simplifies, using primitive type reasoning, to
Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (REV X2)) X2)
(EQUAL (REV (APPEND (REV X2) (LIST X1)))
(CONS X1 X2))).
We now use the hypothesis by cross-fertilizing (REV (REV X2)) for X2
and throwing away the hypothesis. This produces
Subgoal *1/2'5'
(EQUAL (REV (APPEND (REV X2) (LIST X1)))
(CONS X1 (REV (REV X2)))).
We generalize this conjecture, replacing (REV X2) by RV. This produces
Subgoal *1/2'6'
(EQUAL (REV (APPEND RV (LIST X1)))
(CONS X1 (REV RV))).
Name the formula above *1.1.
Subgoal *1/1
(IMPLIES (ENDP X)
(EQUAL (REV (REV X)) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(EQUAL (REV (REV X)) X)).
This simplifies, using the :definition REV, the :executable-counterpart
of REV and primitive type reasoning, to
Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X)).
Name the formula above *1.2.
No induction schemes are suggested by *1.2. Consequently, the proof
attempt has failed.
Summary
Form: ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART REV)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.13 seconds (prove: 0.08, print: 0.03, other: 0.02)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>
Did you find the first simplification checkpoint above? The next slide
reproduces the ACL2 input and output shown on this slide, but contains a
comment analyzing that checkpoint.
[top] [prev] [next]
ACL2 !>(defthm rev-rev
(equal (rev (rev x))
x))
Name the formula above *1.
Perhaps we can prove *1 by induction. One induction scheme is suggested
by this conjecture.
We will induct according to a scheme suggested by (REV X). If we let
(:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP). When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (REV (REV (CDR X))) (CDR X)))
(EQUAL (REV (REV X)) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (REV (REV (CDR X))) (CDR X)))
(EQUAL (REV (REV X)) X)).
This simplifies, using the :definition REV, to
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(EQUAL (REV (REV (CDR X))) (CDR X)))
(EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X))))
X)).
The goal just above is the first simplification checkpoint. (Notice the use of
destructor elimination below.) Can you think of a lemma that might lead to a
useful simplification of some subterm of the goal above? After thinking about
that question, on to the next slide by scrolling down to the
[next] link or clicking here.
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
(EQUAL (REV (REV X2)) X2))
(EQUAL (REV (APPEND (REV X2) (LIST X1)))
(CONS X1 X2))).
This simplifies, using primitive type reasoning, to
Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (REV X2)) X2)
(EQUAL (REV (APPEND (REV X2) (LIST X1)))
(CONS X1 X2))).
We now use the hypothesis by cross-fertilizing (REV (REV X2)) for X2
and throwing away the hypothesis. This produces
Subgoal *1/2'5'
(EQUAL (REV (APPEND (REV X2) (LIST X1)))
(CONS X1 (REV (REV X2)))).
We generalize this conjecture, replacing (REV X2) by RV. This produces
Subgoal *1/2'6'
(EQUAL (REV (APPEND RV (LIST X1)))
(CONS X1 (REV RV))).
Name the formula above *1.1.
Subgoal *1/1
(IMPLIES (ENDP X)
(EQUAL (REV (REV X)) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(EQUAL (REV (REV X)) X)).
This simplifies, using the :definition REV, the :executable-counterpart
of REV and primitive type reasoning, to
Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X)).
Name the formula above *1.2.
No induction schemes are suggested by *1.2. Consequently, the proof
attempt has failed.
Summary
Form: ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART REV)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.13 seconds (prove: 0.08, print: 0.03, other: 0.02)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>
(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))))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-append
(equal (rev (append x y))
(append (rev y) (rev x))))
Name the formula above *1.
This proof fails. This failure is a bit unusual in that we find that some
simplification checkpoint other than the first suggests a particularly useful
lemma. Scroll down through the proof and look for the blue comments.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.
We will induct according to a scheme suggested by (BINARY-APPEND X Y).
If we let (:P X Y) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
(:P X Y))
(IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT X) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following two nontautological
subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (APPEND (REV (APPEND (CDR X) Y))
(LIST (CAR X)))
(APPEND (REV Y)
(REV (CDR X))
(LIST (CAR X))))).
The mention of destructor terms below suggests that the goal above is a
simplification checkpoint. Although you may find a rewrite rule suggested by
this checkpoint, let us scroll further down and look for more simplification checkpoints.
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
(EQUAL (REV (APPEND X2 Y))
(APPEND (REV Y) (REV X2))))
(EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (APPEND X2 Y))
(APPEND (REV Y) (REV X2)))
(EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1)))).
Just above is another simplification checkpoint (as the description below
points to equality substitution rather than further simplification). But we do
not yet see a term that suggests a really nice rewrite rule.
We now use the hypothesis by substituting (APPEND (REV Y) (REV X2))
for (REV (APPEND X2 Y)) and throwing away the hypothesis. This produces
Subgoal *1/2'5'
(EQUAL (APPEND (APPEND (REV Y) (REV X2))
(LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1))).
AHA! The simplification checkpoint just above does clearly suggest that we prove the
associativity of the append operator. We push such a lemma onto
our exsting to do list, (rev-append rev-rev rev-is-rev3). You are
welcome to scroll to the end of this failed proof, but we suggest that you take
the action of an experienced ACL2 user, which is to ignore the rest of the
proof now that we have discovered a suitable rewrite rule to prove and go do
it! So click here.
We generalize this conjecture, replacing (REV X2) by RV and (REV Y)
by RV0. This produces
Subgoal *1/2'6'
(EQUAL (APPEND (APPEND RV0 RV) (LIST X1))
(APPEND RV0 RV (LIST X1))).
Name the formula above *1.1.
Subgoal *1/1
(IMPLIES (ENDP X)
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
This simplifies, using the :definitions BINARY-APPEND and REV, to
Subgoal *1/1''
(IMPLIES (NOT (CONSP X))
(EQUAL (REV Y) (APPEND (REV Y) NIL))).
We generalize this conjecture, replacing (REV Y) by RV. This produces
Subgoal *1/1'''
(IMPLIES (NOT (CONSP X))
(EQUAL RV (APPEND RV NIL))).
We suspect that the term (NOT (CONSP X)) is irrelevant to the truth
of this conjecture and throw it out. We will thus try to prove
Subgoal *1/1'4'
(EQUAL RV (APPEND RV NIL)).
Name the formula above *1.2.
Perhaps we can prove *1.2 by induction. One induction scheme is suggested
by this conjecture.
We will induct according to a scheme suggested by (BINARY-APPEND RV 'NIL).
If we let (:P RV) denote *1.2 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP RV)) (:P (CDR RV)))
(:P RV))
(IMPLIES (ENDP RV) (:P RV))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT RV) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following two nontautological
subgoals.
Subgoal *1.2/2
(IMPLIES (AND (NOT (ENDP RV))
(EQUAL (CDR RV) (APPEND (CDR RV) NIL)))
(EQUAL RV (APPEND RV NIL))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.2/2'
(IMPLIES (AND (CONSP RV)
(EQUAL (CDR RV) (APPEND (CDR RV) NIL)))
(EQUAL RV (APPEND RV NIL))).
But simplification reduces this to T, using the :definition BINARY-
APPEND, primitive type reasoning and the :rewrite rule CAR-CDR-ELIM.
Subgoal *1.2/1
(IMPLIES (ENDP RV)
(EQUAL RV (APPEND RV NIL))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.2/1'
(IMPLIES (NOT (CONSP RV))
(EQUAL RV (APPEND RV NIL))).
This simplifies, using the :definition BINARY-APPEND and primitive
type reasoning, to
Subgoal *1.2/1''
(IMPLIES (NOT (CONSP RV)) (NOT RV)).
Name the formula above *1.2.1.
No induction schemes are suggested by *1.2.1. Consequently, the proof
attempt has failed.
Summary
Form: ( DEFTHM REV-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:ELIM CAR-CDR-ELIM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CDR-ELIM)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS))
Warnings: None
Time: 0.25 seconds (prove: 0.13, print: 0.10, other: 0.02)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm append-assoc
(equal (append (append x y) z)
(append x (append y z))))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm append-assoc
(equal (append (append x y) z)
(append x (append y z))))
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.
We will induct according to a scheme suggested by (BINARY-APPEND X Y).
If we let (:P X Y Z) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y Z))
(:P X Y Z))
(IMPLIES (ENDP X) (:P X Y Z))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT X) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following two nontautological
subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (APPEND (APPEND (CDR X) Y) Z)
(APPEND (CDR X) Y Z)))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X Y Z))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (APPEND (APPEND (CDR X) Y) Z)
(APPEND (CDR X) Y Z)))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X Y Z))).
But simplification reduces this to T, using the :definition BINARY-
APPEND, primitive type reasoning and the :rewrite rules CAR-CONS and
CDR-CONS.
Subgoal *1/1
(IMPLIES (ENDP X)
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X Y Z))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X Y Z))).
But simplification reduces this to T, using the :definition BINARY-
APPEND and primitive type reasoning.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM APPEND-ASSOC ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS))
Warnings: None
Time: 0.07 seconds (prove: 0.03, print: 0.02, other: 0.02)
APPEND-ASSOC
ACL2 !>
(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))))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-append
(equal (rev (append x y))
(append (rev y) (rev x))))
Name the formula above *1.
The proof fails once again. You are welcome to scroll through the proof.
However, we are happy to give you a shortcut by directing you to the simplification checkpoint
that we think most clearly suggests some useful lemmas. Click here if you would like that shortcut.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.
We will induct according to a scheme suggested by (BINARY-APPEND X Y).
If we let (:P X Y) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
(:P X Y))
(IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT X) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following two nontautological
subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (APPEND (REV (APPEND (CDR X) Y))
(LIST (CAR X)))
(APPEND (REV Y)
(REV (CDR X))
(LIST (CAR X))))).
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
(EQUAL (REV (APPEND X2 Y))
(APPEND (REV Y) (REV X2))))
(EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (APPEND X2 Y))
(APPEND (REV Y) (REV X2)))
(EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1)))).
We now use the hypothesis by substituting (APPEND (REV Y) (REV X2))
for (REV (APPEND X2 Y)) and throwing away the hypothesis. This produces
Subgoal *1/2'5'
(EQUAL (APPEND (APPEND (REV Y) (REV X2))
(LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1))).
By the simple :rewrite rule APPEND-ASSOC we reduce the conjecture to
Subgoal *1/2'6'
(EQUAL (APPEND (REV Y) (REV X2) (LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1))).
But we reduce the conjecture to T, by primitive type reasoning.
Subgoal *1/1
(IMPLIES (ENDP X)
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
This simplifies, using the :definitions BINARY-APPEND and REV, to
Subgoal *1/1''
(IMPLIES (NOT (CONSP X))
(EQUAL (REV Y) (APPEND (REV Y) NIL))).
The simplification checkpoint above suggests two rewrite rules. One, which we call
append-nil, says that (append x nil) is equal to
x under suitable hypotheses. What are those hypotheses? We need
to know that the last cdr of x is nil.
(Note: This kind of thinking is sometimes annoying to beginning users of ACL2,
but with a little practice one gets used to the need for
hypotheses of the form (true-listp ...), where the function
true-listp recognizes lists whose last cdr is
nil.) Here are some examples related to this notion of true
list.
ACL2 !>(cons 1 nil) (1) ACL2 !>(cons 2 (cons 1 nil)) (2 1) ACL2 !>(true-listp (cons 1 nil)) T ACL2 !>(true-listp (cons 2 (cons 1 nil))) T ACL2 !>(true-listp (cons 2 (cons 1 7))) NIL ACL2 !>Now in order to apply this rewrite rule, rewriting
(EQUAL (REV Y) (APPEND (REV Y) NIL))nil, we need to know that (REV Y) is a true list.
This observation leads us to prove a second lemma,
true-listp-rev. So at the moment our to do stack is:(append-nil true-listp-rev rev-append rev-rev rev-is-rev3)
We recommend that you click here to move to the next slide.
We generalize this conjecture, replacing (REV Y) by RV. This produces
Subgoal *1/1'''
(IMPLIES (NOT (CONSP X))
(EQUAL RV (APPEND RV NIL))).
We suspect that the term (NOT (CONSP X)) is irrelevant to the truth
of this conjecture and throw it out. We will thus try to prove
Subgoal *1/1'4'
(EQUAL RV (APPEND RV NIL)).
Name the formula above *1.1.
Perhaps we can prove *1.1 by induction. One induction scheme is suggested
by this conjecture.
We will induct according to a scheme suggested by (BINARY-APPEND RV 'NIL).
If we let (:P RV) denote *1.1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP RV)) (:P (CDR RV)))
(:P RV))
(IMPLIES (ENDP RV) (:P RV))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT RV) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following two nontautological
subgoals.
Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP RV))
(EQUAL (CDR RV) (APPEND (CDR RV) NIL)))
(EQUAL RV (APPEND RV NIL))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/2'
(IMPLIES (AND (CONSP RV)
(EQUAL (CDR RV) (APPEND (CDR RV) NIL)))
(EQUAL RV (APPEND RV NIL))).
But simplification reduces this to T, using the :definition BINARY-
APPEND, primitive type reasoning and the :rewrite rule CAR-CDR-ELIM.
Subgoal *1.1/1
(IMPLIES (ENDP RV)
(EQUAL RV (APPEND RV NIL))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/1'
(IMPLIES (NOT (CONSP RV))
(EQUAL RV (APPEND RV NIL))).
This simplifies, using the :definition BINARY-APPEND and primitive
type reasoning, to
Subgoal *1.1/1''
(IMPLIES (NOT (CONSP RV)) (NOT RV)).
Name the formula above *1.1.1.
No induction schemes are suggested by *1.1.1. Consequently, the proof
attempt has failed.
Summary
Form: ( DEFTHM REV-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:ELIM CAR-CDR-ELIM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE APPEND-ASSOC)
(:REWRITE CAR-CDR-ELIM)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS))
Warnings: None
Time: 0.23 seconds (prove: 0.15, print: 0.06, other: 0.02)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm append-nil
(implies (true-listp x)
(equal (append x nil) x)))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm append-nil
(implies (true-listp x)
(equal (append x nil) x)))
Name the formula above *1.
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (BINARY-APPEND X 'NIL).
If we let (:P X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT X) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following three nontautological
subgoals.
Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (APPEND (CDR X) NIL) (CDR X))
(TRUE-LISTP X))
(EQUAL (APPEND X NIL) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/3'
(IMPLIES (AND (CONSP X)
(EQUAL (APPEND (CDR X) NIL) (CDR X))
(TRUE-LISTP X))
(EQUAL (APPEND X NIL) X)).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, primitive type reasoning and the :rewrite rule
CAR-CDR-ELIM.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(NOT (TRUE-LISTP (CDR X)))
(TRUE-LISTP X))
(EQUAL (APPEND X NIL) X)).
But we reduce the conjecture to T, by primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (ENDP X) (TRUE-LISTP X))
(EQUAL (APPEND X NIL) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X))
(EQUAL (APPEND X NIL) X)).
But simplification reduces this to T, using the :definition TRUE-LISTP,
the :executable-counterparts of BINARY-APPEND, CONSP and EQUAL and
primitive type reasoning.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM APPEND-NIL ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION IMPLIES)
(:DEFINITION NOT)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART BINARY-APPEND)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CDR-ELIM))
Warnings: None
Time: 0.07 seconds (prove: 0.03, print: 0.02, other: 0.02)
APPEND-NIL
ACL2 !>
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)))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm true-listp-rev
(true-listp (rev x)))
Name the formula above *1.
The proof succeeds, so we can pop this lemma off our to do list, leaving us
with:(rev-append rev-rev rev-is-rev3)
Perhaps we can prove *1 by induction. One induction scheme is suggested
by this conjecture.
We will induct according to a scheme suggested by (REV X). If we let
(:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP). When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(TRUE-LISTP (REV (CDR X))))
(TRUE-LISTP (REV X))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(TRUE-LISTP (REV (CDR X))))
(TRUE-LISTP (REV X))).
This simplifies, using the :definition REV, to
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(TRUE-LISTP (REV (CDR X))))
(TRUE-LISTP (APPEND (REV (CDR X)) (LIST (CAR X))))).
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
(TRUE-LISTP (REV X2)))
(TRUE-LISTP (APPEND (REV X2) (LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1/2'4'
(IMPLIES (TRUE-LISTP (REV X2))
(TRUE-LISTP (APPEND (REV X2) (LIST X1)))).
We generalize this conjecture, replacing (REV X2) by RV. This produces
Subgoal *1/2'5'
(IMPLIES (TRUE-LISTP RV)
(TRUE-LISTP (APPEND RV (LIST X1)))).
Name the formula above *1.1.
Subgoal *1/1
(IMPLIES (ENDP X) (TRUE-LISTP (REV X))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(TRUE-LISTP (REV X))).
But simplification reduces this to T, using the :definition REV and
the :executable-counterpart of TRUE-LISTP.
So we now return to *1.1, which is
(IMPLIES (TRUE-LISTP RV)
(TRUE-LISTP (APPEND RV (LIST X1)))).
Perhaps we can prove *1.1 by induction. Two induction schemes are
suggested by this conjecture. These merge into one derived induction
scheme.
We will induct according to a scheme suggested by
(BINARY-APPEND RV (CONS X1 'NIL)). If we let (:P RV X1) denote *1.1
above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP RV)) (:P (CDR RV) X1))
(:P RV X1))
(IMPLIES (ENDP RV) (:P RV X1))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT RV) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following three nontautological
subgoals.
Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP RV))
(TRUE-LISTP (APPEND (CDR RV) (LIST X1)))
(TRUE-LISTP RV))
(TRUE-LISTP (APPEND RV (LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/3'
(IMPLIES (AND (CONSP RV)
(TRUE-LISTP (APPEND (CDR RV) (LIST X1)))
(TRUE-LISTP RV))
(TRUE-LISTP (APPEND RV (LIST X1)))).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, primitive type reasoning and the :type-prescription
rule BINARY-APPEND.
Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP RV))
(NOT (TRUE-LISTP (CDR RV)))
(TRUE-LISTP RV))
(TRUE-LISTP (APPEND RV (LIST X1)))).
But we reduce the conjecture to T, by primitive type reasoning.
Subgoal *1.1/1
(IMPLIES (AND (ENDP RV) (TRUE-LISTP RV))
(TRUE-LISTP (APPEND RV (LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/1'
(IMPLIES (AND (NOT (CONSP RV)) (TRUE-LISTP RV))
(TRUE-LISTP (APPEND RV (LIST X1)))).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, the :executable-counterpart of CONSP and primitive
type reasoning.
That completes the proofs of *1.1 and *1.
Q.E.D.
The storage of TRUE-LISTP-REV depends upon the :type-prescription rule
TRUE-LISTP.
Summary
Form: ( DEFTHM TRUE-LISTP-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION TRUE-LISTP))
Warnings: None
Time: 0.12 seconds (prove: 0.04, print: 0.06, other: 0.02)
TRUE-LISTP-REV
ACL2 !>
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-append
(equal (rev (append x y))
(append (rev y) (rev x))))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-append
(equal (rev (append x y))
(append (rev y) (rev x))))
Name the formula above *1.
The proof succeeds, so we can pop this lemma off our to do list, leaving us
with:(rev-rev rev-is-rev3)
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to two.
However, one of these is flawed and so we are left with one viable
candidate.
We will induct according to a scheme suggested by (BINARY-APPEND X Y).
If we let (:P X Y) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y))
(:P X Y))
(IMPLIES (ENDP X) (:P X Y))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT X) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following two nontautological
subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
This simplifies, using the :definitions BINARY-APPEND and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(EQUAL (REV (APPEND (CDR X) Y))
(APPEND (REV Y) (REV (CDR X)))))
(EQUAL (APPEND (REV (APPEND (CDR X) Y))
(LIST (CAR X)))
(APPEND (REV Y)
(REV (CDR X))
(LIST (CAR X))))).
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
Subgoal *1/2'''
(IMPLIES (AND (CONSP (CONS X1 X2))
(EQUAL (REV (APPEND X2 Y))
(APPEND (REV Y) (REV X2))))
(EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1/2'4'
(IMPLIES (EQUAL (REV (APPEND X2 Y))
(APPEND (REV Y) (REV X2)))
(EQUAL (APPEND (REV (APPEND X2 Y)) (LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1)))).
We now use the hypothesis by substituting (APPEND (REV Y) (REV X2))
for (REV (APPEND X2 Y)) and throwing away the hypothesis. This produces
Subgoal *1/2'5'
(EQUAL (APPEND (APPEND (REV Y) (REV X2))
(LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1))).
By the simple :rewrite rule APPEND-ASSOC we reduce the conjecture to
Subgoal *1/2'6'
(EQUAL (APPEND (REV Y) (REV X2) (LIST X1))
(APPEND (REV Y) (REV X2) (LIST X1))).
But we reduce the conjecture to T, by primitive type reasoning.
Subgoal *1/1
(IMPLIES (ENDP X)
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(EQUAL (REV (APPEND X Y))
(APPEND (REV Y) (REV X)))).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, primitive type reasoning and the :rewrite rules APPEND-
NIL and TRUE-LISTP-REV.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM REV-APPEND ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:ELIM CAR-CDR-ELIM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE APPEND-ASSOC)
(:REWRITE APPEND-NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE TRUE-LISTP-REV))
Warnings: None
Time: 0.17 seconds (prove: 0.11, print: 0.04, other: 0.02)
REV-APPEND
ACL2 !>
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-rev
(equal (rev (rev x))
x))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-rev
(equal (rev (rev x))
x))
Name the formula above *1.
Perhaps we can prove *1 by induction. One induction scheme is suggested
by this conjecture.
We will induct according to a scheme suggested by (REV X). If we let
(:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP). When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (REV (REV (CDR X))) (CDR X)))
(EQUAL (REV (REV X)) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(EQUAL (REV (REV (CDR X))) (CDR X)))
(EQUAL (REV (REV X)) X)).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterparts of CONSP and REV, primitive
type reasoning and the :rewrite rules CAR-CDR-ELIM, CAR-CONS, CDR-CONS
and REV-APPEND.
Subgoal *1/1
(IMPLIES (ENDP X)
(EQUAL (REV (REV X)) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(EQUAL (REV (REV X)) X)).
This simplifies, using the :definition REV, the :executable-counterpart
of REV and primitive type reasoning, to
Below is the only simplification checkpoint.
It says that every non-cons is nil. Well, 3 (for example)
is a non-cons that is not nil. You can see clearly that 3 is a
counterexample to the following conjecture by executing the following form,
which ACL2 proves:(thm (IMPLIES (NOT (CONSP 3)) (NOT 3)))(thm (not (equal (rev (rev 3)) 3)))X is a true list. But first, a question: To what value is
(rev (rev 3)) provably equal? How can we check our conjecture
with ACL2? One way to do this is shown on the next
slide.
Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X)).
Name the formula above *1.1.
No induction schemes are suggested by *1.1. Consequently, the proof
attempt has failed.
Summary
Form: ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART REV)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CDR-ELIM)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE REV-APPEND))
Warnings: None
Time: 0.05 seconds (prove: 0.02, print: 0.01, other: 0.02)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>
[top] [prev] [next]
[top] [prev] [next] ACL2 !>(thm (equal (rev (rev 3)) nil))[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(thm (equal (rev (rev 3)) nil))
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL and REV.
Q.E.D.
Summary
Form: ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART REV))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
Proof succeeded.
ACL2 !>
Well, this use of THM has been a fun diversion, but let us return
to our proof. Our to do list at this point is (rev-rev
rev-is-rev3).
[top] [prev] [next]
ACL2 !>(defthm rev-rev
(implies (true-listp x)
(equal (rev (rev x))
x)))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-rev
(implies (true-listp x)
(equal (rev (rev x))
x)))
Name the formula above *1.
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (REV X). If we let
(:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP). When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
(EQUAL (REV (REV (CDR X))) (CDR X))
(TRUE-LISTP X))
(EQUAL (REV (REV X)) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/3'
(IMPLIES (AND (CONSP X)
(EQUAL (REV (REV (CDR X))) (CDR X))
(TRUE-LISTP X))
(EQUAL (REV (REV X)) X)).
But simplification reduces this to T, using the :definitions BINARY-
APPEND, REV and TRUE-LISTP, the :executable-counterparts of CONSP and
REV, primitive type reasoning and the :rewrite rules CAR-CDR-ELIM,
CAR-CONS, CDR-CONS and REV-APPEND.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(NOT (TRUE-LISTP (CDR X)))
(TRUE-LISTP X))
(EQUAL (REV (REV X)) X)).
But we reduce the conjecture to T, by primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (ENDP X) (TRUE-LISTP X))
(EQUAL (REV (REV X)) X)).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X))
(EQUAL (REV (REV X)) X)).
But simplification reduces this to T, using the :definition TRUE-LISTP,
the :executable-counterparts of CONSP, EQUAL and REV and primitive
type reasoning.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION IMPLIES)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART REV)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CDR-ELIM)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE REV-APPEND))
Warnings: None
Time: 0.07 seconds (prove: 0.01, print: 0.04, other: 0.02)
REV-REV
ACL2 !>
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-is-rev3
(equal (rev x)
(rev3 x)))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-is-rev3
(equal (rev x)
(rev3 x)))
ACL2 Warning [Subsume] in ( DEFTHM REV-IS-REV3 ...): The newly proposed
:REWRITE rule REV-IS-REV3 probably subsumes the previously added :REWRITE
rules REV-REV and REV-APPEND, in the sense that REV-IS-REV3 will now
probably be applied whenever the old rules would have been.
Name the formula above *1.
The proof fails. In fact we can look through the proof attempt below and see
that the lemma rev-rev, which we proved for the specific purpose
of simplifying a checkpoint produced by an earlier proof attempt, was never
applied to any goal. Why not? This time, rather than looking over the failed
proof, let us try another technique, using the so-called
proof-builder.. (See also the ACL2 documentation page on
PROOF-BUILDER.) Click here to go to the next slide, where
we illustrate the use of the proof-builder.
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]
[top] [prev] [next]
ACL2 !>(verify (equal (rev x)
(rev3 x)))
verify puts us into an interactive loop, where we
can issue commands at a lower level than we have seen above. We will precede
each proof-builder command on the next slide by a comment (in blue) that
explains what it does.
[top] [prev] [next]
ACL2 !>(verify (equal (rev x)
(rev3 x)))
Experience suggests that this sort of lemma, the equivalence of two recursively
defined functions, will require a proof by induction. So we instruct the
proof-builder to replace the goal by base and induction steps.
->: induct
***** Now entering the theorem prover *****
[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 ``THeorem'') to view the current goal.
->: th *** Top-level hypotheses: 1. (NOT (ENDP X)) 2. (NOT (ENDP (CDR X))) 3. (EQUAL (REV (CDR X)) (REV3 (CDR X))) The current subterm is: (EQUAL (REV X) (REV3 X))No particular idea comes to mind for how to proceed (we are willing to forge ahead at this point without a great deal of thought). So we issue a command,
bash, to simplify the current goal using the full power
of the ACL2 simplifier.
->: bash
***** Now entering the theorem prover *****
[Note: A hint was supplied for our processing of the goal above.
Thanks!]
By the simple :definition ENDP we reduce the conjecture to
Goal'
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X))))
(EQUAL (REV X) (REV3 X))).
This simplifies, using the :definitions REV and REV3, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to
Goal''
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X))))
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
(CONS (CAR (REV (CDR X)))
(APPEND (REV (REV (CDR (REV (CDR X)))))
(LIST (CAR X)))))).
This simplifies, using the :definition BINARY-APPEND, to the following
two conjectures.
Subgoal 2
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X)))
(CONSP (REV (CDR X))))
(EQUAL (CONS (CAR (REV (CDR X)))
(APPEND (CDR (REV (CDR X)))
(LIST (CAR X))))
(CONS (CAR (REV (CDR X)))
(APPEND (REV (REV (CDR (REV (CDR X)))))
(LIST (CAR X)))))).
This simplifies, using primitive type reasoning and the :rewrite rule
CONS-EQUAL, to
Subgoal 2'
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X)))
(CONSP (REV (CDR X))))
(EQUAL (APPEND (CDR (REV (CDR X)))
(LIST (CAR X)))
(APPEND (REV (REV (CDR (REV (CDR X)))))
(LIST (CAR X))))).
But we have been asked to pretend that this goal is subsumed by the
as-yet-to-be-proved |PROOF-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 (Print) is like th, except that
it prints only the current subterm, not the hypotheses. Notice that the
preceding dv command has taken effect; the current subterm is now
the (REV (REV ..)) subterm of the goal's conclusion.
->: p (REV (REV (CDR (REV (CDR X)))))We would like to apply the rewrite rule
rev-rev to the above
term. There is, in fact, a proof-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]
[top] [prev] [next]
ACL2 !>(defthm true-listp-cdr-rev
(true-listp (cdr (rev x))))
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm true-listp-cdr-rev
(true-listp (cdr (rev x))))
Name the formula above *1.
The theorem prover has to work a bit harder than we might have guessed in order
to prove this lemma, but it does succeed in doing so (in much less than a
second). So click here to move on to the next slide;
again, there is rarely significant value in looking over a successful proof.
Perhaps we can prove *1 by induction. One induction scheme is suggested
by this conjecture.
We will induct according to a scheme suggested by (REV X). If we let
(:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP). When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X))
(TRUE-LISTP (CDR (REV (CDR X)))))
(TRUE-LISTP (CDR (REV X)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(TRUE-LISTP (CDR (REV (CDR X)))))
(TRUE-LISTP (CDR (REV X)))).
This simplifies, using the :definition REV, to
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(TRUE-LISTP (CDR (REV (CDR X)))))
(TRUE-LISTP (CDR (APPEND (REV (CDR X))
(LIST (CAR X)))))).
This simplifies, using the :definition BINARY-APPEND, to the following
two conjectures.
Subgoal *1/2.2
(IMPLIES (AND (CONSP X)
(TRUE-LISTP (CDR (REV (CDR X))))
(CONSP (REV (CDR X))))
(TRUE-LISTP (CDR (CONS (CAR (REV (CDR X)))
(APPEND (CDR (REV (CDR X)))
(LIST (CAR X))))))).
By the simple :rewrite rule CDR-CONS we reduce the conjecture to
Subgoal *1/2.2'
(IMPLIES (AND (CONSP X)
(TRUE-LISTP (CDR (REV (CDR X))))
(CONSP (REV (CDR X))))
(TRUE-LISTP (APPEND (CDR (REV (CDR X)))
(LIST (CAR X))))).
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
Subgoal *1/2.2''
(IMPLIES (AND (CONSP (CONS X1 X2))
(TRUE-LISTP (CDR (REV X2)))
(CONSP (REV X2)))
(TRUE-LISTP (APPEND (CDR (REV X2)) (LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1/2.2'''
(IMPLIES (AND (TRUE-LISTP (CDR (REV X2)))
(CONSP (REV X2)))
(TRUE-LISTP (APPEND (CDR (REV X2)) (LIST X1)))).
We generalize this conjecture, replacing (REV X2) by L. This produces
Subgoal *1/2.2'4'
(IMPLIES (AND (TRUE-LISTP (CDR L)) (CONSP L))
(TRUE-LISTP (APPEND (CDR L) (LIST X1)))).
The destructor terms (CAR L) and (CDR L) can be eliminated by using
CAR-CDR-ELIM to replace L by (CONS L1 L2), generalizing (CAR L) to
L1 and (CDR L) to L2. This produces the following goal.
Subgoal *1/2.2'5'
(IMPLIES (AND (CONSP (CONS L1 L2))
(TRUE-LISTP L2))
(TRUE-LISTP (APPEND L2 (LIST X1)))).
This simplifies, using primitive type reasoning, to
Subgoal *1/2.2'6'
(IMPLIES (TRUE-LISTP L2)
(TRUE-LISTP (APPEND L2 (LIST X1)))).
Name the formula above *1.1.
Subgoal *1/2.1
(IMPLIES (AND (CONSP X)
(TRUE-LISTP (CDR (REV (CDR X))))
(NOT (CONSP (REV (CDR X)))))
(TRUE-LISTP (CDR (LIST (CAR X))))).
But we reduce the conjecture to T, by the :executable-counterpart of
TRUE-LISTP and the simple :rewrite rule CDR-CONS.
Subgoal *1/1
(IMPLIES (ENDP X)
(TRUE-LISTP (CDR (REV X)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(TRUE-LISTP (CDR (REV X)))).
But simplification reduces this to T, using the :definition REV and
the :executable-counterparts of CDR and TRUE-LISTP.
So we now return to *1.1, which is
(IMPLIES (TRUE-LISTP L2)
(TRUE-LISTP (APPEND L2 (LIST X1)))).
Perhaps we can prove *1.1 by induction. Two induction schemes are
suggested by this conjecture. These merge into one derived induction
scheme.
We will induct according to a scheme suggested by
(BINARY-APPEND L2 (CONS X1 'NIL)). If we let (:P L2 X1) denote *1.1
above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP L2)) (:P (CDR L2) X1))
(:P L2 X1))
(IMPLIES (ENDP L2) (:P L2 X1))).
This induction is justified by the same argument used to admit BINARY-
APPEND, namely, the measure (ACL2-COUNT L2) is decreasing according
to the relation E0-ORD-< (which is known to be well-founded on the
domain recognized by E0-ORDINALP). When applied to the goal at hand
the above induction scheme produces the following three nontautological
subgoals.
Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP L2))
(TRUE-LISTP (APPEND (CDR L2) (LIST X1)))
(TRUE-LISTP L2))
(TRUE-LISTP (APPEND L2 (LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/3'
(IMPLIES (AND (CONSP L2)
(TRUE-LISTP (APPEND (CDR L2) (LIST X1)))
(TRUE-LISTP L2))
(TRUE-LISTP (APPEND L2 (LIST X1)))).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, primitive type reasoning and the :type-prescription
rule BINARY-APPEND.
Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP L2))
(NOT (TRUE-LISTP (CDR L2)))
(TRUE-LISTP L2))
(TRUE-LISTP (APPEND L2 (LIST X1)))).
But we reduce the conjecture to T, by primitive type reasoning.
Subgoal *1.1/1
(IMPLIES (AND (ENDP L2) (TRUE-LISTP L2))
(TRUE-LISTP (APPEND L2 (LIST X1)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/1'
(IMPLIES (AND (NOT (CONSP L2)) (TRUE-LISTP L2))
(TRUE-LISTP (APPEND L2 (LIST X1)))).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and TRUE-LISTP, the :executable-counterpart of CONSP and primitive
type reasoning.
That completes the proofs of *1.1 and *1.
Q.E.D.
The storage of TRUE-LISTP-CDR-REV depends upon the :type-prescription
rule TRUE-LISTP.
Summary
Form: ( DEFTHM TRUE-LISTP-CDR-REV ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION BINARY-APPEND)
(:TYPE-PRESCRIPTION TRUE-LISTP))
Warnings: None
Time: 0.20 seconds (prove: 0.07, print: 0.11, other: 0.02)
TRUE-LISTP-CDR-REV
ACL2 !>
[top] [prev] [next]
[top] [prev] [next] ACL2 !>:u
true-listp-cdr-rev, using the
keyword command shown: :u. We do not need to do so; the
proof of rev-is-rev3 will succeed now. But
true-listp-rev is a pretty ugly lemma, so here we show a way to
avoid it.
Some experienced ACL2 users would have made
true-listp-rev (above) a
:type-prescription rule instead of (or in addition to) a
:rewrite rule (the default). This would have made the immediately
preceding lemma, true-listp-cdr-rev, unnecessary. Let us undo
this lemma and replace it with a :type-prescription rule now. See
the ACL2 documentation page RULE-CLASSES for other kinds of rules.
[top] [prev] [next]
ACL2 !>:u
7:x(DEFTHM REV-REV ...)
ACL2 !>
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm true-listp-rev-type-prescription
(true-listp (rev x))
:rule-classes :type-prescription)
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm true-listp-rev-type-prescription
(true-listp (rev x))
:rule-classes :type-prescription)
ACL2 Observation in ( DEFTHM TRUE-LISTP-REV-TYPE-PRESCRIPTION ...):
Our heuristics choose (REV X) as the :TYPED-TERM.
But we reduce the conjecture to T, by the simple :rewrite rule TRUE-
LISTP-REV.
Q.E.D.
Summary
Form: ( DEFTHM TRUE-LISTP-REV-TYPE-PRESCRIPTION ...)
Rules: ((:REWRITE TRUE-LISTP-REV))
Warnings: None
Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
TRUE-LISTP-REV-TYPE-PRESCRIPTION
ACL2 !>
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(defthm rev-is-rev3
(equal (rev x)
(rev3 x)))
[top] [prev] [next]
ACL2 !>(defthm rev-is-rev3 ; succeeds -> to do list is empty!
(equal (rev x)
(rev3 x)))
ACL2 Warning [Subsume] in ( DEFTHM REV-IS-REV3 ...): The newly proposed
:REWRITE rule REV-IS-REV3 probably subsumes the previously added :REWRITE
rules REV-REV and REV-APPEND, in the sense that REV-IS-REV3 will now
probably be applied whenever the old rules would have been.
Name the formula above *1.
The proof succeeds! We might as well skip to the
end now.
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. Subsumption reduces that number to one.
We will induct according to a scheme suggested by (REV3 X). If we
let (:P X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ENDP X))
(NOT (ENDP (CDR X)))
(:P (CDR X)))
(:P X))
(IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X)))
(:P X))
(IMPLIES (ENDP X) (:P X))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
E0-ORD-< (which is known to be well-founded on the domain recognized
by E0-ORDINALP). When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (AND (NOT (ENDP X))
(NOT (ENDP (CDR X)))
(EQUAL (REV (CDR X)) (REV3 (CDR X))))
(EQUAL (REV X) (REV3 X))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/3'
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X))))
(EQUAL (REV X) (REV3 X))).
This simplifies, using the :definitions REV and REV3, primitive type
reasoning, the :rewrite rules CAR-CONS, CDR-CONS and REV-REV and the
:type-prescription rule TRUE-LISTP-REV-TYPE-PRESCRIPTION, to
Subgoal *1/3''
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X))))
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
(CONS (CAR (REV (CDR X)))
(APPEND (CDR (REV (CDR X)))
(LIST (CAR X)))))).
This simplifies, using the :definition BINARY-APPEND, to
Subgoal *1/3'''
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL (REV (CDR X)) (REV3 (CDR X)))
(NOT (CONSP (REV (CDR X)))))
(EQUAL (LIST (CAR X))
(CONS (CAR (REV (CDR X)))
(APPEND (CDR (REV (CDR X)))
(LIST (CAR X)))))).
This simplifies, using the :definition BINARY-APPEND, the :executable-
counterparts of CAR, CDR and CONSP, primitive type reasoning, the :rewrite
rule CDR-CONS and the :type-prescription rule TRUE-LISTP-REV-TYPE-PRESCRIPTION\
, to
Subgoal *1/3'4'
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(NOT (REV3 (CDR X))))
(CONSP (REV (CDR X)))).
The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to
X1 and (CDR X) to X2. This produces the following goal.
Subgoal *1/3'5'
(IMPLIES (AND (CONSP (CONS X1 X2))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
This simplifies, using primitive type reasoning, to
Subgoal *1/3'6'
(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
(CONSP (REV X2))).
Name the formula above *1.1.
Subgoal *1/2
(IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X)))
(EQUAL (REV X) (REV3 X))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))))
(EQUAL (REV X) (REV3 X))).
This simplifies, using the :definitions REV and REV3, to
Subgoal *1/2''
(IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))))
(EQUAL (APPEND (REV (CDR X)) (LIST (CAR X)))
(LIST (CAR X)))).
But simplification reduces this to T, using the :definitions BINARY-
APPEND and REV, the :executable-counterpart of CONSP and primitive
type reasoning.
Subgoal *1/1
(IMPLIES (ENDP X)
(EQUAL (REV X) (REV3 X))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP X))
(EQUAL (REV X) (REV3 X))).
But simplification reduces this to T, using the :definitions REV and
REV3 and the :executable-counterpart of EQUAL.
So we now return to *1.1, which is
(IMPLIES (AND (CONSP X2) (NOT (REV3 X2)))
(CONSP (REV X2))).
Perhaps we can prove *1.1 by induction. Two induction schemes are
suggested by this conjecture. Subsumption reduces that number to one.
We will induct according to a scheme suggested by (REV3 X2). If we
let (:P X2) denote *1.1 above then the induction scheme we'll use
is
(AND (IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(:P (CDR X2)))
(:P X2))
(IMPLIES (AND (NOT (ENDP X2)) (ENDP (CDR X2)))
(:P X2))
(IMPLIES (ENDP X2) (:P X2))).
This induction is justified by the same argument used to admit REV3,
namely, the measure (ACL2-COUNT X2) is decreasing according to the
relation E0-ORD-< (which is known to be well-founded on the domain
recognized by E0-ORDINALP). When applied to the goal at hand the above
induction scheme produces the following five nontautological subgoals.
Subgoal *1.1/5
(IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(CONSP (REV (CDR X2)))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/5'
(IMPLIES (AND (CONSP X2)
(CONSP (CDR X2))
(CONSP (REV (CDR X2)))
(NOT (REV3 X2)))
(CONSP (REV X2))).
But simplification reduces this to T, using the :definitions REV and
REV3, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rule TRUE-LISTP-REV-TYPE-PRESCRIPTION.
Subgoal *1.1/4
(IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(REV3 (CDR X2))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/4'
(IMPLIES (AND (CONSP X2)
(CONSP (CDR X2))
(REV3 (CDR X2))
(NOT (REV3 X2)))
(CONSP (REV X2))).
But simplification reduces this to T, using the :definitions REV and
REV3, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rule TRUE-LISTP-REV-TYPE-PRESCRIPTION.
Subgoal *1.1/3
(IMPLIES (AND (NOT (ENDP X2))
(NOT (ENDP (CDR X2)))
(NOT (CONSP (CDR X2)))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
But we reduce the conjecture to T, by case analysis.
Subgoal *1.1/2
(IMPLIES (AND (NOT (ENDP X2))
(ENDP (CDR X2))
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1.1/2'
(IMPLIES (AND (CONSP X2)
(NOT (CONSP (CDR X2)))
(NOT (REV3 X2)))
(CONSP (REV X2))).
But simplification reduces this to T, using the :definition REV3 and
primitive type reasoning.
Subgoal *1.1/1
(IMPLIES (AND (ENDP X2)
(CONSP X2)
(NOT (REV3 X2)))
(CONSP (REV X2))).
But we reduce the conjecture to T, by case analysis.
That completes the proofs of *1.1 and *1.
Q.E.D.
Summary
Form: ( DEFTHM REV-IS-REV3 ...)
Rules: ((:DEFINITION BINARY-APPEND)
(:DEFINITION ENDP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION REV3)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE REV-REV)
(:TYPE-PRESCRIPTION TRUE-LISTP-REV-TYPE-PRESCRIPTION))
Warnings: Subsume
Time: 0.24 seconds (prove: 0.16, print: 0.06, other: 0.02)
REV-IS-REV3
ACL2 !>
rev3, where we had to substitute rev for
rev3 in two of the three recursive calls.
We use an encapsulate event to introduce a new function,
triple-rev (we have to pick a new name since "rev3"
has already been used). The new function has the defining axiom we desire, and
is ``witnessed'' by rev3. That is, this encapsulate
directs ACL2 to check that rev3 satisfies the axiom introduced
for triple-rev. The theorem rev-is-rev3 proved above
is what allows ACL2 to make that deduction.
[top] [prev] [next] ACL2 !>(encapsulateBelow is a list of signatures:
triple-rev takes one argument and returns one value.
(((triple-rev *) => *))
triple-rev.
(local (defun triple-rev (x)
(rev3 x)))
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))))
:rule-classes ((:definition :clique (triple-rev)
:controller-alist ((triple-rev t)))))
)
[top] [prev] [next]
[top] [prev] [next]
ACL2 !>(encapsulate
(((triple-rev *) => *))
(local (defun triple-rev (x)
(rev3 x)))
(defthm triple-rev-def
(equal (triple-rev x)
(cond
((endp x)
nil)
((endp (cdr x))
(list (car x)))
(t
(let* ((b@c (cdr x))
(c@rev-b (triple-rev b@c)) ; recursive call
(rev-b (cdr c@rev-b))
(b (triple-rev rev-b)) ; recursive call
(a (car x))
(a@b (cons a b))
(rev-b@a (triple-rev a@b)) ; recursive call
(c (car c@rev-b))
(c@rev-b@a (cons c rev-b@a)))
c@rev-b@a))))
:rule-classes ((:definition :clique (triple-rev)
:controller-alist ((triple-rev t)))))
)
To verify that the two encapsulated events correctly extend the current
theory we will evaluate them. The theory thus constructed is only
ephemeral.
Go ahead and scroll quickly through a couple of screens or so of output.
Encapsulated Events:
ACL2 !>>(LOCAL (DEFUN TRIPLE-REV (X) (REV3 X)))
Since TRIPLE-REV is non-recursive, its admission is trivial. We observe
that the type of TRIPLE-REV is described by the theorem
(OR (CONSP (TRIPLE-REV X)) (EQUAL (TRIPLE-REV X) NIL)). We used the
:type-prescription rule REV3.
Summary
Form: ( DEFUN TRIPLE-REV ...)
Rules: ((:TYPE-PRESCRIPTION REV3))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
TRIPLE-REV
ACL2 !>>(DEFTHM TRIPLE-REV-DEF
(EQUAL (TRIPLE-REV X)
(COND ((ENDP X) NIL)
((ENDP (CDR X)) (LIST (CAR X)))
(T (LET* ((B@C (CDR X))
(C@REV-B (TRIPLE-REV B@C))
(REV-B (CDR C@REV-B))
(B (TRIPLE-REV REV-B))
(A (CAR X))
(A@B (CONS A B))
(REV-B@A (TRIPLE-REV A@B))
(C (CAR C@REV-B))
(C@REV-B@A (CONS C REV-B@A)))
C@REV-B@A))))
:RULE-CLASSES
((:DEFINITION :CLIQUE (TRIPLE-REV)
:CONTROLLER-ALIST ((TRIPLE-REV T)))))
ACL2 Warning [Non-rec] in ( DEFTHM TRIPLE-REV-DEF ...): The :DEFINITION
rule generated from TRIPLE-REV-DEF will be triggered only by terms
containing the non-recursive function symbol TRIPLE-REV. Unless this
function is disabled, TRIPLE-REV-DEF is unlikely ever to be used.
ACL2 Warning [Subsume] in ( DEFTHM TRIPLE-REV-DEF ...): The newly
proposed :DEFINITION rule TRIPLE-REV-DEF probably subsumes the previously
added :REWRITE rule TRIPLE-REV, in the sense that TRIPLE-REV-DEF will
now probably be applied whenever the old rule would have been.
ACL2 Warning [Subsume] in ( DEFTHM TRIPLE-REV-DEF ...): The previously
added rule TRIPLE-REV subsumes the newly proposed :DEFINITION rule
TRIPLE-REV-DEF, in the sense that the old rule rewrites a more general
target. Because the new rule will be tried first, it may nonetheless
find application.
By the simple :definition TRIPLE-REV we reduce the conjecture to
Goal'
(EQUAL (REV3 X)
(AND (NOT (ENDP X))
(IF (ENDP (CDR X))
(LIST (CAR X))
(LET ((C@REV-B (REV3 (CDR X))))
(CONS (CAR C@REV-B)
(REV3 (CONS (CAR X)
(REV3 (CDR C@REV-B))))))))).
This simplifies, using the :definition ENDP, to the following three
conjectures.
Subgoal 3
(IMPLIES (NOT (CONSP X))
(EQUAL (REV3 X) NIL)).
But simplification reduces this to T, using the :definition REV3 and
the :executable-counterpart of EQUAL.
Subgoal 2
(IMPLIES (AND (CONSP X) (CONSP (CDR X)))
(EQUAL (REV3 X)
(CONS (CAR (REV3 (CDR X)))
(REV3 (CONS (CAR X)
(REV3 (CDR (REV3 (CDR X))))))))).
But simplification reduces this to T, using the :definition REV3, primitive
type reasoning and the :rewrite rule REV-IS-REV3.
Subgoal 1
(IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))))
(EQUAL (REV3 X) (LIST (CAR X)))).
But simplification reduces this to T, using the :definition REV3 and
primitive type reasoning.
Q.E.D.
Summary
Form: ( DEFTHM TRIPLE-REV-DEF ...)
Rules: ((:DEFINITION ENDP)
(:DEFINITION REV3)
(:DEFINITION TRIPLE-REV)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE REV-IS-REV3))
Warnings: Subsume and Non-rec
Time: 0.10 seconds (prove: 0.05, print: 0.02, other: 0.03)
TRIPLE-REV-DEF
End of Encapsulated Events.
Having verified that the encapsulated events validate the signatures
of the ENCAPSULATE event, we discard the ephemeral theory and extend
the original theory as directed by the signatures and the non-LOCAL
events.
The following constraint is associated with the function TRIPLE-REV:
(EQUAL
(TRIPLE-REV X)
(AND
(NOT (ENDP X))
(IF
(ENDP (CDR X))
(LIST (CAR X))
(LET
((B@C (CDR X)))
(LET ((C@REV-B (TRIPLE-REV B@C)))
(LET ((REV-B (CDR C@REV-B)))
(LET ((B (TRIPLE-REV REV-B)))
(LET ((A (CAR X)))
(LET ((A@B (CONS A B)))
(LET ((REV-B@A (TRIPLE-REV A@B)))
(LET ((C (CAR C@REV-B)))
(LET ((C@REV-B@A (CONS C REV-B@A)))
C@REV-B@A))))))))))))
Summary
Form: ( ENCAPSULATE (((TRIPLE-REV * ...) ...) ...) ...)
Rules: NIL
Warnings: Subsume and Non-rec
Time: 0.18 seconds (prove: 0.05, print: 0.02, other: 0.11)
T
ACL2 !>
[top] [prev] [next]
[top] [prev] [next]We are done! All that remains is to see just where we are, and to make a few remarks.
[top] [prev] [next] ACL2 !>:pbt 0
The command above means: print back through command number 0 (the start of the session).
[top] [prev] [next]
[top] [prev] [next] ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN REV (X) ...) L 2 (DEFUN REV3 (X) ...) 3 (DEFTHM APPEND-ASSOC ...) 4 (DEFTHM APPEND-NIL ...) 5 (DEFTHM TRUE-LISTP-REV ...) 6 (DEFTHM REV-APPEND ...) 7 (DEFTHM REV-REV ...) 8 (DEFTHM TRUE-LISTP-REV-TYPE-PRESCRIPTION ...) 9 (DEFTHM REV-IS-REV3 ...) 10:x(ENCAPSULATE (((TRIPLE-REV *) ...)) ...) ACL2 !>
Theencapsulateabove was printed in very abbreviated form. Let us take a look at it in more detail using the command:pcb(print command block). Many other keyword commands are available for browsing the current ACL2 database (also called the ACL2 world); see the ACL2 documentation topic HISTORY.
[top] [prev] [next]
[top] [prev] [next] ACL2 !>:pcb! :x[top] [prev] [next]
[top] [prev] [next] ACL2 !>:pcb! :x 10:x(ENCAPSULATE (((TRIPLE-REV *) => *)) (LOCAL (DEFUN TRIPLE-REV (X) (REV3 X))) (DEFTHM TRIPLE-REV-DEF (EQUAL (TRIPLE-REV X) (COND ((ENDP X) NIL) ((ENDP (CDR X)) (LIST (CAR X))) (T (LET* ((B@C (CDR X)) (C@REV-B (TRIPLE-REV B@C)) (REV-B (CDR C@REV-B)) (B (TRIPLE-REV REV-B)) (A (CAR X)) (A@B (CONS A B)) (REV-B@A (TRIPLE-REV A@B)) (C (CAR C@REV-B)) (C@REV-B@A (CONS C REV-B@A))) C@REV-B@A)))) :RULE-CLASSES ((:DEFINITION :CLIQUE (TRIPLE-REV) :CONTROLLER-ALIST ((TRIPLE-REV T)))))) (DEFTHM TRIPLE-REV-DEF (EQUAL (TRIPLE-REV X) (COND ((ENDP X) NIL) ((ENDP (CDR X)) (LIST (CAR X))) (T (LET* ((B@C (CDR X)) (C@REV-B (TRIPLE-REV B@C)) (REV-B (CDR C@REV-B)) (B (TRIPLE-REV REV-B)) (A (CAR X)) (A@B (CONS A B)) (REV-B@A (TRIPLE-REV A@B)) (C (CAR C@REV-B)) (C@REV-B@A (CONS C REV-B@A))) C@REV-B@A)))) :RULE-CLASSES ((:DEFINITION :CLIQUE (TRIPLE-REV) :CONTROLLER-ALIST ((TRIPLE-REV T))))) ACL2 !>[top] [prev] [next]
[top] [prev] [next]Here are a few points that we have not yet made.
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.
[top] [prev]This concludes the tutorial. We thank Rob Sumners for useful comments on an earlier draft.