/
Prop_J.v
2871 lines (2355 loc) · 140 KB
/
Prop_J.v
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
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(** * Prop_J: 命題と根拠 *)
(* $Date: 2011-06-27 09:22:51 -0400 (Mon, 27 Jun 2011) $ *)
(** "アルゴリズムは計算可能な証明である。"(Robert Harper) *)
Require Export Poly_J.
(* ##################################################### *)
(* ##################################################### *)
(** * 命題によるプログラミング *)
(* _Note to readers_: Some of the concepts in this chapter may
seem quite abstract on a first encounter. We've included a _lot_
of exercises, most of which should be quite approachable even if
you're still working on understanding the details of the text.
Try to work as many of them as you can, especially the one-starred
exercises. *)
(** 読者への注意: この章で紹介するコンセプトは、初めて見た時には抽象的すぎるように感じられるかもしれません。
たくさんの練習問題を用意しておいたので、テキストの詳細を理解する途中であっても大部分は解けるはずです。
できるかぎり多くの問題、特に★の問題には重点的に挑戦するようにしてください。 *)
(* So far, the only statements we have been able to state and
prove have been in the form of _equalities_. However, the
language of mathematical statements and proofs is much richer than
this! In this chapter we will take a much closer and more
fundamental look at the sorts of mathematical statements
(_propositions_) we can make in Coq, and how we go about proving
them by providing logical _evidence_. *)
(** これまで宣言したり証明した文は等式の形をしたものだけでした。
しかし、数学で用いられる文や証明にはもっと豊かな表現力があります。
この章では Coq で作れる数学的な文(命題; _proposition_ )の種類と、その証明を「根拠( _evidence_ )を与えること」でどのように進めていくか、もう少し詳しく、基本的な部分から見ていきましょう。
*)
(* A _proposition_ is a statement expressing a factual claim,
like "two plus two equals four." In Coq, propositions are written
as expressions of type [Prop]. Although we haven't mentioned it
explicitly, we have already seen numerous examples. *)
(** 命題( _proposition_ )は、"2足す2は4と等しい"のような事実に基づく主張を表現するための文です。
Coq において命題は [Prop] 型の式として書かれます。
これまであまりそれについて明示的に触れてはきませんでしたが、皆さんはすでに多くの例を見てきています。 *)
Check (2 + 2 = 4).
(* ===> 2 + 2 = 4 : Prop *)
Check (ble_nat 3 2 = false).
(* ===> ble_nat 3 2 = false : Prop *)
(* Both provable and unprovable claims are perfectly good
propositions. Simply _being_ a proposition is one thing; being
_provable_ is something else! *)
(** 証明可能な主張も証明不能な主張も、どちらも完全な命題であると言えます。
しかし単に命題であるということと、証明可能であるということは別ものです! *)
Check (2 + 2 = 5).
(* ===> 2 + 2 = 5 : Prop *)
(** [2 + 2 = 4] も [2 + 2 = 5] も [Prop] の型をもった妥当な式です。 *)
(* We've seen one way that propositions can be used in Coq: in
[Theorem] (and [Lemma] and [Example]) declarations. *)
(** これまで Coq の中で命題を使う方法は1つしか見ていません。 [Theorem](あるいは [Lemma]、[Example])の宣言の中でだけです。 *)
Theorem plus_2_2_is_4 :
2 + 2 = 4.
Proof. reflexivity. Qed.
(* But they can be used in many other ways. For example, we
can give a name to a proposition using a [Definition], just as we
have given names to expressions of other sorts (numbers,
functions, types, type functions, ...). *)
(** しかし命題にはもっといろいろな使い方があります。
例えば、他の種類の式(数字、関数、型、型関数など)と同様に、[Definition] を使うことで命題に名前を与えることができます。 *)
Definition plus_fact : Prop := 2 + 2 = 4.
Check plus_fact.
(* ===> plus_fact : Prop *)
(* Now we can use this name in any situation where a proposition is
expected -- for example, as the claim in a [Theorem]
declaration. *)
(** こうすることで、命題が使える場所ならどこでも、例えば、[Theorem] 宣言内の主張などとして使うことができます。 *)
Theorem plus_fact_is_true :
plus_fact.
Proof. reflexivity. Qed.
(* So far, all the propositions we have seen are equality
propositions. We can also form new propositions out of old
ones. For example, given propositions [P] and [Q], we can form
the proposition "[P] implies [Q]." *)
(** ここまでに登場したすべての命題は等式の形をした命題でした。
それ以外にも新しい命題の形を作ることができます。
例えば、命題 [P] と [Q] が与えられば、" [P] ならば [Q] "という命題を作れます。
*)
Definition strange_prop1 : Prop :=
(2 + 2 = 5) -> (99 + 26 = 42).
(* Also, given a proposition [P] with a free variable [n], we can
form the proposition [forall n, P]. *)
(** また、自由変数[n]を含む命題 [P] が与えられれば、[forall n, P] という形の命題を作れます。 *)
Definition strange_prop2 :=
forall n, (ble_nat n 17 = true) -> (ble_nat n 99 = true).
(* Finally, we can define _parameterized propositions_. For
example, what does it mean to claim that "a number n is even"? We
have written a function that tests evenness, so one possible
definition of what it means to be even is "[n] is even iff [evenb
n = true]." *)
(** 最後に、パラメータ化された命題(_parameterized proposition_ )の定義を紹介します。
例えば、"数nが偶数である"という主張はどのようになるでしょうか?
偶数を判定する関数は書いてあるので、偶数であるという定義は" [n] が偶数であることと [evenb n = true] は同値である"が考えられます。 *)
Definition even (n:nat) : Prop :=
evenb n = true.
(* This defines [even] as a _function_ that, when applied to a number
[n], _yields a proposition_ asserting that [n] is even. *)
(** これは [even] を関数として定義します。
この関数は数 [n] を適用されると、[n] が偶数であることを示す命題を返します。 *)
Check even.
(* ===> even : nat -> Prop *)
Check (even 4).
(* ===> even 4 : Prop *)
Check (even 3).
(* ===> even 3 : Prop *)
(* The type of [even], [nat->Prop], can be pronounced in three
ways: (1) "[even] is a _function_ from numbers to
propositions," (2) "[even] is a _family_ of propositions, indexed
by a number [n]," or (3) "[even] is a _property_ of numbers." *)
(** [even]の型 [nat -> Prop]は3つの意味を持っています。
(1) "[even]は数から命題への関数である。"
(2) "[even]は数[n]でインデックスされた命題の集りである"。
(3) "[even]は数の性質(_property_)である。" *)
(* Propositions -- including parameterized propositions -- are
first-class citizens in Coq. We can use them in other
definitions: *)
(** 命題(パラメータ化された命題も含む)はCoqにおける第一級(_first-class_)市民です。
このため、ほかの定義の中でこれらの命題を使うことができます。 *)
Definition even_n__even_SSn (n:nat) : Prop :=
(even n) -> (even (S (S n))).
(* We can define them to take multiple arguments... *)
(** 複数の引数を受け取るように定義することや.. *)
Definition between (n m o: nat) : Prop :=
andb (ble_nat n o) (ble_nat o m) = true.
(* ... and then partially apply them: *)
(** ...部分適用もできます。 *)
Definition teen : nat->Prop := between 13 19.
(* We can even pass propositions -- including parameterized
propositions -- as arguments to functions: *)
(** 他の関数に、引数として命題(パラメータ化された命題も含む)を渡すことすらできます。 *)
Definition true_for_zero (P:nat->Prop) : Prop :=
P 0.
Definition true_for_n__true_for_Sn (P:nat->Prop) (n:nat) : Prop :=
P n -> P (S n).
(* (Names of the form [x__y], with two underscores in a row, can be
read "[x] implies [y].") *)
(** 2つのアンダースコアを続けた [x__y] という形式の名前は、" [x] ならば [y] である"と読みます。 *)
(* Here are two more examples of passing parameterized
propositions as arguments to a function. The first makes the
claim that a whenever a proposition [P] is true for some natural
number [n'], it is also true by the successor of [n']: *)
(** パラメータ化された命題を引数として渡す関数をさらに2つ紹介します。
1つ目の関数は、ある自然数 [n'] について [P] が真ならば常に [n'] の次の数でも [P] が真であることを述べています。
*)
Definition preserved_by_S (P:nat->Prop) : Prop :=
forall n', P n' -> P (S n').
(* And this one simply claims that a proposition is true for
all natural numbers: *)
(** そして次の関数は、すべての自然数について与えられた命題が真であることを述べています。 *)
Definition true_for_all_numbers (P:nat->Prop) : Prop :=
forall n, P n.
(* We can put these pieces together to manually restate the
principle of induction for natural numbers. Given a parameterized
proposition [P], if [P] is true for [0], and [P (S n')] is true
whenever [P n'] is, then [P] is true for all natural numbers. *)
(** これらを一つにまとめることで、自然数に関する帰納法の原理を自分で再宣言できます。
パラメータ化された命題 [P] が与えられた場合、[0] について [P] が真であり、[P n'] が真のとき [P (S n')] が真であるならば、すべての自然数について [P] は真である。
*)
Definition our_nat_induction (P:nat->Prop) : Prop :=
(true_for_zero P) ->
(preserved_by_S P) ->
(true_for_all_numbers P).
(* * Evidence *)
(** * 根拠 *)
(* We've seen that well-formed expressions of type [Prop] can
embody both provable and unprovable propositions. Naturally,
we're particularly interested in the provable ones. When [P] is a
proposition and [e] is a proof of [P] -- i.e., [e] is evidence
that [P] is true -- we'll write "[e : P]." This overloading of
the "has type" or "inhabits" notation is not accidental: we'll see
that there is a fundamental and fruitful analogy between data
values inhabiting types and evidence "inhabiting" propositions. *)
(** [Prop]型として妥当な式には証明可能な命題と証明不能な命題の両方があることは既にお話ししました。
当然、証明可能なものの方に興味が向かいます。
[P] が命題であり [e] が [P] の証明である場合、すなわち [e] が「 [P] が真である」ということの根拠となっている場合、それを" [e : P] "と書くことができます。
"型を持っている"や"属している"を表わす記法と同じなのは決して偶然ではありません。
型に属する値と命題に"属する"根拠の間には根本的で有益な類似性があるのです。 *)
(* The next question is "what are proofs?" -- i.e., what sorts of
things would we be willing to accept as evidence that particular
propositions are true? *)
(** 次の疑問は"証明とはなにか?"です。
すなわち、ある命題が真であるという根拠として使えるものは、どのようなものでしょうか? *)
(* ##################################################### *)
(* ** Inductively Defined Propositions *)
(** ** 帰納的に定義された命題 *)
(* The answer, of course, depends on the form of the
proposition -- evidence for implication propositions ([P->Q]) is
different from evidence for conjunctions ([P/\Q]), etc. In this
chapter and the next, we'll address a number of specific cases.
To begin with, consider _atomic_ propositions -- ones that aren't
built into the logic we're using, but are rather introduced to
model useful concepts in a particular domain. For example, having
defined a type [day] as we did in Basics.v, we might have some
concept in our minds about certain days, say the fact that
[saturday] and [sunday] are "good" ones. If we want to use Coq to
state and prove theorems involving good days, we need to begin by
telling it what we mean by "good" -- that is, we need to specify
what counts as as evidence that some day [d] is good (namely, that
[d] is either [saturday] or [sunday]. The following declaration
achieves this: *)
(** もちろん、その答は命題の形に依存します。
例えば、含意の命題 [P->Q] に対する根拠と連言の命題 [P/\Q] に対する根拠は異なります。
この章では以後、たくさんの具体的な例を示します。
まずは、不可分( _atomic_ )な命題を考えましょう。
それは私達が使っている論理にあらかじめ組み込まれているものはなく、特定のドメイン(領域)に有用な概念を導入するものです。
例えば、Basic_J.v で [day] 型を定義したので、[saturday] と [sunday] は"良い"日であるといったような、特定の日に対して何らかの概念を考えてみましょう。
良い日に関する定理を宣言し証明したい場合はまず、"良い"とはどういう意味かをCoqに教えなければなりません。
ある日 [d] が良い(すなわち [d] が [saturday] か [sunday] である)とする根拠として何を使うかを決める必要があります。
このためには次のように宣言します。 *)
Inductive good_day : day -> Prop :=
| gd_sat : good_day saturday
| gd_sun : good_day sunday.
(* The [Inductive] keyword means exactly the same thing whether
we are using it to define sets of data values (in the [Type]
world) or sets of evidence (in the [Prop] world). Consider the
parts of the definition above:
- The first line declares that [good_day] is a proposition indexed
by a day.
- The second line declares that the constructor [gd_sat] can be
taken as evidence for the assertion [good_day saturday].
- The third line declares that the constructor [gd_sun] can be
taken as evidence for the assertion [good_day sunday]. *)
(** [Inductive] キーワードは、「データ値の集合を定義する場合( [Type] の世界)」であっても「根拠の集合を定義する場合( [Prop] の世界)」であってもまったく同じ意味で使われます。
上記の定義の意味はそれぞれ次のようになっています:
- 最初の行は「 [good_day] は日によってインデックスされた命題であること」を宣言しています。
- 二行目は [gd_sat] コンストラクタを宣言しています。このコンストラクタは [good_day saturday] という主張の根拠として使えます。
- 三行目は [gd_sun] コンストラクタを宣言しています。このコンストラクタは [good_day sunday] という主張の根拠として使えます。
*)
(* That is, we're _defining_ what we mean by days being good by
saying "Saturday is good, sunday is good, and that's all." Then
someone can _prove_ that Sunday is good simply by observing that
we said it was when we defined what [good_day] meant. *)
(** 言い換えると、ある日が良いということを"土曜日は良い、日曜日は良い、それだけだ"と言うことで定義しています。
これによって、日曜日が良いということを証明したいときは、[good_day] の意味を定義したときにそう言っていたかを調べるだけで済みます。 *)
Theorem gds : good_day sunday.
Proof. apply gd_sun. Qed.
(* The constructor [gd_sun] is "primitive evidence" -- an _axiom_ --
justifying the claim that Sunday is good. *)
(** コンストラクタ [gd_sun] は、日曜日が良いという主張を正当化する"原始的(primitive)な根拠"、つまり公理です。*)
(* Similarly, we can define a proposition [day_before]
parameterized by _two_ days, together with axioms stating that
Monday comes before Tuesday, Tuesday before Wednesday, and so
on. *)
(** 同様に、月曜日は火曜日の前に来て、火曜日は水曜日の前に来て、...、ということを宣言する公理を、2つの日をパラメータとして取る命題 [day_before] として定義できます。*)
Inductive day_before : day -> day -> Prop :=
| db_tue : day_before tuesday monday
| db_wed : day_before wednesday tuesday
| db_thu : day_before thursday wednesday
| db_fri : day_before friday thursday
| db_sat : day_before saturday friday
| db_sun : day_before sunday saturday
| db_mon : day_before monday sunday.
(* The axioms that we introduce along with an inductively
defined proposition can also involve universal quantifiers. For
example, it is well known that every day is a fine day forsinging a song: *)
(** 帰納的な定義による命題で導入される公理では全称記号を使うこともできます。
例えば、「どの日だって歌いだしたくなるほど素敵な日だ」という事実については、
わざわざ説明する必要もないでしょう *)
Inductive fine_day_for_singing : day -> Prop :=
| fdfs_any : forall d:day, fine_day_for_singing d.
(* The line above declares that, if [d] is a day, then [fdfs_any d]
can be taken as evidence for [fine_day_for_singing d]. That is,
we can construct evidence that [d] is a [fine_day_for_singing]
by applying the constructor [fdfs_any] to [d].
In particular, Wednesday is a fine day for singing. *)
(** この行は、もし [d] が日ならば、[fdfs_any d] は [fine_day_for_singing d] の根拠として使えるということを宣言してます。
言い換えると、[d] が [fine_day_for_singing] であるという根拠を [fdfs_any] を [d] に適用することで作ることができます。
要するに、水曜日は「歌いだしたくなるほど素敵な日」だということです。
*)
Theorem fdfs_wed : fine_day_for_singing wednesday.
Proof. apply fdfs_any. Qed.
(* As always, the first line here can be read "I'm about to
show you some evidence for the proposition [fine_day_for_singing
wednesday], and I want to introduce the name [fdfs_wed] to refer
to that evidence later on." The second line then instructs Coq
how to assemble the evidence. *)
(** これも同じように、最初の行は"私は命題 [fine_day_for_singing wednesday] に対する根拠を示し、その根拠をあとで参照するために [fdfs_wed] という名前を導入しようと思っている"と解釈できます。
二行目は、Coqにその根拠をどのように組み立てるかを示しています。 *)
(* ##################################################### *)
(* ** Proof Objects *)
(** ** 証明オブジェクト *)
(* There's another -- more primitive -- way to accomplish the
same thing: we can use a [Definition] whose left-hand side is the
name we're introducing and whose right-hand side is the evidence
_itself_, rather than a script for how to build it. *)
(** 同じことができる、もっと原始的な方法もあります。
[Definiton] の左辺を導入しようとしている名前にし、右辺を根拠の構築方法ではなく、根拠そのものにすればいいのです。 *)
Definition fdfs_wed' : fine_day_for_singing wednesday :=
fdfs_any wednesday.
Check fdfs_wed.
Check fdfs_wed'.
(* The expression [fdfs_any wednesday] can be thought of as
instantiating the parameterized axiom [fdfs_any] with the specific
argument [wednesday]. Alternatively, we can think of [fdfs_any]
as a primitive "evidence constructor" that, when applied to a
particular day, stands as evidence that that day is a fine day for
singing; its type, [forall d:day, fine_day_for_singing d],
expresses this functionality, in the same way that the polymorphic
type [forall X, list X] in the previous chapter expressed the fact
that the constructor [nil] can be thought of as a function from
types to empty lists with elements of that type. *)
(** 式 [fdfs_any wednesday] は、パラメータを受け取る公理 [fdfs_any]を 特定の引数 [wednesday] によって具体化したものととらえることができます。
別の見方をすれば、[fdfs_any] を原始的な"根拠コンストラクタ"として捉えることもできます。この根拠コンストラクタは、特定の日を適用されると、その日が「歌わずにはいられないほどよい日」である根拠を表します。
型 [forall d:day, fine_day_for_singing d] はこの機能を表しています。
これは、前章で登場した多相型 [forall X, list X] において [nil] コンストラクタが型からその型を持つ空リストを返す関数であったことと同様です。 *)
(* Let's take a slightly more interesting example. Let's say
that a day of the week is "ok" if either (1) it is a good day or
else (2) it falls the day before an ok day. *)
(** もうちょっと面白い例を見てみましょう。
"OK"な日とは(1)良い日であるか(2)OKな日の前日であるとしましょう。*)
Inductive ok_day : day -> Prop :=
| okd_gd : forall d,
good_day d ->
ok_day d
| okd_before : forall d1 d2,
ok_day d2 ->
day_before d2 d1 ->
ok_day d1.
(* The first constructor can be read "One way to show that [d]
is an ok day is to present evidence that [d] is good." The second
can be read, "Another way to show that a day [d1] is ok is to
present evidence that it is the day before some other day [d2]
together with evidence that [d2] is ok." *)
(** 最初のコンストラクタは"[d]がOKな日であることを示す一つ目の方法は、[d]が良い日であるという根拠を示すことである"と読めます。
二番目のは"[d1]がOKであることを示す別の方法は、その日が別の日 [d2] の前日であり、[d2]がOKであるという根拠を示すことである"と読めます。 *)
(* Now suppose that we want to prove that [wednesday] is ok.
There are two ways to do it. First, we have the primitive way,
where we simply write down an expression that has the right
type -- a big nested application of constructors: *)
(** ここで [wednesday] がOKであることを証明したいとしましょう。
証明するには2つの方法があります
1つめは原始的な方法であり、コンストラクタの適用を何度もネストすることで、
正しい型を持つ式を書き下します。 *)
Definition okdw : ok_day wednesday :=
okd_before wednesday thursday
(okd_before thursday friday
(okd_before friday saturday
(okd_gd saturday gd_sat)
db_sat)
db_fri)
db_thu.
(* Second, we have the machine-assisted way, where we go into [Proof]
mode and Coq guides us through a series of goals and subgoals
until it is finally satisfied: *)
(** 2つめの方法は、機械に支援してもらう方法です。証明モードに入り、最終的に満たされるまでゴールやサブゴールを通してCoqに案内してもらいます。 *)
Theorem okdw' : ok_day wednesday.
Proof.
(* wednesday is OK because it's the day before an OK day *)
apply okd_before with (d2:=thursday).
(* "subgoal: show that thursday is ok". *)
(* thursday is OK because it's the day before an OK day *)
apply okd_before with (d2:=friday).
(* "subgoal: show that friday is ok". *)
(* friday is OK because it's the day before an OK day *)
apply okd_before with (d2:=saturday).
(* "subgoal: show that saturday is ok". *)
(* saturday is OK because it's good! *)
apply okd_gd. apply gd_sat.
(* "subgoal: show that the day before saturday is friday". *)
apply db_sat.
(* "subgoal: show that the day before friday is thursday". *)
apply db_fri.
(* "subgoal: show that the day before thursday is wednesday". *)
apply db_thu. Qed.
(* Fundamentally, though, these two ways of making proofs are the
same, in the sense that what Coq is actually doing when it's
following the commands in a [Proof] script is _literally_
attempting to construct an expression with the desired type. *)
(** しかし、根本的なところでこの2つの証明方法は同じです。
証明スクリプト内のコマンドを実行するときにCoqが実際にやっていることは、目的の型を持つ式を構築することと全く同じです。
*)
Print okdw'.
(* ===> okdw' = okd_before wednesday thursday
(okd_before thursday friday
(okd_before friday saturday
(okd_gd saturday gd_sat) db_sat)
db_fri)
db_thu
: ok_day wednesday *)
(* These expressions are often called _proof objects_. *)
(** この式は一般的に証明オブジェクト(Proof object)と呼ばれます。 *)
(* Proof objects are the bedrock of Coq. Tactic proofs are
essentially _programs_ that instruct Coq how to construct proof
objects for us instead of our writing them out explicitly. Here,
of course, the proof object is actually shorter than the tactic
proof. But the proof objects for more interesting proofs can
become quite large and complex -- building them by hand would be
painful. Moreover, we'll see later on in the course that Coq has
a number of automation tactics that can construct quite complex
proof objects without our needing to specify every step. *)
(** 証明オジェクトはCoqの根本を支えています。
タクティックによる証明は、自分で証明オブジェクトを書く代わりに、証明オブジェクトを構築する方法をCoqに指示する基本的なプログラムです。
もちろん、この例では証明オブジェクトはタクティックによる証明よりも短くなっています。
しかし、もっと興味深い証明では証明オブジェクトを手で構築することが苦痛に思えるほど大きく複雑になります。
この後の章では、各ステップを書くことなく複雑な証明オブジェクトを構築できる自動化されたタクティックをたくさん紹介します。 *)
(* ##################################################### *)
(* ** The Curry-Howard Correspondence *)
(** ** カリー・ハワード対応 *)
(* The analogy
<<
propositions ~ sets / types
proofs ~ data values
>>
is called the _Curry-Howard correspondence_ (or _Curry-Howard
isomorphism_). Many wonderful things follow from it. *)
(** この
<<
命題 ~ 集合 / 型
証明 ~ 元、要素 / データ値
>>
という類似性は、カリー・ハワード対応(もしくはカリー・ハワード同型, Curry-Howard correspondence, Curry-Howard isomorphism)と呼ばれます。
これにより多くのおもしろい性質が導けます。
*)
(* Just as a set can be empty, a singleton, finite, or infinite -- it
can have zero, one, or many inhabitants -- a proposition may be
inhabited by zero, one, many, or infinitely many proofs. Each
inhabitant of a proposition [P] is a different way of giving
evidence for [P]. If there are none, then [P] is not provable.
If there are many, then [P] has many different proofs. *)
(** 集合に空集合、単集合、有限集合、無限集合があり、それぞれが0個、1個、多数の元を持っているように、命題も0個、1個、多数、無限の証明を持ちえます。
命題 [P] の各要素は、それぞれ異なる [P] の根拠です。
もし要素がないならば、[P] は証明不能です。
もしたくさんの要素があるならば、[P] には多数の異なった証明があります。 *)
(* ##################################################### *)
(* ** Implication *)
(** ** 含意 *)
(* We've seen that the [->] operator (implication) builds bigger
propositions from smaller ones. What constitutes evidence for
propositions built in this way? Consider this statement: *)
(** これまで [->] 演算子(含意)を小さい命題から大きな命題を作るために使ってきました。
このような命題に対する根拠はどのようになるでしょうか?
次の文を考えてみてください。 *)
Definition okd_before2 := forall d1 d2 d3,
ok_day d3 ->
day_before d2 d1 ->
day_before d3 d2 ->
ok_day d1.
(* In English: if we have three days, [d1] which is before [d2]
which is before [d3], and if we know [d3] is ok, then so is
[d1].
It should be easy to see how we'd construct a tactic proof of
[okd_before2]... *)
(** これを日本語で書くと、もし3つの日があるとして、[d1] が [d2] の前日であり、[d2] が [d3] の前日であり、かつ [d3] がOKであるということがわかっているならば、[d1] もOKである、という意味になります。
[okd_before2] をタクティッックを使って証明するのは簡単なはずです... *)
(* **** Exercise: 1 star, optional (okd_before2_valid) *)
(** **** 練習問題: ★, optional (okd_before2_valid) *)
Theorem okd_before2_valid : okd_before2.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(* But what should the corresponding proof object look like?
Answer: We've made a notational pun between [->] as implication
and [->] as the type of functions. If we take this pun seriously,
then what we're looking for is an expression with _type_ [forall
d1 d2 d3, ok_day d3 -> day_before d2 d1 -> day_before d3 d2 ->
ok_day d1], and so what we want is a _function_ that takes six
arguments (three days and three pieces of evidence) and returns a
piece of evidence! Here it is: *)
(** ところで、これに対応する証明オブジェクトはどんな感じでしょうか?
答: 含意としての [->] と、関数の型の [->] の記法はそっくりです。
これをそのまま解釈すると、[forall d1 d2 d3, ok_day d3 -> day_before d2 d1 -> day_before d3 d2 -> ok_day d1] という型をもった式を見付ける必要があります。
なので探すものは6個の引数(3個の日と、3個の根拠)を受け取り、1個の根拠を返す関数です!
それはこんな感じです。
*)
Definition okd_before2_valid' : okd_before2 :=
fun (d1 d2 d3 : day) =>
fun (H : ok_day d3) =>
fun (H0 : day_before d2 d1) =>
fun (H1 : day_before d3 d2) =>
okd_before d1 d2 (okd_before d2 d3 H H1) H0.
(* **** Exercise: 1 star, optional (okd_before2_valid_defn) *)
(** **** 練習問題: ★, optional (okd_before2_valid_defn) *)
(* Predict what Coq will print in response to this: *)
(** 下記の結果としてCoqが出力するものを予測しなさい。 *)
Print okd_before2_valid.
(* ##################################################### *)
(* ** Induction Principles for Inductively Defined Types *)
(** ** 帰納的に定義された型に対する帰納法の原理 *)
(* Every time we declare a new [Inductive] datatype, Coq
automatically generates an axiom that embodies an _induction
principle_ for this type.
The induction principle for a type [t] is called [t_ind]. Here is
the one for natural numbers: *)
(** [Inductive] でデータ型を新たに定義するたびに、Coqは帰納法の原理に対応する公理を自動生成します。
型[t]に対応する帰納法の原理は[t_ind]という名前になります。
ここでは自然数に対するものを示します。 *)
Check nat_ind.
(* ===> nat_ind : forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n *)
(* Note that this is exactly the [our_nat_induction] property from
above. *)
(** これは先ほど定義した [our_nat_induction] の性質とまったく同じであることに注意してください。 *)
(* The [induction] tactic is a straightforward wrapper that, at
its core, simply performs [apply t_ind]. To see this more
clearly, let's experiment a little with using [apply nat_ind]
directly, instead of the [induction] tactic, to carry out some
proofs. Here, for example, is an alternate proof of a theorem
that we saw in the [Basics] chapter. *)
(** [induction] タクティックは、基本的には [apply t_ind] の単純なラッパーです。
もっとわかりやすくするために、[induction] タクティックのかわりに [apply nat_ind] を使っていくつかの証明をしてみる実験をしてみましょう。
例えば、[Basics_J] の章で見た定理の別の証明を見てみましょう。 *)
Theorem mult_0_r' : forall n:nat,
n * 0 = 0.
Proof.
apply nat_ind.
Case "O". reflexivity.
Case "S". simpl. intros n IHn. rewrite -> IHn.
reflexivity. Qed.
(* This proof is basically the same as the earlier one, but a
few minor differences are worth noting. First, in the induction
step of the proof (the ["S"] case), we have to do a little
bookkeeping manually (the [intros]) that [induction] does
automatically.
Second, we do not introduce [n] into the context before applying
[nat_ind] -- the conclusion of [nat_ind] is a quantified formula,
and [apply] needs this conclusion to exactly match the shape of
the goal state, including the quantifier. The [induction] tactic
works either with a variable in the context or a quantified
variable in the goal.
Third, the [apply] tactic automatically chooses variable names for
us (in the second subgoal, here), whereas [induction] lets us
specify (with the [as...] clause) what names should be used. The
automatic choice is actually a little unfortunate, since it
re-uses the name [n] for a variable that is different from the [n]
in the original theorem. This is why the [Case] annotation is
just [S] -- if we tried to write it out in the more explicit form
that we've been using for most proofs, we'd have to write [n = S
n], which doesn't make a lot of sense! All of these conveniences
make [induction] nicer to use in practice than applying induction
principles like [nat_ind] directly. But it is important to
realize that, modulo this little bit of bookkeeping, applying
[nat_ind] is what we are really doing. *)
(** この証明は基本的には前述のものと同じですが、細かい点で特筆すべき違いがあります。
1つめは、帰納段階の証明(["S"] の場合)において、[induction] が自動でやってくれること([intros])を手作業で行なう必要があることです。
2つめは、[nat_ind] を適用する前にコンテキストに [n] を導入していないことです。
[nat_ind] の結論は限量子を含む式であり、[apply] で使うためにはこの結論と限量子を含んだゴールの形とぴったりと一致する必要があります。
[induction] タクティックはコンテキストにある変数にもゴール内の量子化された変数のどちらにでも使えます。
3つめは、[apply] タクティックは変数名(この場合はサブゴール内で使われる変数名)を自動で選びますが、[induction] は([as ...] 節によって)使う名前を指定できることです。
実際には、この自動選択にはちょっと不都合な点があります。元の定理の [n] とは別の変数として [n] を再利用してしまいます。
これは [Case] 注釈がただの [S] だからです。
ほかの証明で使ってきたように省略しない形で書くと、これは [n = S n] という意味のなさない形になってしまいます。
このようなことがあるため、実際には [nat_ind] のような帰納法の原理を直接適用するよりも、素直に [induction] を使ったほうがよいでしょう。
しかし、ちょっとした例外を除けば実際にやりたいのは [nat_ind] の適用であるということを知っておくことは重要です。 *)
(* **** Exercise: 2 stars (plus_one_r') *)
(** **** 練習問題: ★★ (plus_one_r') *)
(* Complete this proof without using the [induction] tactic. *)
(** [induction] タクティックを使わずに、下記の証明を完成させなさい。 *)
Theorem plus_one_r' : forall n:nat,
n + 1 = S n.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(* The induction principles that Coq generates for other
datatypes defined with [Inductive] follow a similar pattern. If we
define a type [t] with constructors [c1] ... [cn], Coq generates a
theorem with this shape:
[[
t_ind :
forall P : t -> Prop,
... case for c1 ... ->
... case for c2 ... ->
... ->
... case for cn ... ->
forall n : t, P n
]]
The specific shape of each case depends on the arguments to the
corresponding constructor. Before trying to write down a general
rule, let's look at some more examples. First, an example where
the constructors take no arguments: *)
(** ほかの [Inductive] によって定義されたデータ型に対しても、Coqは似た形の帰納法の原理を生成します。
コンストラクタ [c1] ... [cn] を持った型 [t] を定義すると、Coqは次の形の定理を生成します。
[[
t_ind :
forall P : t -> Prop,
... c1の場合 ... ->
... c2の場合 ... ->
... ->
... cnの場合 ... ->
forall n : t, P n
]]
各場合分けの形は、対応するコンストラクタの引数の数によって決まります。
一般的な規則を紹介する前に、もっと例を見てみましょう。
最初は、コンストラクタが引数を取らない場合です。
*)
Inductive yesno : Type :=
| yes : yesno
| no : yesno.
Check yesno_ind.
(* ===> yesno_ind : forall P : yesno -> Prop,
P yes ->
P no ->
forall y : yesno, P y *)
(* **** Exercise: 1 star (rgb) *)
(** **** 練習問題: ★ (rgb) *)
(* Write out the induction principle that Coq will generate for
the following datatype. Write down your answer on paper, and
then compare it with what Coq prints. *)
(** 次のデータ型に対してCoqが生成する帰納法の原理を予測しなさい。
紙に答えを書いたのち、Coqの出力と比較しなさい。 *)
Inductive rgb : Type :=
| red : rgb
| green : rgb
| blue : rgb.
Check rgb_ind.
(** [] *)
(* Here's another example, this time with one of the constructors
taking some arguments. *)
(** 別の例を見てみましょう。引数を受け取るコンストラクタがある場合です。 *)
Inductive natlist : Type :=
| nnil : natlist
| ncons : nat -> natlist -> natlist.
Check natlist_ind.
(* ===> (modulo a little tidying)
natlist_ind :
forall P : natlist -> Prop,
P nnil ->
(forall (n : nat) (l : natlist), P l -> P (ncons n l)) ->
forall n : natlist, P n *)
(* **** Exercise: 1 star (natlist1) *)
(** **** 練習問題: ★ (natlist1) *)
(* Suppose we had written the above definition a little
differently: *)
(** 上記の定義をすこし変えたとしましょう。 *)
Inductive natlist1 : Type :=
| nnil1 : natlist1
| nsnoc1 : natlist1 -> nat -> natlist1.
(* Now what will the induction principle look like? *)
(** このとき、帰納法の原理はどのようになるでしょうか? *)
(** [] *)
(* From these examples, we can extract this general rule:
- The type declaration gives several constructors; each
corresponds to one clause of the induction principle.
- Each constructor [c] takes argument types [a1]...[an].
- Each [ai] can be either [t] (the datatype we are defining) or
some other type [s].
- The corresponding case of the induction principle
says (in English):
- "for all values [x1]...[xn] of types [a1]...[an], if
[P] holds for each of the [x]s of type [t], then [P]
holds for [c x1 ... xn]". *)
(** これらの例より、一般的な規則を導くことができます。
- 型宣言は複数のコンストラクタを持ち、各コンストラクタが帰納法の原理の各節に対応する。
- 各コンストラクタ [c] は引数 [a1]..[an] を取る。
- [ai] は [t](定義しようとしているデータ型)、もしくは別の型 [s] かのどちらかである。
- 帰納法の原理において各節は以下のことを述べている。
- "型 [a1]...[an] のすべての値 [x1]...[xn] について、各 [x] について [P] が成り立つならば、[c x1 ... xn] についても [P] が成り立つ"
*)
(* **** Exercise: 1 star (ExSet) *)
(** **** 練習問題: ★ (ExSet) *)
(* Here is an induction principle for an inductively defined
set.
[[
ExSet_ind :
forall P : ExSet -> Prop,
(forall b : bool, P (con1 b)) ->
(forall (n : nat) (e : ExSet), P e -> P (con2 n e)) ->
forall e : ExSet, P e
]]
Give an [Inductive] definition of [ExSet]: *)
(** 帰納的に定義された集合に対する帰納法の原理が次のようなものだとします。
[[
ExSet_ind :
forall P : ExSet -> Prop,
(forall b : bool, P (con1 b)) ->
(forall (n : nat) (e : ExSet), P e -> P (con2 n e)) ->
forall e : ExSet, P e
]]
[ExSet] の帰納的な定義を示しなさい。 *)
Inductive ExSet : Type :=
(* FILL IN HERE *)
.
(** [] *)
(* What about polymorphic datatypes?
The inductive definition of polymorphic lists
[[
Inductive list (X:Type) : Type :=
| nil : list X
| cons : X -> list X -> list X.
]]
is very similar to that of [natlist]. The main difference is
that, here, the whole definition is _parameterized_ on a set [X]:
that is, we are defining a _family_ of inductive types [list X],
one for each [X]. (Note that, wherever [list] appears in the body
of the declaration, it is always applied to the parameter [X].)
The induction principle is likewise parameterized on [X]:
[[
list_ind :
forall (X : Type) (P : list X -> Prop),
P [] ->
(forall (x : X) (l : list X), P l -> P (x :: l)) ->
forall l : list X, P l
]]
Note the wording here (and, accordingly, the form of [list_ind]):
The _whole_ induction principle is parameterized on [X]. That is,
[list_ind] can be thought of as a polymorphic function that, when
applied to a type [X], gives us back an induction principle
specialized to the type [list X]. *)
(** 多相的なデータ型ではどのようになるでしょうか?
多相的なリストの帰納的定義は [natlist] によく似ています。
[[
Inductive list (X:Type) : Type :=
| nil : list X
| cons : X -> list X -> list X.
]]
ここでの主な違いは、定義全体が集合 [X] によってパラメータ化されていることです。
つまり、それぞれの [X] ごとに帰納型 [list X] を定義していることになります。
(定義本体で [list] が登場するときは、常にパラメータ [X] に適用されていることに
注意してください。)
帰納法の原理も同様に [X] によってパラメータ化されます。
[[
list_ind :
forall (X : Type) (P : list X -> Prop),
P [] ->
(forall (x : X) (l : list X), P l -> P (x :: l)) ->
forall l : list X, P l
]]
この表現(と [list_ind] の全体的な形)に注目してください。帰納法の原理全体が
[X] によってパラメータ化されています。
別の見方をすると、[list_ind] は多相関数と考えることができます。この関数は、型
[X] が適用されると、[list X] に特化した帰納法の原理を返します。 *)
(* **** Exercise: 1 star (tree) *)
(** **** 練習問題: ★ (tree) *)
(* Write out the induction principle that Coq will generate for
the following datatype. Compare your answer with what Coq
prints. *)
(** 次のデータ型に対してCoqが生成する帰納法の原理を予測しなさい。
答えが書けたら、それをCoqの出力と比較しなさい。 *)
Inductive tree (X:Type) : Type :=
| leaf : X -> tree X
| node : tree X -> tree X -> tree X.
Check tree_ind.
(** [] *)
(* **** Exercise: 1 star (mytype) *)
(** **** 練習問題: ★ (mytype) *)
(* Find an inductive definition that gives rise to the
following induction principle:
[[
mytype_ind :
forall (X : Type) (P : mytype X -> Prop),
(forall x : X, P (constr1 X x)) ->
(forall n : nat, P (constr2 X n)) ->
(forall m : mytype X, P m ->
forall n : nat, P (constr3 X m n)) ->
forall m : mytype X, P m
]]
*)
(** 以下の帰納法の原理を生成する帰納的定義を探しなさい。
[[
mytype_ind :
forall (X : Type) (P : mytype X -> Prop),
(forall x : X, P (constr1 X x)) ->
(forall n : nat, P (constr2 X n)) ->
(forall m : mytype X, P m ->
forall n : nat, P (constr3 X m n)) ->
forall m : mytype X, P m
]]
*)
(** [] *)
(* **** Exercise: 1 star, optional (foo) *)
(** **** 練習問題: ★, optional (foo) *)
(* Find an inductive definition that gives rise to the
following induction principle:
[[
foo_ind :
forall (X Y : Type) (P : foo X Y -> Prop),
(forall x : X, P (bar X Y x)) ->
(forall y : Y, P (baz X Y y)) ->
(forall f1 : nat -> foo X Y,
(forall n : nat, P (f1 n)) -> P (quux X Y f1)) ->
forall f2 : foo X Y, P f2
]]
*)
(** 以下の帰納法の原理を生成する帰納的定義を探しなさい。
[[
foo_ind :
forall (X Y : Type) (P : foo X Y -> Prop),
(forall x : X, P (bar X Y x)) ->
(forall y : Y, P (baz X Y y)) ->
(forall f1 : nat -> foo X Y,
(forall n : nat, P (f1 n)) -> P (quux X Y f1)) ->
forall f2 : foo X Y, P f2
]]
*)
(** [] *)
(* **** Exercise: 1 star, optional (foo') *)
(** **** 練習問題: ★, optional (foo') *)
(* Consider the following inductive definition: *)
(** 次のような帰納的定義があるとします。 *)
Inductive foo' (X:Type) : Type :=
| C1 : list X -> foo' X -> foo' X
| C2 : foo' X.
(* What induction principle will Coq generate for [foo']? Fill
in the blanks, then check your answer with Coq.)
[[
foo'_ind :
forall (X : Type) (P : foo' X -> Prop),
(forall (l : list X) (f : foo' X),
_______________________ ->
_______________________ ) ->
___________________________________________ ->
forall f : foo' X, ________________________
]]
*)
(** [foo'] に対してCoqはどのような帰納法の原理を生成するでしょうか?
空欄を埋め、Coqの結果と比較しなさい
[[
foo'_ind :
forall (X : Type) (P : foo' X -> Prop),
(forall (l : list X) (f : foo' X),
_______________________ ->
_______________________ ) ->
___________________________________________ ->
forall f : foo' X, ________________________
]]
*)
(** [] *)
(* ##################################################### *)
(* ** Induction Hypotheses *)
(** ** 帰納法の仮定 *)
(* Where does the phrase "induction hypothesis" fit into this
picture?
The induction principle for numbers
[[
forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n
]]
is a generic statement that holds for all propositions
[P] (strictly speaking, for all families of propositions [P]