机上の計算ではできたものの

http://d.hatena.ne.jp/m-hiyama/20081022/1224640248
http://d.hatena.ne.jp/ku-ma-me/20081023

最近はやりの Seven Trees を解いてみた。
机上の計算ではできたっぽいのだが、やはり自信がない。
まめっちはいい加減にテストをしていたみたいだが、やはり総当りでないと心配なので書いてみた。

Section SevenTree.

Inductive Tree : Set :=
  | Leaf
  | Node : Tree -> Tree -> Tree.

Inductive Tree7 : Set :=
  | T7 : Tree -> Tree -> Tree -> Tree ->
          Tree -> Tree -> Tree -> Tree7.

Definition f (ts : Tree7) : Tree :=
match ts with
(* ひみつ *)
end.

Definition g (t : Tree) : Tree7 :=
match t with
(* ひみつ *)
end.

Theorem fg_id : forall t, f (g t) = t.
Proof.
intros.
destruct t; auto.
destruct t2; auto.
destruct t2_2; auto.
destruct t2_2_2; auto.
destruct t2_2_2_2; auto.
destruct t2_2_2_1; auto.
destruct t2_2_2_1_2; auto.
destruct t2_2_2_1_2_2; auto.
destruct t2_2_2_1_2_2_2; auto.
destruct t2_2_2_2_2; auto.
Qed.

Theorem gf_id : forall t, g (f t) = t.
Proof.
intros.
destruct t; auto.
destruct t; auto.
destruct t0; auto.
destruct t1; auto.
destruct t2; auto.
destruct t3; auto.
destruct t4; auto.
destruct t5; auto.
destruct t5_2; auto.
destruct t5_2_2; auto.
destruct t5_2_2_2; auto.
Qed.

End SevenTree.

場合わけ多すぎだろ。なんか聞くところによると５種類でいいらしいのだが…。