Coq.Arith.MinMax 見てみた

Coq のモジュールシステムについて，使い方がいまいちつかめてない気がしたので stdlib でどう使われてるのか見てみました。

はじめに，モジュールとはどういうものかを一応言語化してみる。Coq の module はまあいわゆる module だと思っていればよいと思うのですが，そうすると module type は module の仕様を書いたものです。その型をもつ module が仕様の実装ということになります。別の module に依存した module のことを functor といって，functor type は functor の仕様です。functor の仕様というのは具体的には，引数の型のところに依存する module にどんな仕様を要求するかを書いて，戻り型に自分の満たすつもりの仕様を書くよになっています。言葉の使い方はだいたい OCaml と同じなのだと思いますが，言葉で一般的な説明をしてもなんだかよくわからないので，実際の使い方をいろいろ見たほうがよい気がします。

とりあえず Coq.Arith.MinMax を読んでみる。nat の min と max を定義してその性質を証明していますが，途中で一般の順序に対する結果を適用するのに module が使われます。

最初の max, min の定義は自然なやり方で。

Fixpoint max n m : nat :=
  match n, m with
    | O, _ => m
    | S n', O => n
    | S n', S m' => S (max n' m')
  end.

Fixpoint min n m : nat :=
  match n, m with
    | O, _ => 0
    | S n', O => 0
    | S n', S m' => S (min n' m')
  end.

で，モジュールを作る。

Lemma max_l : forall x y, y<=x -> max x y = x.

Lemma max_r : forall x y, x<=y -> max x y = y.

Lemma min_l : forall x y, x<=y -> min x y = x.

Lemma min_r : forall x y, y<=x -> min x y = y.

Module NatHasMinMax <: HasMinMax Nat_as_OT.
 Definition max := max.
 Definition min := min.
 Definition max_l := max_l.
 Definition max_r := max_r.
 Definition min_l := min_l.
 Definition min_r := min_r.
End NatHasMinMax.

何をやっているかというと，NatHasMinMax という module を定義しています。型が書いてありますが，単に宣言されているものが入っていると思っておけばよさそうなので，とりあえず気にしないことにしましょう。

最後に，一般論から導かれるいくつかの定理を nat の場合に具体化したようなモジュールを生成して export しています。ここで一般論において仮定されている「上限・下限の公理」みたいなもの (実際にはもっと弱いことしか要求していません) を与えてやらないといけないので，上で定義した NatHasMinMax を使います。

Module Export MMP := UsualMinMaxProperties Nat_as_OT NatHasMinMax.

イメージとしては，一般の順序集合で成り立つ性質がいくつかすでに証明されていて，nat の場合に対して特別な名前を付けるという感じでしょうか。

この流れは普通の数学のやり方と半分似ていて半分違っているような気がします。一般論として任意の順序集合でこんなことがいえる，という議論をするところは同じですが，数学では「N は順序集合だから……」と言って順序集合に対する一般的な定理を直接引用して使います。別の言い方をすると，使うときに初めてパラメータを具体化します。Coq の standard library でやっていることはこれとは違っていて，後で使うためにあらかじめパラメータを具体化した定理に名前をつけています (正確には，一般の場合の定理を具体化したものを，同じ名前で違う名前空間に生成する，などと言うべきかもしれません)。

残りの部分は nat に固有の定理がいくつか並んでいるだけなので省略。