众所周之，一颗二叉树的定义是：
空的，或
一个元素，加上两颗二叉树树（一个结点）
Inductive Tree T :=
| Empty
| Node : Tree T -> T -> Tree T -> Tree T.
T可以是任何东西，比如说自然数，链表，字符串，另一个Tree等等．．．
那T可不可以是unit，不带有任何信息？换句话说，可不可能T的所有元素皆相等于一个常数？在此之下，Tree有没有意义？
Inductive Tree :=
| Empty
| Node : Tree -> Tree -> Tree.
当然可以！那没，既然树没有保留任何关于元素的信息，有什么意义？
尽管树不保存元素，就如同list unit并不是毫无意义，而是跟自然数同构一样，树自身的结构已经保留了一定的信息．
那这棵树有什么特别的地方吗？他跟一个结构有着很简单的同构关系（一一映射）．
跟他自己．不，跟7个他自己 ．换句话说，Tree~=Tree^7．
具体证明在Seven Trees in One at Steven Landsburg ，我们今天要试着把这个用Coq证明一遍．
我们先给出一个简写：
Notation "[ a , b ]" := (Node a b).
Notation "0" := Empty.
这里是把七棵树合并的定义：
Definition Combine_helper (T1 T2 T3 T4 T5 T6 T7 : Tree) : Tree :=
match (T1, T2, T3, T4) with
| (Empty, Empty, Empty, Empty) =>
match T5 with
| Node T5a T5b => [[[[Empty, T7], T6], T5a], T5b]
| Empty =>
match T6 with
| Node _ _ => [[[[[T6, T7], Empty], Empty], Empty], Empty]
| Empty =>
match T7 with
| [[[[T7a, T7b], T7c], T7d], T7e] =>
[[[[[Empty, T7a], T7b], T7c], T7d], T7e]
| _ => T7
end
end
end
| _ => [[[[[[T7, T6], T5], T4], T3], T2], T1]
end.
这个把七棵树分开：
Definition Split (T : Tree) :=
match T with
| [[[[[0, T7a], T7b], T7c], T7d], T7e] => (0, 0, 0, 0, 0, 0, [[[[T7a, T7b], T7c], T7d], T7e])
| [[[[[T6, T7], 0], 0], 0], 0] => (0, 0, 0, 0, 0, T6, T7)
| [[[[0, T7], T6], T5a], T5b] => (0, 0, 0, 0, [T5a, T5b], T6, T7)
| [[[[[[T7, T6], T5], T4], T3], T2], T1] => (T1, T2, T3, T4, T5, T6, T7)
| _ => (0, 0, 0, 0, 0, 0, T)
end.
这个是Combine_helper的wrapper：
Definition Combine X :=
match X with (t1, t2, t3, t4, t5, t6, t7) => Combine_helper t1 t2 t3 t4 t5 t6 t7 end.
接下来我们开始证明：
Goal forall T, Combine (Split T) = T.
intros; compute.
先做一点基本的简化 ．
这是Goal：
1 subgoal
T : Tree
______________________________________(1/1)
(let
(y, t7) :=
match T with
| 0 => (0, 0, 0, 0, 0, 0, T)
| [0, _] => (0, 0, 0, 0, 0, 0, T)
| [[0, _], _] => (0, 0, 0, 0, 0, 0, T)
| [[[0, _], _], _] => (0, 0, 0, 0, 0, 0, T)
| [[[[0, T4], T3], T2], T1] => (0, 0, 0, 0, [T2, T1], T3, T4)
| [[[[[0, T5], T4], T3], T2], T1] => (0, 0, 0, 0, 0, 0, [[[[T5, T4], T3], T2], T1])
| [[[[[[T7, T8] as T6, T5], 0 as T4], 0 as T3], 0 as T2], 0] => (0, 0, 0, 0, 0, T6, T5)
| [[[[[[T7, T8] as T6, T5], 0 as T4], 0 as T3], 0 as T2], [_, _] as T1] =>
(T1, T2, T3, T4, T5, T8, T7)
| [[[[[[T7, T8] as T6, T5], 0 as T4], 0 as T3], [_, _] as T2], T1] =>
(T1, T2, T3, T4, T5, T8, T7)
| [[[[[[T7, T8] as T6, T5], 0 as T4], [_, _] as T3], T2], T1] => (T1, T2, T3, T4, T5, T8, T7)
| [[[[[[T7, T8] as T6, T5], [_, _] as T4], T3], T2], T1] => (T1, T2, T3, T4, T5, T8, T7)
end in
let
(y0, t6) := y in
let
(y1, t5) := y0 in
let
(y2, t4) := y1 in
let
(y3, t3) := y2 in
let
(t1, t2) := y3 in
match t1 with
| 0 =>
match t2 with
| 0 =>
match t3 with
| 0 =>
match t4 with
| 0 =>
match t5 with
| 0 =>
match t6 with
| 0 =>
match t7 with
| 0 => t7
| [0, _] => t7
| [[0, _], _] => t7
| [[[0, _], _], _] => t7
| [[[[T7a, T7b], T7c], T7d], T7e] =>
[[[[[0, T7a], T7b], T7c], T7d], T7e]
end
| [_, _] => [[[[[t6, t7], 0], 0], 0], 0]
end
| [T5a, T5b] => [[[[0, t7], t6], T5a], T5b]
end
| [_, _] => [[[[[[t7, t6], t5], t4], t3], t2], t1]
end
| [_, _] => [[[[[[t7, t6], t5], t4], t3], t2], t1]
end
| [_, _] => [[[[[[t7, t6], t5], t4], t3], t2], t1]
end
| [_, _] => [[[[[[t7, t6], t5], t4], t3], t2], t1]
end) = T
当然，这道题可以用多次case analysis直接做出，不过内样太丑，我们试试看写一个tactic帮助我们做这件事：
Ltac match_context_destruct H :=
match H with
| context[match ?x with _ => _ end] =>
destruct x eqn:?
end.
Ltac match_destruct :=
match goal with
| H : _ |- _ => let HT := type of H in match_context_destruct HT
| |- ?H => match_context_destruct H
end.
现在可以试着证明：
Goal forall T, Combine (Split T) = T.
intros; compute.
repeat(match_destruct; trivial).
120 subgoals
T : Tree
p : Tree * Tree * Tree * Tree * Tree * Tree
t : Tree
Heqt0 : T = 0
p0 : Tree * Tree * Tree * Tree * Tree
t0 : Tree
p1 : Tree * Tree * Tree * Tree
t1 : Tree
p2 : Tree * Tree * Tree
t2 : Tree
p3 : Tree * Tree
t3, t4, t5 : Tree
Heqt6 : t4 = 0
Heqt1 : t5 = 0
Heqp4 : p3 = (0, 0)
Heqt2 : t3 = 0
Heqp3 : p2 = (0, 0, 0)
Heqt3 : t2 = 0
Heqp2 : p1 = (0, 0, 0, 0)
Heqt4 : t1 = 0
Heqp1 : p0 = (0, 0, 0, 0, 0)
Heqt5 : t0 = 0
Heqp0 : p = (0, 0, 0, 0, 0, 0)
t6_1, t6_2 : Tree
Heqt8 : t6_1 = 0
Heqt7 : t = [0, t6_2]
Heqp : (0, 0, 0, 0, 0, 0, 0) = (0, 0, 0, 0, 0, 0, [0, t6_2])
______________________________________(1/120)
[0, t6_2] = 0
match_destruct生成了很多等式，我们可以用subst进行替换，消除一大部分：
Goal forall T, Combine (Split T) = T.
intros; compute.
repeat(match_destruct; subst; trivial).
120 subgoals
t0_2 : Tree
Heqp : (0, 0, 0, 0, 0, 0, 0) = (0, 0, 0, 0, 0, 0, [0, t0_2])
______________________________________(1/120)
[0, t0_2] = 0
这个等式很明显不成立，用discriminate可以消除．
Goal forall T, Combine (Split T) = T.
intros; compute.
repeat(discriminate||match_destruct; subst; trivial).
16 subgoals
t0_2, t0_3 : Tree
Heqp : (0, 0, 0, 0, 0, 0, [0, t0_2]) = (0, 0, 0, 0, 0, 0, [0, t0_3])
______________________________________(1/16)
[0, t0_3] = [0, t0_2]
discriminate是廉价操作，所以智能度不高，有一定的等式不能否证，可以用congruence．
Goal forall T, Combine (Split T) = T.
intros; compute.
repeat(congruence||match_destruct; subst; trivial).
Qed.
这下过了，然而很慢，我们可以通过ltac match避免使用congruence来提速．
Goal forall T, Combine (Split T) = T.
intros; compute.
repeat(
match goal with H : _ = _ |- _ =>
inversion H; subst end ||
match_destruct;
subst;
trivial).
Qed.
这下ltac再次进入死循环，我们如果单步执行，我们会发现同一等式被inversion多次．因为inversion不会丢失信息，我们可以在inversion后clear：
Goal forall T, Combine (Split T) = T.
intros; compute.
repeat(
match goal with H : _ = _ |- _ =>
inversion H; subst; clear H end ||
match_destruct;
subst;
trivial).
Qed.
这下ltac再次进入死循环，单步执行后发现有的时候inversion会产生一个一模一样的新等式，所以我们要减小match的成功率：
Goal forall T, Combine (Split T) = T.
intros; compute.
repeat(
match goal with H : (_,_) = (_,_) |- _ =>
inversion H; subst; clear H end ||
match_destruct;
subst;
trivial).
Qed.
很好，过了．
Goal forall T, Split (Combine T) = T.
intros; compute.
repeat(
match goal with H : (_,_) = (_,_) |- _ => inversion H; subst; clear H end ||
match goal with H : [_,_] = [_,_] |- _ => inversion H; subst; clear H end ||
discriminate ||
match_destruct;
subst;
trivial).
Qed.
如发炮制，除了要多加一个match．
inversion, subst, clear三连击经常出现，所以我们可以重构成单一tactic．
最终代码：
Set Implicit Arguments.
Inductive Tree :=
| Empty
| Node : Tree -> Tree -> Tree.
Notation "[ a , b ]" := (Node a b).
Notation "0" := Empty.
Definition Combine_helper (T1 T2 T3 T4 T5 T6 T7 : Tree) : Tree :=
match (T1, T2, T3, T4) with
| (0, 0, 0, 0) =>
match T5 with
| Node T5a T5b => [[[[0, T7], T6], T5a], T5b]
| 0 =>
match T6 with
| Node _ _ => [[[[[T6, T7], 0], 0], 0], 0]
| 0 =>
match T7 with
| [[[[T7a, T7b], T7c], T7d], T7e] =>
[[[[[0, T7a], T7b], T7c], T7d], T7e]
| _ => T7
end
end
end
| _ => [[[[[[T7, T6], T5], T4], T3], T2], T1]
end.
Definition Split (T : Tree) :=
match T with
| [[[[[0, T7a], T7b], T7c], T7d], T7e] => (0, 0, 0, 0, 0, 0, [[[[T7a, T7b], T7c], T7d], T7e])
| [[[[[T6, T7], 0], 0], 0], 0] => (0, 0, 0, 0, 0, T6, T7)
| [[[[0, T7], T6], T5a], T5b] => (0, 0, 0, 0, [T5a, T5b], T6, T7)
| [[[[[[T7, T6], T5], T4], T3], T2], T1] => (T1, T2, T3, T4, T5, T6, T7)
| _ => (0, 0, 0, 0, 0, 0, T)
end.
Definition Combine X :=
match X with (t1, t2, t3, t4, t5, t6, t7) => Combine_helper t1 t2 t3 t4 t5 t6 t7 end.
Ltac match_context_destruct H :=
match H with
| context[match ?x with _ => _ end] =>
destruct x eqn:?
end.
Ltac match_destruct :=
match goal with
| H : _ |- _ => let HT := type of H in match_context_destruct HT
| |- ?H => match_context_destruct H
end.
Ltac invcs H := inversion H; subst; clear H.
Goal forall T, Combine (Split T) = T.
intros; compute.
repeat(
match goal with H : (_,_) = (_,_) |- _ => invcs H end ||
match_destruct;
subst;
trivial).
Qed.
Goal forall T, Split (Combine T) = T.
intros; compute.
repeat(
match goal with H : (_,_) = (_,_) |- _ => invcs H end ||
match goal with H : [_,_] = [_,_] |- _ => invcs H end ||
discriminate ||
match_destruct;
subst;
trivial).
Qed.
这样，就没什么亮点地完成了任务． 在续集，我们会在此代码上玩很好玩的东西，敬请期待（雾
本系列上，完！