Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
This answer is in the form of an ACL2 script sufficient to lead ACL2 to a proof.
(defun rev (x)
(if (endp x)
nil
(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.
