圏論でCoq

色々とよく分からない話とかまとまらない話。ここで使用しているCoqのバージョンは8.3

(1)TypeとSetとProp
この3つ、どう使いわけんの?という話。このうち、Propは他二者との違いは直感的には分かりやすい。問題は、Typeを使うべきか、Setを使うべきか、基準がよく分からないこと

Inductive nat' : Type :=  O : nat' | S : nat' -> nat'.
Inductive nat' : Set :=  O : nat' | S : nat' -> nat'.
Inductive nat' : Prop :=  O : nat' | S : nat' -> nat'.

は、3つとも、ちゃんと定義できる。このうち、3つ目では、nat'とnat'_indしか定義されないのに対して、後の2つでは、nat'_rect,nat'_rec ,nat'_case,nat'_beqも定義される。そんなわけで、PropとSet/Typeは明確に違うけど、SetとTypeは違いが判然としない。唯一の違いは、Typeの型はTypeで、Setの型もTypeであること。それ以外では、SetをTypeに置き換えても、いつでも問題はないように見える。推測では、Agdaの場合、Setの上に、Set1/Set2/...という階層があって、Coqでもそれは同じだけど、Set1以上の階層は、全部まとめてTypeになってるんじゃないかと思う。じゃあ、いっそ、SetもTypeに入れてしまって、Setを廃止すればいい気もするけど、なんでこうなってるのか、よく分からない。何となく、数学の集合をイメージしている時にSetを使えばいいかとも思うけど、商集合とかがないので、やはりよろしくない気がする

(2)equalityの話
Coqの等号は、

Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : eq A x x.

によって定義されている模様(Print eqで見れる)。CoqのeqはLeibnitz equalityだと、あちこち見ると書いてある。でも、Leibnitz equalityは、例えば

Definition eq' (A:Type) (a b:A) :Prop := forall P:A->Prop,P a->P b.

とかで定義される。この二つの定義が一致することは、自明だとは思えない(少なくとも、わたしには)。Agdaだと、Leibnitz equalityは、型{A : Set} -> A -> A -> Set1になるので、微妙に違うものになる

この2つのequalityが等価であることの証明は、Coqで簡単に書ける

Goal forall (A:Type) (a b:A),eq' A a b -> a=b.
Proof.
intros A a b H;apply H;auto.
Qed.

Goal forall (A:Type) (a b:A),a=b -> eq' A a b.
Proof.
unfold eq';intros A a b H P;rewrite H;auto.
Qed.

(* eq_ind *)
Goal forall (A:Type) (x:A) (P:A->Prop),P x->forall y:A,eq' A x y-> P y.
Proof.
unfold eq';intros A x P H y H0;exact (H0 P H).
Qed.

ちなみに、Leibnitz equalityが関数の外延的等価性

forall (A B:Type) (f g : A -> B) ,(forall x, f x = g x) -> f = g.

を持つことをCoqでは証明できないよう。
http://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html
とかいうライブラリがあるので。具体例として、

forall (A1 A2:Type),(fun x:prod A1 A2=>(fst x,snd x))=(fun x=>x)

は外延的等価性の仮定なしには、Coqでは証明できない気がする。これが言えないと、CoqのTupleは圏論的な意味での直積にはなっていることが証明できない

(3)自然数
Coqで自然数は、

Inductive nat : Type :=  O : nat | S : nat -> nat.

という形で定義できる。しかし、このように定義しないといけないという理由もない(nat_indが付いてくるとか便利な点を除けば)

別の定義として、チャーチ数による定義もありえる。

Definition polynat := forall (X:Type),X->(X->X)->X.

Definition nat_reflect : forall f : nat -> Type, f O -> (forall x, f x -> f (S x)) -> forall x, f x.
intros f H0 HS.
induction x.
exact H0.
exact (HS x IHx).
Defined.


Definition dec (n:polynat):nat :=  n nat O S.
Definition suc (n:polynat) :polynat := (fun X x f=> f (n X x f)).
Definition enc (n:nat):polynat := nat_reflect (fun _=>polynat) (fun _ x _=>x) (fun _ => suc) n.

nat_reflectは、数学的帰納法nat_indがforall f: nat->Prop,f 0 -> (forall n , f n -> f (S n)) -> forall n,f nという型で、使いづらいため作り直しただけ。

listの場合も、list_indから同じような"関数"が作れて、foldrのようなものになる

Definition list_reflect : forall (A:Type) (f:list A->Type),f nil->(forall (a:A) (ls:list A),f ls->f (cons a ls))->forall ls:list A,f ls.
intros A f H0 HS.
induction ls.
exact H0.
exact (HS a ls IHls).
Defined.

(* length,app ,etc..@standard library *)
Definition len (A:Type) (ls:list A) := list_reflect A (fun _=>nat) 0 (fun _ _ n=>S n) ls.

Definition concat (A:Type) (xs:list A) (ys:list A) := list_reflect A (fun _=>list A) ys (fun z _ zs=>(z::zs)%list) xs.

