; A Brief ACL2 Tutorial
; Matt Kaufmann, Advanced Micro Devices, Inc.
; J Strother Moore, Department of Computer Sciences,
; University of Texas at Austin
; Our goal in this demo is to illustrate how one interacts with ACL2. This
; demo therefore differs somewhat from the Flying Demo, which covers a lot more
; ground by proving a much more diverse and interesting collection of theorems.
; The present demo focuses in considerable detail on a simple problem that is
; not quite trivial, in order to help the ACL2 beginner get up to speed on
; using this theorem prover effectively.
; The problem. Suppose that for whatever reason, we wish to investigate
; properties of a reverse function that is defined only using a recursive call
; and built-in functions endp, cons, car, cdr. The algorithm coded in rev3
; below is due to Landin (we believe). The natural encoding of that algorithm
; is not, however, admissible in the ACL2 logic, because the second and third
; recursive calls (see below) need information about the result of the first
; recursive call of rev3, 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 recursive call 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 ``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 checkpoints.
; In a demo we would execute the following in the ACL2 loop:
#|
(start-proof-tree)
(quote "Execute meta-x start-proof-tree now.")
|#
; See also the ACL2 documentation topic THE-METHOD for a description of the
; process illustrated in this demo. As described there, we keep an informal
; ``to do list'' below of goals to be proved.
; The first form in a certified book must always be an in-package form.
; Usually the package is "ACL2", but users can define their own packages.
(in-package "ACL2")
; Here is a straightforward definition of reverse.
(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x))
(list (car x)))))
; Here is the algorithm discussed above. We use variable names that contain
; the character @ to suggest concatenation, for improved readability. For
; example, we write c@rev-b to suggest the result of concatenating c to the
; front of the reverse of b.
(defun rev3 (x)
(cond
((endp x)
nil)
((endp (cdr x))
(list (car x))) ; if x instead, then (rev3 x) != (rev x) for x = (3 . 4)
(t
; 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 to the concatenation of c with the reverse of b,
; and so on.
(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 rather than recursive call
(a (car x))
(a@b (cons a b))
(rev-b@a (rev a@b)) ; note call of rev rather than recursive call
(c (car c@rev-b))
(c@rev-b@a (cons c rev-b@a)))
c@rev-b@a))))
; We assign ourselves the following goal: prove that (rev x) equals (rev3 x).
#| GOAL:
(defthm rev-is-rev3 ; proof fails
(equal (rev x)
(rev3 x)))
Here is the first checkpoint from our attempt to prove rev-is-rev3 using the
appropriate definition of rev3.
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))))).
|#
; To do list: (rev-is-rev3).
; Notice the term of the form (rev (rev u)) on the second-to-last line just
; above. This could suggest the following rewrite rule, whose proof
; unfortunately fails at this point.
#|
(defthm rev-rev ; fails -> to do list: (rev-rev rev-is-rev3)
(equal (rev (rev x))
x))
|#
; The first checkpoint has a term of the form (rev (append u v)):
#|
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(EQUAL (REV (REV (CDR X))) (CDR X)))
(EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X))))
X)).
|#
; So we attempt to prove the following in order to put such terms in a
; ``simpler'' form.
(defthm rev-append
(equal (rev (append x y))
(append (rev y) (rev x))))
; The proof succeeds. To do list: (rev-rev rev-is-rev3).
; When we try rev-rev at this point
#|
(defthm rev-rev ; fails -> to do list: (rev-rev rev-is-rev3)
(equal (rev (rev x))
x))
|#
; we get the following checkpoint.
#|
Subgoal *1/1''
(IMPLIES (NOT (CONSP X)) (NOT X)).
|#
; This suggests that our goal might not be true; consider some x that is not a
; consp and yet is not nil. For example, if we try this
#|
(thm (equal (rev (rev 3)) nil))
|#
; then that proof succeeds.
; Here is a revised statement that is indeed a theorem.
(defthm rev-rev ; succeeds -> to do list: (rev-is-rev3)
(implies (true-listp x)
(equal (rev (rev x))
x)))
; We now try rev-is-rev3 once again. The proof succeeds! But we got a bit
; lucky; for example, we can turn off a proof technique used in that proof in
; order to make the proof fail.
#|
(defthm rev-is-rev3 ; fails
(equal (rev x)
(rev3 x))
:hints (("Goal" :do-not '(eliminate-destructors))))
|#
; So let us use this opportunity to explore the use of the proof-builder, which
; is invoked with VERIFY.
#|
(verify (equal (rev x)
(rev3 x)))
Now try the following commands, in this order. We include below an abbreviated
display of the output.
->: induct ; replace goal by base and induction steps
->: th ; print current goal
*** 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))
->: bash ; simplify current goal
->: th ; print current goal
*** Top-level hypotheses:
1. (CONSP X)
2. (CONSP (CDR X))
3. (NOT (REV3 (CDR X)))
The current subterm is:
(CONSP (REV (CDR X)))
->:
; AHA! It looks like hypotheses 2 and 3 are contradictory. It seems
; that ACL2 would know that if only it would expand the definition
; of REV3 on (CDR X). The proof finally succeeds with such a hint:
->: exit
|#
(defthm rev-is-rev3 ; succeeds -> to do list is empty! ;
(equal (rev x)
(rev3 x))
:hints (("Goal"
:do-not '(eliminate-destructors)
:expand ((rev3 (cdr x))))))
; Having finally proved this lemma, we can now "define" rev3. (We have to pick
; a new name since rev3 has already been used.)
(encapsulate
; Signature: triple-rev takes one argument and returns one value.
(((triple-rev *) => *))
; Local definition: Properties below are to be proved using this definition of
; triple-rev.
(local (defun triple-rev (x)
(rev3 x)))
; Here is the definition we wanted to make when we defined rev3. Notice that
; triple-rev does not call rev or any other function other than itself and
; a few built-ins (endp, list, car, cdr, cons).
(defthm triple-rev-def
(equal (triple-rev x)
(cond
((endp x)
nil)
((endp (cdr x))
(list (car x)))
(t
;; Think of x as a@b@c where a and c are single elements.
(let* ((b@c (cdr x))
(c@rev-b (triple-rev b@c)) ; recursive call
(rev-b (cdr c@rev-b))
(b (triple-rev rev-b)) ; recursive call
(a (car x))
(a@b (cons a b))
(rev-b@a (triple-rev a@b)) ; recursive call
(c (car c@rev-b))
(c@rev-b@a (cons c rev-b@a)))
c@rev-b@a))))
; Here we specify that the formula above be used like a definition. Details
; may be found on the ACL2 documentation page RULE-CLASSES.
:rule-classes ((:definition :clique (triple-rev)
:controller-alist ((triple-rev t)))))
) ; end of encapsulate
; We are done! We can submit the form
#|
(pbt 0) ; or, :pbt 0
|#
; to get a summary of the stack of successfully-issued commands. Other such
; commands are documented in the ACL2 documentation page HISTORY, for example:
#|
(pcb! :x) ; or, :pcb! :x
|#