dramforever

coding, thoughts and stuff irl

七树归一

2016-02-10

(2015-02-12:代码已经修改,本文以 tag seven-trees-blog 为准)

(本文假定读者有一定程度 Coq 基础)

代码在代码仓库中的 seven_trees.vseven_trees.cppMakefile 很可能也有用。

我们如下定义“(无标记)二叉树” \(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 familiesGeneralized 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]\)...,每个格子里可以放任意多个棋子(可以不放),每步可以进行下列两个操作之一:

  1. combine:从 \(A[k-1]\) 和 \(A[k+1]\) 各取走一个棋子,在 \(A[k]\) 放上一个棋子
  2. 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 的解决办法,但是毕竟很好地体现了思考的过程:

另外,拿程序生成这个证明,好像能带来一种诡异的喜悦。