Coq中无需良基递归实现K树到二叉树的编码函数

问题背景 #

先给出Coq中二叉树和多分支树（K树）的标准定义（为简化处理，硬编码使用nat类型）：

Inductive bintree : Type :=
  | Leaf : bintree
  | Node : bintree -> nat -> bintree -> bintree.

Inductive tree :=
  | TNode : nat -> list tree -> tree.

目标是定义函数encode : tree -> bintree，将多分支树转换为包含相同节点的二叉树，后续还要实现decode : bintree -> tree并证明forall t, decode (encode t) = t等性质。

一种简单的编码思路是：将节点为x、子节点列表为ts的多分支树，编码为一棵二叉树——其左子树是ts中左子节点的编码结果，右子树是x右侧相邻节点的编码结果。对应的Haskell实现如下：

data Tree a = TNode a [Tree a]
data BinTree a = Leaf | BNode (BinTree a) a (BinTree a)

encode :: Tree a -> BinTree a
encode t = go [t]
 where
  go [] = Leaf
  go ((TNode x ts) : ts') = BNode (go ts) x (go ts')

直接定义的问题 #

尝试在Coq中编写类似的递归定义时，会出现合法性错误：

Fixpoint encode_list (l: list ntree) :=
  match l with
    | [] => Leaf
    | (TNode x ts) :: ts' => Node (encode_list ts) x (encode_list ts')
  end.

报错信息：

Error: Recursive definition of encode_list is ill-formed.
(* ... *)
Recursive call to encode_list has principal argument equal to "ts" instead of "ts'".
Recursive definition is:
"fun l : list tree =>
 match l with
 | [] => Leaf
 | t :: ts' =>
     match t with
     | TNode x ts => Node (encode_list ts) x (encode_list ts')
     end
 end".

尽管ts和ts'都是输入列表l的严格子项，但Coq的结构递归启发式规则无法识别这一点，因此拒绝该定义。

双参数递归尝试的失败 #

我尝试过另一种思路，通过同时遍历当前节点和其右侧兄弟节点列表来定义编码函数，但同样无法通过Coq的递归检查：

(* ns : right siblings of t *)
Fixpoint encode' (t: tree) (ns: list tree) :=
  let '(TNode x cs) := t in
    match cs, ns with
      | [], [] => Node Leaf x Leaf
      | [], n :: ns' => Node Leaf x (encode' n ns')
      | c :: cs', [] => Node (encode' c cs') x Leaf
      | c :: cs', n :: ns' => Node (encode' c cs') x (encode' n ns')
    end.

(* Error: Cannot guess decreasing argument of fix. *)
(* Definition encode (t: tree) = encode' t []. *)

Coq无法自动推断出哪个参数是递减的，因此该定义无效。

基于良基递归的可行实现 #

最终我通过Program Fixpoint结合树列表的总节点数作为度量（measure），成功定义了编码函数，完整代码如下：

Require Coq.Program.Wf.
Require Import Lia.

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Inductive bintree (A: Type) : Type :=
  | Leaf : bintree A
  | Node : bintree A -> A -> bintree A -> bintree A.

Inductive tree (A: Type) :=
  | TNode : A -> list (tree A) -> tree A.

Definition ntree := tree nat.

Arguments Leaf {A}.
Arguments TNode [A].

Fixpoint n_nodes (t: ntree) :=
  let '(TNode n ns) := t in
  let fix n_nodes_list (l: list ntree) :=
    match l with
      | [] => 0
      | x :: xs => n_nodes x + n_nodes_list xs
    end
  in 1 + n_nodes_list ns.

Fixpoint sum_n_nodes (l: list ntree) :=
  match l with
    | [] => 0
    | t :: ts => n_nodes t + sum_n_nodes ts
  end.

Program Fixpoint encode_list (l: list ntree) {measure (sum_n_nodes l)} :=
  match l with
    | [] => Leaf
    | (TNode x ts) :: ts' => Node (encode_list ts') x (encode_list ts)
  end.

Next Obligation.
destruct ts'; simpl; lia.
Defined.

Next Obligation.
destruct ts.
simpl; lia.
simpl sum_n_nodes at 1.
replace (sum_n_nodes (TNode x (t :: ts) :: ts')) with (1 + n_nodes t + sum_n_nodes ts + sum_n_nodes ts') at 1 by reflexivity.
lia.
Defined.

Definition encode (l: ntree) := encode_list [l].

疑问 #

目前的实现依赖于良基递归，我想了解：是否可以不使用良基递归，仅通过嵌套fix的技巧来完成这个编码函数的定义？

内容的提问来源于stack exchange，提问作者shooqie