在七树归一（上）里 ，我们成功地找出了同构关系，并且作出证明，最后再对所有东西进行了重构，看似完美结束了．然而要玩，还是有地方能重构的．
比如说，我们的核心定义，
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.
尽管不长，然而信息量很大，而且杂乱无章，只读不可写，如果不是我们已经证明了正确性，我们又对这团代码的正确性有几成把握？谁又可以从这些代码后面学习到什么？
然而这就是定义．定义就如此，该怎么写才能提供更高的可读性？
很简单，不写．
正如同无招胜有招一样，无代码胜有代码．如果我们能让机械按照我们的需求生成符合需求的代码，我们为什么要理解生成的东西？需求，程序生成器，有的时候可比根据奇怪的需求生成的ad-hoc代码好理解多了．
我们今天，要写出一个ad-hoc的程序生成器，然后用来生成Split，降低代码的ad-hoc度－注意，尽管程序生成器同样是ad-hoc的，但是可读性比Split好很多．
我们先把Split改成Strong Specification的，这样只要定义出来了，就不会错．
Definition Split_helper(T : Tree) :
{ T1 : Tree &
{ T2 : Tree &
{ T3 : Tree &
{ T4 : Tree &
{ T5 : Tree &
{ T6 : Tree &
{ T7 : Tree | Combine_helper T1 T2 T3 T4 T5 T6 T7 = T } } } } } } }.
1 subgoal
T : Tree
______________________________________(1/1)
{T1 : Tree &
{T2 : Tree &
{T3 : Tree &
{T4 : Tree &
{T5 : Tree &
{T6 : Tree &
{T7 : Tree |
Combine_helper T1 T2 T3 T4 T5 T6 T7 = T}}}}}}}
我们接下来对Goal进行基本的简化．
repeat econstructor; compute.
1 subgoal
T : Tree
______________________________________(1/1)
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
到达一个很眼熟的地方，与以前的最大不同是，我们match里的，是existential variable（evar），我们可以给予之一个合理的值．然而要给什么？
如果我们手动地输入evar的值，我们跟以前的手动定义Split大同小异－信息只是存在proof script了，并没有改变信息很ad hoc的事实．
所幸Coq8.5中tactic有backtracking功能，可以用来让Coq搜索出正确算法．
我们这下要怎么做变得简单起来：
- 找出一个match内的existential variable
- 分两个branch，一个branch把该元素unify为Empty，一个branch生成两个evar，再把该元素unify为Branch ? ?
- 如果能用基础tactic证明正确性，这样做
- 循环往复
找出一个match内的existential variable
Ltac get_goal :=
match goal with
| |- ?x => x
end.
Ltac get_match H F :=
match H with
| context [match ?n with _ => _ end] => F n
end.
get_match ltac:get_goal ltac:(fun x => x)
分两个branch，
Ltac act := let res := get_match ltac:get_goal ltac:(fun x => x) in l res + r res.
一个branch把该元素unify为Empty，
Ltac l T := unify T Empty; simpl in *.
一个branch生成两个evar，再把该元素unify为Branch ? ?
Ltac r T :=
let lt := fresh in
let rt := fresh in
evar (lt : Tree); evar (rt : Tree); unify T (Node lt rt); simpl in *.
如果能用基础tactic证明正确性，这样做，循环往复
solve [repeat (trivial; act)].
Error: No applicable tactic.
对面不动如山．．．
我们试下debug
try solve [repeat (trivial; act); let g := get_goal in idtac g].
(0 = T)
([0, ?H0] = T)
([[0, ?t0], ?H0] = T)
([[[0, ?t2], ?t0], ?H0] = T)
([[[[[0, ?t], ?t3], ?t2], ?t0], ?H0] = T)
([[[[[[?H, ?H0], ?T7], 0], 0], 0], 0] = T)
([[[[0, ?T7], ?T6], ?H], ?H0] = T)
([[[[[[?T7, ?T6], ?T5], [?H, ?H0]], 0], 0], 0] = T)
([[[[[[?T7, ?T6], ?T5], ?T4], [?H, ?H0]], 0], 0] = T)
([[[[[[?T7, ?T6], ?T5], ?T4], ?T3], [?H, ?H0]], 0] = T)
([[[[[[?T7, ?T6], ?T5], ?T4], ?T3], ?T2], [?H, ?H0]] = T)
可以看到，我们需要对表达式的右面进行分析－这无可厚非，我们这个函数要用Tree生成7个符合的Tree，我们不对传入的Tree做分析，难不成返回常数？
当然，这颗Tree需要多次destruct，我们对他手动分析也很low，还是想想办法写一个Tactic搞清要对什么进行destruct．
try solve
[
repeat (trivial; act);
let g := get_goal in match g with _ = ?x => idtac x end
].
T
T
T
T
T
T
T
T
T
T
T
很接近了，然而现在有一个致命问题：我们现在只能执行代码，并不能进行任何返回．
我们也不能现在对T进行destruct，因为destruct了的生成物并不在evar的context内，destruct了也无法使用．我们现在进入一个两难：我们要在econstructor之前用destruct，然而要知道destruct什么，只能先用econstructor!
解开这个难题并不是不可能，我们只需要写一个
- 写一个Tactic，在Goal中加入需要的信息，除此之外并无任何副作用．
- 用该Tactic后，对该信息destruct
- 判断还是否需要再用该Tactic destruct，如果不需要，我们用我们本文上面的已有tactic完成任务．
写一个Tactic，在Goal中加入需要的信息，除此之外并无任何副作用．
这点是唯一困难的地方，其他的都没有难度，然而我们如何在Goal中加入需要的信息？我们又如何加入信息后取消一切动作？
后者其实不难，我们只需要assert(False->original_conclusion)则可．
至于前者，我们可以再次使用existential variable：我们创建新的evar，然后我们在assert内进行任意探索，最后unify该evar，退出assertion，清除assertion，就可以天衣无缝地取得我们所需的元素！
我们照着这个intuition，定义一个频道，用于传递信息，再定义一个沙盒，用于随意进行探索．
Definition channel P NT (N : NT) : Type := P.
Ltac set_result N T := match goal with | _ := ?X : channel _ N |- _ => unify X T end.
Ltac get_result N := match goal with | _ := ?X : channel _ N |- _ => X end.
Ltac clear_result N := match goal with | H := _ : channel _ N |- _ => clear H end.
Inductive sandbox_closer : Prop := ms : sandbox_closer -> sandbox_closer.
Theorem sandbox_closer_exit : sandbox_closer -> False. induction 1;trivial. Qed.
Arguments channel : simpl never.
Ltac make_sandbox T N :=
let f := fresh in
evar (f : channel T N);
let g := get_goal in
let H := fresh in
assert(sandbox_closer -> g) as H;[intro|clear H].
Ltac exit_sandbox :=
exfalso;
match goal with
| X : sandbox_closer |- _ => apply sandbox_closer_exit in X;tauto
end.
很好，现在我们定义主要的部件：
Ltac prepare_work := repeat econstructor; compute.
Ltac work :=
prepare_work;
solve [repeat (trivial; compute; act)].
Ltac get_destruct_next N :=
prepare_work;
repeat act; repeat f_equal;
match goal with
|- _ = ?X => is_var X; set_result N X
end.
Ltac detect_destruct :=
make_sandbox Tree tt;
[
get_destruct_next tt;
exit_sandbox|
];
let ret := get_result tt in destruct ret;
clear_result tt.
现在我们清空一切proof script，直接用repeat (work||detect_destruct)：
All the remaining goals are on the shelf:
Tree
Tree
Tree
Tree
Tree
Tree
Tree
很好．最后那7个remaining goals，经过拆开repeat，debug后可发现，纯属exit_sandbox时有evar存在，因为一切行动都会被清除（除了set_result），我们直接unify为Empty：
Ltac detect_destruct :=
make_sandbox Tree tt;
[
get_destruct_next tt;
repeat match get_goal with context [?t] => is_evar t; l t end;
exit_sandbox|
];
let ret := get_result tt in destruct ret;
clear_result tt.
再运行一次script，我们就成功地让Coq找出正确的算法．
证明反向的七树归一无任何新意，就不贴上来了．
最终代码在Coq_code/seven_trees_in_one.v at master · lolisa/Coq_code · GitHub．