(続) Seven trees

[註] この記事には解答はありませんが，Coq の証明が読める人にはヒントになってしまうかもしれません．[追記] 解答の公開が解禁されたそうなので遅ればせながら公開致します．Blassのものと同じ定義なのであまり参考にならないと思います．

id:kikx さんが Seven trees 問題の解答を Coq で証明されているようなのでこちらも確認してみました．

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

Inductive tree7 : Set :=
| Seven : tree -> tree -> tree -> tree -> tree -> tree -> tree -> tree7.

Definition seven2one (ts:tree7) : tree := match ts with
| Seven Leaf Leaf Leaf Leaf Leaf Leaf
  (Node (Node (Node (Node t1 t2) t3) t4) t5)
  => Node (Node (Node (Node (Node Leaf t1) t2) t3) t4) t5
| Seven Leaf Leaf Leaf Leaf Leaf Leaf t
  => t
| Seven Leaf Leaf Leaf Leaf Leaf t1 t2
  => Node (Node (Node (Node (Node t1 t2) Leaf) Leaf) Leaf) Leaf
| Seven Leaf Leaf Leaf Leaf (Node t1 t2) t3 t4
  => Node (Node (Node (Node Leaf t4) t3) t1) t2
| Seven t1 t2 t3 t4 t5 t6 t7
  => Node (Node (Node (Node (Node (Node t7 t6) t5) t4) t3) t2) t1
end.

Definition one2seven (t:tree) : tree7 := match t with
| Node (Node (Node (Node (Node (Node t1 t2) t3) Leaf) Leaf) Leaf) Leaf
  => Seven Leaf Leaf Leaf Leaf Leaf (Node t1 t2) t3
| Node (Node (Node (Node (Node (Node t1 t2) t3) t4) t5) t6) t7
  => Seven t7 t6 t5 t4 t3 t2 t1 
| Node (Node (Node (Node (Node Leaf t1) t2) t3) t4) t5
  => Seven Leaf Leaf Leaf Leaf Leaf Leaf
           (Node (Node (Node (Node t1 t2) t3) t4) t5)
| Node (Node (Node (Node Leaf t1) t2) t3) t4
  => Seven Leaf Leaf Leaf Leaf (Node t3 t4) t2 t1
| t
  => Seven Leaf Leaf Leaf Leaf Leaf Leaf t
end.

Theorem one2one : forall (t:tree), seven2one (one2seven t) = t.
Proof.
intro.
destruct t as[|[|[|[|[|[|??]?][|??]][|??]][|??]][|?]];auto.
Qed.

Theorem seven2seven : forall (t:tree7), one2seven (seven2one t) = t.
Proof.
intro.
destruct t as[[|][|?][|??][|??][|??][|??][|[|[|[|]]]]];auto.
Qed.

Coq の証明でまでゴルフしたくなるのはもう病気ですね．