如何仅展开一次Coq中的fix递归函数？

问题场景 #

我通过fix定义了一个基于良基递归（依赖Acc谓词）的自然数函数，现在需要证明它的重写等式。以下是简化的示例代码：

Require Import Wf_nat PeanoNat.

Definition test (n: nat): nat. 
refine (
  let test := 
    fix test n (H: Acc lt n) {struct H} := 
      if Nat.eq_dec 0 n 
      then n 
      else n + test (n-1) _ 
  in 
    test n (Wf_nat.lt_wf n)).

  apply H; auto with arith.
Defined.

(* 单元测试验证功能 *)
Check eq_refl (test 4 = 4 + test 3).  

我需要证明的目标是：

Goal forall n, test (S n) = S n + test n.

在执行以下证明步骤后：

Proof. 
   induction n. 
   reflexivity.
   unfold test.

证明目标中出现了原始的fix test项，我需要仅单次展开这个fix函数（即展开外层的fix应用，不递归展开内部的test调用），但cbv delta会过度求值，请问该如何实现？

当前的证明义务如下：

n: nat
IHn: test (S n) = test n + S n
1/1
(fix test (n0 : nat) (H : Acc lt n0) {struct H} : nat :=
   match Nat.eq_dec 0 n0 with
   | left _ => n0
   | right H0 =>
       n0 +
       test (n0 - 1)
         (match H with
          | Acc_intro _ H1 => H1
          end (n0 - 1)
            (Nat.sub_lt n0 1
               (Arith_prebase.gt_le_S_stt 0 n0
                  (Arith_prebase.neq_0_lt_stt n0 H0)) 
               (le_n 1)))
   end) (S (S n)) (lt_wf (S (S n))) =
(fix test (n0 : nat) (H : Acc lt n0) {struct H} : nat :=
   match Nat.eq_dec 0 n0 with
   | left _ => n0
   | right H0 =>
       n0 +
       test (n0 - 1)
         (match H with
          | Acc_intro _ H1 => H1
          end (n0 - 1)
            (Nat.sub_lt n0 1
               (Arith_prebase.gt_le_S_stt 0 n0
                  (Arith_prebase.neq_0_lt_stt n0 H0)) 
               (le_n 1)))
   end) (S n) (lt_wf (S n)) + S (S n)

解决方案 #

可以通过以下几种方式实现单次展开fix函数：

• 方法1：使用cbn策略
  cbn（call-by-need归约）会按需展开项，仅展开外层的fix应用，不会递归展开内部的test调用。在unfold test之后直接执行：

  cbn.
  

  这会将左右两边的fix应用展开为对应的match表达式，同时保留内部的test调用不变，正好符合单次展开的需求。

• 方法2：使用lazy策略
  lazy策略与cbn类似，也会执行按需归约，避免过度展开。执行：

  lazy beta iota delta [test].
  

  其中beta iota delta指定归约的类型，[test]限制仅展开test的定义，同样可以实现单次展开。

• 方法3：手动利用fix的等式展开
  对于带Acc的递归函数，还可以通过rewrite结合Acc的性质手动展开。例如，先对左边的项应用lt_wf的定义，再展开fix的一次应用：

  rewrite (lt_wf (S (S n))).
  unfold test at 1.
  cbn.
  

  这种方式更精细，适合需要精确控制展开位置的场景。

后续证明提示 #

展开完成后，你可以通过case_eq (Nat.eq_dec 0 (S (S n)))拆分match分支，再结合归纳假设IHn和自然数的算术性质（如Nat.sub_1_r、plus_comm等）完成证明。

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