自定义alt_nat类型下f2函数报“无法推测fix递减参数”的问题咨询

为什么会报错？ #

Coq（即现在的Rocq）对递归函数有硬性要求：必须满足良基递归——每次递归调用时，得有一个参数严格递减，且这个递减关系要能被证明不会无限循环。

标准nat类型是Coq内置的，系统默认就认可它的<关系是良基的，写递归时能自动检测到参数的递减性。但你自定义的alt_nat，哪怕逻辑上和nat完全等价，Coq也不知道它的构造对应的递减规则。所以写f2的时候，系统找不到哪个参数在递归过程中变小，也不知道用什么规则验证递归能终止，就抛出了“Cannot guess decreasing argument of fix”的错误。

怎么修复？ #

有两种常用的解决办法：

方法1：显式指定递减依据 #

用Function命令（需先导入FunInd库），明确告诉Coq用什么来判断参数递减。比如你可以先实现一个把alt_nat转成标准nat的函数，让Coq用这个转换后的nat值的<关系来验证终止性：

Require Import FunInd.

// 先实现alt_nat到nat的转换函数
Fixpoint alt_nat_to_nat (n : alt_nat) : nat :=
  match n with
  | alt_nat_zero => O
  | alt_nat_succ m => S (alt_nat_to_nat m)
  end.

// 定义f2时用measure指定递减依据
Function f2 (a b : alt_nat) {measure (alt_nat_to_nat a)} : alt_nat * alt_nat :=
  match alt_nat_lt a b with
  | true => (alt_nat_zero, a)
  | false => let (q, r) := f2 (alt_nat_sub a b) b in (alt_nat_succ q, r)
  end.

这里的measure子句就是告诉Coq：每次递归调用时，a转成nat后的值会严格变小，以此保证递归终止。如果Coq需要你证明这个递减关系，会自动生成证明义务让你补全。

方法2：给自定义类型注册递归原理 #

如果你的alt_nat是用类似Inductive alt_nat := alt_nat_zero | alt_nat_succ (n : alt_nat).的方式定义的，可以用Scheme命令为它生成和nat一致的递归原理，让Coq自动识别递减规则：

Scheme alt_nat_ind := Induction for alt_nat Sort Prop.
Scheme alt_nat_rec := Minimality for alt_nat Sort Set.

生成完递归原理后，再定义f2时，Coq就能像处理nat一样，自动检测到递归调用中alt_nat参数的递减性，无需额外指定。

注意事项 #

• 确保你实现的alt_nat_lt、alt_nat_sub等函数的逻辑和标准nat的<、sub一致，尤其是alt_nat_sub a b的结果必须确实比a“小”（转成nat后的值更小）。
• 用Function命令时，可能需要手动证明一些小引理来满足Coq的终止性检查要求，跟着系统提示完成即可。

内容的提问来源于stack exchange，提问作者David Roman-Ferriere