如何移除Coq中Fixpoint定义的maxIter参数？

问题描述 #

定义如下树类型：

Inductive tree : Set :=
  | Node : list tree -> tree.

现有如下函数定义，靠maxIter参数保证被Coq接受：

Fixpoint getThemAll_aux (trees: list tree) (maxIter:nat): list tree :=
 
  match maxIter with
   | O => nil
   | S n => 
       match trees with
             | nil => nil
             | xx::rest =>  let newCandidates := generateCandidates xx in
                                  let newRest := addAllIfDifferent tree eq_tree newCandidates rest in 
                                     addAllIfDifferent tree eq_tree newCandidates (getThemAll_aux newRest n)
       end
    end.

Definition getThemAll (seed:tree) : list tree :=
    getThemAll_aux (seed::nil) 999.

已完成以下证明：

• generateCandidates生成的每个树，其Node数量与输入树相同
• eq_tree和addAllIfDifferent符合预期语义（实现去重添加逻辑）
  且此时函数必然终止。请问能否移除maxIter参数？

解答 #

可以移除maxIter参数，但不能直接写成普通Fixpoint——因为Coq的普通递归要求调用必须针对严格子结构，而newRest并非trees的严格子结构（甚至可能更长），Coq会直接拒绝这种定义。需要借助良基递归结合你已有的证明来让Coq认可终止性，具体做法如下：

方法1：使用Program Fixpoint配合度量与终止性证明 #

首先定义一个用于衡量递归参数“大小”的度量函数，比如基于树的Node数量总和：

Fixpoint size_tree (t : tree) : nat :=
  match t with
  | Node ts => 1 + sum (map size_tree ts)
  end.

Definition size_treelist (ts : list tree) : nat :=
  sum (map size_tree ts).

然后用Program Fixpoint定义函数，并附加度量约束：

Program Fixpoint getThemAll_aux (trees: list tree) {measure (size_treelist trees)} : list tree :=
  match trees with
  | nil => nil
  | xx::rest => 
      let newCandidates := generateCandidates xx in
      let newRest := addAllIfDifferent tree eq_tree newCandidates rest in 
      addAllIfDifferent tree eq_tree newCandidates (getThemAll_aux newRest)
  end.

此时Coq会生成一个证明义务，要求你证明size_treelist newRest < size_treelist (xx::rest)。你可以利用已有的引理（比如generateCandidates生成的树与输入树大小一致、addAllIfDifferent仅添加不重复的树）来完成这个终止性证明。

方法2：基于已处理树集合的良基递归 #

如果更适合你的场景，也可以用“已处理过的独特树的数量”作为度量：维护一个已处理树的集合，每次递归时这个集合的大小严格递增（因为只添加新树），而自然数的严格小于关系是良基的。同样需要结合你的引理完成终止性证明。

总之，移除maxIter的核心是给Coq提供一个明确的“递归参数在每次调用中都会按良基关系变小”的证明，而你已有的结论正好可以支撑这个证明。

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