型によるしりとりの成立判定

(12/12更新)
eq型のパターンマッチを使って型を書き換えるテクニックを
知ったので、mcomposeの書き直し。
型がMorphism A B -> Morphism B C -> Morphism A Cで、計算できるものができた。
ただし諸定理の定義をDefined.でTransparentにしておかないとうまくいかない模様。

概要

依存型プログラミング(Coq)の練習のために
モニャドセミナー第1回
http://d.hatena.ne.jp/m-hiyama/20090414/1239686984
で知ったしりとりの圏
http://d.hatena.ne.jp/m-hiyama/20090424/1240552575
を実装しようと試みている。
(4/25少し更新。)

依存型と圏の射

Coqを知らない人に見てほしいことは
mkobuta(Morphismとしてのこぶた)が"Morphism こ た",
(「こ」で始まり、「た」で終わる文字列)
mtanukiが(Morphismとしてのたぬき)"Morphism た き"
(「た」で始まり、「き」で終わる文字列)
という型をもつこと、
および
mkobuta ++ mtanukiは型が合っているので計算されるが
mkobuta ++ mkobutaは型が合っていないので
コンパイルが通らないこと。
つまり、型チェックによってしりとりが成立しているかどうか判定されるのだ！

課題があり、
mcomposeの型をMorphism A B -> Morphism B C -> Morphism A Cにしたいが
そうなっていない。12/12解決

Coqは定理証明するためのものなので
・mcomposeは結合的
・mid Aがcomposeの単位元になっている
ことなどが帰納法で示せるはず。
もう少し作業がいります。

(4/26更新)
id:yoshihiro503さんが
すでに別のMorphismの定義で
Morphism A B -> Morphism B C -> Morphism A Cのcompositionを実現されています。
compositionの結合性、およびidが左、右単位元になっていることも証明
されています。
http://d.hatena.ne.jp/yoshihiro503/20090425/p1

(4/27更新)
id:yoshihiro503さんにならい、
型をMorphism A B -> Morphism B C -> Morphism A Cにした
mcomposeを対話的に作ってみた。
しかし結合性、単位元などは証明できる気がしない。
また、mcomposeがどんな関数かさっぱり分からなくなったのでオマケ的に最後に載せておく。

Section Shiritori.

Set Implicit Arguments.
(* 1要素以上のconsリスト *)
Inductive list1 (A : Type) : Type :=
  | singleton1 : A -> list1 A
  | cons1 : A -> list1 A -> list1 A.

(* singletonおよびconsのノーテーション *)
Notation "[ a ]" := (singleton1 a) : shiritori_scope.
Notation "a :: x" := (cons1 a x)(at level 60, right associativity) : shiritori_scope.
Open Scope shiritori_scope.

Section functions.
Variable A : Type.
(* 先頭を取ってくる関数 *)
Definition head1 (x : list1 A) : A :=
  match x with
  | [a] => a
  | a :: x' => a
  end.

(* 末尾を取ってくる関数 *)
Fixpoint last1 (x : list1 A) : A :=
  match x with
  | [a] => a
  | a :: x' => last1 x'
  end.

(* 一つ目のリストの末尾以外を二つ目に結合 *)
Fixpoint app_minus1 (x y : list1 A){struct x} : list1 A :=
  match x with
  | [a] => y
  | a :: x' => a :: (app_minus1 x' y)
  end.

End functions.

(* 平仮名はすべてコンストラクタ *)
Inductive Kana : Set :=
  | こ : Kana
  | ぶ : Kana
  | た : Kana
  | ぬ : Kana
  | き : Kana
  | つ : Kana
  | ね : Kana.

(* 文字列はKanaのリストとする *)
Definition String1 := list1 Kana.

Definition kobuta : String1 :=  (こ :: ぶ :: [た]).
Definition tanuki : String1 := (た :: ぬ :: [き]).
(* こ *)
Eval compute in head1 kobuta.
(* た *)
Eval compute in last1 kobuta.
(* こぶこぶた *)
Eval compute in app_minus1 kobuta kobuta.
(* こぶたぬき *)
Eval compute in app_minus1 kobuta tanuki.

(* Object = Kana *)
Definition Object : Set := Kana.

