CafeOBJ の雰囲気が分かった所で今度は Coq に挑戦。かなり難しいですが、あきらめずに Coq in a Hurry http://cel.archives-ouvertes.fr/inria-00001173 を元に勉強しています。
起動と終了
起動は coqtop で終了は Quit. です。また、macports でインストールすると emacs 用のスクリプトがついてきます。 M-x load-library coq-inferior M-x run-coq で実行すると便利。
Check: 要素から型を探す。
Check コマンドを使うと、関数型言語みたいに使えます。ただし計算はせずに型だけ表示します。nat が自然数型で、Prop が命題型(「ある」か「ない」かをあらわす)、Prop と似たようなのに bool (論理型) がありますが、使い分けるそうです。
Coq < Check True. True : Prop Coq < Check 3 + 4. 3 + 4 : nat Coq < Check 3 = 4. 3 = 4 : Prop
Check 型名. のようにすると、型も他の型に含まれる事が分かります。例えば 7 の型、7 の型の型と順ぐりに調べると、7 ∈ nat ∈ Set ∈ Type ∈ Type ∈ ... のようになっています(勝手に ∈ の記号を型の要素の意味で使っています)。
もっと難しい型もあります。例えば fun 構文を使って関数を表現します。関数の型の表し方は Haskell と同じです。あと、forall (全ての) や exists (存在する) などの言い方も出来ます。forall x:nat, x = 3 (すべての自然数は 3 である) みたいな感じです。その答えは True か False なので型は Prop になります。型は無くても適当に補ってくれて便利です。
Coq < Check fun x => x * 2. fun x : nat => x * 2 : nat -> nat Coq < Check forall x:nat, x = 3. forall x : nat, x = 3 : Prop
どんどん型を調べた結果をまとめて、逆順に書いてみました。
- Type ∋ Set ∋ nat ∋ 7
- Type ∋ Set ∋ (nat -> nat) ∋ (fun x => x * 2)
- Type ∋ Prop ∋ True
- Type ∋ Prop ∋ (forall x:nat, x = 3)
Search: 型から要素を探す。
Check とは逆に、型から要素を探すには Search を使います。<= などの演算子は直接探せないので、Locate を使って別名を探します。
Coq < Search True. I: True Coq < Search nat. O: nat S: nat -> nat pred: nat -> nat plus: nat -> nat -> nat mult: nat -> nat -> nat minus: nat -> nat -> nat Coq < Locate "<=". Notation Scope "n <= m" := le n m : nat_scope (default interpretation)
Eval: 簡約
折角関数を作ったので計算したいという時、Eval を使うと一応出来ます。一応と書いたのは、どういう訳か <= のような物をこれ以上短くしてもらえません。
Coq < Eval compute in 3 + 4. = 7 : nat Coq < Eval compute in 3 <= 4. = 3 <= 4 : Prop
証明
証明はなんだか難しいので分かった事だけ書きます。これ以下激しく間違っている可能性があります。間違ってたら是非教えてください！これまではA : B という表記がある時、「A の型は B である」という意味ですが、それ以外に「A は B の証明である」という意味もあるそうです。この二つの言い方の対応を「カリー・ハワード対応」と言います。証明の言い方を使うと、0 : nat は、0 は nat の存在証明だという事になります。例えば、「喋る猫は存在するか」という命題に対し、シャミセン : 喋る猫 のように証明します。
Coq in Hurry では、このやり方で 0 <= 1 の証明をしているので、作り直してみます。全部定理を作り直す方法をマニュアルで探すと、Axiom というのがあったので、これを使って自然数を定義してゆきます。suji は数字、z はゼロ s は次の数字のつもりです。
(* セットの要素として数字型を作ります。*) Coq < Axiom suji : Set. (* ゼロは数字です。*) Coq < Axiom z : suji. (* 関数 s によってもう一つ数字を作る事が出来ます。1 = s z, 2 = s (s z), 3 = s (s (s z)) という事にします。*) Coq < Axiom s : suji -> suji. (* 関数 less (<= のつもり) を作ります。 *) Coq < Axiom less : suji -> suji -> Prop. (* 最初の性質として、同じ数字 (n) 同士では n <= n が成り立ちます。*) Coq < Axiom less_n : forall n:suji, less n n. (* 次に、n <= m が成り立つときは n <= 1 + m も成り立ちます。 *) Coq < Axiom less_s : forall n m:suji, less n m -> less n (s m).
あとは、「なんとか : less z (s z)」になるような「なんとか」を探せば、それが 0 <= 1 の証明になります。
ここで最初の性質 less_n : forall n:suji, less n n を見てみます。「全ての n について n <= n が成り立つ」という意味ですが、という事は 0 <= 0 も 1 <= 1 も成り立つ訳です。forall はこのような個々の命題たくさんいっぺんに纏めて書いたものと考える事が出来ます。その中から 0 <= 0 の場合だけ取り出すには less_n z のように、less_n を関数として考えます。
Coq < Check less_n z. less_n z : less z z
これで、less_n のルールを使って 0 <= 0 が証明出来た事になります。次に、less_s を使って「0 <= 0 が成り立つなら 0 <= 1 も成り立つ」という事を証明します。
Coq < Check less_s z z. less_s z z : less z z -> less z (s z)
これも理屈は同じです。less_s のルールはあらゆる二つの数字の組について述べられているので、その中から両方が 0 の場合だけを取り出すのです。これで完成！と思いきや、まだ何か変です。less z z -> less z (s z) は、「0 <= 0 ならば 0 <= 1」と読みます。-> は関数型をあらわすと同時にこのように条件文を現すのです。f : A -> B かつ a : A の時の関数適用の値は f a : B なので、less z z -> less z (s z) かつ less z z も関数適用の記法を使って次のように書けます。
Coq < Check less_s z z (less_n z). less_s z z (less_n z) : less z (s z)
日本語に直すと、「0 <= 0 の時 0 <= 1 (less_s z z)」のかつ、「0 <= 0 (less_n z)」なので、「0 <= 1 が成り立つ (less z (s z))」という感じでしょうか。
というわけで 0 <= 1 がめでたく証明出来ました。まだ私も理解が浅くて説明が無茶苦茶ですが、今後精進します。
