Ｔｈｅ Ｃｏｑ Ｐｒｏｏｆ Ａｓｓｉｓｔａｎｔ Ａ Ｔｕｔｏｒｉａｌ (2) 定義
前回の続きです．
今回は，定義についてです．
coq-interface の初期化の際に読みこまれるプレリュードは，いくつか数学的定義を含んでいます．
例えば，前回扱った nat は，数学的概念 (mathematical collection) (Set 型) として定義されています．また，定数 O (オー) や S，plus なども，それぞれ nat，nat -> nat，nat -> nat -> nat という型のオブジェクトとして定義が用意されています．
では，O と S を用いて，自然数を定義してみましょう．ここでは，一番最初の自然数 O と，次の自然数を求める関数 S の存在を前堤とします．
1 は，どのように定義すれば良いでしょう ? そうです，1 は O の次の数ですね．
1 が定義されたら，それを使って 2 を定義することができます．1 の時は型は省略しましたが，もちろん型を明示しても OK です．ちなみに，一度した宣言を取り消すには，Reset を使います．
plus を使用して，与えられた数を 2 倍する double を定義してみましょう．
与えられた引数だけではなく，自由変数 (グローバル変数) にアクセスするような関数を定義することもできます．
変数は，量化限定することができます．
これにより，「全ての (全称 ; forall ; ∀) 〜 は P」「少なくとも一つ P であるような 〜 が存在する (存在 ; exists ; ∃)」のような状況を表現することができるようになります．これは，後々述語論理に入ると重要になってくる考え方です．
# ちなみに，量化は，今でこそ常識になっていますが，実はこれは長年多くの論理学者を悩ませ続けてきた超難問だったのです．
# 20 世紀に入って，ようやくフレーゲの量化理論によりこの難問がエレガントに解決された後，アリストテレス以来 2000 年もの間停滞していた論理学は劇的な発展を遂げ，やがて計算機の発明へとドラマティックにつながっていくことになります．
量化限定子を用いることにより，自然言語ではうまく表現できないような，より複雑な状況を，完全に明示的に厳密に記述できるようになります．
# 私は，未だに∃と∀が組合わさった論理式を見ると，どっちがどっちにかかっているのかとっさにわからず，混乱してしまいます (^^;
# またまた完全に余談ですけど，論理プログラミングでは，最初から論理式を計算機に処理させやすい形にエンコードしてから与えているので，量化記号などは出てこない場合が多いです．
# 例えば Prolog などでは，「節 (ホーン節)」という型式に変型された論理式を扱いますが，これは全ての変数が全称量化されているので，明示的には量化記号がでてきません．論理式から存在量化を取り除いて，全ての量化記号が頭のところにきた冠頭連言標準型に変換するためには，スコーレム化とか，いろいろややこしいアルゴリズムを用いた後，ド・モルガン則などを駆使する必要があって，なかなか大変．
次回からは，いよいよ Coq の本体，証明機構 (推論エンジン) を使用して行きます．
今回は，定義についてです．
coq-interface の初期化の際に読みこまれるプレリュードは，いくつか数学的定義を含んでいます．
例えば，前回扱った nat は，数学的概念 (mathematical collection) (Set 型) として定義されています．また，定数 O (オー) や S，plus なども，それぞれ nat，nat -> nat，nat -> nat -> nat という型のオブジェクトとして定義が用意されています．
では，O と S を用いて，自然数を定義してみましょう．ここでは，一番最初の自然数 O と，次の自然数を求める関数 S の存在を前堤とします．
1 は，どのように定義すれば良いでしょう ? そうです，1 は O の次の数ですね．
$ coq-interface
Welcome to Coq 8.0pl3 (Jan 2006)
Coq < Section Declaration.
Coq < Definition one := (S O).
one is defined
Coq < Check O.
0
: nat
Coq < Check S.
S
: nat -> nat
Coq < Check one.
one
: nat
1 が定義されたら，それを使って 2 を定義することができます．1 の時は型は省略しましたが，もちろん型を明示しても OK です．ちなみに，一度した宣言を取り消すには，Reset を使います．
Coq < Definition two := S one.
two is defined
Coq < Definition two : nat := S one.
User error: two already exists
Coq < Reset two.
Coq < Definition two : nat := S one.
two is defined
Coq < Definition three := S two.
three is defined
plus を使用して，与えられた数を 2 倍する double を定義してみましょう．
Coq < Definition double (m:nat) := plus m m.
double is defined
与えられた引数だけではなく，自由変数 (グローバル変数) にアクセスするような関数を定義することもできます．
Coq < Variable n : nat.
n is assume
Coq < Definition add_n (m:nat) := plus m n.
add_n is defined
変数は，量化限定することができます．
Coq < Check (forall m:nat, gt m 0).
forall m : nat, m > 0
: Prop
Coq < Check (exists m:nat, gt m 0).
exists m : nat, m > 0
: Prop
これにより，「全ての (全称 ; forall ; ∀) 〜 は P」「少なくとも一つ P であるような 〜 が存在する (存在 ; exists ; ∃)」のような状況を表現することができるようになります．これは，後々述語論理に入ると重要になってくる考え方です．
# ちなみに，量化は，今でこそ常識になっていますが，実はこれは長年多くの論理学者を悩ませ続けてきた超難問だったのです．
# 20 世紀に入って，ようやくフレーゲの量化理論によりこの難問がエレガントに解決された後，アリストテレス以来 2000 年もの間停滞していた論理学は劇的な発展を遂げ，やがて計算機の発明へとドラマティックにつながっていくことになります．
量化限定子を用いることにより，自然言語ではうまく表現できないような，より複雑な状況を，完全に明示的に厳密に記述できるようになります．
# 私は，未だに∃と∀が組合わさった論理式を見ると，どっちがどっちにかかっているのかとっさにわからず，混乱してしまいます (^^;
# またまた完全に余談ですけど，論理プログラミングでは，最初から論理式を計算機に処理させやすい形にエンコードしてから与えているので，量化記号などは出てこない場合が多いです．
# 例えば Prolog などでは，「節 (ホーン節)」という型式に変型された論理式を扱いますが，これは全ての変数が全称量化されているので，明示的には量化記号がでてきません．論理式から存在量化を取り除いて，全ての量化記号が頭のところにきた冠頭連言標準型に変換するためには，スコーレム化とか，いろいろややこしいアルゴリズムを用いた後，ド・モルガン則などを駆使する必要があって，なかなか大変．
次回からは，いよいよ Coq の本体，証明機構 (推論エンジン) を使用して行きます．
