The Coq Proof Assistant A Tutorial (1) 宣言
The Coq Proof Assistant A Tutorial を参考にしつつ，Coq について勉強していこうと思っています．
まずは，Windows を使っている人は，ここから， coq-8.0pl3-win.exeをダウンロードして，ダブルクリックして Coq (IDE 付き) をインストールしておいてください．
Coq は Calculuc of Inductive Constructions という論理体系に基づいた，定理証明支援系なのだそうです．
対話的に形式的な証明を構成していくことができて，さらにそれを，そのまま関数型プログラムの仕様として扱うことができるとのこと．
このチュートリアルでは Gallina と呼ばれる基本的な言語仕様だけを扱うそうで，発展的な情報は Coq Reference Manual とか Coq'Art を参照せよ，とのこと．
とりあえず，C:\Program Files\Coq 内にあるアイコンを，デスクトップにおいて置きましょう．IDE はまだよくわかんないので，とりあえず coq と書かれたニワトリをダブルクリックしてみてください．
と表示されたコンソール (DOS 窓) が開くはずです．
終了する時は，
でバッチシです．意外とインタプリタの終了って，exit だったり quit だったりで迷いますよね．Coq のコマンドは，基本的にみんな大文字で始まるみたいです．
Gallina では，宣言 (declarations) と定義 (definitions) の 2 つをメインに行っていくことになります．今回は，宣言を中心に見ていきましょう．
宣言は，名前と仕様を結び付けます．名前というのは，プログラミング言語における識別子のようなもので，文字で始まる文字や数字の列 ( _ (underscore) や ' (prime) のような一部の ASCII シンボルも使用することができます) です．
大文字と小文字は区別され，一部の文字列は，キーワードとして Coq に予約されているため，使用することができません．
仕様とは，概念を分類するための，形式的な表現のことで，論理命題 (logical propositions) ･数学的概念 (mathematical collections) ･抽象型 (abstract types) の 3 種類があります．
それぞれはシステムにおける基本的なソート Prop，Set，Type として扱われ，それら自体もアトミックで抽象的な型です．
Gallina において正しいとされる式は，全て type τ(E) と呼ばれる仕様と関連付けられています．e :τ(E) とは，e は型 E である，ということです．
型をチェックするためには，Check コマンドを使います．ためにしに，O ※ の型を調べて見ましょう．
O 識別子の型は，nat (自然数) ということがわかります．
※ アルファベットのオーです．数字の 0 は，なぜかここでは使用しません．多分，数を数と意識せず，「形式的」な側面を強調したいためでしょう．なぜか，O は最初から nat 型として定義されており，0 でも O でも，どっちを使っても，結果は同じです．
では，nat の型は何でしょう ?
Set は，Gallina 言語の基本ソート，つまり単なるラベルです．何の意味も無い，形式的な抽象型です．
おっと，ここまでチュートリアルを読んできて，いまさら気が付きました．O (オー) も nat も，算術プレリュードであらかじめ定義されているらしいです．プレリュードは，Coq が起動すると自動的に読み込まれます．
ところで，形式的体系においては，何らかの無条件で受け入れる前提 (hypothese : 仮説) や定義が無ければ，何も始まりません．
しかし，仮説と証明をごちゃ混ぜにするのはご法度です．ちゃんと明確に区別しないと混乱を招く恐れがあります．
# ここらへんの話は，ゲーデル･エッシャー･バッハが詳しいです．仮説を押し込んだら，もとの世界に戻ってくるまえに，ちゃんと後始末をしてから戻ってこないと駄目なのです :-)
形式的体系では，定義されていないものは一切導入してはいけません．現実世界とは異なり，定義されていないものは存在しないのです．暗黙の了解，あうんの呼吸は，現実世界では重要ですが，ここでは忘れてください．
# 今はとりあえず，算術の数学的概念 (mathematical collections) は最初から与えられているものとしますが，これはちゃんと定義しなおすこともできます．ここら辺は次回に詳しく見ていきませう．
というわけで，新しい概念を現在の環境に導入する場合は，Section コマンドを使用してスコープを切り替えましょう．
これで，宣言のスコープに切り替わりました．試しに「n を自然数とする (let n be a natural number)」という宣言を行って見ましょう．
これで，環境に型 nat を持つ変数 n が導入されました．同様に，前提を宣言することもできます．
# n を任意の (∀ ; forall) 自然数とする，のような，より詳細な宣言については，次回ということで．基本的に，チュートリアルを読みながら書いているので，どんどん言っていることが変わっていくかもしれません．あまり書いてあることを信用しないでください （；^ω^）
「n を正の (0 よりも大きい) 自然数とする」のような，より厳密な前提を宣言してみましょう．
gt n 0 は，プレリュードで定義されている，(n > 0) を意味する論理命題 (真偽のいずれかの値を取る表現) です.
型を調べて見ると，
と表示されます．これは，gt という識別子は，nat を二つ引数に取って，論理命題を返す関数である，ということを意味しています．
ちなみに nat -> nat -> Prop は，nat -> (nat -> Prop) の省略形で，nat を受け取って，アロー関数構築子 (->) により，nat から Prop への関数 (関数型という型を持つ表現) を作って返す関数と見ることもできます．
関数型 nat -> Prop の型を調べて見ると
となります．nat -> nat -> Prop は，自然数の集合上の二項関係を意味します．
ここで，任意の式 f が，任意の集合 A から B への関数型とすると，型 E の式 e に対して f を適用することにより，型 B の (f e) という式を作ることができます．
このような，関数型の概念と記法を導入すると，カリー化という概念が，実に自然に表現できます．
gt は，nat 型の式を 2 つ引数に取る関数，とのことでした．多くの手続き型言語には，関数型や関数構築子のような概念が無いため，引数が足りないと，単にコンパイルエラーになるだけです．
しかし，関数型の文脈では，(gt n O) のような関数呼び出しは，実は単なる ((gt n) O) の省略形です．(gt n) は，これだけで，関数型 nat -> Prop という，正しい型を持つ式です．
ふぅ，横道にそれすぎて，疲れてきました．
非常に中途半端ですが，とりあえず，今日はこの辺で勘弁したるわ ! と吉本新喜劇ばりに強引に終わらせます．
まずは，Windows を使っている人は，ここから， coq-8.0pl3-win.exeをダウンロードして，ダブルクリックして Coq (IDE 付き) をインストールしておいてください．
Coq は Calculuc of Inductive Constructions という論理体系に基づいた，定理証明支援系なのだそうです．
対話的に形式的な証明を構成していくことができて，さらにそれを，そのまま関数型プログラムの仕様として扱うことができるとのこと．
このチュートリアルでは Gallina と呼ばれる基本的な言語仕様だけを扱うそうで，発展的な情報は Coq Reference Manual とか Coq'Art を参照せよ，とのこと．
とりあえず，C:\Program Files\Coq 内にあるアイコンを，デスクトップにおいて置きましょう．IDE はまだよくわかんないので，とりあえず coq と書かれたニワトリをダブルクリックしてみてください．
Welcome to Coq 8.0pl3 (Jan 2006)
Coq <
と表示されたコンソール (DOS 窓) が開くはずです．
終了する時は，
Coq < Quit.
でバッチシです．意外とインタプリタの終了って，exit だったり quit だったりで迷いますよね．Coq のコマンドは，基本的にみんな大文字で始まるみたいです．
Gallina では，宣言 (declarations) と定義 (definitions) の 2 つをメインに行っていくことになります．今回は，宣言を中心に見ていきましょう．
宣言は，名前と仕様を結び付けます．名前というのは，プログラミング言語における識別子のようなもので，文字で始まる文字や数字の列 ( _ (underscore) や ' (prime) のような一部の ASCII シンボルも使用することができます) です．
大文字と小文字は区別され，一部の文字列は，キーワードとして Coq に予約されているため，使用することができません．
仕様とは，概念を分類するための，形式的な表現のことで，論理命題 (logical propositions) ･数学的概念 (mathematical collections) ･抽象型 (abstract types) の 3 種類があります．
それぞれはシステムにおける基本的なソート Prop，Set，Type として扱われ，それら自体もアトミックで抽象的な型です．
Gallina において正しいとされる式は，全て type τ(E) と呼ばれる仕様と関連付けられています．e :τ(E) とは，e は型 E である，ということです．
型をチェックするためには，Check コマンドを使います．ためにしに，O ※ の型を調べて見ましょう．
Coq < Check O.
0
: nat
O 識別子の型は，nat (自然数) ということがわかります．
※ アルファベットのオーです．数字の 0 は，なぜかここでは使用しません．多分，数を数と意識せず，「形式的」な側面を強調したいためでしょう．なぜか，O は最初から nat 型として定義されており，0 でも O でも，どっちを使っても，結果は同じです．
では，nat の型は何でしょう ?
Coq < Check nat.
nat
: Set
Set は，Gallina 言語の基本ソート，つまり単なるラベルです．何の意味も無い，形式的な抽象型です．
おっと，ここまでチュートリアルを読んできて，いまさら気が付きました．O (オー) も nat も，算術プレリュードであらかじめ定義されているらしいです．プレリュードは，Coq が起動すると自動的に読み込まれます．
ところで，形式的体系においては，何らかの無条件で受け入れる前提 (hypothese : 仮説) や定義が無ければ，何も始まりません．
しかし，仮説と証明をごちゃ混ぜにするのはご法度です．ちゃんと明確に区別しないと混乱を招く恐れがあります．
# ここらへんの話は，ゲーデル･エッシャー･バッハが詳しいです．仮説を押し込んだら，もとの世界に戻ってくるまえに，ちゃんと後始末をしてから戻ってこないと駄目なのです :-)
形式的体系では，定義されていないものは一切導入してはいけません．現実世界とは異なり，定義されていないものは存在しないのです．暗黙の了解，あうんの呼吸は，現実世界では重要ですが，ここでは忘れてください．
# 今はとりあえず，算術の数学的概念 (mathematical collections) は最初から与えられているものとしますが，これはちゃんと定義しなおすこともできます．ここら辺は次回に詳しく見ていきませう．
というわけで，新しい概念を現在の環境に導入する場合は，Section コマンドを使用してスコープを切り替えましょう．
Coq < Section Declaration.
これで，宣言のスコープに切り替わりました．試しに「n を自然数とする (let n be a natural number)」という宣言を行って見ましょう．
Coq < Variable n : nat.
n is assumed
これで，環境に型 nat を持つ変数 n が導入されました．同様に，前提を宣言することもできます．
# n を任意の (∀ ; forall) 自然数とする，のような，より詳細な宣言については，次回ということで．基本的に，チュートリアルを読みながら書いているので，どんどん言っていることが変わっていくかもしれません．あまり書いてあることを信用しないでください （；^ω^）
「n を正の (0 よりも大きい) 自然数とする」のような，より厳密な前提を宣言してみましょう．
Coq < Hypothesis Pos_n : (gt n 0).
Pos_n is assumed
gt n 0 は，プレリュードで定義されている，(n > 0) を意味する論理命題 (真偽のいずれかの値を取る表現) です.
型を調べて見ると，
Coq < Check gt.
gt
: nat -> nat -> Prop
と表示されます．これは，gt という識別子は，nat を二つ引数に取って，論理命題を返す関数である，ということを意味しています．
ちなみに nat -> nat -> Prop は，nat -> (nat -> Prop) の省略形で，nat を受け取って，アロー関数構築子 (->) により，nat から Prop への関数 (関数型という型を持つ表現) を作って返す関数と見ることもできます．
関数型 nat -> Prop の型を調べて見ると
Coq < Check (nat -> Prop).
nat -> Prop
: Type
となります．nat -> nat -> Prop は，自然数の集合上の二項関係を意味します．
ここで，任意の式 f が，任意の集合 A から B への関数型とすると，型 E の式 e に対して f を適用することにより，型 B の (f e) という式を作ることができます．
このような，関数型の概念と記法を導入すると，カリー化という概念が，実に自然に表現できます．
gt は，nat 型の式を 2 つ引数に取る関数，とのことでした．多くの手続き型言語には，関数型や関数構築子のような概念が無いため，引数が足りないと，単にコンパイルエラーになるだけです．
しかし，関数型の文脈では，(gt n O) のような関数呼び出しは，実は単なる ((gt n) O) の省略形です．(gt n) は，これだけで，関数型 nat -> Prop という，正しい型を持つ式です．
Coq < Check gt.
gt
: nat -> nat -> Prop
Coq < Check gt n.
gt n
: nat -> Prop
Coq < Check gt n O.
n > 0
: Prop
ふぅ，横道にそれすぎて，疲れてきました．
非常に中途半端ですが，とりあえず，今日はこの辺で勘弁したるわ ! と吉本新喜劇ばりに強引に終わらせます．
