aboutsummaryrefslogtreecommitdiff
path: root/posts/len-combinations.md
blob: 7d0e3388379674ed828d0fea8797fc571cc35d59 (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
title: ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた
id: len-combinations
date: 2021-09-02 01:45
updated: 2021-09-02 10:30
---

## はじめに

ACL2 でリストから k 個取り出す全ての組み合わせを求める関数 `combinations` と、組み合わせの数を求める関数 `comb`
を定義し、`(equal (len (combinations x n)) (comb (len x) n))` を証明します。



## きっかけ

[acl2-kernel](https://github.com/tani/acl2-kernel)
を使ってブログ記事を書いてみたいというのが本記事の主な動機です。今回良い感じに書けたら、今後も
ACL2 でなんかやってみた記事を `acl2-kernel` を使って書いてみようと思います。



## LICENSE

下記に例示するプログラムのライセンスを明示します。

    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.



## combinations 関数を定義する

リストから k 個の要素を取り出す全ての組み合せを求める関数 `combinations` 関数を定義します。

### 補助関数 cons-all を定義する

`combinations` を作成するためには全てのリストの先頭に要素を一つ追加する `cons-all` 関数が必要です。
`cons-all` の停止性は ACL2 が自動証明してくれました。 `cons-all`
の第二引数は真リストしか渡らないようにガードを設定していますが、ガードの証明も問題なく自動証明されました。



``` acl2
(defun cons-all (e x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      nil
      (cons (cons e (car x))
            (cons-all e (cdr x)))))
```


``` 



Summary
Form:  ( RESET-PREHISTORY NIL ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 :NEW-PREHISTORY-SET









The admission of CONS-ALL 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 X).  We observe that the type of CONS-ALL is described
by the theorem (TRUE-LISTP (CONS-ALL E X)).  We used primitive type
reasoning.

Computing the guard conjecture for CONS-ALL....

The guard conjecture for CONS-ALL is trivial to prove, given primitive
type reasoning.  CONS-ALL is compliant with Common Lisp.

Summary
Form:  ( DEFUN CONS-ALL ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 CONS-ALL

```




### combinations 関数

リスト x から k 個を取り出す全ての組み合せのリストを求める関数 `combinations` を定義します。

再帰によって `combinations` 関数を定義します。 `combinations`
関数を作成するにはリストの先頭の要素を含む場合と含まない場合に分けて分離して考えてそれらを連結するのがよいです。

#### リストの先頭の要素を含む組み合せを求める

リストの先頭の要素を含む場合は、まずリストの先頭の要素を含まない全ての組み合せを `combinations` 関数により求めます。その後に
`cons-all` 関数を用いて全ての組み合せのそれぞれに先頭の要素を追加します。

    (cons-all (car x)
              (combinations (cdr x) (- n 1)))

#### リストの先頭の要素を含まない組み合せを求める

リストの先頭の要素を含まない場合は簡単で、下記のように `combinations`
関数を使ってリストの先頭の要素を含めない場合を求めるだけです。

    (combinations (cdr x) n)

#### combinations 関数の基底部を考える

基底部として考えられるケースには与えられた自然数が 0 の場合と与えられたリストが空の場合があります。 リストから 0
個取り出す組み合せはただ一つ存在し、空リストです。よってリストから0個取り出す場合の全ての組み合せは
`(list nil)` です。

空のリストからは 1 以上取り出す組み合せを求めることは不可能です(空リストから 0
個を取り出す組み合せを求めることは可能で結果は上述した通りです)。不可能なわけですから、空リストから
1 以上取り出す場合の全ての組み合せは `nil` です。

#### combinations 関数

上記をまとめると、`combinations` 関数は下記のように実装できます。 停止性とガードは補助定理なしで ACL2
が自動証明してくれました。



``` acl2
(defun combinations (x n)
  (declare (xargs :guard (and (true-listp x)
                              (natp n))))
  (cond
    ((zp n) (list nil))
    ((endp x) nil)
    (t
     (append (cons-all (car x)
                       (combinations (cdr x) (- n 1)))
             (combinations (cdr x) n)))))
```


``` 












The admission of COMBINATIONS 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 X).  We observe that the type of COMBINATIONS is
described by the theorem (TRUE-LISTP (COMBINATIONS X N)).  We used
the :type-prescription rules BINARY-APPEND and TRUE-LISTP-APPEND.

Computing the guard conjecture for COMBINATIONS....

The guard conjecture for COMBINATIONS is trivial to prove, given the
:compound-recognizer rules NATP-COMPOUND-RECOGNIZER and 
ZP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription
rules COMBINATIONS and CONS-ALL.  COMBINATIONS is compliant with Common
Lisp.

Summary
Form:  ( DEFUN COMBINATIONS ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION COMBINATIONS)
        (:TYPE-PRESCRIPTION CONS-ALL)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 COMBINATIONS

```




## comb 関数を定義する

n 個から k 個を取り出す組み合せの数を求める関数を定義します。 `combinations`
の定義を参照しながら対応するように記述しましょう。

  - 0 個を取り出す組み合せは空リストただ一つなので、組み合せの数は 1
  - 長さ 0 のリストから 1 個以上取り出すことはできないため、組み合せの数は 0
  - 先頭要素を含む組み合せの数は `(comb (- n 1) (- k 1))`
      - cons-all 関数は与えられたリストの長さを変えないことに注意
  - 先頭要素を含まない組み合せの数は `(comb (- n 1) k)`



``` acl2
(defun comb (n k)
  (cond
    ((zp k) 1)
    ((zp n) 0)
    (t (+ (comb (- n 1) (- k 1))
          (comb (- n 1) k)))))
```


``` 






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.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 COMB

```




## len-combinations 定理

`(len (combinations x k))` が `(comb (len x) k)` と一致することを証明します。 これは ACL2
が補助定理を必要とせずに自動証明してくれました。



``` acl2
(defthm len-combinations
  (equal (len (combinations x k))
         (comb (len x) k)))
```


``` 






*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  These merge into one derived induction scheme.

We will induct according to a scheme suggested by (COMBINATIONS X K).
This suggestion was produced using the :induction rules COMBINATIONS
and LEN.  If we let (:P K X) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ZP K))
                   (NOT (ENDP X))
                   (:P (+ -1 K) (CDR X))
                   (:P K (CDR X)))
              (:P K X))
     (IMPLIES (AND (NOT (ZP K)) (ENDP X))
              (:P K X))
     (IMPLIES (ZP K) (:P K X))).
This induction is justified by the same argument used to admit COMBINATIONS.
Note, however, that the unmeasured variable K is being instantiated.
When applied to the goal at hand the above induction scheme produces
three nontautological subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/3'''
Subgoal *1/3'4'
Subgoal *1/3'5'
Subgoal *1/3'6'
Subgoal *1/3'7'
Subgoal *1/3'8'
Subgoal *1/3'9'
Subgoal *1/3'10'

([ A key checkpoint while proving *1 (descended from Goal):

Subgoal *1/3''
(IMPLIES (AND (NOT (ZP K))
              (CONSP X)
              (EQUAL (LEN (COMBINATIONS (CDR X) (+ -1 K)))
                     (COMB (LEN (CDR X)) (+ -1 K)))
              (EQUAL (LEN (COMBINATIONS (CDR X) K))
                     (COMB (LEN (CDR X)) K)))
         (EQUAL (LEN (APPEND (CONS-ALL (CAR X)
                                       (COMBINATIONS (CDR X) (+ -1 K)))
                             (COMBINATIONS (CDR X) K)))
                (+ (COMB (LEN (CDR X)) K)
                   (COMB (LEN (CDR X)) (+ -1 K)))))

*1.1 (Subgoal *1/3'10') is pushed for proof by induction.

])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1

So we now return to *1.1, which is

(IMPLIES (AND (TRUE-LISTP CS0) (TRUE-LISTP CS))
         (EQUAL (LEN (APPEND (CONS-ALL X1 CS0) CS))
                (+ (LEN CS) (LEN CS0)))).
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/1
Subgoal *1.1/1'

*1.1 and *1 are COMPLETED!
Thus key checkpoints Subgoal *1/3'' and Goal are COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM LEN-COMBINATIONS ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION BINARY-APPEND)
        (:DEFINITION COMB)
        (:DEFINITION COMBINATIONS)
        (:DEFINITION CONS-ALL)
        (:DEFINITION ENDP)
        (:DEFINITION FIX)
        (:DEFINITION LEN)
        (:DEFINITION NOT)
        (:DEFINITION SYNP)
        (:DEFINITION TRUE-LISTP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION COMBINATIONS)
        (:INDUCTION CONS-ALL)
        (:INDUCTION LEN)
        (:INDUCTION TRUE-LISTP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-2-OF-+)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE FOLD-CONSTS-IN-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION COMBINATIONS)
        (:TYPE-PRESCRIPTION CONS-ALL)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  5105
 LEN-COMBINATIONS

```




## おわりに

無事に組み合せを求める関数と組み合せの数を求める関数の関係が意図した通りであることを証明できました。
今回は二つの関数の定義がほとんど同じであったため補助定理を考える必要もなく証明できたのですが、通常はもう少し難しいことが多いです。

`comb` の定義の方法は他にもあるため、他の定義による組み合せの数と一致するかについての証明を試みても良いかもしれません。