rev-rev

某ProofCafeではCoqでやってみたという話の、
リストの反転問題。
reverse (reverse xs) = xs
http://study-func-prog.blogspot.com/2010/04/coq-reverse-reverse-xs-xs.html

ACL2ではどうなんのかな、と思ってやってみた。
環境はACL2s。

(in-package "ACL2")
(defun rev (x)
  (if (endp x)
    nil
    (append (rev (cdr x)) (list (car x)))))

(defthm rev-rev
  (implies (true-listp a)
           (equal (rev (rev a)) a)))

自動的に証明ができてしまうようだ。

Coq陣営と議論するネタになるかな。