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) nil (append (rev (cdr x)) (list (car x))))) ; Trying
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 triple-revsucceeds. (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-revis also discoverable by The Method because it is ; suggested by the statement of triple-revitself: 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.