INTRODUCTORY-CHALLENGE-PROBLEM-1.html -- ACL2 Version 6.2

challenge problem 1 for the new user of ACL2

Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER

Start in a fresh ACL2, either by restarting your ACL2 image from scratch or executing

:ubt! 1

which will undo everything since the first user event.

Then define this function:

(defun rev (x)
  (if (endp x)
      nil
      (append (rev (cdr x)) (list (car x)))))

Then use The Method to prove:

(defthm triple-rev
  (equal (rev (rev (rev x))) (rev x)))

When you've solved this problem, compare your answer to ours; see introductory-challenge-problem-1-answer.

Then, use your browser's Back Button to return to introductory-challenges.