Coq で Setoid を作る。: Theorem Prover Advent Calendar 2014 Day 10

せっせと作ろう Setoid。

1 この記事は、

  1. Theorem Prover Advent Calendar 2014 の 10 日目の記事です。
  2. Coq で Setoid を作る 我流 の方法を解説しています。
  3. Coq の色んな機能が出て来て解説しきれないので、開き直ります。
  4. 載っているコードはそのまま coqc 出来ます。コードを抽出したものは こちら
  5. Coq のことを少し知っていればなんとなくわかるかもしれません。

1.1 参考文献など

A Gentle Introduction to Type Classes and Relations in Coq.
タイトルの通り、 Coq の型クラスや(同値)関係を利用した証明などについて解説している文書。Gentle とありますが、本当にわかりやすいです。 Pierre 先生すごい。
@tmiya_ さんの Coq で Setoid を作るスライド
2011 年の資料ですが、そもそも Setoid って何よ? という話や、当時の Coq の機能でどのように Setoid を利用するのか、という話が載っています。 Add なんちゃらというコマンドはは使ったことがありませんのでわからんです。
Packaging Mathematical Structures
群とか環みたいな色々内包している数学的構造を、 Coq でどう表現しどう扱うか、構造が様々な方向へ拡大したり交差する中でいかに頑強な設計とするか、というお話。とても面白いのですが、未だに咀嚼しきれていません。今回はあまり関りませんが、 Cat_on_Coq の設計では大いに参考にしております。

1.2 省略可能な前説

Coq を使って圏論をやろうと思って 実際にやっている のですが、 定理証明系で圏論を展開するにあたって、 「射の等価性」の扱いをどうしたものかという悩みがあります。

Coq の eq をそのまま使うと、どうしたって外延的等価性を仮定することになります。 「射」の代表例の一つが関数ですからね。

\[ f,g \in Y^X,\; f = g :\Leftrightarrow \forall x \in X.\; f(x)=g(x) \]

これは外延的等価性ですが、これくらいならまだ仮定してもいいかな?と思えなくもないんですよ。 もちろん eq の意味は変わりますし、 Axiom 追加するのはあまり好きではないので避けたいですけどね。

問題は、「射が等しい」の「等しい」がもっと変なやつだったりすることなんです。

やせた圏の有名な例が半順序集合ですが、そこでは「順序の成立」が「射」です。 すると「射が等しい」って何よ?証明の等価性?え? Proof Irrelevance も使うの? みたいな展開になります。

この辺りで、そもそも eq を射の等価性に使うのはあまり賢くはなさそうだね?と思いました。 圏論の主役は射、というか射が形作る可換図ではないのか? そしてその可換図を式に表わしたものが射の等式なのだから、 そういう大事なものをありあわせの eq なんかでまかなおうなんて ちょっと雑なんじゃないの? と。

そんなこんなで圏を定義するときの「射のあつまり」を記述するために Setoid を使おうという結論に至り、Cat_on_Coq では Setoid の定義からやり直しました。

そうする中でどんな定義の仕方をしていくとやり易いかなぁとか、 どんな仕組みを使うと楽に議論を進められるかなぁとか試行錯誤した結果、 ああ、こんな感じでよさそうというところに落ち着いたので、 それを紹介してみようという記事です。

ということは、去年、前半を書いたきりで続きのないあの記事の続きでもあります。

2 準備:インポートしたり。

これから記述していくコードは、以下のような設定とモジュールを利用した上で進めていきます。

Set Implicit Arguments.
Unset Strict Implicit.

Require Export Basics Tactics Setoid Morphisms.

上 2 行は引数をいい感じに省略したりできるようにするための設定です。 モジュールについては軽く触れておきますね。

Basics & Tactics
Program コマンドを使うコードの場合、大抵これらをインポートしてます。 何のためだったかは忘れました
Setoid & Morphisms
Morphisms で定義されている Proper が非常に素敵な働きをしてくれます。 rewrite 万歳。 SetoidMorphisms モジュールが参照しているものどもがごっそりエクスポートされているので Morphisms を使うなら一緒にインポートしておくとよいです。

3 Setoid 型の定義

Setoid は、型とその上の同値関係からなる構造です。 集合に対する商集合のようなものと捉えるとわかりやすいですね。

ある型の値たちを どんな基準で区別するのか は、時に様々です。

その基準として同値関係を採用し、型と同値関係の組で一つの構造と見做したものが Setoid というわけです。

そういった Setoid たちの「型」を Setoid とすることにしましょう。 Setoid 型の値、それが Setoid である、というわけです。 すると、 Setoid はときに Set のように振舞えるとよさそうです。

こういったことを踏まえつつ、早速 Setoid を Coq で定義するとしましょう。

定義は以下の通りです。

Structure Setoid :=
  {
    carrier:> Type;
    equal: relation carrier;

    prf_Setoid:> Equivalence equal
  }.
