能否通过参数规模缩减证明让Coq接受一类Fixpoint函数？

你定义了任意元数的树结构：

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

用Fixpoint能正常定义节点计数函数，因为递归调用直接作用于原树的子节点列表，Coq能自动验证这些子节点结构更小，满足终止性要求：

Fixpoint nodecount (tree: Tree ) : nat :=
    match tree with
     | Node trs => S (sum (map nodecount trs))
    end.

但用Function加filter时，哪怕是恒真过滤，Coq也报错——因为filter返回的列表元素，Coq无法自动确认其结构一定小于原树，默认不允许这类递归调用。

可行解决思路：提供终止性证明 #

你可以通过指定递归度量+证明递归调用参数的递减性，让Coq接受这类函数。具体步骤如下：

1. 导入依赖库
   确保导入List和Arith库，用到sum、filter以及自然数相关的证明工具：

Require Import List Arith.

2. 定义树的大小度量
   用一个函数表示树的大小（和你写的nodecount逻辑一致），作为终止性的判断依据：

Fixpoint treesize (t : Tree) : nat :=
  match t with
  | Node ts => S (sum (map treesize ts))
  end.

3. 证明关键引理
   需要证明：过滤后的列表中，任意元素的大小都小于原树（Node trs）的大小：

Lemma filter_subsize : forall (P : Tree -> bool) (ts : list Tree) (t : Tree),
  In t (filter P ts) -> treesize t < treesize (Node ts).
Proof.
  intros P ts t H.
  unfold treesize.
  rewrite sum_cons, Nat.add_comm; simpl.
  apply Nat.lt_succ_r.
  induction ts as [|t' ts' IH]; simpl in H.
  - inversion H.
  - destruct (P t') eqn:HP.
    + left; assumption.
    + right; apply IH; assumption.
Qed.

4. 带证明的递归函数定义
   用Function定义函数时，通过{measure treesize tree}指定终止度量，然后在生成的证明义务中，用上面的引理完成证明：

Function nodecount' (tree: Tree ) : nat {measure treesize tree} :=
    match tree with
     | Node trs => S (sum (map nodecount' ( filter ( fun x => true) trs)))
    end.
Proof.
  intros tree trs Heq.
  unfold treesize in Heq.
  rewrite Heq.
  apply filter_subsize with (P := fun x => true).
  simpl.
  intro t.
  rewrite filter_true; auto.
Qed.

核心逻辑 #

Coq要求所有递归函数必须终止，Fixpoint只支持直接的结构递归（调用参数是原项的直接子项），而Function允许更灵活的递归，但需要你提供证明，说明递归调用的参数在某个良基关系（这里是自然数的小于关系）下严格递减。通过定义大小度量并证明过滤后的元素大小更小，就能让Coq确认函数会终止，从而接受这个定义。

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