Coq中定义互递归树比较函数报递归结构错误如何解决

你遇到的报错是Coq互递归终止检查的限制导致的：两个互相调用的递归函数需要明确满足「所有递归调用的参数都是初始参数的严格子结构」，你原来的拆分写法中，Coq无法自动关联compare_children的参数xs和内部调用compare_info时传入的x'的子结构关系，因此拒绝通过检查。

以下是两种无需Program Fixpoint、完全符合Coq语法要求的改写方案，均保留你需要的短路比较逻辑，且不影响后续性质证明：

方案1：复用标准库列表字典序比较（推荐） #

直接使用Coq标准库的List.lexcompare函数实现子节点列表的比较，无需显式定义互递归函数，逻辑和你原始实现完全一致，终止检查可以直接通过：

Require Import Coq.Lists.List.
Import Coq.Lists.List.ListNotations.

Inductive Info: Type :=
  mkInfo :
    forall
    (value: nat)
    (children: list Info)
    (hash: nat),
  Info.

Fixpoint compare_info (x y: Info) {struct x} : comparison :=
  match x, y with
  | mkInfo xvalue xchildren xhash, mkInfo yvalue ychildren yhash =>
    match Nat.compare xhash yhash with
    | Lt => Lt
    | Gt => Gt
    | Eq =>
      match Nat.compare xvalue yvalue with
      | Lt => Lt
      | Gt => Gt
      | Eq => List.lexcompare compare_info xchildren ychildren
      end
    end
  end.

List.lexcompare是标准库原生实现的字典序列表比较，行为和你写的compare_children完全相同：逐个比对对应位置元素，遇到第一个不等结果直接短路返回，长度不同时短列表更小，完全符合你的需求。后续证明时可以直接复用标准库中关于lexcompare的现成引理，反而能简化证明工作量。

方案2：嵌套fix实现自定义子节点比较 #

如果你希望完全自己实现比较逻辑不依赖lexcompare，可以将子节点比较函数作为嵌套的fix定义在compare_info内部，改写后的代码如下：

Require Import Coq.Lists.List.
Import Coq.Lists.List.ListNotations.

Inductive Info: Type :=
  mkInfo :
    forall
    (value: nat)
    (children: list Info)
    (hash: nat),
  Info.

Fixpoint compare_info (x y: Info) {struct x} : comparison :=
  let fix compare_children (xs ys: list Info) {struct xs} : comparison :=
    match xs, ys with
    | [], [] => Eq
    | [], _ => Lt
    | _, [] => Gt
    | x'::xs', y'::ys' =>
      match compare_info x' y' with
      | Eq => compare_children xs' ys'
      | res => res
      end
    end in
  match x, y with
  | mkInfo xvalue xchildren xhash, mkInfo yvalue ychildren yhash =>
    match Nat.compare xhash yhash with
    | Lt => Lt
    | Gt => Gt
    | Eq =>
      match Nat.compare xvalue yvalue with
      | Lt => Lt
      | Gt => Gt
      | Eq => compare_children xchildren ychildren
      end
    end
  end.

这种写法的逻辑和你原始实现100%一致，嵌套的compare_children作为内部函数，Coq可以自动识别到调用compare_info时传入的列表元素是外层Info参数的严格子结构，因此可以通过终止检查，后续证明和普通Fixpoint没有区别。

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