Library Coq.ZArith.Zgcd_alt
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.
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).