Library Coq.ZArith.Zgcd_alt



Zgcd_alt : an alternate version of Zgcd, based on Euler's algorithm


Author: Pierre Letouzey

The alternate Zgcd_alt given here used to be the main Zgcd function (see file Znumtheory), but this main Zgcd is now based on a modern binary-efficient algorithm. This earlier version, based on Euler's algorithm of iterated modulo, is kept here due to both its intrinsic interest and its use as reference point when proving gcd on Int31 numbers

Require Import ZArith_base.
Require Import ZArithRing.
Require Import Zdiv.
Require Import Znumtheory.

Open Scope Z_scope.

In Coq, we need to control the number of iteration of modulo. For that, we use an explicit measure in nat, and we prove later that using 2*d is enough, where d is the number of binary digits of the first argument.

 Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b =>
   match n with
     | O => 1
     | S n => match a with
                | Z0 => Zabs b
                | Zpos _ => Zgcdn n (Zmod b a) a
                | Zneg a => Zgcdn n (Zmod b (Zpos a)) (Zpos a)
              end
   end.

 Definition Zgcd_bound (a:Z) :=
   match a with
     | Z0 => S O
     | Zpos p => let n := Psize p in (n+n)%nat
     | Zneg p => let n := Psize p in (n+n)%nat
   end.

 Definition Zgcd_alt a b := Zgcdn (Zgcd_bound a) a b.

A first obvious fact : Zgcd a b is positive.

 Lemma Zgcdn_pos : forall n a b,
   0 <= Zgcdn n a b.

 Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b.

We now prove that Zgcd is indeed a gcd.

1) We prove a weaker & easier bound.

 Lemma Zgcdn_linear_bound : forall n a b,
   Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b).

2) For Euclid's algorithm, the worst-case situation corresponds to Fibonacci numbers. Let's define them:

 Fixpoint fibonacci (n:nat) : Z :=
   match n with
     | O => 1
     | S O => 1
     | S (S n as p) => fibonacci p + fibonacci n
   end.

 Lemma fibonacci_pos : forall n, 0 <= fibonacci n.

 Lemma fibonacci_incr :
   forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m.

3) We prove that fibonacci numbers are indeed worst-case: for a given number n, if we reach a conclusion about gcd(a,b) in exactly n+1 loops, then fibonacci (n+1)<=a /\ fibonacci(n+2)<=b

 Lemma Zgcdn_worst_is_fibonacci : forall n a b,
   0 < a < b ->
   Zis_gcd a b (Zgcdn (S n) a b) ->
   Zgcdn n a b <> Zgcdn (S n) a b ->
   fibonacci (S n) <= a /\
   fibonacci (S (S n)) <= b.

3b) We reformulate the previous result in a more positive way.

 Lemma Zgcdn_ok_before_fibonacci : forall n a b,
   0 < a < b -> a < fibonacci (S n) ->
   Zis_gcd a b (Zgcdn n a b).

4) The proposed bound leads to a fibonacci number that is big enough.

 Lemma Zgcd_bound_fibonacci :
   forall a, 0 < a -> a < fibonacci (Zgcd_bound a).


 Lemma Zgcdn_is_gcd :
   forall n a b, (Zgcd_bound a <= n)%nat ->
     Zis_gcd a b (Zgcdn n a b).

 Lemma Zgcd_is_gcd :
   forall a b, Zis_gcd a b (Zgcd_alt a b).