Coq 无法在 Z 上计算一个有根据的函数，但它可以在 nat 上运行
Coq can't compute a well-founded function on Z, but it works on nat
我正在（为我自己）写一篇关于如何在 Coq 中进行有根据的递归的解释。 （参见 Coq'Art 书，第 15.2 章）。首先我做了一个基于 nat 的示例函数并且工作正常，但后来我又为 Z 做了一次，当我使用 Compute 来评估它时，它并没有减少所有下降到 Z 值的方式。为什么？
这是我的示例（我将文本放在注释中，以便您可以将整个内容复制粘贴到您的编辑器中）：
(* 有根据的递归测试 *)
(* TL;DR: 做有根据的递归，
首先创建 'functional' 然后
使用创建递归函数
Acc_iter，可访问关系的迭代器
*)
(* 例如，计算从 1 到 n 的序列之和，
像这样的草图：
fix f n := (if n = 0 then 0 else n + f (n-1))
现在，让我们不对 n 使用结构递归。
相反，我们对 n 使用有根据的递归，
使用小于 ('lt') 的关系是
有根据的。函数 f 终止是因为
递归调用是在结构上进行的
较小的术语（在递减的 Acc 链中）。
*)
(* 首先我们为 nat *)
Require Import Arith.Arith.
Require Import Program.Utils. (* for 'dec' *)
Require Import Wellfounded.
(* 从证明关系是有根据的，
我们可以得到一个特定元素的证明
在其域中是可访问的。
这里的检查命令不是必需的，只是为了
文档，亲爱的 reader。
*)
Check well_founded : forall A : Type, (A -> A -> Prop) -> Prop.
Check lt_wf : well_founded lt.
Check (lt_wf 4711 : Acc lt 4711).
(* 首先为f定义一个'functional' F。它是一个函数
将 'recursive call' 的函数 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，还有一个'default value'
到 return 以防 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 在那里是因为 return 类型可能依赖于参数，
但在我们的例子中，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 是可访问的。
迭代器 returns 将 f 的值应用于 n。
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 <= 0 then 0 else ...'
所以我们 return 零参数小于零。
*)
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，所以我尝试通过复制证明并以 [=30 结束引理来使其成为 Transparent =] 而不是 Qed. 但这没有帮助...
新增观察：
如果我用 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)).
使 Zwf_well_founded 透明无济于事，因为它在标准库中的定义方式：
Lemma Zwf_well_founded : well_founded (Zwf c).
...
case (Z.le_gt_cases c y); intro; auto with zarith.
...
Qed.
如果将上面证明中的行替换为
case (Z_le_gt_dec c y); intro; auto with zarith.
并将 Qed. 替换为 Defined.（您已经这样做了）一切都应该有效。这是因为原始证明依赖于逻辑项，这会阻止评估者进行模式匹配，因为逻辑实体 Z.le_gt_cases 是不透明的，而计算实体 Z_le_gt_dec 是透明的。参见 Gregory Malecha 的 Using Coq's evaluation mechanisms in anger blog post by Xavier Leroy. You might also find useful Qed Considered Harmful post。
您可以像这样重用 Zlt_0_rec 而不是修改 Zwf_well_founded 的证明：
Require Import Coq.ZArith.ZArith.
Open Scope Z.
Definition H (x:Z) (H_rec : (forall y : Z, 0 <= y < x -> Z)) (nonneg : 0 <= x) : Z.
refine (if Z_zerop x then 0 else x + (H_rec (Z.pred x) _ )).
auto with zarith.
Defined.
Definition h (z : Z) : Z :=
match Z_lt_le_dec z 0 with left _ => 0 | right pf => (Zlt_0_rec _ H z pf) end.
Check eq_refl : h 100 = 5050.
不太方便，因为现在我们必须处理h中的负数。
我正在（为我自己）写一篇关于如何在 Coq 中进行有根据的递归的解释。 （参见 Coq'Art 书，第 15.2 章）。首先我做了一个基于 nat 的示例函数并且工作正常，但后来我又为 Z 做了一次，当我使用 Compute 来评估它时，它并没有减少所有下降到 Z 值的方式。为什么？
这是我的示例（我将文本放在注释中，以便您可以将整个内容复制粘贴到您的编辑器中）：
(* 有根据的递归测试 *)
(* TL;DR: 做有根据的递归， 首先创建 'functional' 然后 使用创建递归函数 Acc_iter，可访问关系的迭代器 *)
(* 例如，计算从 1 到 n 的序列之和， 像这样的草图：
fix f n := (if n = 0 then 0 else n + f (n-1))
现在，让我们不对 n 使用结构递归。
相反，我们对 n 使用有根据的递归， 使用小于 ('lt') 的关系是 有根据的。函数 f 终止是因为 递归调用是在结构上进行的 较小的术语（在递减的 Acc 链中）。 *)
(* 首先我们为 nat *)
Require Import Arith.Arith.
Require Import Program.Utils. (* for 'dec' *)
Require Import Wellfounded.
(* 从证明关系是有根据的， 我们可以得到一个特定元素的证明 在其域中是可访问的。
这里的检查命令不是必需的，只是为了 文档，亲爱的 reader。 *)
Check well_founded : forall A : Type, (A -> A -> Prop) -> Prop.
Check lt_wf : well_founded lt.
Check (lt_wf 4711 : Acc lt 4711).
(* 首先为f定义一个'functional' F。它是一个函数 将 'recursive call' 的函数 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，还有一个'default value' 到 return 以防 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 在那里是因为 return 类型可能依赖于参数，
但在我们的例子中，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 是可访问的。 迭代器 returns 将 f 的值应用于 n。
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 <= 0 then 0 else ...' 所以我们 return 零参数小于零。 *)
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，所以我尝试通过复制证明并以 [=30 结束引理来使其成为 Transparent =] 而不是 Qed. 但这没有帮助...
新增观察：
如果我用 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)).
使 Zwf_well_founded 透明无济于事，因为它在标准库中的定义方式：
Lemma Zwf_well_founded : well_founded (Zwf c). ... case (Z.le_gt_cases c y); intro; auto with zarith. ... Qed.
如果将上面证明中的行替换为
case (Z_le_gt_dec c y); intro; auto with zarith.
并将 Qed. 替换为 Defined.（您已经这样做了）一切都应该有效。这是因为原始证明依赖于逻辑项，这会阻止评估者进行模式匹配，因为逻辑实体 Z.le_gt_cases 是不透明的，而计算实体 Z_le_gt_dec 是透明的。参见 Gregory Malecha 的 Using Coq's evaluation mechanisms in anger blog post by Xavier Leroy. You might also find useful Qed Considered Harmful post。
您可以像这样重用 Zlt_0_rec 而不是修改 Zwf_well_founded 的证明：
Require Import Coq.ZArith.ZArith.
Open Scope Z.
Definition H (x:Z) (H_rec : (forall y : Z, 0 <= y < x -> Z)) (nonneg : 0 <= x) : Z.
refine (if Z_zerop x then 0 else x + (H_rec (Z.pred x) _ )).
auto with zarith.
Defined.
Definition h (z : Z) : Z :=
match Z_lt_le_dec z 0 with left _ => 0 | right pf => (Zlt_0_rec _ H z pf) end.
Check eq_refl : h 100 = 5050.
不太方便，因为现在我们必须处理h中的负数。