CoqのInductiveとDefinition

Inductive

Inductiveは帰納的な型とその構成子を定義するコマンドです。

有限個の要素からなる型

帰納的とはいったものの有限個の要素を列挙することもできるので，まずはそこから。
例えば，鰭脚類(ききゃくるい)の型にはアシカ科・アザラシ科・セイウチ科の三種類があることを

Inductive Pinniped: Type :=
	| Otariidae (* アシカ科 *)
	| Phocidae (* アザラシ科 *)
	| Odobenidae. (* セイウチ科 *)

のようにかけます。この3つをPinniped(という型)の構成子と呼びます。

自然数の型

自然数Nを次のように定めることができます。

Inductive nat: Type :=
	| O: nat
	| S: nat -> nat.

これは自然数の型natを最初の数Oと，入力nに対してn+1を出力する関数Sだけで構成したという意味です。つまり，1つ1つ要素を列挙しなくても自然数を生成する関数を構成子として持つこともできるわけです。
今回の定義の仕方だと，Oが0, S Oが1, S (S O)が2, ...という意味になります。

このようにしてInductiveで定義したものについては帰納法を用いた証明が行えるようになります。
具体的には

forall P : nat -> Prop,
P O -> (forall n: nat, P n -> P (S n)) -> forall n: nat, P n.

という命題を真だと認めることになります。
他にもPropの部分がType, SProp, Setになっているものもあります。

Definition

Definitionは関数の定義などに使えます。
ある意味では，既存のものに別の名前をつけただけとも言えます。

実際に定義する

例えば，以下では「入力nに対して，n-1を出力する関数」を定義しています。

Definition Pre (n:nat) :nat :=
	match n with
	| O => O
	| S m => m
	end.

ここで注意が必要なのは，自然数に0より前の値は存在しないので，入力がOの場合はOを返すようにしている点です。

これは見方を変えれば，OにPre Oという新しい名前を与えて，mにPre (S m)という新しい名前をつけたにすぎません。定義とは，何か新しいものを築くというより(人が認知しているかはさておき)既存の概念に新しく名前をつけることで取り扱いを便利にすることに他なりません。

関数を使ってみよう

せっかく扱いやすく名前をつけたので実際に使ってみましょう。ということで，関数の使い方についてです。
一番てっとりばやい方法は，

Eval simpl in (* ここに入力 *).

というコマンドを使う方法です。

Eval simpl in Pre (S (S O)).

とすればS Oが出力されることを確認しましょう。
ここで，simplというタクティクスは「できるだけ簡単な形になおせ。」という命令です。

とても簡単な証明

実はDefinitionコマンドにはもう一つ使い方があります。
それは，

Definition (命題の名前): (命題).

という形で，命題を証明することができます。

証明

今回は自明な命題「S (S O)の2つ前の数はOである。」を証明してみましょう。仮に命題の名前をProp1とでもしておきます。

Definition prop1: Pre (Pre (S (S O))) = O.
Proof.
simpl.
reflexivity.
Qed.

simplは上でも出てきましたが，ゴール(示したいもの)に対して，その形を簡単にします。
reflexivityは○＝○という形の等式が真だというタクティクスです。
また，これくらい簡単な形をしているものならば，simplタクティクスを省いてもreflexivityタクティクスが簡単な形にしてから左右の比較をしてくれます。

ちなみにreflexivityというタクティクスは等号「＝」の反射律を適用することで命題が真であるという主張なので，"apply relf_equal"という書き方をしても構いません。

最後に，証明が完了し証明モードから抜ける際にはQed.コマンドを使います。

おわりに

今回の証明はあまりにも簡単だったので，次回はFixpointを用いた再起的な関数の定義と，帰納法を用いた証明について扱います。