（2015-02-12：代码已经修改，本文以 tag seven-trees-blog 为准）
（本文假定读者有一定程度 Coq 基础）
代码在代码仓库中的 seven_trees.v 和 seven_trees.cpp。Makefile 很可能也有用。
我们如下定义“（无标记）二叉树” \(T\)：
为了下面方便，我把它的定义写成了 \(T = 1 + T^2\) 的形式。
Inductive tree : Set := mk_tree (x : unit + tree * tree).有一个经典的定理如下：在 \(T^7\) 和 \(T\) 之间存在一个 \(O(1)\) 的同构（其中乘方使用笛卡尔积），我们来证明它。
当然，我们可以对应的两个函数，然后对输入做分类讨论来解决这个问题。（不用归纳法，因为函数是 \(O(1)\) 的）但是这样说起来容易做起来难，比如，大家可以欣赏一下左边到右边的函数：（摘自 The Dairy of Marisa）（然而我并没有那个功夫把它适配到我那个定义上。）
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.尽管不长，然而信息量很大，而且杂乱无章，只读不可写，如果不是我们已经证明了正确性，我们又对这团代码的正确性有几成把握？谁又可以从这些代码后面学习到什么？
所以，我们就不要写两个函数了。
不，一个函数也别写了。
不，也不让程序生成函数了。
还有办法么？
既然我们要得到一个同构，而且我们怕写出的两个函数不是正好对应的，我们就拿着同构关系玩好了。
(* iso A B: Types A and B are isomorphic *)
Definition iso (A B : Set) : Prop :=
exists (fw : A -> B) (bw : B -> A),
(forall x, fw (bw x) = x) /\ (forall x, bw (fw x) = x).接下来，我写了一个叫 iso的 tactic，用于处理一些简单的需要得到同构关系的定理。
(* ... *)
Ltac iso := dintuition; de_iso; mk_iso; work_iso.嗯，同构关系有什么性质呢？看到刚刚我写的 \(T = 1 + T^2\)，你可能已经想到了，“类型可以做加法和乘法”。将其形式化，就是：类型在同构意义下构成一个半环（semiring）。Coq 有一个 tactic 叫 ring，我们来告诉 ring 这一点。如果想了解更多的话，可以看看 Coq Reference Manual 中的 The ring and field tactic families 和 Generalized rewriting。
(* ... *)
Definition iso_ring_theory : semi_ring_theory Empty_set unit sum prod iso.
iso. Qed.
Add Ring iso_ring : iso_ring_theory.这样我们遇到像 iso (A + B + C + D) (A + (B + C) + D) 这样的目标的时候就可以直接使用 ring 搞定了, 而且还可以对 iso 这个 setoid 使用 rewrite。
所以呢？我们就是要从：
Lemma iso_tree : iso tree (unit + tree * tree).
Proof.
(* ... *)
Qed.推出：
Theorem seven_trees : iso (tree^7) (tree^1).哎呀，差点忘了这个了：
Fixpoint exps (T : Set) (n : nat) : Set :=
match n with
| 0 => unit
| S n' => (exps T n') * T
end.
Infix "^" := exps (at level 30, right associativity).在这个演讲稿中（被墙），给出了这样一个看似废话的引理：
Lemma tree_split : forall n, iso (tree^S n) (tree^n + tree^S (S n)).
intro.
simpl.
rewrite iso_tree at 2.
ring.
Qed.然后呢？然后我们就可以把目标一直保持为左右两边都是若干个 tree 的幂的和，如 iso (tree^6 + tree^8) (tree^0 + tree^2)。
作者还给了一个非常有意思的看这个问题的角度：
有格子 \(A[0]\), \(A[1]\), \(A[2]\)...，每个格子里可以放任意多个棋子（可以不放），每步可以进行下列两个操作之一：
- combine：从 \(A[k-1]\) 和 \(A[k+1]\) 各取走一个棋子，在 \(A[k]\) 放上一个棋子
- split：从 \(A[k]\) 取走一个棋子，在 \(A[k-1]\) 和 \(A[k+1]\) 各放上一个棋子
要求：不能从没有棋子的格子取；不能把棋子放到负数格子去（两句废话不是么）
Task: 初始有且仅有一个棋子在 \(A[1]\)，进行若干次操作使其“到达” \(A[7]\) （最终有且仅有一个棋子在 \(A[7]\)）
\(A[k]\) 上有 \(n\) 个棋子，代表 tree^k 有 \(n\) 项。解决这个游戏，我们就证明了七树归一。那这个游戏怎么办呢？
嗯，搜索树是无穷的，就 BFS 吧。
状态用每一项的指数表示就好了。判重就先排序一下，再用哈希表。
初始状态和最终状态都比较简单，提示我们使用双向 BFS。这样做的话，我们就从 7 和 1 两边开始 split（多进行 split 不会影响 combine 的可行性，所以不会丢失解）。这样做一不小心有个巨大的好处：split 比 combine 简单多了。
首先，在搜索的时候我们就不需要找到一对 \(k-1\) 和 \(k+1\)，而是只要找一个正的 \(k\)；更重要的是，我们生成证明脚本的时候，不需要把 tree^(k-1) + tree^(k+1) 分离出来，而是直接 rewrite (tree_split (k-1)) at 1。（是的，项的顺序和 + 的括号情况也不重要，因为只要有 tree^k 这一项，rewrite 就能把它搞定。）
7 那边 split 完，来个 symmetry，再做 1 这边的 split，最后 ring 收尾。
要启发式搜索吗？经鉴定不需要。我只是优先考虑项个数少的状态，就很快出解了，而本来生成状态的就是项个数从小到大的顺序的。（因为我们是 BFS，每次 split 后项个数 +1）
完工，代码共 103 行 Coq 和 142 行 C++。这个绝对远多于直接拿两个函数证明，而且也是一个 ad hoc 的解决办法，但是毕竟很好地体现了思考的过程：
另外，拿程序生成这个证明，好像能带来一种诡异的喜悦。