我正在（为我自己）写一篇关于如何在 Coq 中进行有根据的递归的解释。 （参见 Coq'Art 书，第 15.2 章）。首先我做了一个基于的示例函数nat效果很好，但后来我又做了一次Z，当我使用Compute来评估它，它并没有一直降低到Z价值。为什么？
这是我的示例（我将文本放在注释中，以便可以将整个内容复制粘贴到编辑器中）：
(* 有根据的递归测试 *)
(* TL;DR: 为了进行有根据的递归，
首先创建“功能”，然后
使用创建递归函数
Acc_iter，可访问关系的迭代器
*)
(* 作为示例，计算从 1 到 n 的级数之和，
像这样的草图：
修复 f n := （如果 n = 0 则 0 否则 n + f (n-1)）
现在，让我们not对 n 使用结构递归。
相反，我们对 n 使用有根据的递归，
使用小于 ('lt') 的关系是
有根据的。函数 f 终止是因为
递归调用是在结构上进行的
较小的项（在递减的 Acc 链中）。
*)
(* 首先我们为 nat 做这件事 *)
Require Import Arith.Arith.
Require Import Program.Utils. (* for 'dec' *)
Require Import Wellfounded.
(* 从证明关系是有充分根据的，
我们可以得到一个特定元素的证明
在其域内是可访问的。
这里的Check命令不是必须的，只是为了
文档，亲爱的读者。
*)
Check well_founded : forall A : Type, (A -> A -> Prop) -> Prop.
Check lt_wf : well_founded lt.
Check (lt_wf 4711 : Acc lt 4711).
(* 首先为 f 定义一个“函数”F。它是一个函数
将“递归调用”的函数 F_rec 作为参数。
因为我们需要知道第二个分支中的 n 0
我们使用 'dec' 将布尔 if 条件转换为
总和。我们将有关它的信息发送到分支机构。
我们把大部分内容写得精炼，留下一些漏洞
稍后再补充战术。
*)
Definition F (n:nat) (F_rec : (forall y : nat, y < n -> nat)): nat.
refine ( if dec (n =? 0) then 0 else n + (F_rec (n-1) _ ) ).
(* now we need to show that n-1 < n, which is true for nat if n<>0 *)
destruct n; now auto with *.
Defined.
(* 迭代器可以使用函数来调用 f
根据需要多次。
旁注：我们可以创建一个迭代器来获取最大值
递归深度 d 作为 nat 参数，并在 d 上递归，但是
那么必须提供 d，以及一个“默认值”
如果 d 达到零并且必须终止则返回
早期的。
有根据的递归的巧妙之处在于
迭代器可以在有根据的证明上递归
并且不需要任何其他结构或默认值
以保证它会终止。
*)
(* Acc_iter 的类型非常多 *)
Check Acc_iter :
forall (A : Type) (R : A -> A -> Prop) (P : A -> Type),
(forall x : A, (forall y : A, R y x -> P y) -> P x) -> forall x : A, Acc R x -> P x.
(* P 存在是因为返回类型可能取决于参数，
但在我们的例子中，f:nat->nat，并且 R = lt，所以我们有
*)
Check Acc_iter (R:=lt) (fun _:nat=>nat) :
(forall n : nat, (forall y : nat, y < n -> nat) -> nat) ->
forall n : nat, Acc lt n -> nat.
(* 这里第一个参数是迭代器采用的函数，
第二个参数 n 是 f 的输入，第三个参数是
n 可访问的证明。
迭代器返回应用于 n 的 f 值。
Acc_iter 的一些参数是隐式的，有些是可以推断的。
因此我们可以简单地定义 f 如下：
*)
Definition f n := Acc_iter _ F (lt_wf n).
(*它就像一个魅力*)
Compute (f 50). (* This prints 1275 *)
Check eq_refl : f 50 = 1275.
(* 现在让我们为 Z 做这件事。这里我们不能使用 lt，
或 lt_wf 因为它们用于 nat。对于Z我们
可以使用 Zle 和 (Zwf c) 来获取下限。
它需要一个下界，在该下界下我们知道函数
将始终终止以保证终止。
这里我们使用 (Zwf 0) 来表示我们的函数将
总是在 0 或以下终止。我们还必须
将 if 语句更改为“if n
Require Import ZArith.
Require Import Zwf.
Open Scope Z.
(* 现在我们根据泛函 G 定义函数 g *)
Definition G (n:Z) (G_rec : (forall y : Z, Zwf 0 y n -> Z)) : Z.
refine (if dec (n<?0) then 0 else n + (G_rec (n-1) _ )).
(* now we need to show that n-1 < n *)
now split; [ apply Z.ltb_ge | apply Z.lt_sub_pos].
Defined.
Definition g n := Acc_iter _ G (Zwf_well_founded 0 n).
(* 但现在我们无法计算！*)
Compute (g 1).
(* 我们刚刚得到一个以
= (fix
Ffix (x : Z)
(x0 : Acc
(fun x0 x1 : Z =>
(match x1 with
| 0 => Eq
| Z.pos _ => Lt
| Z.neg _ => Gt
end = Gt -> False) /\
match x0 with
| 0 => match x1 with
| 0 => Eq
| Z.pos _ => Lt
| Z.neg _ => Gt
end
| Z.pos x2 =>
...
end) 1 (Zwf_well_founded 0 1)
: (fun _ : Z => Z) 1
)
评论：我注意到了Zwf_well_founded定义为Opaque在图书馆，所以我试着做到Transparent通过复制证明并结束引理Defined.代替Qed.但这没有帮助...
补充观察：
如果我定义f' for nat with Fixpoint相反，并递归
可访问性证明，并结束于Defined.然后它会计算。但如果我以Qed.它并没有减少。这有关系吗？我认为定义存在透明度问题G or g某处...或者我完全错了？
Fixpoint f' (n:nat) (H: Acc lt n) : nat.
refine (if dec (n<=?0) then 0 else n + (f' (n-1) (Acc_inv H _))).
apply Nat.leb_gt in e.
apply Nat.sub_lt; auto with *.
Defined. (* Compute (f' 10 (lt_wf 10)). doesn't evaluate to a nat if ended with Qed. *)
无论如何，我的问题仍然存在Z.
Fixpoint g' (n:Z) (H: Acc (Zwf 0) n) : Z.
refine (if dec (n<=?0) then 0 else n + (g' (n-1) (Acc_inv H _))).
split; now apply Z.leb_gt in e; auto with *.
Defined.
Compute (g' 10 (Zwf_well_founded 0 10)).
