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.