関数の定義、型の定義

Coqでは関数や型を定義するための簡単なコマンドが三つある。
Definition, Fixpoint, Inductiveである。

Definitionについて

CoqではDefinitionコマンドを使って関数を定義することができる。

Coq < Definition f x := x+1.
f is defined

OCamlの「let 〜;;」のようなものと思えばわかりやすいだろう。

文法 [Definition 変数名 := 値.]

もちろんポリモルフィックな関数も定義できる。ポリモルフィックよりもっともっと複雑な関数も定義できるが、難しいのでここでは触れない。ただ、その圧倒的な表現力のために関数型言語などの普通のプログラムにあるような型推論がCoqでは失われる。

Coq < Variable A : Set.
Coq < Variable B : Set.
Coq < Variable C : Set.
Coq < Definition composit (f:A->B)(g:B->C)(x:A) : C := g (f x).
composit is defined

Fixpointについて

OCamlでは再帰関数を宣言するときに「let rec」というキーワードを使う。
Coqでそれに対応するのがFixpointだ。
試しに 0 から n までの和を計算する関数を定義してみよう。

Coq < Fixpoint sum (n:nat) : nat :=
Coq <   match n with
Coq <   | O => O
Coq <   | S p => n + sum p
Coq <   end.
sum is recursively defined

（余談：Coqのマッチ文はOCamlのそれとよく似ているが、最後にendと必ず書くことに注意しよう。これによってmatch文が入れ子になるときの記述を楽にしてくれる。）

Inductiveについて

OCamlで型を宣言するときは「type」を使うが、CoqではInductiveというコマンドに対応する。この宣言によって定義される型をInductiveな型というが、OCamlを知っている人は普通の型のことと思えばよい。

Inductiveな型、リストを定義する。

Coq < Inductive list (A:Set) : Set :=
Coq <   | nil : list A
Coq <   | cons : A -> list A -> list A.
list is defined
list_rect is defined
list_ind is defined
list_rec is defined

Inductiveな型を定義すると、自動的にそれにまつわる便利な補題などが自動的に生成される。