全ての回答に目を通しましたが，後で回答する方が適切と考えた質問はここ
では答えていません．そのうち答えます．また講義中に説明したと考えている
質問についても回答していません．回答に納得できない場合は，またしてくだ
さい．また，似た質問はひとつにまとめたり，質問の文章は適宜変更していま
す．
全体的に nat の O と S を使った記法と，アラビア数字表記のつながりが魔法
のようで紛らわしかったようです．下の質問への回答にも書きましたが，実は
nat という名前の型はテキストの Module Playground ... End Playground の
間とライブラリで二度定義されています．後者についてのみシステムがアラビ
ア数字表記と対応が取れるように細工をしてくれていますが，前者については，
テキストで新たに定義したものなので，そういうサポートがありません．
(Module は定義が使える範囲を区切るための仕組み)ですので，例えば
- 参考書はないの？
- すみません，日本語で出版された本はありません．他に参考情報があれば適宜講義で紹介してきます．
- 証明の際，最初に「Proof.」と書かなくても証明を進めることができるが，書いたほうがよいか．
- 究極的には人間にとっての可読性の問題なので，演習の採点，という観点からは書かなくてもよいですが，「良いプログラミングスタイル」としては書くことを薦めます
- match 式で
match n, m with
| _, O => 式1
| O, _ => 式2
...
end
のようにパターン間で当てはまる条件に重複がある場合，上から順番に処理されていく，という認識で正しいでしょうか？また，条件が被る状況は避けた方がよいか？
- 上から順番に条件にあてはまるか試していきます．ですので，n=0, m=0 の場合は式1がmatch全体の値になります．また，自分がきっちりわかっていれば条件が被る状況があっても構わないと思います．被らないように書きにくい場合もあるので．
- O, S O, S (S O), …について，それぞれが表す自然数が異なることは自明ですか．
- (実は)よい質問です．自明，というより「定義により異なる(Coq はそういう風にできている)ことになっている」というところでしょうか．
- nat の S や O が特に何も定義していないのに，0, や +1 したものとして扱われるのがなぜかわからなかった．もとからそのように定義されているのか Coq が nat の定義からそのように読みとって理解したのだろうか．
- アラビア数字表記(例えば 5) が S(S(S(S(S(O))))) になってく
れるのは Coq でそのように定義されているから，です．ただし，nat の型定義
をした時点で，O をゼロ，S を「次の数」だと思おう，というのはある意味で
は我々の勝手に押しつけた見方です．O をゼロ，S を「次の次の数」と思えば，
偶数を定義したと考えることもできます(ただし，奇数がないので，これが偶数だと
思ってもあんまり面白い結論がでてこないですけど :-)
- evenb の定義などで出てくる n' は何を表しているのですか？
- まず，パターンで出てくる n' などは，何かを指すために使う
名前(これを我々は変数と読んでいます)です．その意味では，関数の仮引数と
同じような役割(後で与えられる実引数を指すという意味で)を果たします．
evenb の定義における n' は S(S n') というパターンで出てきますが，これは
「(match の対象であるところの) n が S (S ...) という形をしていた時の
... 部分」を表しています．
ちなみに n' は，これ以上分解できないひとつの名前です．Coq では変数名として，
「一文字目がアルファベット(大文字・小文字含む)かアンダースコア，
二文字目以降としては加えて数字とプライムからなる文字列」が使えるようです．
詳しくは Reference Manual 1.1 Lexical conventions を見てください．
仮名を含む(!)一部の unicode 文字も使えるようですね．
- Module Playground1 ... End Playground1 で囲むと
この中で定義した関数(例えば foo) を，この外では Playground1.foo という形で
呼べる，ということですか？
- はい．その通りです．よくわかりましたね :-)
- minus の定義で n - m が n < m の時 0 になることの説明が予めないのはなぜか．
- 著者に聞いてみないと本当のところはわかりません(笑)が，業界(…って何だ…)では，よくやる定義なので，親切に説明するのを忘れてしまったのでしょう．確かに初学者には不親切ですね．(著者に伝えておきます．)
- nat_scope, type_scope の意味がよくわからない．
- Notation は(記号の読み替えをする)マクロ定義みたいなものな
のですが，同じ名前でも書く場所によってどう展開するかが変わる場合があり
ます．この場所を示すのが〜scope です．nat_scope は自然数を書くことが期
待されるところで，type_scope は型が期待されるところで有効になる，くらいの意味です．
- beq_nat 関数は n = m のときだけ真となる関数という解釈でよい？
- はい．定義のちょっと上に "The beq_nat function tests natural numbers for equality" と書いてある通りです．
- test_next_weekday を証明しただけで，なぜすべての曜日の次の次の平日の曜日を出す証明になるのか．
- いえ，なりません．例の名前から一般的な性質を何か証明した
と思ってしまったかもしれませんが，これはあくまで saturdayの次の次が
tuesday になる，という一例を示しただけです．
- 序盤 nat 型の定義の辺りで，何故出力がしっかりと自然数として(五十嵐注…アラビア数字表記で？)出てくるのが謎でした．
- 実は nat という名前の型はテキストの Module Playground ... End Playground の間と，ライブラリで二度定義されています．後者についてはシステムがアラビア数字表記と対応が取れるように細工をしてくれていますが，前者についてはそのサポートがありません．ですので，例えば Check S(S(S(O))). をして，しっかり自然数として出てくるのは，
End Playground の外(つまりテキストの定義の有効範囲を出た後)に限られるはずです．試してみてください．
- S の中身を明示的に定義していないのに -1 (五十嵐注… +1のこと？)する関数として働くのはなぜか？
- 他の質問への回答でも書きましたが，O をゼロ，S を +1 のこ
と，と思っているのは，ある意味で我々の都合です．true と false を 1 と
0 で表す(ことにすると，いろいろ便利)というのと似ているかもしれません．
重要なのは，O と S を nat の定義の仕方で組み合わせると，「自然数と同型」
な集合が作れる(つまり，各要素を自然数と思い込んでも問題がない)，という
ことです．
- pred の定義で詰まってしまいました．S についての定義がないのに，minustwo が定義できているのは何故でしょう．(中略)予想として考えたのが，自然数に1を足したものは自然数という公理が知らないうちにどこかで定義されているか，もともとSに上記のような意味があったのではないか(…などなど)．
- その通り，型 nat の定義の(S の部分)がまさに「自然数に 1
を足したものは自然数」という公理を示しています!
- nand の定義で二段階で場合分けを行ったが他に方法はないか？
- minus の定義でやったように b1 と b2 の両方についていっぺんに場合分けを行ってもよいです．
match b1, b2 with
| true, true => ...
| true, false => ...
| false, true => ...
| false, false => ...
end
- 関数の仮引数の宣言で (n:nat) (m:nat) と (n m:nat) は違うのか？(同じ，と予想)
- 正解! 同じです．
- Definition 中に関数をいくつか作って相互再帰のような形にできないのか．
- できます．例えば自然数の偶奇を判定する関数 evenb, oddb を相互再帰的に同時に定義するには
Fixpoint evenb (n : nat) : bool :=
match n with O => true | S n' => oddb n' end
with oddb (n : nat) : bool :=
match n with O => false | S n' => evenb n' end.
といった形で定義を with でつなぎます．
- proof は自分で打つのか，それとも自動生成されるのか．
- short answer は「自分で打つ」です．Coq には自動証明機能も
それなりに強力なものが備わっていて，教科書で扱う問題のかなりの部分は自
動で証明してくれます．ただし，それだと何も身につかないので，みなさんに
は手打ちをしてもらいます．
後になると proof にも二種類 proof script と proof object というのがある，
という話が出てきて，この話題と関係するのですが，そのうち説明します．お楽しみに :-)
- 場合分けを2回繰り返すことは可能ですか？(andb3を定義するときに andb などを使わずに定義できますか？)
- はい，できます．beq_nat の定義などがその例です．
- Eval simpl と Eval compute の違いはなんですか？
- ふたつは「どれくらい計算をしてくれるか」の度合が違います．
特に，式に変数が含まれていたりするために計算が中途半端に終わらざるを得
ない場合(例えば plus n 0 の計算)に違いが現れます．正確に違いを述べるた
めにはかなり準備が必要なので省略しますが，compute の方が計算を積極的に
進めてくれる一方，関数定義なども積極的に展開してしまうので，結果が巨大
になってかえってわかりずらくなってしまうことがあります．例えば，
Eval simpl in forall n: nat, plus n 0 = n.
Eval compute in forall n: nat, plus n 0 = n.
を試してみると，違いがわかります．また，simpl は Definition で定義され
た関数の計算をすすめてくれない，という特徴もあります．
- 複数の変数に対し場合分けによる証明が必要な場合に
destruct の記述はどうなるのでしょう．例えば自然数 m, n, のそれぞれに対し
0 かそれ以外であるかという場合わけが必要な場合に
...
destruct m as [| m']. destruct n as [| n'].
reflexivity. (* m=0, n=0 の場合 *)
reflexivity. (* m=0, n=S n' の場合 *)
reflexivity. (* m=S m', n=0 の場合 *)
reflexivity. (* m=S m', n=S n' の場合 *)
...
のような記述になるのでしょうか．reflexivity を4回も記述することになるが回避する
手段はありますか？
- 前半については基本的には yes です．match を入れ子にせず
同時にふたつ以上のものについて場合わけができたのと同様，m, n を同時に
場合わけすることもできますが，4通りのサブゴールができることはかわりありません．
後半の質問については，上のように場合分けのどの場合も同じように証明でき
る場合であれば，4回書かずに済ます方法はあります．しかし，この講義の中で
は，「場合わけをしっかり意識して，後で人が読んでも構造がわかる証明を書
く」ことを，身につけてもらいたいので，特に紹介しない予定です．(自分で調べて，
使い方がわかった上で演習の解答で使ってもらう分には構いません．)
- blt_nat の演習問題で，定義を与えて
Example test_blt_nat1: (blt_nat 2 2) = false.
Proof. simpl.
とやった時点では左辺が全く計算されず．simpl. の代わりに compute. とやる
必要があった．(ただし，simpl. の後に構わず reflexivity. をすれば証明は
完了した．)
- おそらく blt_nat を Definition を使って定義したのだと
思います．
別の質問への回答にも書いたように，simpl は Definition で定義された関数
の計算をしてくれません．ですので，blt_nat を Definition で定義する限り，
"a simple, elegant solution for which simpl suffices" なる解答がないよ
うですので，教科書の Note 以下の注は無視してください．(著者に代わってご
めんなさいです．)
次に reflexivity の機能ですが，これは資料にも書いたように「両辺は等しい
はずだ! 計算してみろ!」と Coq に命令するタクティックです．この時の「計
算」にはsimpl ではなく compute を使っていると思って(ほぼ)構いません．
実は，この章に出てくる多くの証明で reflexivity. の前に simpl. をやって
いるのは，人間がゴールの変化(両辺の simpl による計算結果)を確認するため
のもので，Coq にとっては必要のないものです．面倒くさくなってきたら，
省略してもらって構いません．