如何证明Coq中range函数的终止性：寻找合适的良基关系

你的核心问题是测度的选择有点绕远路了——其实不需要引入option nat和自定义关系，直接用一个自然数测度就能解决，而且逻辑更简洁。我们先拆解问题，再给出具体实现：

为什么你最初的abs(to - from)测度没生效？ #

你提到当from >= to时测度会递增，但其实此时函数不会进入递归分支（if from <? to为假，直接返回[]），所以根本不需要考虑这种情况的测度变化。真正需要证明的是：当from < to时，递归调用range (from+1) to的测度严格小于当前测度。

用abs(to - from)的问题在于，你可能没正确完成Coq生成的证明义务，或者没把测度绑定到自然数的<良基关系上——实际上当from < to时，递归调用的测度abs(to - (from+1)) = (to - from) - 1确实比当前测度小，只是需要明确证明这一点。

更简洁的解决方案：用非负差值作为测度 #

我们直接把测度定义为to - from的非负部分转换成自然数，这样既能覆盖所有情况，又能轻松证明递归的严格递减性。

完整代码实现 #

Require Import ZArith Program List.

Program Fixpoint range (from to : Z) {measure (Z.to_nat (Z.max (to - from) 0))} : list Z :=
  if from <? to then from :: range (from + 1) to else [].
Next Obligation.
  (* 证明递归调用的测度严格小于当前测度 *)
  unfold Z.max.
  case (Z.le_gt_dec (to - (from + 1)) 0).
  - intro H. rewrite H. simpl. apply Nat.lt_0_succ.
  - intro H. rewrite Z.max_r by assumption.
    simpl. apply Nat.lt_succ_diag_r.
Qed.

代码解释 #

1. 测度定义：Z.max (to - from) 0确保我们只取非负的差值，转换成自然数Z.to_nat后，就可以用自然数的<关系（Coq默认认可它是良基的）。
2. 证明义务处理：
   • 分两种情况讨论递归调用的差值：如果to - (from+1) <= 0，说明递归调用的测度是0，而当前测度至少是1（因为from < to），所以0 < 1成立；
   • 如果to - (from+1) > 0，则测度是(to - from) - 1，显然小于当前的to - from，用Nat.lt_succ_diag_r即可证明。

关于你之前option nat思路的问题 #

你的思路本身不是完全错误，但属于过度设计：因为range函数只有在from < to时才会递归，此时to - from一定是正整数，完全不需要用None来表示空范围的情况。引入option nat后，你需要处理的关系复杂度反而上升，还会遇到良基性的问题（比如None和None的比较），其实完全没必要。

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