【发布时间】：2017-05-25 17:47:31
【问题描述】：
我正在（为自己）写一篇关于如何在 Coq 中进行有根据的递归的解释。 （参见 Coq'Art 书，第 15.2 章）。首先，我基于nat 做了一个示例函数，效果很好，但后来我又为Z 做了一个，当我使用Compute 评估它时，它并没有一直降低到@ 987654326@ 值。为什么？
这是我的示例（我将文本放在 cmets 中，以便可以将整个内容复制粘贴到您的编辑器中）：
(* 有根据的递归测试 *)
(* TL;DR: 做有根据的递归， 首先创建“功能”，然后 使用创建递归函数 acc_iter，可访问关系的迭代器 *)
(* 例如，计算从 1 到 n 的系列之和， 像这样的草图：
修正 f n := (如果 n = 0 那么 0 否则 n + f (n-1))
现在，让我们不要在 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 条件转换为 苏姆布尔。我们会在分支中获取有关它的信息。
我们大部分都是用refine来写的，留下一些漏洞 以后用战术来填充。 *)
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，所以我尝试通过复制证明并以Defined. 而不是Qed. 结束引理来使其成为Transparent，但这并没有没救了……
添加观察：
如果我用Fixpoint 代替nat 定义f'，并在
可访问性证明，并以 Defined. 结尾，然后计算。但如果我以Qed. 结尾，它不会减少。这有关系吗？我猜G 或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)).
【问题讨论】：