Coqで圏論(2)

Coqのバージョンは8.3

どうでもいい話その1。集合の代わりにSetoidを使うという点について。色々見てると、数学をCoqで形式化する際には、Setoidを使うのが割と普通であるらしい。その正当性は、何によって保証されるのか?とか思うものの、そもそもZFC集合論だって基礎として認められるようになって100年にも満たないわけで、その正当性は、1930年だか40年だか、そのあたりに知られていた数学の結果を形式化するのに困らなそうという程度の理由で保証されてるだけだと思うので、例えばSetoidをベースに同じことができるなら、まあいいのかとも思う。

このへんで気になるのは、選択公理に依存してる定理(ベクトル空間の基底の存在とか、代数的閉包の存在等)だけれども、ちゃんと証明できるんだろうか(これらの定理が成立しなくても、大して問題ないとも思うけれど)。

また、そもそも、圏論の場合、特定の集合論に依存してるわけでもないという気がする。「対象の集まり」の集まりを、素朴に集合として解釈してしまうと、集合の圏とか考えたときに、集合の集合!?とかなってしまうので、教科書見ると、このへんは適当に誤魔化されているように思う。わたしが最初に圏に触れた「ホモロジー代数学」という教科書では、ベルナイス=ゲーデル流の集合論で、類とか持ち出せば云々という話が注釈で書いてあった記憶がある(読んだのは10年以上前だし、本も手元にないのでうろ覚えだけど)。

思うに、圏論で集合が出てくるのは便宜的なもので、何か"別の集合の圏"的なもの(トポスと言いたいけど、個人的にはトポスはあまり自然な概念とは思わないので、どうなんでしょう)でenrichされた圏で考えても、同じ議論が通るのだと思ってる。線形代数では、基底に依存しない議論をしているのだけど、計算するには、まず基底を決める必要があるというのと似てなくもない。というように解釈すると、対象の「集まり」と射の「集まり」という二つの「集まり」は別種のものと解釈することが自然。

まあでも、これらの理由は、ZFC集合論である必要は必ずしもないというだけで、Setoidをベースにしてもよいという理由にもならない。けどまあ悩んでも結論は出なそうだし、そもそも数学にとっては、基礎が何であっても、あまり関係ない気がする。基底の存在しないベクトル空間が存在するという奇妙な事が起きたりするかもしれないけど、そういうのは病的なケースであって、普通の数学者が普段扱う健全な数学では関係ないんじゃないかね。

どうでもいい話その2。Coqの標準ライブラリにも、Setoidは定義されている。こいつを使えばいいんじゃね?とか思った。けれども、よく見るとSetoid型とかBuild_Setoidなどはもう存在しない。8.3で、自然数のSetoidを定義するには、以下のようにするっぽい。

Require Import Setoid.
Inductive NatT : Type := Z : NatT | Suc : NatT -> NatT.

Definition eq_nat (n m:NatT) := n=m.

Lemma eq_nat_equiv :Setoid_Theory NatT eq_nat.
Proof.
unfold Setoid_Theory.
apply Build_Equivalence.
exact (eq_refl (A:=NatT)).
exact (eq_sym (A:=NatT)).
exact (eq_trans (A:=NatT)).
Qed.

Add Setoid NatT eq_nat eq_nat_equiv as Nat.

Setoidクラスというものがあった時代もあったよう。標準(?)ライブラリの癖に、簡単にインターフェースが変更されるってのは、どういうことなんだろうか。ConCaTが自前で、Setoidとかを定義しているのは、そういう事情からなのかもしれない。8.3で書くなら、

Require Import Relation_Definitions.
Require Import Coq.Classes.RelationClasses.
Class Setoid := {
  carrier : Type;
  equal : relation carrier;
  equal_prop : Equivalence equal}.

Inductive NatT : Type := Z : NatT | Suc : NatT -> NatT.
Definition eq_nat := fun (n:NatT) (m:NatT) => n=m.

