ssreflect ライブラリ紹介(eqType編)

この記事はTheorem Proving Advent Calendar 2011の13日目の記事です。

ssreflectライブラリ紹介

この前はssreflectのtacticの紹介をやったので、ライブラリの紹介をします。ライブラリの概要は http://coqfinitgroup.gforge.inria.fr/ssreflect-1.3/ を見れば何か数学寄りだなというのが分かると思いますが、まあ完全に数学寄りです。しかもtrunkでは http://coqfinitgroup.gforge.inria.fr/ のように大変膨大になっております。

eqType

というわけで、一番根っこの部分にあるeqTypeを今回のメインにしましょう。

Coqを使い始めると、まあ誰でもこんな感じに書きたくなるでしょう。

Definition nat_gt0 := { x : nat | x > 0 }.
Definition nat_gt1 := { x : nat | x > 1 }.
Definition nat_gt0_succ : nat_gt0 -> nat_gt1 := (* うんたらかんたら *).

これにより、定義域を正の自然数に限定した関数 nat_gt0_succ が定義できました。プログラミングならこれでいいのですが、数学になると困ったことが起こります。例えば、この関数が単射であること:

Lemma nat_gt0_succ_inj : forall x y, nat_gt0_succ x = nat_gt0_succ y -> x = y.

これの証明は大変です。なぜかというと、xとyには各々が正であることの証明がくっついていますが、その証明が等しいことを示すのが困難だからです。すなわち、次のことを証明する必要があります。

Goal forall x (p1 p2 : x > 0), p1 = p2.

p1とp2はそれぞれxが正であることの証明で、それらが等しいことを示したいわけです。このように証明が等しいという性質をProof irrelevanceといいます。この問題の一番簡単な解決策は公理を導入することです。標準ライブラリの「Coq.Logic.ProofIrrelevance」を使うと「任意の命題がProof irrelevantである」が公理に追加されます。

ほとんどの場合で、この公理は不要です。eqTypeライブラリを使うとこの問題をほとんど解決してくれます。eqTypeは型クラスのようなもので、Canonical StructureというCoqの機能を使っています。まあほとんど型クラスのようなものです。eqTypeを実装した型Tは次の二つの値を持っています。

eq_op : T -> T -> bool.
eqP : forall x y, reflect (x = y) (eq_op x y).

ここで、「reflect」は一つ目の命題と二つ目のbool値が同値であることを示します。すなわち、等値性を計算できるというのがeqTypeのもっている特長です。もちろん

eq_dec : forall x y, { x = y } + { x <> y }. 

は上の二つと同値です。たったこれだけなので、導ける定理も少ないというか重要なのはただ一つだけで、「eq_irrelevance」はeqTypeを実装していれば、命題「x = y」はProof irrelevantであるになります。系として、

Lemma bool_irrelevance : forall (x y : bool) (p1 p2 : x = y), p1 = p2.

が得られます。よって、{ x : T | P x } の述語の部分を「f x = true」の形に書ける場合はこの型の値を簡単に比較できるわけです。ssreflectではbool -> PropのCoercionを「is_true」で定めているので、これは単に { x : T | f x } と書くことが出来ます。

subType

型 { x : T | f x } の持っているインターフェースを抽出した型クラスが subType になります。そして、eqTypeのsubTypeは自動的にeqTypeを実装します。他にもtupleとかmatrixなんかがsubTypeを使ってeqTypeを実装していたりします。

次回予告

次はchoiceライブラリ？ exists x, P xから { x | P x }を取り出せる性質をもった型クラスを紹介するかも。