しりとりの圏をCoqで実装してみた

Coq 圏論 しりとりの圏 Set Implicit Arguments Inductive Qed Defined

Coq で しりとりの圏を形式化した記事を見つけた。
型によるしりとりの成立判定 - コンピュータってすごいらしい
via 完全実装付きでもう一度お送りします、しりとりの圏 - 檜山正幸のキマイラ飼育記

すばらしかったので、私もちょっと真似して実装してみた。亜鉛さんと同様に依存型を使ったのでしりとりが可能なときにのみ定義される合成(composition)をいい感じに実装できた。依存型グレイト！

comp関数は依存型が複雑で直接定義する事が難しかったので型だけ宣言してあとから証明木をtacticで作って実装した。
ただ、最後にQed.としてしまうと隠蔽されちゃってunfoldとかができなくなるみたい(http://www.lix.polytechnique.fr/coq/distrib/current/refman/Reference-Manual009.html#@default423 の6.9.1Opaque 参照)だったのでDefined.で締めくくる必要があるみたいだった(このことは依存型を扱う上で重要そうだが、今まで知らなかった)。

(**
  Shiritori Category
*)

Set Implicit Arguments.

(* 対象 object *)
Inductive Obj : Set := こ | ぶ | た | ぬ | き | つ | ね.

(* 射 morphism *)
Inductive Mor : Obj -> Obj -> Set :=
  | single : forall A, Mor A A
  | cons : forall A' B (A: Obj) (tl: Mor A' B), Mor A B.

(* 合成 composition *)
Definition comp A B C (f: Mor A B) (g: Mor B C) : Mor A C.
 intros. induction f.
 exact g.
 exact (cons A (IHf g)).
Defined.

(* 恒等射 identity *)
Definition id A : Mor A A := single A.

(* 単位元律 unit law 01 *)
Theorem unit_l : forall (A B: Obj) (f: Mor A B), comp (id A) f = f.
Proof.
  intros; simpl.
  reflexivity.
Qed.

(* 単位元律 unit law 02 *)
Theorem unit_r : forall (A B: Obj) (f: Mor A B), comp f (id B) = f.
Proof.
 intros.
 induction f.
  simpl.
  reflexivity.
  simpl.
  rewrite IHf.
  reflexivity.
Qed.

(* 結合律 associative low *)
Theorem assoc : forall A B C D (f: Mor A B) (g: Mor B C) (k: Mor C D),
  comp f (comp g k) = comp (comp f g) k.
Proof.
 intros.
 induction f.
  simpl.
  reflexivity.
  simpl.
  rewrite IHf.
  reflexivity.
Qed.

(* 合成のテスト *)
Definition w1 := cons こ (cons ぶ (single た)).
Definition w2 := cons た (cons ぬ (single き)).
Eval compute in comp w1 w2.

Coq の 応答 (Coq version 8.1pl2)

     = cons こ (cons ぶ (cons た (cons ぬ (single き))))
     : Mor こ き