Lemma eq_nat_equiv :Equivalence eq_nat.
Proof.
apply Build_Equivalence.
exact (eq_refl (A:=NatT)).
exact (eq_sym (A:=NatT)).
exact (eq_trans (A:=NatT)).
Qed.

Instance Nat : Setoid := {
  carrier := NatT;
  equal := eq_nat;
  equal_prop := eq_nat_equiv}.

というようにやるっぽい。Build_Setoid NatT eq_nat eq_nat_equivでもよいらしい。

ClassはHaskellの型クラスのようなものなので、例えば、関手がモナドになることは、ConCaTを使って、以下のように定義できる。

Require Import Functor.
Require Import IdCAT.
Require Import Ntransformation.

Section monad_def.
Variables (C:Category).

Class Monad (T:Functor C C) := {
  eta : NT (Id_CAT C) T;
  mu : NT (T o_F T) T;
  assocl : forall (a:C), (eta (T a)) o (mu a) =_S (Id (T a));
  assocr : forall (a:C), (((FMap T a (T a)) (eta a)) o (mu a) =_S (Id (T a)));
  idlaw : forall (a:C) , (mu (T a)) o (mu a) =_S ((FMap T ((T o_F T) a) (T a)) (mu a)) o (mu a)
}.
End monad_def.

このとき、Monadの型は、forall C:Category,Functor C C->Typeとなるらしい。まあ、型クラスは、あまり嬉しくない気がする

本題。CoqでMonoidの圏を作る

Require Import Category.
Require Import Monoid.

(* 射の合成がちゃんと閉じていること *)
Section composition_of_monoid_morphism.
Variables (A B C :Monoid).

Definition CompMonMap (f:MonMor A B) (g:MonMor B C) := Comp_map (MonMap f) (MonMap g).

Lemma CompMMonUnit : forall (f:MonMor A B) (g:MonMor B C) , MonUnit_law (CompMonMap f g).
Proof.
intros;unfold MonUnit_law.
simpl;unfold Comp_fun.
assert(X:=(Pres1 g (x:=(f (Munit A))) (y:=(Munit B)))).
assert(Y:=(X (MMon_unit f))).
assert(Z:=(Trans (x:=(g (f (Munit A)))) (y:=(g (Munit B))) (z:=(Munit C)))).
exact (Z Y (MMon_unit g)).
Qed.

Lemma CompMMonOp  : forall (f:MonMor A B) (g:MonMor B C) , MonOp_law (CompMonMap f g).
Proof.
intros;unfold MonOp_law;simpl.
unfold Comp_fun;intros.
assert(X:=(MMon_op f a b)).
assert(Y:=(MMon_op g (f a) (f b))).
assert(Z:=(Pres1 g (x:=(f (a +_M b))) (y:=(f a +_M f b)))).
assert(W:=(Z X)).
exact (Trans W Y).
Qed.


Definition comp_monoid_morph (f:MonMor_setoid A B) (g:MonMor_setoid B C) : (MonMor_setoid A C)
 := Build_MonMor (CompMMonUnit f g) (CompMMonOp f g).

End composition_of_monoid_morphism.


(* 恒等射の存在 *)
Section id_is_monoid_morph.
Variable A:Monoid.

Definition Id_mon (x : A) := x.
Lemma Id_mon_map_law : Map_law Id_mon.
Proof.
unfold Map_law in |- *; trivial.
Qed.

Canonical Structure id_morph : Map A A := Id_mon_map_law.

Lemma MonUnitLaw_id : MonUnit_law id_morph.
Proof.
unfold MonUnit_law;simpl;unfold Id_fun.
exact (Refl (Munit A)).
Qed.

Lemma MonOpLaw_id : MonOp_law id_morph.
Proof.
unfold MonOp_law;simpl;unfold Id_fun.
intros;exact (Refl (a +_M b)).
Qed.

Definition Id_Mon : MonMor_setoid A A := Build_MonMor MonUnitLaw_id MonOpLaw_id.
End id_is_monoid_morph.

(* monoidの圏の構築 *)
Lemma comp_monmor_congl : Congl_law comp_monoid_morph.
Proof.
unfold Congl_law;simpl.
unfold Equal_MonMor.
unfold Ext in |-*;simpl.
unfold Comp_fun;auto.
Qed.

