Coq中如何对BinNums.Z类型进行归纳并定义合法递归函数？

问题核心原因 #

Coq默认的Fixpoint要求递归调用的参数必须是输入参数的结构子项，而BinNums.Z类型不具备可用于结构递归的归纳结构，你代码中的n - 1、n + 1都不属于n的子项，因此无法通过终止性校验。

可选用的解决方案 #

• 方案1：直接使用非递归实现
  你定义的函数实际逻辑是不管输入值是什么，最终都会返回0，完全不需要递归，直接写极简实现即可：

  Require Import ZArith.
  Definition find_0 (n : BinNums.Z) := 0%Z.
  

  该实现没有任何终止性问题，性能也是最优的。

• 方案2：用Program Fixpoint指定测度实现递归
  如果你需要保留递归写法（比如学习测试场景），可以用Program Fixpoint手动指定递归的递减测度，向Coq证明每次递归的测度严格减小：

  Require Import Program ZArith Lia.
  
  Program Fixpoint find_0 (n : Z) {measure (Z.abs_nat n)} :=
    match n with
    | Z0 => n
    | Zpos _ => find_0 (n - 1)
    | Zneg _ => find_0 (n + 1)
    end.
  Next Obligation.
    destruct n; simpl; lia.
  Qed.
  Next Obligation.
    destruct n; simpl; lia.
  Qed.
  

  这里用Z.abs_nat n把输入整数转换为对应的自然数绝对值作为测度，每次递归调用时测度都会严格减1，配合lia策略可以自动完成证明义务。

• 方案3：用Function命令定义带测度的递归
  和Program Fixpoint逻辑类似，使用Recdef模块提供的Function命令也可以实现：

  Require Import ZArith Recdef Lia.
  
  Function find_0 (n : Z) {measure (Z.abs_nat n)} :=
    match n with
    | Z0 => n
    | Zpos _ => find_0 (n - 1)
    | Zneg _ => find_0 (n + 1)
    end.
  Proof.
    all: destruct n; simpl; lia.
  Qed.
  

注意：非必要场景下优先使用方案1，递归实现对于大数值输入会产生极高的性能消耗。

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