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 值。为什么？

I'm writing (for myself) an explanation of how to do well-founded recursion in Coq. (see i.e. the Coq'Art book, chapter 15.2). First I made an example function based on nat and that worked fine, but then I did it again for Z, and when I use Compute to evaluate it, it doesn't reduce all the way down to a Z value. Why?

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

Here is my example (I put the text inside comments so one can copy-paste the whole thing into your editor):

（* *有根据的递归检验*）

(* Test of well-founded recursion *)

（* TL; DR：To做有充分依据的递归，
首先创建函数，然后
使用
Acc_iter（可访问关系的迭代器
*）

(* TL;DR: To do well-founded recursion, first create 'functional' and then create the recursive function using Acc_iter, the iterator for accessible relations *)

（*例如，计算从1到n的序列之和，
类似于此草图：

(* As an example, compute the sum of the series from 1 to n, something like this sketch:

fix fn：=（如果n = 0则为0否则n + f（n-1））

现在，让我们 not 在n上使用结构递归。

Now, let's not use structural recursion on n.

相反，我们在n，
上使用有充分依据的递归，使用的关系小于（（lt ）是
的基础。函数f终止是因为
的递归调用是在结构上较小的
项（在递减的Acc链中）。
*）

Instead, we use well-founded recursion on n, using that the relation less-than ('lt') is wellfounded. The function f terminates because the recursive call is made on a structurally smaller term (in the decreasing Acc-chain). *)

（*首先，我们这样做是为了nat *）

(* First we do it for nat *)

Require Import Arith.Arith.
Require Import Program.Utils. (* for 'dec' *)
Require Import Wellfounded.

（**通过证明关系是有根据的，
可以证明

