ACL2 で非末尾再帰と末尾再帰の階乗関数が等しいことを証明した
追記: タイトルを「ACL2 のリハビリに非末尾再帰と末尾再帰の階乗関数が等しいことを証明した」から「ACL2 の非末尾再帰と末尾再帰の階乗関数が等しいことを証明した」に変更しました。
ここ最近は自分のサーバーまわりの作業ばかりをやっていて、 全然 ACL2 をやっていなくてほとんど忘れてしまった感じがするので練習のために簡単なことから始めて慣れようと思う。
末尾再帰版の階乗と非末尾再帰版の階乗を書いて、それぞれの関数の戻り値が等しくなることを証明した。
こっちが非末尾再帰の普通の階乗
(defun factorial (n) (if (zp n) 1 (* n (factorial (- n 1)))))
これが末尾再帰版の階乗
(defun factorial-tail (n a) (if (zp n) a (factorial-tail (- n 1) (* n a))))
いきなり下記のように直接証明を試みても失敗する。
(defthm factorial-tail-factorial
(equal (factorial-tail n 1)
(factorial n)))
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal
(EQUAL (FACTORIAL-TAIL N 1)
(FACTORIAL N))
*** Key checkpoint under a top-level induction: ***
Subgoal *1/2'
(IMPLIES (AND (NOT (ZP N))
(EQUAL (FACTORIAL-TAIL (+ -1 N) 1)
(FACTORIAL (+ -1 N))))
(EQUAL (FACTORIAL-TAIL (+ -1 N) N)
(* N (FACTORIAL (+ -1 N)))))
ACL2 Error [Failure] in ( DEFTHM FACTORIAL-TAIL-FACTORIAL ...): See
:DOC failure.
******** FAILED ********
:ERROR
キーチェックポイントをみても、 正しそうな数学的帰納法を試みているだけで式変形が進んでいないのでこれだとおそらく詰み。
こういうのは、 1 を変数に置き換えて一般化すると証明できるようになる。
(defthm factorial-tail-factorial-generic
(implies (integerp a)
(equal (factorial-tail n a)
(* a (factorial n)))))
Summary
Form: ( DEFTHM FACTORIAL-TAIL-FACTORIAL-GENERIC ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
(:DEFINITION FACTORIAL)
(:DEFINITION FACTORIAL-TAIL)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION FACTORIAL)
(:INDUCTION FACTORIAL-TAIL)
(:REWRITE ASSOCIATIVITY-OF-*)
(:REWRITE COMMUTATIVITY-OF-*)
(:REWRITE UNICITY-OF-1)
(:TYPE-PRESCRIPTION FACTORIAL))
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted: 1455
---
The key checkpoint goals, below, may help you to debug this failure.
See :DOC failure and see :DOC set-checkpoint-summary-limit.
---
*** Key checkpoint at the top level: ***
Goal
(IMPLIES (INTEGERP A)
(EQUAL (FACTORIAL-TAIL N A)
(* A (FACTORIAL N))))
*** Key checkpoint under a top-level induction: ***
Subgoal *1/3'''
(IMPLIES (AND (NOT (ZP N))
(EQUAL (FACTORIAL-TAIL (+ -1 N) (* A N))
(* N A (FACTORIAL (+ -1 N))))
(INTEGERP A))
(EQUAL (FACTORIAL-TAIL (+ -1 N) (* A N))
(* A N (FACTORIAL (+ -1 N)))))
ACL2 Error [Failure] in ( DEFTHM FACTORIAL-TAIL-FACTORIAL-GENERIC ...):
See :DOC failure.
******** FAILED ********
:ERROR
今度は式変形が進んでいるが、途中で止まってしまった。
Subgoal *1/3''' では、仮定の式に (* N A (FACTORIAL (+ -1 N))) 、
帰結の式に (* A N (FACTORIAL (+ -1 N))) がある。
これは、積の交換則から等しいが ACL2 はどういうわけか等しいと気づいてくれない(Rewriteルールがない)。
裸の ACL2 にも積の交換則のRewriteルールとして COMMUTATIVITY-OF-* が用意されているが、
(equal (* a b c) (* b a c)) のような状況には対応していない。
この問題は arithmetic という ACL2 のコミュニティブックによって解決されている。
下記を実行してブックを読み込む。
(local (include-book "arithmetic/top-with-meta" :dir :system))
再度、 factorial-tail-factorial-generic を試す。
(defthm factorial-tail-factorial-generic
(implies (integerp a)
(equal (factorial-tail n a)
(* a (factorial n)))))
こんどは証明に成功した。
下記の Summary に COMMUTATIVITY-2-OF-* があることに注目して欲しい。
(* a b c) と (* b a c) が等しいことを表現するRewriteルールで、
これが使われたことで無事に証明に成功している。
Q.E.D.
Summary
Form: ( DEFTHM FACTORIAL-TAIL-FACTORIAL-GENERIC ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
(:DEFINITION FACTORIAL)
(:DEFINITION FACTORIAL-TAIL)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION FACTORIAL)
(:INDUCTION FACTORIAL-TAIL)
(:REWRITE ASSOCIATIVITY-OF-*)
(:REWRITE COMMUTATIVITY-2-OF-*)
(:REWRITE COMMUTATIVITY-OF-*)
(:REWRITE UNICITY-OF-1))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 362
FACTORIAL-TAIL-FACTORIAL-GENERIC
今回証明したいことは今証明したことの特殊な場合なので、 この定理を証明したあとであれば普通に自動証明に成功する。
(defthm factorial-tail-factorial
(equal (factorial-tail n 1)
(factorial n)))
FACTORIAL-TAIL-FACTORIAL-GENERIC が使われて証明に成功した。
Q.E.D.
Summary
Form: ( DEFTHM FACTORIAL-TAIL-FACTORIAL ...)
Rules: ((:DEFINITION FIX)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE FACTORIAL-TAIL-FACTORIAL-GENERIC)
(:REWRITE UNICITY-OF-1)
(:TYPE-PRESCRIPTION FACTORIAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 42
FACTORIAL-TAIL-FACTORIAL
無事に目的を達成できた。
COMMUTATIVITY-2-OF-* が必要になったので驚いたが、
これは知ってたので解決できた。
一応、公式のチュートリアルのFAQの下記の質問のところに (include-book "arithmetic/top-with-meta" :dir :system)
しろと書いてあるのでこれを読めば解決できる問題ではある。
Q. ACL2 doesn't know simple arithmetic that can simplify the term (+ 1 -1 x).
https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS
learn-acl2 という ACL2 の勉強用のリポジトリを作ったので、 今回のを含めてこれから学習のために書いた ACL2 のコードはここ置いていくこととする。
コード: factorial.lisp CI: https://ci.tojo.tokyo/jobs/acl2-verify/523