ACL2 で組み合せの数とその階乗表現の関係について証明してみた
目次
投稿日: 2021-09-05 日
1. 注意
この記事はいま思うとあまりよく分かっていなかったときに書いたものなので参考にしない方がいいです。 近々、本当に役に立つ初心者向けの記事を書く予定なので作成しだいここにリンクを張る予定です。
2. はじめに
本記事は前回の ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた – TojoQK の続きです。未読の方は先に読んでからお読みください。
前回、リスト中の要素の全ての組み合わせを求める関数 combinations
と組み合わせの数を求める関数 comb を求め、 (len (combinations x k))
と (comb (len x) k) が等しいことを証明しました。ただし、=combinations=
と comb の定義は同じ構造をしているため、ACL2
で自動証明ができたといってもありがたみを感じにくい例だったかと思います。
よって、今回は組み合わせの数を階乗で表現した式と前回の comb
が等しいことを証明します。
プログラムのライセンスは3条項BSDライセンスとします。
3. 組み合せの数を求める関数 comb を定義する
前回の記事で作成した組み合わせの数を求める関数
comb です。
関数の定義については前回の記事で説明しているので必要であれば参照してください
(defun comb (n k)
(cond
((zp k) 1)
((zp n) 0)
(t (+ (comb (- n 1) k)
(comb (- n 1) (- k 1))))))
The admission of COMB is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT N). We observe that the type of COMB is described by the theorem (AND (INTEGERP (COMB N K)) (<= 0 (COMB N K))). We used primitive type reasoning. Summary Form: ( DEFUN COMB ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.01) COMB
ただ、前回の comb
の説明はアルゴリズムに関するものだけで、関数中で使用している zp
関数については特に説明していませんでした。=zp= 関数は Common Lisp (ACL2
は Common Lisp のサブセットです)には存在していない関数であり、Common
Lisp にもある 0 かどうかを調べる関数の zerop
とは挙動が異なります。=zp= を使用している理由については ACL2
の関数定義の仕様について軽く説明する必要があります。
3.1. ACL2 と停止性の証明
ACL2 では全ての関数は停止しないといけません。ACL2 は defun
で関数を定義するときに毎回停止性について証明しています(今までの例では一度も停止性の証明に失敗していません)。
重要なのは関数にどのような値を与えても停止しないといけないということです。ACL2
は型なしの言語なので ACL2
で利用可能な全てのデータ型の値が関数に渡る可能性があります。自然数のみを引数に取る関数のつもりで書いていたなどという言い訳は
ACL2 には通用しないのです。 zp 関数は 0
だけでなく自然数(0を含む)以外の全ての値を 0 として処理します。なので
zerop とは異なり=(zp -1)= や (zp 'a) も t です。 zp
関数により基底部へ分岐する判定をすることで自然数以外の予期しない値が与えられた場合であっても確実に関数が停止することを証明できるのです。
具体的にどうやって停止性の証明をするのかについてはいつか別に記事を作成して説明しようという気持ちはありますが実際のスケジュールは未定のため、興味のある方は
ACL2
のドキュメントを読むか『定理証明手習い』(ラムダノート社)を参照することをおすすめします。
zp 関数の詳細については zp 関数のドキュメント を参照してください。
また、ACL2 が型なしであることについて不安に感じた静的型付きのプログラミング言語を好む方は XDOC — Guard を軽く読んでみてください。初心者向けの機能ではないのですが、実際に関数に渡る値を静的に制限することができます(停止性の証明時にあらゆる値について考慮しないといけないことは Guard を使用しても変わりません)。
3.2. comb の性質
comb と階乗の関係の性質について証明する前に comb
について既に分かっている性質については先に証明しておきましょう。 特に
comb の次に説明する階乗表現を定義する際には「k が n よりも大きいときは
(comb n k) は 0」という性質を利用します。 なので、下記の comb-zero
という定理を先に証明しておきます。
(defthm comb-zero
(implies (and (natp n)
(natp k)
(< n k))
(equal (comb n k) 0)))
Goal'
([ A key checkpoint:
Goal'
(IMPLIES (AND (INTEGERP N)
(<= 0 N)
(INTEGERP K)
(<= 0 K)
(< N K))
(EQUAL (COMB N K) 0))
*1 (Goal') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. One induction scheme is suggested
by this conjecture.
We will induct according to a scheme suggested by (COMB N K). This
suggestion was produced using the :induction rule COMB. If we let
(:P K N) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (ZP K))
(NOT (ZP N))
(:P K (+ -1 N))
(:P (+ -1 K) (+ -1 N)))
(:P K N))
(IMPLIES (AND (NOT (ZP K)) (ZP N))
(:P K N))
(IMPLIES (ZP K) (:P K N))).
This induction is justified by the same argument used to admit COMB.
Note, however, that the unmeasured variable K is being instantiated.
When applied to the goal at hand the above induction scheme produces
twelve nontautological subgoals.
Subgoal *1/12
Subgoal *1/11
Subgoal *1/10
Subgoal *1/9
Subgoal *1/8
Subgoal *1/7
Subgoal *1/6
Subgoal *1/5
Subgoal *1/4
Subgoal *1/3
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
*1 is COMPLETED!
Thus key checkpoint Goal' is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM COMB-ZERO ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
(:DEFINITION COMB)
(:DEFINITION NATP)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART INTEGERP)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION COMB))
Time: 0.03 seconds (prove: 0.02, print: 0.01, other: 0.00)
Prover steps counted: 707
COMB-ZERO
4. 階乗を求める関数 factorial を定義する
階乗の定義は下記の通りです。
- 0 の階乗は 1
- n が 0 より大きい自然数のとき、n の階乗は n と n - 1 の階乗の積
これをそのまま ACL2に翻訳した factorial
の定義を示します(厳密には前述した通り基底部の判定に zp
関数を使用するため全く同じというわけではありません)。
(defun factorial (n)
(if (zp n)
1
(* n (factorial (- n 1)))))
The admission of FACTORIAL is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT N). We observe that the type of FACTORIAL is described
by the theorem (AND (INTEGERP (FACTORIAL N)) (< 0 (FACTORIAL N))).
We used the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive
type reasoning.
Summary
Form: ( DEFUN FACTORIAL ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
FACTORIAL
5. comb-factorial 定理を証明する
では、comb 関数と階乗の関係について証明してみましょう。 高校の数学 1A にて組み合わせの数について学んだ方は下記の公式について学んだ記憶がある かもしれません。
n! -------- (n-k)!k!
何故かについては「組み合せの数 公式」とかで適当に検索してください(やる気なし)。 ということで上記の式を ACL2 に翻訳してみましょう。分母が 0 になったり結果が分数になにならないように調節しています。
(defthm comb-factorial
(implies (and (natp n))
(equal (comb n k)
(cond
((zp k) 1)
((or (zp n) (< n k)) 0)
(t (/ (factorial n)
(* (factorial (- n k))
(factorial k))))))))
ACL2 Warning [Subsume] in ( DEFTHM COMB-FACTORIAL ...): A newly proposed
:REWRITE rule generated from COMB-FACTORIAL probably subsumes the previously
added :REWRITE rule COMB-ZERO, in the sense that the new rule will
now probably be applied whenever the old rule would have been.
Goal'
Subgoal 4
Subgoal 3
Subgoal 2
Subgoal 2'
([ A key checkpoint:
Subgoal 2'
(IMPLIES (AND (<= 0 N)
(NOT (ZP K))
(NOT (ZP N))
(<= K N))
(EQUAL (COMB N K)
(* (FACTORIAL N)
(/ (* (FACTORIAL K)
(FACTORIAL (+ (- K) N)))))))
*1 (Subgoal 2') is pushed for proof by induction.
])
Subgoal 1
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to one.
We will induct according to a scheme suggested by (COMB N K). This
suggestion was produced using the :induction rules COMB and FACTORIAL.
If we let (:P K N) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ZP K))
(NOT (ZP N))
(:P K (+ -1 N))
(:P (+ -1 K) (+ -1 N)))
(:P K N))
(IMPLIES (AND (NOT (ZP K)) (ZP N))
(:P K N))
(IMPLIES (ZP K) (:P K N))).
This induction is justified by the same argument used to admit COMB.
Note, however, that the unmeasured variable K is being instantiated.
When applied to the goal at hand the above induction scheme produces
eight nontautological subgoals.
Subgoal *1/8
Subgoal *1/8'
Subgoal *1/8''
Splitter note (see :DOC splitter) for Subgoal *1/8'' (2 subgoals).
if-intro: ((:DEFINITION FACTORIAL)
(:DEFINITION NOT)
(:REWRITE ZP-OPEN))
Subgoal *1/8.2
Subgoal *1/8.2'
Subgoal *1/8.2''
Subgoal *1/8.2'''
Subgoal *1/8.2'4'
Subgoal *1/8.2'5'
Subgoal *1/8.2'6'
Subgoal *1/8.2'7'
Subgoal *1/8.2'8'
Subgoal *1/8.2'9'
Subgoal *1/8.2'10'
Subgoal *1/8.2'11'
Subgoal *1/8.2'12'
Subgoal *1/8.2'13'
Subgoal *1/8.2'14'
Subgoal *1/8.2'15'
Subgoal *1/8.2'16'
Subgoal *1/8.2'17'
([ A key checkpoint while proving *1 (descended from Subgoal 2'):
Subgoal *1/8.2'
(IMPLIES (AND (NOT (ZP K))
(NOT (ZP N))
(EQUAL (COMB (+ -1 N) K)
(* (FACTORIAL (+ -1 N))
(/ (* K (FACTORIAL (+ -1 K))
(FACTORIAL (+ -1 (- K) N))))))
(< 0 (+ (- K) N))
(EQUAL (COMB (+ -1 N) (+ -1 K))
(* (FACTORIAL (+ -1 N))
(/ (* (FACTORIAL (+ -1 K))
(+ (- K) N)
(FACTORIAL (+ -1 (- K) N))))))
(<= 0 N)
(<= K N))
(EQUAL (+ (COMB (+ -1 N) K)
(COMB (+ -1 N) (+ -1 K)))
(* N (FACTORIAL (+ -1 N))
(/ (* K (FACTORIAL (+ -1 K))
(+ (- K) N)
(FACTORIAL (+ -1 (- K) N)))))))
*1.1 (Subgoal *1/8.2'17') is pushed for proof by induction.
])
Subgoal *1/8.1
Subgoal *1/8.1'
Subgoal *1/7
Subgoal *1/7'
Subgoal *1/7''
Subgoal *1/6
Subgoal *1/5
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/4''
Subgoal *1/4'''
Subgoal *1/4'4'
Subgoal *1/4'5'
Subgoal *1/4'6'
Subgoal *1/4'7'
Subgoal *1/4'8'
([ A key checkpoint while proving *1 (descended from Subgoal 2'):
Subgoal *1/4'5'
(IMPLIES (AND (NOT (ZP N))
(< 0 (+ -1 N))
(EQUAL (+ 1 (COMB (+ -2 N) 1))
(* (/ (FACTORIAL (+ -2 N)))
(+ -1 N)
(FACTORIAL (+ -2 N))))
(<= 0 N)
(<= 1 N))
(EQUAL (+ 2 (COMB (+ -2 N) 1)) N))
*1.2 (Subgoal *1/4'8') is pushed for proof by induction.
])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
So we now return to *1.2, which is
(IMPLIES (AND (INTEGERP K)
(<= 0 K)
(INTEGERP I)
(< 0 I)
(INTEGERP J)
(NOT (ZP N))
(EQUAL (+ 1 K)
(* (/ (FACTORIAL J)) I (FACTORIAL J)))
(<= 0 N)
(<= 1 N))
(EQUAL (+ 2 K) N)).
Subgoal *1.2/3
Subgoal *1.2/3'
Subgoal *1.2/3''
Subgoal *1.2/3'''
Subgoal *1.2/3'4'
Subgoal *1.2/3'5'
Subgoal *1.2/3'6'
*1.2.1 (Subgoal *1.2/3'6') is pushed for proof by induction.
Subgoal *1.2/2
Subgoal *1.2/1
Subgoal *1.2/1'
Subgoal *1.2/1''
Subgoal *1.2/1'''
Subgoal *1.2/1'4'
*1.2.2 (Subgoal *1.2/1'4') is pushed for proof by induction.
So we now return to *1.2.2, which is
(IMPLIES (AND (ZP J)
(INTEGERP K)
(<= 0 K)
(INTEGERP J)
(NOT (ZP N))
(<= 0 N)
(<= 1 N))
(EQUAL (+ 2 K) N)).
No induction schemes are suggested by *1.2.2. Consequently, the proof
attempt has failed.
Summary
Form: ( DEFTHM COMB-FACTORIAL ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
(:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
(:DEFINITION COMB)
(:DEFINITION FACTORIAL)
(:DEFINITION FIX)
(:DEFINITION NATP)
(:DEFINITION NOT)
(:DEFINITION SYNP)
(:EXECUTABLE-COUNTERPART <)
(:EXECUTABLE-COUNTERPART BINARY-*)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART COMB)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART FACTORIAL)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:EXECUTABLE-COUNTERPART UNARY--)
(:EXECUTABLE-COUNTERPART UNARY-/)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION COMB)
(:INDUCTION FACTORIAL)
(:REWRITE ASSOCIATIVITY-OF-*)
(:REWRITE ASSOCIATIVITY-OF-+)
(:REWRITE COMB-ZERO)
(:REWRITE COMMUTATIVITY-2-OF-+)
(:REWRITE COMMUTATIVITY-OF-*)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
(:REWRITE FOLD-CONSTS-IN-+)
(:REWRITE INVERSE-OF-*)
(:REWRITE INVERSE-OF-+)
(:REWRITE UNICITY-OF-0)
(:REWRITE UNICITY-OF-1)
(:REWRITE ZP-OPEN)
(:TYPE-PRESCRIPTION COMB)
(:TYPE-PRESCRIPTION FACTORIAL))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION FACTORIAL)
(:DEFINITION NOT)
(:REWRITE ZP-OPEN))
Warnings: Subsume
Time: 0.15 seconds (prove: 0.13, print: 0.01, other: 0.00)
Prover steps counted: 15441
---
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: ***
Subgoal 2'
(IMPLIES (AND (<= 0 N)
(NOT (ZP K))
(NOT (ZP N))
(<= K N))
(EQUAL (COMB N K)
(* (FACTORIAL N)
(/ (* (FACTORIAL K)
(FACTORIAL (+ (- K) N)))))))
*** Key checkpoints under a top-level induction: ***
Subgoal *1/8.2'
(IMPLIES (AND (NOT (ZP K))
(NOT (ZP N))
(EQUAL (COMB (+ -1 N) K)
(* (FACTORIAL (+ -1 N))
(/ (* K (FACTORIAL (+ -1 K))
(FACTORIAL (+ -1 (- K) N))))))
(< 0 (+ (- K) N))
(EQUAL (COMB (+ -1 N) (+ -1 K))
(* (FACTORIAL (+ -1 N))
(/ (* (FACTORIAL (+ -1 K))
(+ (- K) N)
(FACTORIAL (+ -1 (- K) N))))))
(<= 0 N)
(<= K N))
(EQUAL (+ (COMB (+ -1 N) K)
(COMB (+ -1 N) (+ -1 K)))
(* N (FACTORIAL (+ -1 N))
(/ (* K (FACTORIAL (+ -1 K))
(+ (- K) N)
(FACTORIAL (+ -1 (- K) N)))))))
Subgoal *1/4'5'
(IMPLIES (AND (NOT (ZP N))
(< 0 (+ -1 N))
(EQUAL (+ 1 (COMB (+ -2 N) 1))
(* (/ (FACTORIAL (+ -2 N)))
(+ -1 N)
(FACTORIAL (+ -2 N))))
(<= 0 N)
(<= 1 N))
(EQUAL (+ 2 (COMB (+ -2 N) 1)) N))
ACL2 Error in ( DEFTHM COMB-FACTORIAL ...): See :DOC failure.
******** FAILED ********
なんと、ACL2 による自動証明は失敗してしまいました。 Key checkpoints の
Subgoal *1/8.2' のところをみてみましょう。=implies=
の第一引数は仮定で第二引数は帰結なのですが、仮定のところに
(EQUAL (COMB (+ -1 N) K) ...) という式と
(EQUAL (COMB (+ -1 N) (+ -1 K)) ...) という式があって、帰結の部分に
(COMB (+ -1 N) K) と (COMB (+ -1 N) (+ -1 K))
があることに注目してください。
上記の仮定の式を使って帰結の式を置き換えると下記のように FACTORIAL
関数のみを使った式が出てきます(仮定は省略)。
(EQUAL (+ (* (FACTORIAL (+ -1 N))
(/ (* K (FACTORIAL (+ -1 K))
(FACTORIAL (+ -1 (- K) N)))))
(* (FACTORIAL (+ -1 N))
(/ (* (FACTORIAL (+ -1 K))
(+ (- K) N)
(FACTORIAL (+ -1 (- K) N))))))
(* N (FACTORIAL (+ -1 N))
(/ (* K (FACTORIAL (+ -1 K))
(+ (- K) N)
(FACTORIAL (+ -1 (- K) N))))))
これが真であることを示せばいいので、ACL2
で証明するのは不可能ではなさそうな気がしますね(実際、手計算で等しいことを確認しました)。ただ、標準の
ACL2
でこういう四則演算をたくさん含んだ式について証明するのはあまり簡単ではありません。
ACL2
ではよく使われる定理ライブラリも一緒に配布されていて、その中に算術に関する証明をするのに大変便利な
arithmetic という定理ライブラリが入っています。今回はこれを使います。
(include-book "arithmetic/top" :dir :system)
Summary Form: ( INCLUDE-BOOK "arithmetic/top" ...) Rules: NIL Time: 0.43 seconds (prove: 0.00, print: 0.00, other: 0.43) "/gnu/store/cj54gk0b9qqxfh0pz8mrh7j8iwrbz4p4-acl2-8.4/lib/acl2/books/arithmetic/top.lisp"
もう一度 comb-factorial の証明を試みます。
(defthm comb-factorial
(implies (and (natp n)
(natp k))
(equal (comb n k)
(if (< n k)
0
(/ (factorial n)
(* (factorial (- n k))
(factorial k)))))))
ACL2 Warning [Subsume] in ( DEFTHM COMB-FACTORIAL ...): A newly proposed
:REWRITE rule generated from COMB-FACTORIAL probably subsumes the previously
added :REWRITE rule COMB-ZERO, in the sense that the new rule will
now probably be applied whenever the old rule would have been.
Goal'
Subgoal 2
Subgoal 1
Subgoal 1'
([ A key checkpoint:
Subgoal 1'
(IMPLIES (AND (NATP N) (NATP K) (<= K N))
(EQUAL (FACTORIAL N)
(* (FACTORIAL K)
(COMB N K)
(FACTORIAL (+ (- K) N)))))
*1 (Subgoal 1') is pushed for proof by induction.
])
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. Subsumption reduces that number to one.
We will induct according to a scheme suggested by (COMB N K). This
suggestion was produced using the :induction rules COMB and FACTORIAL.
If we let (:P K N) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (AND (NOT (ZP K))
(NOT (ZP N))
(:P K (+ -1 N))
(:P (+ -1 K) (+ -1 N)))
(:P K N))
(IMPLIES (AND (NOT (ZP K)) (ZP N))
(:P K N))
(IMPLIES (ZP K) (:P K N))).
This induction is justified by the same argument used to admit COMB.
Note, however, that the unmeasured variable K is being instantiated.
When applied to the goal at hand the above induction scheme produces
nine nontautological subgoals.
Subgoal *1/9
Subgoal *1/9'
Subgoal *1/9''
Splitter note (see :DOC splitter) for Subgoal *1/9'' (2 subgoals).
if-intro: ((:DEFINITION FACTORIAL)
(:DEFINITION NOT)
(:REWRITE ZP-OPEN))
Subgoal *1/9.2
Subgoal *1/9.2'
Subgoal *1/9.1
Subgoal *1/9.1'
Subgoal *1/8
Subgoal *1/8'
Subgoal *1/8''
Subgoal *1/7
Subgoal *1/6
Subgoal *1/5
Subgoal *1/4
Subgoal *1/3
Subgoal *1/2
Subgoal *1/1
Subgoal *1/1'
Subgoal *1/1''
*1 is COMPLETED!
Thus key checkpoint Subgoal 1' is COMPLETED!
Q.E.D.
Summary
Form: ( DEFTHM COMB-FACTORIAL ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
(:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
(:DEFINITION COMB)
(:DEFINITION FACTORIAL)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION SYNP)
(:EXECUTABLE-COUNTERPART BINARY-*)
(:EXECUTABLE-COUNTERPART BINARY-+)
(:EXECUTABLE-COUNTERPART FACTORIAL)
(:EXECUTABLE-COUNTERPART NATP)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART TAU-SYSTEM)
(:EXECUTABLE-COUNTERPART UNARY--)
(:EXECUTABLE-COUNTERPART ZP)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:FORWARD-CHAINING NATP-FC-1)
(:INDUCTION COMB)
(:INDUCTION FACTORIAL)
(:REWRITE <-0-+-NEGATIVE-1)
(:REWRITE ASSOCIATIVITY-OF-*)
(:REWRITE ASSOCIATIVITY-OF-+)
(:REWRITE COMB-ZERO)
(:REWRITE COMMUTATIVITY-2-OF-*)
(:REWRITE COMMUTATIVITY-2-OF-+)
(:REWRITE COMMUTATIVITY-OF-*)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE DISTRIBUTIVITY)
(:REWRITE DISTRIBUTIVITY-OF-/-OVER-*)
(:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
(:REWRITE EQUAL-*-/-1)
(:REWRITE EQUAL-*-/-2)
(:REWRITE EQUAL-*-X-Y-X)
(:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT)
(:REWRITE INVERSE-OF-+)
(:REWRITE MINUS-CANCELLATION-ON-LEFT)
(:REWRITE TIMES-ZERO)
(:REWRITE UNICITY-OF-0)
(:REWRITE UNICITY-OF-1)
(:REWRITE ZP-OPEN)
(:TYPE-PRESCRIPTION COMB)
(:TYPE-PRESCRIPTION FACTORIAL)
(:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))
Splitter rules (see :DOC splitter):
if-intro: ((:DEFINITION FACTORIAL)
(:DEFINITION NOT)
(:REWRITE ZP-OPEN))
Warnings: Subsume
Time: 0.06 seconds (prove: 0.06, print: 0.01, other: 0.00)
Prover steps counted: 4875
COMB-FACTORIAL
証明に成功しました。定理ライブラリの力は凄いですね。
6. おわりに
前回作成した組み合わせの数を求める関数とその階乗表現が等しいことを証明できました。
本当は comb-factorial の証明に失敗したときの出力を見てから補助定理
comb-zero
を作成する流れにしたかったのですが、証明の失敗時に出力されていた Key
Checkpoints をいくら眺めてもなぜ comb-zero
が必要なのかを説明するのが難しかったので、ちょっと無理矢理ですが先に
comb-zero を証明しておく流れにしました。
Key Checkpoints を読んで必要な補助定理を作成する例としては今回のはちょっと難しすぎたので、また別の機会に簡単な例を出せたらいいなと考えています。
ただ、ACL2 に関心のある方は私の記事を読むよりかは ACL2 のチュートリアル を参照したり、『定理証明手習い』(ラムダノート社) を読んで勉強するのがおすすめです。『定理証明手習い』(ラムダノート社) では ACL2 の使い方について学ぶことはできないのですが、 ACL2 を使うのに必要な前提知識について学べるのでおすすめです。