Existing Instance prf_Setoid.
Notation Setoid_of eq := (@Build_Setoid _ eq _).

以上です。

短いから解説はいらないかな!?

4 解説

はい。

Structure は便利な Record 型です。 Canonical Structure マジ便利ですが、それは Setoid の具体例を挙げるタイミングで触れましょう。

Setoid 型のフィールドはそれぞれ、型、二項関係、同値関係であることの証明を 表わしています。

同値関係とは、反射律、対称律、推移律を満す二項関係のことでした。 Equivalence はそれを記述した述語としての型クラスです。

Print Equivalence.
Record Equivalence (A : Type) (R : relation A) : Prop := Build_Equivalence
  { Equivalence_Reflexive : Reflexive R;
    Equivalence_Symmetric : Symmetric R;
    Equivalence_Transitive : Transitive R }

For Equivalence: Argument A is implicit and maximally inserted
For Equivalence: Argument scopes are [type_scope _]
For Build_Equivalence: Argument scopes are [type_scope _ _ _ _]

Print すると Record なんですけどね、型クラスも Record なんで。 型クラスについて詳しくない方は、三つの述語の連言だと考えてくれればよいです。実際、同型(のはず)です。

次は、定義の中で使っている Coq の機能なりテクニックを説明していきます。

4.1 Coercion

carrier の型宣言部が : ではなく :> となっています。 これは Setoid 型の値を Type 型の値としても扱えるようにするものです。

carrierSetoid から Type への関数となりますが、 この関数 carrier を通して Setoid 型の値を Type 型の値と見做すことができます。

Type 型の値が求められている場面で Setoid 型の値が与えられたら、 暗黙の内に関数 carrier を適用すればよいわけです。

Coq では、この暗黙の関数適用を実現する機能である coercion という仕組みが提供されています。 通常は carrier のような役目を果す関数に Coercion コマンドを使うのですが、 Record 型のフィールド定義で :> を使うと、アクセサ関数に Coercion コマンドを施した場合と同じ結果に至るのですね。 詳しくは Reference Manual の 18 章 を参照してください。 SSReflect でも地味に大活躍している機能です。

次のコマンドを実行すると、その時点で定義されている coercion の情報が手に入ります。

Print Graph.

結果は一部省略していますが、以下のようになります。

...
[carrier] : Setoid >-> Sortclass
[prf_Setoid] : Setoid >-> Equivalence

[f] : A >-> B という記述は、 A 型を関数 f を通じて B 型と見做す、という意味です。 coercion では TypeSet などの Type 型を持つ値は Sortclassforall x: A, B (含 A -> B)という形式の型は Funclass と表現されます。

Cat_on_Coq などの私の書いているコードでは、 Structure を使っているときは大抵 Coercion が付随しています。 ほら、 \(M=\langle M, \bullet, e \rangle\) みたいな記法あるじゃないですか、あれと同じ気持ちです。

4.2 Notation

Notation でなんかよくわからんことしてますね?

あれは、 Program コマンドや refine タクティクを利用して Setoid のインスタンスを定義しやすくするための道具です。

Structure の実体は Record 型であり、 Record 型はコンストラクタをただ一つだけ持つ帰納型です。 そのコンストラクタは特に指定しなければ Build_/typename/ という名前で自動的に生成されます。

(@Build_Setoid _ eq _) とすると、 Setoidequal フィールドだけが与えられることになります。 第一引数の carrierequal から推論できますが、 第三引数の推論は同値関係であることの自動証明となりますので、 大抵の場合は推論できません。

Program コマンドや refine タクティクは、 そういった推論しきれなかったパラメータをゴールとして生成してくれます。 Setoid であれば、同値関係と なるであろう 関係 Aeq を定義して Setoid_of Aeq とすれば、自動的に Aeq の同値関係性の証明に移り、それが終われば Aeq を元にした Setoid の定義も完結します。

Setoid を作るならいきなり Setoid の定義から始めたいですよね? そういうときに ProgramNotation 、ワイルドカードの三つを組み合わせるというテクニックは中々使えると思います。

5 具体例

型を定義したけど値がないなんて寂し過ぎるので、具体例を定義しましょう。

で、定義する前に Setoid を使いやすくするために幾つかの記法を Notation コマンドで作っておきます。

Notation "(== :> S )" := (equal (s:=S)).
Notation "(==)" := (== :> _).
Notation "x == y :> S" := (equal (s:=S) x y)
  (at level 70, y at next level, no associativity).
Notation "x == y" := (x == y :> _) (at level 70, no associativity).

ちなみに、上二つの出番はこの記事にはありません。

5.1 eq の Setoid

eq じゃ物足りんとか宣ってきましたが、もちろん eq も同値関係だから Setoid を作れます。

Program Canonical Structure eq_Setoid (A: Type) := Setoid_of (@eq A).

Program Canonical Structure なんて 滅多に使われない 組み合わせでしょうね。

