Library Coq.ZArith.Zgcd_alt


Zgcd_alt : an alternate version of Z.gcd, based on Euclid's algorithm

Author: Pierre Letouzey
The alternate Zgcd_alt given here used to be the main Z.gcd function (see file Znumtheory), but this main Z.gcd is now based on a modern binary-efficient algorithm. This earlier version, based on Euclid'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.
Require Import Omega.

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 => Z.abs b
                | Zpos _ => Zgcdn n (Z.modulo b a) a
                | Zneg a => Zgcdn n (Z.modulo b (Zpos a)) (Zpos a)
              end
   end.

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

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

A first obvious fact : Z.gcd 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 Z.gcd is indeed a gcd.
1) We prove a weaker & easier bound.

 Lemma Zgcdn_linear_bound : forall n a b,
   Z.abs 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 Zgcd_bound_opp a : Zgcd_bound (-a) = Zgcd_bound a.

 Lemma Zgcdn_opp n a b : Zgcdn n (-a) b = Zgcdn n a b.

 Lemma Zgcdn_is_gcd_pos n a b : (Zgcd_bound (Zpos a) <= n)%nat ->
   Zis_gcd (Zpos a) b (Zgcdn n (Zpos a) b).

 Lemma Zgcdn_is_gcd 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).