Formalization of Setoids-enriched category theory
最近書いてるCoqの話。
主にこれの解説をします:
Yoneda.v · GitHub
Setoidをベースにすることについて
多分圏論formalize業界(狭そう)では有名な話。
Coqの場合はSetoidのequalityに対してもrewrite tacticが使えるのでそれでやる。
Proper
Setoid morphismをここではMapoidとよぶ.
Mapoidは写像(underlying set間の写像)でsetoidのequalityを保つもの.
Structure Mapoid (S S' : Setoid) := { mapping :> S → S'; is_mapoid :> Proper (equality ==> equality) mapping; }. Existing Instance is_mapoid.
ここでのProper (equality ==> equality) mapping
がそれで、
意味としてはmapping
なるfunctionによってequality
relationがequality
relationに写ることを表す(==>
はrelationのimplication).
Proper (R ==> R') f
の元で、rewrite : a R b ~> f a R' f b
なる書き換えができるようになる*1のでここではExisting InstanceによってこのPropernessをトップレベルに展開している。
Proper Instance
さて上のようにProperについてのinstanceを使わないとrewriteはできないので、例えばa == b
からP a == P b
とするにはPがProperであることを証明する必要がある。
上のコードでは、新たに定義したS ** S'
(setoidの直積)のconstructing function Spair : S -> S' -> S ** S'
がProperであることなどは自力で証明を書いて補っている。
rewriteが効いて欲しい場所で効かない場合はProperのinstanceをかこう。
Category, Functor, Natの定義
圏の定義その他については
などが参考になる。
ただしCat_on_Coqでは平易に書き下しているようなPropernessも、上のコードでは「おおもとの定義」では全てSetoid上で作るようにしてある。
つまり、例えばcategoryの定義は
Structure Category := { object :> Type; morphism : object → object → Setoid; identity : forall {x}, carrier (morphism x x); compose : forall {a b c}, morphism b c ** morphism a b -⇒ morphism a c; is_category :> Is_Category (@identity) (@compose); }.
となっていて、composeは2つのSetoidの直積からSetoidへのmapoidになるように定義してある。
あるいはfunctorのarrow partも同じようにfmorphism : forall {a b}, @morphism fdom a b -⇒ @morphism fcod (fobj a) (fobj b);
などと、hom-setoidの間のmapoidであることを要請している。
こうするとcategoryやfunctorの定義の中に「〜のproperness」のような条件がいちいち現れてこないので、「表面上は」通常の圏論でfunctionとされている場所をmapoidに置き換えるだけでいい。
あるいは、ここではすべてSetoids-enriched category theoryをやっていると思えばいいので理論的にはすっきりする。
ただしcategoryのinstanceを与える際にいちいちmapoidで定義するのは面倒なので(データを定めてからmapoidであることを証明する、という順番で行きたい)、上のコードではsetoidベースでない(条件ベタ書きの)categoryも定義しておいて相互変換できるようにしている。
このやり方だとコードが多少長くなるのでこれが嫌な場合はCat_on_Coq方式でいいと思う。
Equational Reasoning
Agdaに毒された自分のような人間はequational reasoningがないと死んでしまうのでNotationで用意した。
参考:
使用例:
Notation "`begin p" := p (at level 20, right associativity). Notation "a =⟨ p 'at' C ⟩ pr" := (@Equivalence_Transitive (@morphism C _ _) _ _ a _ _ p pr) (at level 30, right associativity). Notation "a =⟨ p ⟩ pr" := (@Equivalence_Transitive _ _ _ a _ _ p pr) (at level 30, right associativity). Notation "a ↓⟨ p ⟩ pr" := (a =⟨ p ⟩ pr) (at level 30, right associativity). Notation "a ↑⟨ p ⟩ pr" := (@Equivalence_Transitive _ _ _ a _ _ (@Equivalence_Symmetric p) pr) (at level 30, right associativity). Notation "a `end" := (@Equivalence_Reflexive _ _ _ a) (at level 30). (* 例 *) ... exact (`begin fmap H f ∘ (β a ∘ α a) =⟨ ltac: (rewrite <- assoc_of; reflexivity) ⟩ (fmap H f ∘ β a) ∘ α a =⟨ ltac: (rewrite (naturality_of β); reflexivity) ⟩ (β b ∘ fmap G f) ∘ α a =⟨ ltac: (rewrite assoc_of; reflexivity) ⟩ β b ∘ (fmap G f ∘ α a) =⟨ ltac: (rewrite (naturality_of α); reflexivity) ⟩ β b ∘ (α b ∘ fmap F f) =⟨ ltac: (rewrite <- assoc_of; reflexivity) ⟩ (β b ∘ α b) ∘ fmap F f `end).
ちなみにltac: (...)
と書くとLtacで作った項をCICの項に変換できるので、
reasoning中ではtacticとproof termを混ぜて使うことができる。
意外と便利。
これを使って思ったこととしては、やっぱりAgdaのようなhole推論機能がないと若干苦しい(エラーメッセージからどの部分までreasoningが上手く行っているかを推測する必要がある; ただし慣れればできるようになるため問題ないとも言える)。
しかし読みやすい証明のためには致し方ない。
感想
Universe Polymorphism バンザイ!!!
setoid_rewrite バンザイ!!!!!!
equational reasoning バンザイ!!!!!!!!!!!!!!!!
*1:たぶん…これあってる?