answer to challenge problem 1 for the new user of ACL2

This answer is in the form of an ACL2 script sufficient to lead ACL2 to a proof.

(defun rev (x)
  (if (endp x)
      (append (rev (cdr x)) (list (car x)))))

; Trying triple-rev at this point produces a key checkpoint containing
; (REV (APPEND (REV (CDR X)) (LIST (CAR X)))), which suggests:

(defthm rev-append
  (equal (rev (append a b))
         (append (rev b) (rev a))))

; And now triple-rev succeeds.

(defthm triple-rev
  (equal (rev (rev (rev x))) (rev x)))

; An alternative, and more elegant, solution is to prove the rev-rev
; instead of rev-append:

; (defthm rev-rev
;   (implies (true-listp x)
;            (equal (rev (rev x)) x)))

; Rev-rev is also discoverable by The Method because it is
; suggested by the statement of triple-rev itself:  rev-rev
; simplifies a simpler composition of the functions in triple-rev.

; Both solutions produce lemmas likely to be of use in future proofs
; about rev.

Use your browser's Back Button now to return to introductory-challenge-problem-1.