全ての質問用紙に目を通しましたが，後で回答する方が適切と考えた質問はここでは答えていません．そのうち答えます．また講義中に説明したと考えている質問についても回答していません．回答に納得できない場合は，またしてください．また，似た質問はひとつにまとめたり，質問の文章は適宜変更しています．

Induction.v についての QA (10/21提出分)

帰納法の証明の中で帰納法の証明を試みるとうまくいかない．
これは，帰納法の仮定を使う方の場合の証明中に，再び帰納法を使うと起こります．具体的な例は出しにくいですが，大抵以下のような状況だと思います．
```
 m : nat
  ...
 IHn' : ... m に言及した帰納法の仮定 ... (Q(m) と呼ぶ)
  ...
 ======================================
 ゴール命題 G(m)
```
さて，講義でも説明したように，数学的帰納法は本来「任意の m について P(m)」を証明するための方法です．この「任意の m について」の部分は文脈にある m : nat が相当しています．しかし，上の状況は，実は，「任意の m について G(m)」ではなく，「任意の m について，Q(m) ならば G(m)」というもう少し弱い命題を証明しようとすることに相当しています．ですので，ここで induction m をしても，Coq は「Q(m) ならば G(m)」を「P(m)」と考えて新しいゴールを準備してしまい，その結果うまく証明できない，ということになりがちです．これを回避するためには IHn' を文脈から消してから induction m をする，という手もあるのですが，たいていの場合は，一旦この定理から上に戻って，「任意の m について G(m)」という新たな補題を立てる方がうまくいくと思います．

第一回目の予習での QA (10/14提出分, Preface.v, Basics.vについて)

