作为通过有充分理由的关系理解递归的练习，我决定实现扩展的欧几里德算法。
扩展的欧几里德算法适用于整数，因此我需要一些有效的整数关系。我试图使用Zwf中的关系，但事情没有奏效（我需要看更多的例子）。我决定用Z函数更容易将nat映射到Z.abs_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.结尾。哦，其他的东西是不透明的，但是什么？如果是库定义，那么我不认为在我的代码中重新定义它会很酷。
似乎我的问题与this，this other和this too有关。
我决定试试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工作？
哦，其他的东西是不透明的，但是什么？
wf_inverse_image是不透明的，它所依赖的引理也是如此：Acc_lemma和Acc_inverse_image。如果你使这三个透明的euclids将计算。
良好基础的证据基本上是你进行结构递归的参数，所以它必须是透明的。
以及如何让
euclids工作？
幸运的是，您不必滚动自己的上述标准定义的透明版本，因为well_founded_ltof中的Coq.Arith.Wf_nat引理已经是透明的，因此我们可以重复使用它：
Lemma lt_wf_on_Z : well_founded myR.
Proof. exact (well_founded_ltof Z fabs). Defined.
而已！修复lt_wf_on_Z后，其余的代码就可以了。