Coq实现左式堆merge函数报错：无法推断fix递减参数，如何修复？

问题描述 #

基于Okasaki的《纯函数式数据结构》在Coq中实现左式堆时，编写merge函数遇到以下错误：

• 初始错误：Cannot guess decreasing argument of fix
• 调整结构后的错误：递归调用的主参数为b2而非指定变量，Coq无法识别递归参数的递减性

原始代码及错误 #

原始代码 #

From mathcomp Require Import all_ssreflect.
From Equations Require Import Equations.
Require Import Reals.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Heap.
Open Scope Z_scope.
Inductive Heap := E | T of Z * Z * Heap * Heap.

Definition rank (h : Heap) : Z :=
  match h with
    | E => 0%Z
    | T (r, _, _, _) => r
  end.

Definition makeT (x : Z) (a : Heap) (b : Heap) :=
  let ra : Z := rank a in
  let rb : Z := rank b in
  let zc : comparison := Z.compare ra rb
  in
  match zc with
    | Gt => T((rb + 1), x, a, b)
    | Eq => T((rb + 1), x, a, b)
    | Lt => T((ra + 1), x, b, a)
  end.

Definition empty := E.
Definition isEmpty h :=
  match h with
  | E => true
  | _ => false
  end.

Fixpoint merge h1 h2 :=
  match h1 with
    | E => h2
    | T(r1, x, a1, b1) =>
          match h2 with
            | E => T(r1, x, a1, b1)
            | T(r2, y, a2,b2) =>
              match (Z.compare x y) with
                | Lt => makeT x a1 (merge b1 (T(r2, y, a2, b2)))
                | _ => makeT y a2 (merge b2 (T(r1, x, a1, b1)))
              end
           end
   end.
End Heap.

初始错误信息 #

Coq Error: Cannot guess decreasing argument of fix.

调整后的代码及错误 #

调整后的merge函数片段 #

match h1 with
  | E => h2
  | T(r1, x, a1, b1) =>
      match h2 with
        | E => T(r1, x, a1, b1)
        | T(r2, y, a2,b2) =>
          match (Z.compare x y) with
            | Lt => makeT x a1 (merge b1 (T(r2, y, a2, b2)))
            | _ => makeT y a2 (merge b2 (T(r1, x, a1, b1)))
          end
       end
 end.

调整后的错误信息 #

Recursive call to merge has principal argument equal to "b2" instead of
one of the following variables: "p" "p0" "b1" "a1".
Recursive definition is:
"fun h1 h2 : Heap =>
 match h1 with
 | E => h2
 | T (r1, x, a1, b1) =>
     match h2 with
     | E => T (r1, x, a1, b1)
     | T (r2, y, a2, b2) =>
         match x ?= y with
         | Lt => makeT x a1 (merge b1 (T (r2, y, a2, b2)))
         | _ => makeT y a2 (merge b2 (T (r1, x, a1, b1)))
         end
     end
 end".

解决方案 #

Coq的Fixpoint要求递归调用的参数必须在良基关系下严格递减，左式堆的merge递归依赖于堆的**秩（rank）**递减——左式堆的右子堆秩必然小于当前堆的秩。当前代码的问题在于Coq无法自动识别递归参数的秩递减性，以下是两种可行的解决方法：

方法1：使用Equations库定义merge（推荐） #

你已经导入了Equations库，它能自动处理递归递减的证明义务，无需手动指定度量：

From mathcomp Require Import all_ssreflect.
From Equations Require Import Equations.
Require Import Reals.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Heap.
Open Scope Z_scope.
Inductive Heap := E | T of Z * Z * Heap * Heap.

Definition rank (h : Heap) : Z :=
  match h with
    | E => 0%Z
    | T (r, _, _, _) => r
  end.

Definition makeT (x : Z) (a : Heap) (b : Heap) :=
  let ra : Z := rank a in
  let rb : Z := rank b in
  match Z.compare ra rb with
    | Gt | Eq => T(rb + 1, x, a, b)
    | Lt => T(ra + 1, x, b, a)
  end.