eq については Equivalence の証明であるところの eq_equivalence なるものが既に定義されています。 Program コマンドはそれなりに頑張ってくれるので、今回は

eq_Setoid has type-checked.
eq_Setoid is defined

という出力が得られして、証明はせずに Setoid の定義完了です。

eq_SetoidSetoidCanonical Structure としたことで、 特に指定せずとも Setoid の具体例として eq_Setoid を使えるようになりました。

どういう意味かというと、

自然数同士の比較

Check 1 == 1.
1 == 1
     : Prop

や bool 値同士の比較、

Check true == false.
true == false
     : Prop

また、関数同士の比較

Eval simpl in S == S.
= S = S
: Prop

でさえ、 Setoid 上の同値関係を使って行えるということです。

最後、 Eval simpl をしたのは、 equal の実体が eq であることを示すためです。 最初の二例も同じく eq になります。

5.2 関数の外延的等価性で Setoid

eq は素朴な例でした。 次はちょっぴり凝って関数の Setoid を作りましょう。

外延的等価性を同値関係として、 Setoid を作ってみます。

Definition ext_eq (X Y: Type)(f g: X -> Y) :=
  forall (x: X), f x = g x.
Arguments ext_eq X Y / f g.
Program Canonical Structure fun_Setoid (X Y: Type): Setoid :=
  Setoid_of (@ext_eq X Y).

はい、一息に外延的等価性の定義と fun_Setoid の定義を行いました。 Arguments のくだりは気にしないで OK です。

ext_eq は上述した外延的等価性の定義通りですね。 それを同値関係とした Setoid が fun_Setoid となりますが、 定義はここでは終わっていません。

これらのコマンドを実行した後の出力は以下のようになっています。

fun_Setoid has type-checked, generating 1 obligation(s)
Solving obligations automatically...
1 obligation remaining
Obligation 1 of fun_Setoid:
forall X Y : Type, Equivalence (ext_eq (Y:=Y)).

ext_eq が同値関係であることの証明が残っています。

Let's Prove!

というわけで、証明を行ったコードがこれになります。

Next Obligation.
  split.
  - intros f x; reflexivity.
  - intros f g Heq x; rewrite Heq; reflexivity.
  - intros f g h Heqfg Heqgh x; rewrite (Heqfg x); apply Heqgh.
Qed.

出力は、

fun_Setoid_obligation_1 is defined
No more obligations remaining
fun_Setoid is defined

はい、終わったみたいですね。 fun_Setoid の定義も完了です。

eq_Setoid と同様に Canonical Structure としましたので、 関数同士の、 外延的等価性による比較 も Setoid の equal で行うことができるようになりました。

Definition plus1 (n: nat): nat := n + 1.
Check (plus1 == S).
plus1 == S
     : Prop

ちなみに、 plus1fun (n: nat) => n + 1 と直書きすると、推論に失敗します。

さて、一つ気になるのは、この equal が本当に eq なのか?という点です。 さきほど eq で Setoid を作ってしまったので、もしかしたらこの equalext_eq ではなく、 eq である可能性が考えられます。

Eval simpl in で確認しましょう。

Eval simpl in S == S.
= forall x : nat, S x = S x
: Prop

というわけで、期待通り ext_eq で比較してくれていました。

Setoid を定義する順番の影響かな?と思った方もいるかもしれませんが、 あとから eq_Setoid を定義して Eval simpl in... としてもちゃんと ext_eq を使ってくれています。 より「具体的な」ものを優先して使うようなアルゴリズムになっているのでしょうね。

6 おわりに

ということで、自分が最近使っている Setoid の定義の仕方の、 利用した機能についての簡単な解説を交えながらの紹介でした。

当初は Setoid 間の「写像」である Map についても触れようかなぁと思っていたのですが、嵩んだので省きました。 Advent Calendar の空いているどこかで Map については書きたいと思います。

もう一個ほど書きたいネタはあるので、それももしかしたら。


さて、 Coq は定理証明支援系、すなわち一つのシステムであり、 様々な機能が備わっています。

ふと Reference Manual を覗いてみたらなんか便利そうな機能を発見したりすることが多々ありますね。

最近では Arguments コマンドのなんでも屋っぷりがすごいなぁという印象です。 引数絡みのことは大抵こいつが担当するのですが、あんたここまでやれんのかい、みたいな機能がちらほらあります。 今回さりげなく「どの引数まで与えられたら定義を展開するか」を制御する機能を使いましたが、これとか地味に便利です。

Coq を使っていて楽しい場面といえばもちろん、命題をガリガリ書いたり証明をゴリゴリ構成しているときなんでですが、 最近では Coq の「支援系」たる部分、様々な機能を如何に使いこなすかを探求していくのもなかなか熱いなぁと思っている今日この頃です。

そんでもって、 8.5 はいつ出るんだろう。

Date: 2015/6/28 1:17:23

Author: mathink

Created: 2015-06-28 Sun 02:42

Validate