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)))))
triple-revat 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
(defthm triple-rev (equal (rev (rev (rev x))) (rev x)))
; An alternative, and more elegant, solution is to prove the
rev-rev; instead of
; (defthm rev-rev ; (implies (true-listp x) ; (equal (rev (rev x)) x)))
Rev-revis also discoverable by The Method because it is ; suggested by the statement of
rev-rev; simplifies a simpler composition of the functions in
; Both solutions produce lemmas likely to be of use in future proofs ; about
Use your browser's Back Button now to return to introductory-challenge-problem-1.