如何解决Coq中‘Cannot guess decreasing argument of fix.’错误

错误原因 #

Coq要求递归函数必须有严格递减的参数（遵循良序关系），以此保证递归终止。你定义的aux函数中，递归调用时的div x_value base无法被Coq自动证明是严格小于原x_value的：

• 当base ≤ 1时，div x_value base不会小于x_value（比如base=1时，div x 1 = x，递归会无限循环）；
• 即使base > 1，Coq也需要明确的逻辑证明来确认递减关系。

修复方案 #

我们需要先明确基数的合法范围，再证明递归参数的递减性，最后用Coq的递归工具完成定义。

步骤1：证明递减引理

先证明当基数大于1且输入值大于0时，除法结果严格小于原数：

Lemma div_lt : forall b x : nat, 1 < b -> 0 < x -> div x b < x.
Proof.
  induction x; intros b H1 H0.
  - inversion H0.
  - simpl. destruct (leb x b) as [Hleb | Hnleb].
    + apply leb_complete in Hleb. rewrite div_leb in Hleb. rewrite Hleb. apply lt_n_S. apply le_0_n.
    + apply IHx. apply H1. apply lt_n_S. apply leb_complete_conv in Hnleb. apply Hnleb.
Qed.

步骤2：定义合法的sum_digits函数

使用Function命令（需要导入FunInd库），它允许我们指定递归的度量参数并提供递减证明：

Require Import FunInd.

(* 定义辅助递归函数，指定以x_value为度量参数 *)
Function sum_digits_aux (sum : nat) (x_value : nat) (base : nat) (H : 1 < base) {measure x_value} : nat :=
  if leb x_value 0 then
    sum
  else
    sum_digits_aux (sum + modulo x_value base) (div x_value base) base H.
(* 完成递减性证明义务 *)
Proof.
  intros sum x_value base H H0. apply div_lt. apply H. apply leb_complete_conv in H0. apply H0.
Qed.

(* 对外暴露的sum_digits函数，处理基数合法性 *)
Definition sum_digits (digits : nat) (base : nat) : nat :=
  match base with
  | 0 => 0 (* base=0非法，可根据需求调整返回值或改用option类型 *)
  | 1 => digits (* base=1时，每一位都是1，和等于原数 *)
  | S (S b) => sum_digits_aux 0 digits (S (S b)) (lt_Sn_O (S b))
  end.

简化替代方案（无需手动证明）

如果不需要严格处理非法基数，也可以用Program Fixpoint（导入Program.Wf库）自动生成证明义务：

Require Import Program.Wf.

Program Fixpoint sum_digits (digits : nat) (base : nat) (H : 1 < base) : nat :=
  let fix aux (sum : nat) (x_value : nat) (Hx : x_value <= digits) : nat :=
    if leb x_value 0 then
      sum
    else
      aux (sum + modulo x_value base) (div x_value base) (div_le _ _)
  in aux 0 digits (le_n digits).
(* 自动生成的证明义务，完成递减性证明 *)
Next Obligation.
  apply div_lt with (b := base). apply H. apply leb_complete_conv in H0. apply H0.
Qed.

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