Mac に Coq をインストールしようと思い INRIA から coqide-8.4pl4.dmg をダウンロード・マウントして，起動してみましたが，「…は壊れているため開けません．ディスクイメージを取り出す必要があります」などと言われてしまいます．どうしたらよいでしょう．
Mac OS のセキュリティ設定の問題で，ダウンロードしたファイルを実行しようとした時に表示されるようです．「システム環境設定」の「セキュリティとプライバシー」を起動し，「一般」タブのところにある［ダウンロードしたアプリケーションの実行許可］欄で［すべてのアプリケーションを許可］を選択してから実行してみてください．
ProofGeneral や CoqIDE でファイルの最後までエラーを出すことなく読み込めることを確認したのに，提出システムでは再提出となります．
多くの場合，Qed. で終えないままの証明があるのが原因です． No more subgoals. までこぎつけても，Qed. をしない限り，証明は完了とみなされません．ProofGeneral の場合 C-c C-p で現在のゴールを表示しますが，ファイルの最後でこれを実行し，
```
Error: No focused proof (No proof-editing in progress).
```
のようにエラーになること(証明中ではないこと)を確認してください．その他の原因として，
- 提出した zip ファイルに _MACOSX という名前のディレクトリがある．(.v ファイルの抽出に失敗することがあります．)
- ファイル名が違う
というのが観察されています．
nat_scope の意味がよくわからない．
Notation は(記号の読み替えをする)マクロ定義みたいなものなのですが，同じ名前でも書く場所によってどう展開するかが変わる場合があります．この場所を示すのが～scope です．nat_scope は自然数を書くことが期待されるところで，type_scope は型が期待されるところで有効になる，くらいの意味です．
自然数定義がこれで十分である理由が分からない．予め定義されている nat は O (オー) は 0 (ゼロ)，S O は 1，S (S O) は 2 というように対応づけられている．これをどのように表現するのか？
自然数の定義の仕方の意味がよくわかりません．O を自然数として， S は自然数を受け取り自然数を返す型．足し算自体は後の方でこれを使って定義しているのに，なぜ自然数を帰納的に定義できているのかあまりよくわかりません．足し算以外の方法で自然数を帰納的に定義しているのでしょうか．
自然数 nat が O : nat, S : nat → nat だけで定義できているのかが直観的に理解できなかった．(予想回答: 自然数のこの定義に対し，我々は O を 0 に，S n を n の次の数とするのが「自然だ」と考え，それをアラビア数字で符号化しているだけで，Coq はそれにもとづいた実装がされているだけ？)
S というのは標準で定義されている (S n) = n + 1 であっていますか？プログラムの中だと 4 という数字は S (S (S (S O))) という形で保持されているってこと？
整数型の定義の部分で O と S が具体的にどういった意味を持つのか理解しかねたが，おそらく，O が数字の 0, S が +1 を表すようなものだとして， O の S を何度も適用することで無限の自然数を表していると予想してみると後の話の流れがうまくいくような気がした．
なぜ pred のこの定義で，1つ前の自然数が返ってくるのか？ (ここでいっている1つ前の自然数というのは単に先の nat の定義における S n の n の部分をいっているだけであるのだろうか．)
S n が n + 1 である定義はどこから来たのかわからなかった．
自然数の定義については，上のようにいくつも質問をもらいました．10/14 の講義でも少し話したつもりですが，10/21 の講義の冒頭でもう少し詳しく話をしたいと思います．
nat 型の定義ができるなら 0 から n までの和は以下のようにできるのではないか．
```
Inductive sum (n : nat) : nat :=
  match n with
  | O => O
  | S p => n + sum p.
```
"Inductive" が "Fixpoint" になるべきなことを除けばその通りです．
"O"(オー)はゼロではなく自然数なのに，ゼロとして扱うのがよくわからない．
なぜ零も自然数なのか，という質問でしょうか．計算機科学分野ではゼロも自然数の仲間に入れることが多いようです．
複数のテストケースを一度に検証する文はある？
まず，そのような文を命題として表現する必要があるわけですが，それには「かつ」を使います．Coq では命題 A かつ B を A /\ B と表現します．例えば next_weekday monday = tuesday /\ next_weekday friday = monday といった具合です．「かつ」を使った命題の証明の仕方は後の章(Logic.v) で学びます．
destruct の as イントロパターンがあまりよくわからなかった．おそらく場合分けごとに今後証明で利用する変数の存在を仮定しているのだろう．
真か偽かが判定できる命題は，有限個の真偽値に基づいて判定できるが，一般の自然数について命題が真と判定できるか．
前者関数のところで出てきた n' という表記に戸惑いました．
n' は二文字でひとつの変数の名前です．Coq では，変数の名前にアルファベット・数字だけでなく下線(アンダースコア)，アポストロフィも使えます．
Coq で論証を解くにあたって，手で示せない問題を解くうまいコツはないのでしょうか？
Coq はあくまで証明を支援するためのツールで，人間の代わりに証明をしてくれるわけではありません(それなりに強力な自動証明機能はありますがメインではありません)．ですので，手で(頭で考えて) 示せない問題は解けない，と思ってもらって構いません．
dayの型定義を行った時に同時に、day_rect, day_ind, day_recが定義されるがこれはどういった定義なのか．
dayに関する公理です．(10/28の講義で少し説明したいと思います．)
Typeとは何か．
大雑把に言うと，「型の型」の一種です．
関数定義時に型を省略することができるが，どのように判断しているのか
「型推論」と呼ばれる，省略された方を推論する技術があります．詳しくはこちらを参照して下さい：http://www.fos.kuis.kyoto-u.ac.jp/~t-sekiym/classes/isle4/text.pdf
DefinitionとFixpointの違いがよく分からなかった．
再帰的関数の定義において，普通の関数と異なりDefinitionではなくFixpointを用いる理由．
FixpointとDefinitionについて．
Fixpointは再帰関数を定義するためのキーワード(予約語)ですが，再帰関数以外の普通の関数も定義することが出来ます．では，Definitionはいらないかというと，そのようなことはありません．例えば，Definition n : nat := 3.のような定義はFixpointでは書くことが出来ません．
simpl. (文字列的一致). とreflexivity. はどの程度の違いがある／ないのか．
simpl.は計算を進めてゴールを変形するだけで，等式が成り立つことを証明するために用いることは出来ません．一方，reflexivity.はゴールの等式の両辺を「出来る限り」計算した後に，その両辺が同一かどうかをチェックします．
admitという定義は不完全な部分をとりあえず無いということにするというものだそうですが，何を不完全として定義するかがよくわかりません．プログラミング言語として不適切ということですか．
無いことにするというよりは，"とりあえず定義が完成したと仮定"して以降の証明などを行うときに使います．ですので定義で導入された名前を参照することはできますが，その定義内容を使うことができません．
プログラムの正しさと数学の関係がいまいちわからないです．
予想されたとおり，この講義を通して分かります．
新しい型の定義でInductive関数を使っていますが，「帰納的」という単語が型の定義で使われているのはなぜでしょうか．
型は集合とみなすことができるため，集合と同様に型を帰納的に定義することが可能です．型を帰納的に定義するためのキーワード(予約語)がInductiveです．
列挙型で曜日の型 day を定義する場合、

