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

Question

As an exercise to understand recursion by a well-founded relation I decided to implement the extended euclidean algorithm.

The extended euclidean algorithm works on integers, so I need some well-founded relation on integers. I tried to use the relations in Zwf, but things didn't worked (I need to see more examples). I decided that would easier to map Z to nat with the Z.abs_nat function and then just use Nat.lt as relation. Our friend wf_inverse_image comes to help me. So here what I did:

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.

The extended euclidean algorithm goes like this:

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. 

Now let's see if it works:

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

I know that can happen if some definition is opaque, however all my definitions end with Defined.. Okey, something else is opaque, but what? If is a library definition, then I don't think that would cool to just redefine it in my code.

It seems that my problem is related with this, this other and this too.

I decided to give Program Fixpoint a try, since I never used it. I was surprised to see that I could just copy and paste my program.

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.

And even more surprise to see that works just fine:

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

What is opaque in euclids that is not in euclids' ? And how to make euclids work?

Answer 1

Okey, something else is opaque, but what?

wf_inverse_image is opaque and so are the lemmas it relies on: Acc_lemma and Acc_inverse_image. If you make these three transparent euclids will compute.

The evidence of well-foundness is basically your parameter you do structural recursion on, so it must be transparent.

And how to make euclids work?

Fortunately, you don't have to roll your own transparent versions of the aforementioned standard definitions as there is well_founded_ltof lemma in Coq.Arith.Wf_nat which is already transparent so we can reuse it:

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

That's it! After fixing lt_wf_on_Z the rest of your code just works.