Coq 无法计算用 Fix 定义的有根据的，但如果用 Program Fixpoint 定义则可以

Question

作为通过有根据的关系理解递归的练习，我决定实施扩展欧几里得算法。

扩展欧几里得算法适用于整数，所以我需要一些整数的有根据的关系。我尝试使用 Zwf 中的关系，但没有成功（我需要查看更多示例）。我决定使用 Z.abs_nat 函数将 Z 映射到 nat 会更容易，然后只使用 Nat.lt 作为关系。我们的朋友 wf_inverse_image 来帮助我。所以这是我所做的：

Require Import ZArith Coq.ZArith.Znumtheory.
Require Import Wellfounded.

Definition fabs := (fun x => Z.abs_nat (Z.abs x)). (* (Z.abs x) is a involutive nice guy to help me in the future *) 
Definition myR (x y : Z) := (fabs x < fabs y)%nat.
Definition lt_wf_on_Z := (wf_inverse_image Z nat lt fabs) lt_wf.

扩展欧氏算法是这样的：

Definition euclids_type (a : Z) := forall b : Z, Z * Z * Z.

Definition euclids_rec : (forall x : Z, (forall y : Z,(myR y x) -> euclids_type y) -> euclids_type x).
  unfold myR, fabs.
  refine (fun a rec b => if (Z_eq_dec a 0) then (b, 0, 1)
                      else let '(g, s, t) :=  rec (b mod a ) _ a 
                           in (g, t - (b / a) * s, s)
                      ).
apply Zabs_nat_lt. split. apply Z.abs_nonneg. apply Z.mod_bound_abs. assumption.
Defined.

Definition euclids := Fix lt_wf_on_Z _ euclids_rec.

现在让我们看看它是否有效：

Compute (euclids 240 46). (* Computation takes a long time and results in a huge term *)

我知道如果某些定义不透明就会发生这种情况，但是我所有的定义都以 Defined. 结尾。好吧，还有其他东西是不透明的，但是什么？如果是一个库定义，那么我认为在我的代码中重新定义它不会很酷。

看来我的问题与, and 有关。

我决定尝试 Program Fixpoint，因为我从未使用过它。我惊讶地发现我可以复制并粘贴我的程序。

Program Fixpoint euclids' (a b: Z) {measure (Z.abs_nat (Z.abs a))} : Z * Z * Z :=
  if Z.eq_dec a 0 then (b, 0, 1)
  else let '(g, s, t) := euclids' (b mod a) a in
       (g, t - (b / a) * s, s).
Next Obligation.
apply Zabs_nat_lt. split. apply Z.abs_nonneg. apply Z.mod_bound_abs. assumption. 
Defined.

更惊喜的是它运行良好：

Compute (euclids' 240 46). (* fast computation gives me (2, -9, 47): Z * Z * Z *)

euclids 中不透明但 euclids' 中不透明的是什么？以及如何使 euclids 工作？

Answer 1

Okey, something else is opaque, but what?

wf_inverse_image 是不透明的，它所依赖的引理也是如此：Acc_lemma 和 Acc_inverse_image。如果你使这三个透明 euclids 将计算。

充分性的证据基本上是您对其进行结构递归的参数，因此它必须是透明的。

And how to make euclids work?

幸运的是，您不必推出自己的上述标准定义的透明版本，因为 Coq.Arith.Wf_nat 中的 well_founded_ltof 引理已经是透明的，因此我们可以重用它：

Lemma lt_wf_on_Z : well_founded myR.
Proof. exact (well_founded_ltof Z fabs). Defined.

就是这样！修复 lt_wf_on_Z 后，您的其余代码就可以正常工作了。

Coq 无法计算用 Fix 定义的有根据的，但如果用 Program Fixpoint 定义则可以

Coq can't compute well-founded defined with Fix, but can if defined with Program Fixpoint

recursion

coq

totality