Coq 无法在 Z 上计算有根据的函数，但它可以在 nat 上工作

Question

我正在（为我自己）写一篇关于如何在 Coq 中进行有根据的递归的解释。（参见 Coq'Art 书，第 15.2 章）。首先，我创建了一个基于 的示例函数，nat效果很好，但后来我又为 做了一次Z，当我使用Compute它来评估它时，它并没有一直减少到一个Z值。为什么？

这是我的示例（我将文本放在注释中，以便可以将整个内容复制粘贴到编辑器中）：

---

(* 有根据的递归测试 *)

(* TL;DR: 要进行有根据的递归，首先创建“函数”，然后使用 Acc_iter（用于可访问关系的迭代器）创建递归函数 *)

(* 作为示例，计算从 1 到 n 的级数之和，如下图所示：

修复 fn := （如果 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 条件转换为 sumbool。这样我们就可以将有关它的信息放入分支中。

我们把大部分内容写得很精炼，留下一些漏洞，稍后用策略来填补。*)

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 <= 0 then 0 else ...' 因此，对于小于零的参数，我们返回零。*)

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' 用natwithFixpoint来定义，并在可访问性证明上递归，并以结尾，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)).

Answer 1

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是透明的。请参阅Xavier Leroy 的在愤怒中使用 Coq 的评估机制博客文章。您可能还会发现 Gregory Malecha 撰写的有用的Qed 认为有害的帖子。

Zwf_well_founded您可以像这样重复使用，而不是修改证明Zlt_0_rec：

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。