Lemma comp_monmor_congr : Congr_law comp_monoid_morph.
Proof.
unfold Congr_law;simpl.
unfold Equal_MonMor;unfold Ext;simpl.
unfold Comp_fun.
intros a b c f g h e x.
apply Pres1;auto.
Qed.

Definition Comp_Monoid := Build_Comp comp_monmor_congl comp_monmor_congr.

Lemma Assoc_MONOID : Assoc_law Comp_Monoid.
unfold Assoc_law;simpl;intros.
unfold Equal_MonMor;unfold Ext;intro x;simpl.
apply Refl.
Qed.

Lemma Idl_MONOID : Idl_law Comp_Monoid Id_Mon.
Proof.
unfold Idl_law;intros.
unfold Cat_comp.
unfold Comp_Monoid;simpl.
unfold Equal_MonMor.
unfold Ext;intros.
simpl.
unfold Comp_fun;simpl;unfold Id_mon.
apply Refl.
Qed.


Lemma Idr_MONOID : Idr_law Comp_Monoid Id_Mon.
Proof.
unfold Idr_law;intros.
unfold Cat_comp.
unfold Comp_Monoid;simpl.
unfold Equal_MonMor.
unfold Ext;simpl.
unfold Id_mon;intros;apply Refl.
Qed.

Canonical Structure MONOID := Build_Category Assoc_MONOID Idl_MONOID Idr_MONOID.

簡単と思ってたが、意外と大変だった。リスト関手を作って、モナドになることも示そうと思ったけど、次回。リスト関手は、Setoidの圏からモノイドの圏への関手として作って、モノイドの圏からSetoidの圏への忘却関手を定義して、それらが互いに随伴であることを示して、合成がSetoidの圏上のモナドになることを示そうと思う。ところで、リストには、関手X->I+S*Xの始代数という観点もあったのだけど、この二つは、ちゃんと一致するんだろうか。この疑問は、一般のCartesian category上で考えられる。

しかし、Coqの証明は、書くのはともかく、読む人には全く優しくない気がする。Coqで順に実行してみれば、証明の進行具合が分かるわけだけれども、それなしで、他人や過去の自分が書いた証明を理解するのは、難しいんじゃないだろうか例えば、unfoldしまくって、introsとかsimplとかすると、その時点で、何がGoalで何が前提なのか、とても把握しづらい。tacticじゃなくもっと関数を書いてるっぽさを前面に出した方がいいんじゃないかねえ。証明を理解する必要はないという見方もあるけど、それも何だか。

例えば、

Lemma S:forall (A B C:Prop),(A->B->C)->(A->B)->A->C.
Proof.
intros A B C H H0 H1.
apply H.
exact H1.
exact (H0 H1).
Qed.

よりも、

Lemma S:forall (A B C:Prop),(A->B->C)->(A->B)->A->C.
Proof.
exact (fun (A B C:Prop) (X:A->B->C) (Y:A->B) (Z:A) => X Z (Y Z)).
Qed.

の方が、書くのは少ししんどいけど、短いし読みやすいんじゃないかと思う(Curry-Howard脳

その他のCoqで書いてみようと思ってるネタ。
・射f:A->Cとg:B->Cのpullbackをf':X->Bとg':X->Aとするとき、fがmonoならばf'もmono
・射f:A->Cとg:B->Cのpullbackをf':X->Bとg':X->Aとするとき、gがmonoならばg' もmono
CLTT p.43に証明なしでさらっと述べられてる話。たいしたことはないけど、なんとなく。

・CCCが単純型付きラムダ計算のモデルになるという話。実は、感覚的にしか理解してないので、ちゃんと理解したい

・淡中双対定理。自分は圏論で一番重要な定理だと思ってるけど、日本語による説明って見たことがない代物(情報科学には関係ないだろうけど)。準備が大変そうだけど、アフィン群スキームしか出てこないので、代数幾何の話にはならず、純代数的に済むはず。