Definition map (A B:Type) (f:A->B) (ls:list A):list B := list_reflect A (fun _=>list B) nil (fun z _ zs =>((f z)::zs)%list) ls.

(* re-definition of plus *)
Definition plus (n m:nat) := nat_reflect (fun _=>nat) m (fun _ x=>S x) n.

Lemma len_map :forall (A B:Type) (f:A->B) (xs:list A),len A xs = len B (map A B f xs).
Proof.
induction xs.
simpl;auto.
simpl;rewrite IHxs;auto.
Qed.

Lemma len_concat : forall (A:Type) (xs ys:list A),len A (concat A xs ys)=plus (len A xs) (len A ys).
Proof.
induction xs.
intros;simpl;auto.
intros;simpl;rewrite IHxs;auto.
Qed.

Lemma map_comp: forall (A B C:Type) (g:A->B) (f:B->C) (ls:list A),map B C f (map A B g ls)=map A C (fun x=> f (g x)) ls.
Proof.
induction ls.
simpl;auto.
simpl;rewrite IHls;auto.
Qed.

Lemma map_concat: forall (A B:Type) (f:A->B) (xs ys:list A), map A B f (concat A xs ys)=concat B (map A B f xs) (map A B f ys).
Proof.
induction xs.
intros;simpl;auto.
intros;simpl;rewrite IHxs;auto.
Qed.

polynatがnatと同じであることを証明できるとよいのだけど、関数の外延的等価性を仮定することなしに証明することはできなそう。具体的には、forall (n:polynat),(enc (dec n))=nの証明ができなそう。

forall (X:Set) (f:X->X) (x:X), n X x f= m X x fという条件で、nとmの等しさの別の定義を持ち込むと、この等価性の下では、上の性質を証明できる。

Goal forall (n:nat),dec (enc n)=n.
Proof.
induction n.
auto.
unfold dec in *|-*.
simpl.
unfold suc.
rewrite IHn.
auto.
Qed.



Definition eq_church (n:polynat) (m:polynat) :Prop := forall (X:Set) (f:X->X) (x:X), n X x f= m X x f.

Goal forall (n m:polynat),n=m -> eq_church n m.
Proof.
unfold eq_church.
intros n m H X f x.
rewrite H.
auto.
Qed.


Goal forall (n:polynat),eq_church (enc (dec n)) n.
Proof.
unfold eq_church.
unfold enc,dec.
auto.
Qed.

(4)CoqのTypeを圏にする話
CoqのTypeをObjectに、Type間の写像を射とするような圏を作ってみる。これによって、Coqが圏論で記述できるとか。以下では、射が等しいことをLeibnitz equalityによって定義しているけれども、外延性によって定義する方法もあると思う。そうして得られる圏は、以下の圏とは別のものになるはず。

Require Import Category.

(* 射の定義 *)
Section type_mors.
Variable A B:Type.

Definition TypeMor:Type := A->B.

Definition Equal_TypeMor (f g:TypeMor) := f=g.

Lemma Equal_TypeMor_equiv : Equivalence Equal_TypeMor.
Proof.
unfold Equal_TypeMor;apply Build_Equivalence.
auto.
apply Build_Partial_equivalence.
unfold Transitive;intros.
exact (eq_trans H H0).
unfold Symmetric;auto.
Qed.

Canonical Structure TypeMor_setoid : Setoid := Equal_TypeMor_equiv.

End type_mors.

(* 恒等射 *)
Section id_morph.
Variable A:Type.
Definition Id_type := (fun (x:A)=>x).
End id_morph.


(* 射の合成 *)
Section composition_of_type_morphism.
Variable A B C:Type.
Definition CompTypeMor (f:TypeMor A B) (g:TypeMor B C):= (fun x=> g (f x)).
End composition_of_type_morphism.


(* 圏の構築 *)
Lemma CompTypeMor_congl:Congl_law CompTypeMor.
Proof.
unfold Congl_law;simpl.
unfold Equal_TypeMor.
intros.
rewrite H;tauto.
Qed.

Lemma CompTypeMor_congr:Congr_law CompTypeMor.
Proof.
unfold Congr_law;simpl.
unfold Equal_TypeMor.
intros.
rewrite H;tauto.
Qed.

Definition Comp_Type := Build_Comp CompTypeMor_congl CompTypeMor_congr.


Lemma Assoc_TYPE : Assoc_law Comp_Type.
Proof.
unfold Assoc_law;simpl;intros.
unfold Equal_TypeMor.
auto.
Qed.


Lemma Idl_TYPE : Idl_law Comp_Type Id_type.
Proof.
unfold Idl_law.
intros;unfold Cat_comp.
unfold Comp_Type,Id_type.
simpl;unfold Equal_TypeMor.
tauto.
Qed.


Lemma Idr_TYPE : Idr_law Comp_Type Id_type.
Proof.
unfold Idr_law;intros.
unfold Cat_comp.
unfold Comp_Type,Id_type.
simpl;unfold Equal_TypeMor.
tauto.
Qed.


Canonical Structure TYPE := Build_Category Assoc_TYPE Idl_TYPE Idr_TYPE.