(* From a proof that a relation is wellfounded, we can get a proof that a particular element in its domain is accessible.

亲爱的读者，这里的Check命令不是必需的，仅用于
文档。 b *）

The Check commands here are not necessary, just for documentation, dear 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定义一个函数F。
是一个函数以递归调用的函数F_rec作为参数
因为我们需要在第二个分支
中知道n <>> 0，所以我们使用'dec'将布尔if条件转换为a
sumbool。这样我们就可以在分支机构中获取有关信息。

(* First define a 'functional' F for f. It is a function that takes a function F_rec for the 'recursive call' as an argument. Because we need to know n <> 0 in the second branch we use 'dec' to turn the boolean if-condition into a sumbool. This we get info about it into the branches.

我们用精炼功能编写了大部分内容，并留了一些空缺

*）

We write most of it with refine, and leave some holes to be filled in with tactics later. *)

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

(* The functional can be used by an iterator to call f as many times as is needed.

侧面说明：可以创建一个将最大
递归深度d作为nat参数的迭代器，然后对d递归，但是
，则必须提供d，并且还必须提供一个默认值
，以防万一d达到零且必须提前终止
。

Side note: One can either make an iterator that takes the maximal recursive depth d as a nat argument, and recurses on d, but then one has to provide d, and also a 'default value' to return in case d reaches zero and one must terminate early.

具有完善的递归的巧妙之处在于，
迭代器可以基于有充分根据的证明
进行递归，并且不需要任何其他结构或默认值
来保证其将终止。 b $ b *）

The neat thing with well-founded recursion is that the iterator can recurse on the proof of wellfoundedness and doesnt need any other structure or default value to guarantee it will terminate. *)

（* * Acc_iter的类型非常有毛*）

(* The type of Acc_iter is pretty hairy *)

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，所以我们有
*）

(* P is there because the return type could be dependent on the argument,
but in our case, f:nat->nat, and R = lt, so we have *)

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的输入，第三个参数是
a证明n是可访问的。
迭代器返回应用于n的f的值。

(* Here the first argument is the functional that the iterator takes, the second argument n is the input to f, and the third argument is a proof that n is accessible. The iterator returns the value of f applied to n.

Acc_iter的几个参数是隐式的，可以推论一些。
因此，我们可以简单地如下定义f：
*）

Several of Acc_iter's arguments are implicit, and some can be inferred. Thus we can define f simply as follows: *)

Definition f n := Acc_iter _ F (lt_wf n).

（*它就像一个符咒*）

(* It works like a charm *)

Compute (f 50). (* This prints 1275 *)
Check eq_refl : f 50 = 1275.

（*现在，我们为Z做它。在这里，我们不能使用lt，
或lt_wf，因为它们是nat的；对于Z我们的
可以使用Zle和（Zwf c）取下限。 $ b它需要一个下界，我们知道函数
将始终终止以保证终止
这里我们使用（Zwf 0）来表示我们的函数
总是终止于或小于0。我们还必须
将if语句更改为如果n< = 0则为0，否则为0 ...
，因此对于小于零的参数，我们返回零。 ）

(* Now let's do it for Z. Here we can't use lt, or lt_wf because they are for nat. For Z we can use Zle and (Zwf c) which takes a lower bound. It needs a lower bound under which we know that the function will always terminate to guarantee termination. Here we use (Zwf 0) to say that our function will always terminate at or below 0. We also have to change the if-statement to 'if n <= 0 then 0 else ...' so we return zero for arguments less than zero. *)

Require Import ZArith.
Require Import Zwf.

Open Scope Z.

（*现在我们定义函数g为基础在功能G上*）

(* Now we define the function g based on the functional 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).

（*但现在我们无法计算！*）

(* But now we can't compute! *)

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 在库中，所以我尝试通过复制证明并以透明 >已定义。而不是 Qed。，但这没有帮助...

---

Comment: I noticed that Zwf_well_founded is defined as Opaque in the library, so I tried to make it Transparent by copying the proof and ending the lemma with Defined. instead of Qed. but that didn't help...

添加的观察结果：

如果我为 nat f' c>改为 Fixpoint ，然后递归
可访问性证明并以 Defined结尾。 然后进行计算。但是，如果我以 Qed结尾。不会减少。有关系吗我想 G 或 g 的定义中存在透明性的问题...还是我完全误解了？

If I define f' for nat with Fixpoint instead, and recurse on the accesibility proof, and end with Defined. then it computes. But if I end with Qed. it doesn't reduce. Is this related? I guess there is an issue of transparency in the definition of G or g somewhere... Or am I completely mistaken?

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 仍然存在。

Anyway, my problem persists for 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 透明无济于事，因为在标准库中定义的方式：

Making Zwf_well_founded transparent won't help, because of the way it is defined in the standard library:

Lemma Zwf_well_founded : well_founded (Zwf c).
...
    case (Z.le_gt_cases c y); intro; auto with zarith.
...
Qed.

如果将上述证明中的行替换为

If you replace the line in the proof above with

     case (Z_le_gt_dec c y); intro; auto with zarith.

并用<$ c替换 Qed。 $ c>已定义。（您已经完成了），一切都应该正常进行。这是由于以下事实：原始证明依赖于逻辑项，并且阻止了评估者进行模式匹配，因为逻辑实体 Z.le_gt_cases 是不透明的，而在计算时实体 Z_le_gt_dec 是透明的。请参阅在愤怒中使用Coq的评估机制博客文章，作者Xavier Leroy。您可能还会发现Gregory Malecha的 Qed被认为有害帖子。

and replace Qed. with Defined. (which you already did) everything should work. This is due the fact that the original proof depends on a logical term, and that prevents the evaluator from doing pattern-matching, because logical entity Z.le_gt_cases is opaque, while computational entity Z_le_gt_dec is transparent. See Using Coq's evaluation mechanisms in anger blog post by Xavier Leroy. You might also find useful Qed Considered Harmful post by Gregory Malecha.

您无需重复修改 Zwf_well_founded 的证明，就可以重复使用 Zlt_0_rec 像这样：

Instead of modifying the proof of Zwf_well_founded you can reuse Zlt_0_rec like so:

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 中的负数。

It's a bit less convenient because now we have to deal with negative numbers in h.

这篇关于Coq无法在Z上计算有据可依的函数，但可以在nat上运行的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！