(* Morphismは二つのオブジェクトを添え字にもつ型で、
  コンストラクタに渡された文字列の先頭と末尾となる *)
Inductive Morphism : Object -> Object -> Set :=
  morphism (str : String1) : Morphism (head1 str) (last1 str).

(* 文字列をMorphismにする表記 *)
Notation " << str >> " := (morphism str) : shiritori_scope.
Open Scope shiritori_scope.

(* Morphismとしてのこぶたとたぬき *)
Definition mkobuta : Morphism こ た := << kobuta >>.
Definition mtanuki : Morphism た き := << tanuki >>.

(* 中のStringを抽出 *)
Definition mextract (A B : Object) (f : Morphism A B) : String1 :=
  match f with
    morphism str => str
  end.

(* termのpattern matchに変えるべき？ *)
Definition domain (A B : Object) (f : Morphism A B) : Object := A.
Definition codomain (A B : Object) (f : Morphism A B) : Object := B.

(* head = domain *)
Theorem head_domain (A B : Object) (f : Morphism A B) :
  head1 (mextract f) = domain f.
  intros.
  induction f.
  induction str.
  unfold domain.
  simpl. trivial.
  unfold domain.
  simpl. trivial.
Defined.

(* last = codomain *)
Theorem last_codomain (A B : Object) (f : Morphism A B) :
  last1 (mextract f) = codomain f.
  intros.
  induction f.
  induction str.
  unfold codomain.
  simpl. trivial.
  unfold codomain.
  simpl. trivial.
Defined.  

(* identity *)
Definition mid (A : Object) : Morphism A A :=
  << [A] >>.

(* 二つのMorphismを結合してStringを出力 *)
Definition mapp (A B C : Object)
  (f : Morphism A B) (g : Morphism B C) : String1 :=
  app_minus1 (mextract f) (mextract g).

(* こぶたぬき *)
Eval compute in mapp mkobuta mtanuki.
(* 型エラー *)
(* Eval compute in mapp mkobuta mkobuta. *)

(* fとgを結合してheadをとるとdomain f *)
Theorem app_head : forall (A B C : Object)
  (f : Morphism A B) (g : Morphism B C),
    head1 (mapp f g) = domain f.
  intros.
  unfold mapp.
  unfold domain.
  induction f.
  unfold mextract at 1.
  induction str.
  simpl.
  simpl in g.
  rewrite head_domain.
  unfold domain.
  trivial.
  unfold domain.
  simpl.
  trivial.
Defined.

(* fとgを結合してlastをとるとcodomain g *)
Theorem app_last : forall (A B C : Object)
  (f : Morphism A B) (g : Morphism B C), 
    last1 (mapp f g) = codomain g.
  intros.
  unfold mapp.
  induction f.
  induction str.
  simpl.
  rewrite last_codomain.
  trivial.
  simpl.
  change (last1 (app_minus1 (mextract (morphism str)) (mextract g)) = codomain g).
  apply IHstr.
Defined.

(* composition、結果の型がMorphism A Cではない。 *)
Definition mcompose_aux (A B C : Object)
  (f : Morphism A B) (g : Morphism B C) : 
    Morphism (head1 (mapp f g)) (last1 (mapp f g))
      := << mapp f g >>.

(* 証明しておいたapp_head, app_lastで型を書き換える *)
Definition mcompose (A B C : Object)
  (f : Morphism A B) (g : Morphism B C) :
    Morphism A C :=
      match (app_head f g) in (_ = T) return Morphism T C with
        | refl_equal => 
          match (app_last f g) in (_ = U) return Morphism _ U with
            | refl_equal => mcompose_aux f g
          end
      end.

Notation "f ++ g" := (mcompose f g) (at level 68, left associativity) : shiritori_scope.

(* <<こぶたぬき>> *)
Eval compute in mcompose mkobuta mtanuki.
(* type error *)
(*
Eval compute in mkobuta ++ mkobuta.
*)

(* <<こぶた>> *)
Eval compute in mid こ ++ mkobuta.
(* <<こぶた>> *)
Eval compute in mkobuta ++ mid た.

