某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陣営と議論するネタになるかな。