### INTRODUCTORY-CHALLENGE-PROBLEM-1-ANSWER

answer to challenge problem 1 for the new user of ACL2
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.