Definition mkitsune := << き :: つ :: [ね] >>.
(* <<こぶたぬきつね>>、ただし型が読みにくい *)
Eval compute in mkobuta ++ mtanuki ++ mkitsune.
(* 単一化によって型を計算させることはできる *)
Let ktk : Morphism こ ね := mkobuta ++ mtanuki ++ mkitsune.
Eval compute in ktk.

End Shiritori.

オマケ: 別バージョンのmcompose

Section Shiritori.

Set Implicit Arguments.
(* 1要素以上のconsリスト *)
Inductive list1 (A : Type) : Type :=
  | singleton1 : A -> list1 A
  | cons1 : A -> list1 A -> list1 A.

(* singletonおよびconsのノーテーション *)
Notation "[ a ]" := (singleton1 a) : shiritori_scope.
Notation "a :: x" := (cons1 a x)(at level 60, right associativity) : shiritori_scope.
Open Scope shiritori_scope.

Section functions.
Variable A : Type.
(* 先頭を取ってくる関数 *)
Definition head1 (x : list1 A) : A :=
  match x with
  | [a] => a
  | a :: x' => a
  end.

(* 末尾を取ってくる関数 *)
Fixpoint last1 (x : list1 A) : A :=
  match x with
  | [a] => a
  | a :: x' => last1 x'
  end.

End functions.

(* 平仮名はKana型のコンストラクタ *)
Inductive Kana : Set :=
  | こ : Kana
  | ぶ : Kana
  | た : Kana
  | ぬ : Kana
  | き : Kana
  | つ : Kana
  | ね : Kana.

(* 文字列はKanaのリスト *)
Definition String1 := list1 Kana.

(* Object = Kana *)
Definition Object : Set := Kana.

(* Morphismは二つのオブジェクトをindexにもつ型で、
  各indexはコンストラクタに渡された文字列の先頭と末尾 *)
Inductive Morphism : Object -> Object -> Set :=
  morphism (str : String1) : Morphism (head1 str) (last1 str).

(* 文字列をMorphismにする表記 *)
Notation " << str >> " := (morphism str) : shiritori_scope.
Open Scope shiritori_scope.

(* domain, codomainは型のindex *)
Definition domain (A B : Object) (f : Morphism A B) : Object := A.
Definition codomain (A B : Object) (f : Morphism A B) : Object := B.

(* Morphismの中のStringを抽出 *)
Definition mextract (A B : Object) (f : Morphism A B) : String1 :=
  match f with
    morphism str => str
  end.

(* identity *)
Definition mid (A : Object) : Morphism A A :=
  << [A] >>.

(* composition *)
Definition mcompose (A B C : Object)
  (f : Morphism A B) (g : Morphism B C) : Morphism A C.
intros.
induction f.
induction str.
simpl.
simpl in g.
apply g.
simpl.
simpl in g.
assert (Morphism (head1 str) C).
apply IHstr.
apply g.
induction H.
apply (<< a :: str0 >>).
Defined.

(* 難解になりました *)
Print mcompose.
Notation "f ++ g" := (mcompose f g) (at level 68, left associativity) : shiritori_scope.

(* 文字列のこぶたとたぬき *)
Definition kobuta : String1 :=  (こ :: ぶ :: [た]).
Definition tanuki : String1 := (た :: ぬ :: [き]).

(* Morphismとしてのこぶたとたぬき *)
Definition mkobuta : Morphism こ た := << kobuta >>.
Definition mtanuki : Morphism た き := << tanuki >>.

(* <<こぶたぬき>> *)
Eval compute in mkobuta ++ mtanuki.
(* type error *)
(* Eval compute in mkobuta ++ mkobuta. *)

(* <<こぶた>> *)
Eval compute in mid こ ++ mkobuta.
(* <<こぶた>> *)
Eval compute in mkobuta ++ mid た.

Definition mkitsune := << き :: つ :: [ね] >>.
Definition mneko := << ね :: [こ] >>.
(* <<きつねこ>>、type annotationを書かないと型が読みにくい *)
Let mkitsuneko := mkitsune ++ mneko.
Eval compute in mkitsuneko.
(* 単一化によって型を計算させることはできる *)
Let mkitsuneko2 : Morphism き こ := mkitsuneko.
Eval compute in mkitsuneko2.

End Shiritori.