; 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))) ; or x, but then (rev3 x) may not equal (rev x) [see below]
   (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)))

Aside.  Below is an interesting checkpoint, from when original version of rev3
was used as described in the comment above, for the case:

   ((endp (cdr x))
    (list (car x))) ; or x, but then (rev3 x) may not equal (rev x) [see below]

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

This subgoal led us to the version of rev3 in which (list (car x)) is returned
instead of x in the case shown above.

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.  Too bad the proof fails.

#|
(defthm rev-append ; fails -> to do list:  (rev-append rev-rev rev-is-rev3)
  (equal (rev (append x y))
         (append (rev y) (rev x))))
|#

; If we look a few checkpoints after the first (which by the way is rarely
; necessary), we find the following:

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

; This suggests the following lemma.

(defthm append-assoc
  (equal (append (append x y) z)
         (append x (append y z))))

; We try rev-append again
#|
(defthm rev-append ; fails -> to do list:  (rev-append rev-rev rev-is-rev3)
  (equal (rev (append x y))
         (append (rev y) (rev x))))
|#

; but we find this checkpoint:

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

; So we prove the following two lemmas (more on true-listp later):

(defthm append-nil
  (implies (true-listp x)
           (equal (append x nil) x)))

(defthm true-listp-rev
  (true-listp (rev x)))

; Now we again try:

(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 the 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.
#|
(defthm rev-is-rev3 ; proof fails -> why didn't rev-rev apply?
  (equal (rev x)
         (rev3 x)))
|#
; Here is the first simplification checkpoint.

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

; Why didn't the lemma rev-rev apply on the second-to-last line above?
; Presumably that's because the true-listp hypothesis was not successfully
; relieved.  We can use the proof-checker:

#|
(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. (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))))
 ->: (dv 2 1) ; dive to the second argument and then the first
 ->: p ; print current conclusion
 (REV (REV (CDR (REV (CDR X)))))
 ->: sr ; show rewrite rules that may apply
 1. REV-REV
   New term: (CDR (REV (CDR X)))
   Hypotheses: ((TRUE-LISTP (CDR (REV (CDR X)))))
 ->: exit ; leave the proof-checker interactive loop
 Exiting....
|#

; The following rewrite rule should suffice to get us past the goal above.

(defthm true-listp-cdr-rev
  (true-listp (cdr (rev x))))

; Some experienced ACL2 users would have made true-listp-rev a
; :type-prescription rule instead of (or in addition to) a :rewrite rule (the
; default), which would also have solved the problem.  We can add such a
; :type-prescription rule here instead of the above, if we like.  See the ACL2
; documentation page RULE-CLASSES for other kinds of rules one can use.

#|
(defthm rev-is-rev3 ; succeeds
  (equal (rev x)
         (rev3 x)))

(u) ; or, :u -- undo the last command
(u)

(defthm true-listp-rev-type-prescription
  (true-listp (rev x))
  :rule-classes :type-prescription)
|#

(defthm rev-is-rev3 ; succeeds -> to do list is empty!
  (equal (rev x)
         (rev3 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
|#