Inductive day : Type :=
| monday : day
| …

のように書くが、1つめの day で型が day であると宣言しているのに、mondayに対してさらに型 day をもつことを明示することが必要なのか。mondayがday以外の型をもつことがあるのか。
この day の場合が冗長に見えるのは無理もありませんが， Inductive の役割はこういう，要素を列挙して型定義をするだけではなく，そういう場合はコンストラクタの型情報が必要となります．自然数(nat)の S のように，何かを受けとって nat になる場合もあるので少なくとも引数の有無，有る場合はその型を明示する必要はあります．また，コンストラクタ毎に返すものの型が異なる場合もある(しばらくはでてきませんが) ので，一般には全部書き下す必要があります．
intros タクティックが使える条件が理解できなかった。
ゴールが forall か -> の形の時だと思ってください．
（"bool -> bool -> bool"のような表現に関して）二引数関数より増えるとうまく表記できないと思った。
講義でもふれましたが，三引数であれば左に「引数の型 ->」を追加して，例えば bool -> bool -> bool -> bool となります．
前者関数のイメージがわかない。
与えられた自然数の前の(1少ない)数を返す，じゃだめですか？
MacでProofGeneralの起動がうまくいかなかった。
もう少し詳しく状況を教えてください．
Days of the Weak の中のコードで一つ目の要素の先頭から"|"（たぶん「または」の意）がついていて、これはなぜ一つ目からついているのか。要素が一つのときには必要なのか。
ひとつ目の "|" はなくても大丈夫ですが，定義を後でいじる時にどの行も統一したフォーマットで書いておいた方がよいことはあるでしょう． (順番をいじりたい，とか．)
Booleansの中で、"Proof. reflexivity. Qed."と"admit"はどう使い分けているのか。
admit は(証明ではなく)定義の中身を省略するためのおまじないです． Admitted. は証明をすっ飛ばすためのおまじないです．Proof... Qed. は証明です．
僕はふだんVimを使っているのですが、ProofGeneralみたいにEmacsでないと困ることって今後結構出てきますか？
vim ユーザではないのであんまりわかりませんが，外部ソフトウェア(この場合 Coq)とのインターフェースをとるのに Emacs は便利なので，Emacs ならサポートがあるという場面は多いと思います．
何がわからないのかわからない。
そうですか，それは辛いですね．もしかして「何がわからないかわからない」こと以外は全部わかっている可能性はありませんか？ :-)
教科書でなく、http://www.iij-ii.co.jp/lab/techdoc/coqt/を読みました。
いいサイトだと思います。特に証明駆動開発入門の章がおもしろかったように記憶しています。でも教科書も読んでくださいね。
再帰的関数定義 Fixpoint において S n と S n' の意味の差異・使い分けについてまだよく分からない。(n' の場合再帰的に呼び出される際に減少していく減少性が発生するのではないかと思っている）
すいません，質問の意味がよく読み取れませんでした．パターン (=> の左側) の変数名は，関数のパラメータと同じでどんな名前を選ぶかはさして重要ではありません．何を選んでも使うところと整合性が取れていればＯＫです．(外側の名前とかぶってしまうと外側は隠されてしまう，という点にさえ注意すれば．)
intros を用いて証明する際、書き換え rewrite -> の行っている処理が理解しづらい。（仮定の式をならばの後の式に適用してreflexivityを使えるようにするための操作に見える。）
はい，そうです．ゴールの両辺が実は等しいことを Coq に教えるためにやっています．