Definition empty := E.
Definition isEmpty h := match h with E => true | _ => false end.

-- 用Equations定义merge，自动处理递归递减证明
Equations merge (h1 h2 : Heap) : Heap :=
merge E h2 := h2;
merge h1 E := h1;
merge (T r1 x a1 b1) (T r2 y a2 b2) with Z.compare x y :=
| Lt => makeT x a1 (merge b1 (T r2 y a2 b2));
| _ => makeT y a2 (merge b2 (T r1 x a1 b1)).

-- 证明递归调用的秩递减性（Equations自动生成义务，完成证明即可）
Next Obligation.
  intros. simpl. unfold rank.
  destruct (T r1 x a1 b1) as [ | [r1 x a1 b1]]; auto.
  apply Z.lt_succ_diag_r.
Qed.

Next Obligation.
  intros. simpl. unfold rank.
  destruct (T r2 y a2 b2) as [ | [r2 y a2 b2]]; auto.
  apply Z.lt_succ_diag_r.
Qed.
End Heap.

方法2：使用Program Fixpoint显式指定度量 #

通过指定递归度量为两个堆的秩之和，让Coq明确递归调用的参数是递减的：

From mathcomp Require Import all_ssreflect.
From Equations Require Import Equations.
Require Import Reals Program.Wf.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Heap.
Open Scope Z_scope.
Inductive Heap := E | T of Z * Z * Heap * Heap.

Definition rank (h : Heap) : Z :=
  match h with
    | E => 0%Z
    | T (r, _, _, _) => r
  end.

Definition makeT (x : Z) (a : Heap) (b : Heap) :=
  let ra : Z := rank a in
  let rb : Z := rank b in
  match Z.compare ra rb with
    | Gt | Eq => T(rb + 1, x, a, b)
    | Lt => T(ra + 1, x, b, a)
  end.

Definition empty := E.
Definition isEmpty h := match h with E => true | _ => false end.

-- 辅助引理：右子堆的秩严格小于当前堆的秩
Lemma rank_right_lt : forall h : Heap, h <> E -> rank (match h with T _ _ _ b => b | _ => E end) < rank h.
Proof.
  destruct h; intros.
  - contradiction.
  - simpl. unfold rank. rewrite Z.add_1_l. apply Z.lt_succ_diag_r.
Qed.

-- 用Program Fixpoint定义merge，指定度量为秩之和
Program Fixpoint merge (h1 h2 : Heap) {measure (rank h1 + rank h2)} : Heap :=
  match h1 with
  | E => h2
  | T r1 x a1 b1 =>
      match h2 with
      | E => h1
      | T r2 y a2 b2 =>
          if Z.compare x y is Lt then
            makeT x a1 (merge b1 h2)
          else
            makeT y a2 (merge b2 h1)
      end
  end.

-- 证明第一个递归调用的度量递减
Next Obligation.
  intros h1 h2 _ _ _.
  simpl. unfold rank.
  destruct h1 as [ | [r1 x a1 b1]]; destruct h2 as [ | [r2 y a2 b2]]; auto.
  rewrite rank_right_lt with (h := h1); auto.
  apply Z.lt_add_l; apply Z.le_refl.
Qed.

-- 证明第二个递归调用的度量递减
Next Obligation.
  intros h1 h2 _ _ _.
  simpl. unfold rank.
  destruct h1 as [ | [r1 x a1 b1]]; destruct h2 as [ | [r2 y a2 b2]]; auto.
  rewrite rank_right_lt with (h := h2); auto.
  apply Z.lt_add_r; apply Z.le_refl.
Qed.
End Heap.

关键说明 #

1. 移除了递归调用中冗余的T构造（直接使用h2而非重新构造T(r2, y, a2, b2)），让Coq更容易识别递归参数。
2. 左式堆的核心性质是右子堆秩 ≤ 左子堆秩，且堆的秩等于右子堆秩+1，这是递归递减的基础。
3. Equations库简化了递归函数的定义和证明，无需手动处理复杂的良基关系证明。

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