aboutsummaryrefslogtreecommitdiff
path: root/posts/comb-factorial.md
blob: 806a99897781f7c3cbf61c1981e02ccdeaac73ed (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
title: ACL2 で組み合せの数とその階乗表現の関係について証明してみた
id: comb-factorial
date: 2021-09-05 13:30
updated: 2021-09-05 14:00
---

## はじめに

本記事は前回の [ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた --
TojoQK](https://www.tojo.tokyo/len-combinations.html)
の続きです。未読の方は先に読んでからお読みください。

前回、リスト中の要素の全ての組み合わせを求める関数 `combinations` と組み合わせの数を求める関数 `comb` を求め、
`(len (combinations x k))` と `(comb (len x) k)`
が等しいことを証明しました。ただし、`combinations` と
`comb` の定義は同じ構造をしているため、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 を定義する

[前回の記事](https://www.tojo.tokyo/len-combinations.html)で作成した組み合わせの数を求める関数
`comb` です。
関数の定義については[前回の記事](https://www.tojo.tokyo/len-combinations.html)で説明しているので必要であれば参照してください



``` acl2
(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
関数のドキュメント](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____ZP)
を参照してください。

また、ACL2 が型なしであることについて不安に感じた静的型付きのプログラミング言語を好む方は [XDOC —
Guard](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____GUARD)
を軽く読んでみてください。初心者向けの機能ではないのですが、実際に関数に渡る値を静的に制限することができます(停止性の証明時にあらゆる値について考慮しないといけないことは
Guard を使用しても変わりません)。



### comb の性質

`comb` と階乗の関係の性質について証明する前に `comb` について既に分かっている性質については先に証明しておきましょう。 特に
`comb` の次に説明する階乗表現を定義する際には「k が n よりも大きいときは (comb n k) は 0」という性質を利用します。
なので、下記の `comb-zero` という定理を先に証明しておきます。



``` acl2
(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
関数を使用するため全く同じというわけではありません)。



``` acl2
(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!
```

何故かについては「組み合せの数
公式」とかで適当に[検索](https://duckduckgo.com/?q=%E7%B5%84%E3%81%BF%E5%90%88%E3%82%8F%E3%81%9B%E3%81%AE%E6%95%B0+%E5%85%AC%E5%BC%8F)してください(やる気なし)。
ということで上記の式を ACL2 に翻訳してみましょう。分母が 0 になったり結果が分数になにならないように調節しています。



``` acl2
(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` という定理ライブラリが入っています。今回はこれを使います。



``` acl2
(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` の証明を試みます。



``` acl2
(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
```




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



## おわりに

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

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

ただ、ACL2 に関心のある方は私の記事を読むよりかは [ACL2
のチュートリアル](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____ACL2-TUTORIAL)
を参照したり、『定理証明手習い』(ラムダノート社) を読んで勉強するのがおすすめです。『定理証明手習い』(ラムダノート社) では ACL2
の使い方について学ぶことはできないのですが、 ACL2 を使うのに必要な前提知識について学べるのでおすすめです。