ACL2 で組み合せの数とその階乗表現の関係について証明してみた

はじめに

本記事は前回の ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた -- TojoQK の続きです。未読の方は先に読んでからお読みください。

前回、リスト中の要素の全ての組み合わせを求める関数 combinations と組み合わせの数を求める関数 comb を求め、 (len (combinations x k))(comb (len x) k) が等しいことを証明しました。ただし、combinationscomb の定義は同じ構造をしているため、ACL2 で自動証明ができたといってもありがたみを感じにくい例だったかと思います。 よって、今回は組み合わせの数を階乗で表現した式と前回の comb が等しいことを証明します。

本記事で例示するプログラムのライセンス

本記事で例示するプログラムのライセンスは3条項BSDであり自由ソフトウェアです。下記にライセンスを明示します。

Copyright (C) 2021 Masaya Tojo <masaya@tojo.tokyo>

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.

3. Neither the name of the copyright holder nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

組み合せの数を求める関数 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 の関数定義の仕様について軽く説明する必要があります。

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 を使用しても変わりません)。

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

階乗を求める関数 factorial を定義する

階乗の定義は下記の通りです。

  1. 0 の階乗は 1
  2. 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

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

証明に成功しました。定理ライブラリの力は凄いですね。

おわりに

前回作成した組み合わせの数を求める関数とその階乗表現が等しいことを証明できました。 本当は comb-factorial の証明に失敗したときの出力を見てから補助定理 comb-zero を作成する流れにしたかったのですが、証明の失敗時に出力されていた Key Checkpoints をいくら眺めてもなぜ comb-zero が必要なのかを説明するのが難しかったので、ちょっと無理矢理ですが先に comb-zero を証明しておく流れにしました。

Key Checkpoints を読んで必要な補助定理を作成する例としては今回のはちょっと難しすぎたので、また別の機会に簡単な例を出せたらいいなと考えています。

ただ、ACL2 に関心のある方は私の記事を読むよりかは ACL2 のチュートリアル を参照したり、『定理証明手習い』(ラムダノート社) を読んで勉強するのがおすすめです。『定理証明手習い』(ラムダノート社) では ACL2 の使い方について学ぶことはできないのですが、 ACL2 を使うのに必要な前提知識について学べるのでおすすめです。