Library Coq.ZArith.Znumtheory
This file contains some notions of number theory upon Z numbers:
- a divisibility predicate Zdivide
- a gcd predicate gcd
- Euclid algorithm euclid
- a relatively prime predicate rel_prime
- a prime predicate prime
- an efficient Zgcd function
Syntax for divisibility
Notation "( a | b )" := (
Zdivide a b) (
at level 0) :
Z_scope.
Results concerning divisibility
Lemma Zdivide_refl :
forall a:Z, (
a |
a).
Lemma Zone_divide :
forall a:Z, (1 |
a).
Lemma Zdivide_0 :
forall a:Z, (
a | 0).
Hint Resolve Zdivide_refl Zone_divide Zdivide_0:
zarith.
Lemma Zmult_divide_compat_l :
forall a b c:Z, (
a |
b) -> (
c *
a |
c *
b).
Lemma Zmult_divide_compat_r :
forall a b c:Z, (
a |
b) -> (
a *
c |
b *
c).
Hint Resolve Zmult_divide_compat_l Zmult_divide_compat_r:
zarith.
Lemma Zdivide_plus_r :
forall a b c:Z, (
a |
b) -> (
a |
c) -> (
a |
b +
c).
Lemma Zdivide_opp_r :
forall a b:Z, (
a |
b) -> (
a | -
b).
Lemma Zdivide_opp_r_rev :
forall a b:Z, (
a | -
b) -> (
a |
b).
Lemma Zdivide_opp_l :
forall a b:Z, (
a |
b) -> (-
a |
b).
Lemma Zdivide_opp_l_rev :
forall a b:Z, (-
a |
b) -> (
a |
b).
Lemma Zdivide_minus_l :
forall a b c:Z, (
a |
b) -> (
a |
c) -> (
a |
b -
c).
Lemma Zdivide_mult_l :
forall a b c:Z, (
a |
b) -> (
a |
b *
c).
Lemma Zdivide_mult_r :
forall a b c:Z, (
a |
c) -> (
a |
b *
c).
Lemma Zdivide_factor_r :
forall a b:Z, (
a |
a *
b).
Lemma Zdivide_factor_l :
forall a b:Z, (
a |
b *
a).
Hint Resolve Zdivide_plus_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l
Zdivide_opp_l_rev Zdivide_minus_l Zdivide_mult_l Zdivide_mult_r
Zdivide_factor_r Zdivide_factor_l:
zarith.
Auxiliary result.
Lemma Zmult_one :
forall x y:Z,
x >= 0 ->
x *
y = 1 ->
x = 1.
Only 1 and -1 divide 1.
Lemma Zdivide_1 :
forall x:Z, (
x | 1) ->
x = 1 \/
x = -1.
If a divides b and b divides a then a is b or -b.
Lemma Zdivide_antisym :
forall a b:Z, (
a |
b) -> (
b |
a) ->
a =
b \/
a = -
b.
Theorem Zdivide_trans:
forall a b c, (
a |
b) -> (
b |
c) -> (
a |
c).
If a divides b and b<>0 then |a| <= |b|.
Zdivide can be expressed using Zmod.
Lemma Zmod_divide :
forall a b:Z,
b > 0 ->
a mod b = 0 -> (
b |
a).
Lemma Zdivide_mod :
forall a b:Z,
b > 0 -> (
b |
a) ->
a mod b = 0.
Zdivide is hence decidable
Lemma Zdivide_dec :
forall a b:Z, {(
a |
b)} + {~ (
a |
b)}.
Theorem Zdivide_Zdiv_eq:
forall a b :
Z,
0 <
a -> (
a |
b) ->
b =
a * (
b /
a).
Theorem Zdivide_Zdiv_eq_2:
forall a b c :
Z,
0 <
a -> (
a |
b) -> (
c *
b)/a =
c * (
b /
a).
Theorem Zdivide_Zabs_l:
forall a b, (
Zabs a |
b) -> (
a |
b).
Theorem Zdivide_Zabs_inv_l:
forall a b, (
a |
b) -> (
Zabs a |
b).
Theorem Zdivide_le:
forall a b :
Z,
0 <=
a -> 0 <
b -> (
a |
b) ->
a <=
b.
Theorem Zdivide_Zdiv_lt_pos:
forall a b :
Z,
1 <
a -> 0 <
b -> (
a |
b) -> 0 <
b /
a <
b .
Lemma Zmod_div_mod:
forall n m a, 0 <
n -> 0 <
m ->
(
n |
m) ->
a mod n = (
a mod m)
mod n.
Lemma Zmod_divide_minus:
forall a b c :
Z, 0 <
b ->
a mod b =
c -> (
b |
a -
c).
Lemma Zdivide_mod_minus:
forall a b c :
Z, 0 <=
c <
b ->
(
b |
a -
c) ->
a mod b =
c.
Greatest common divisor (gcd).
There is no unicity of the gcd; hence we define the predicate gcd a b d
expressing that d is a gcd of a and b.
(We show later that the gcd is actually unique if we discard its sign.)
Inductive Zis_gcd (
a b d:Z) :
Prop :=
Zis_gcd_intro :
(
d |
a) ->
(
d |
b) -> (
forall x:Z, (
x |
a) -> (
x |
b) -> (
x |
d)) ->
Zis_gcd a b d.
Trivial properties of gcd
Extended Euclid algorithm.
Euclid's algorithm to compute the gcd mainly relies on
the following property.
We implement the extended version of Euclid's algorithm,
i.e. the one computing Bezout's coefficients as it computes
the gcd. We follow the algorithm given in Knuth's
"Art of Computer Programming", vol 2, page 325.
The specification of Euclid's algorithm is the existence of
u, v and d such that ua+vb=d and (gcd a b d).
The recursive part of Euclid's algorithm uses well-founded
recursion of non-negative integers. It maintains 6 integers
u1,u2,u3,v1,v2,v3 such that the following invariant holds:
u1*a+u2*b=u3 and v1*a+v2*b=v3 and gcd(u2,v3)=gcd(a,b).
Lemma euclid_rec :
forall v3:Z,
0 <=
v3 ->
forall u1 u2 u3 v1 v2:Z,
u1 *
a +
u2 *
b =
u3 ->
v1 *
a +
v2 *
b =
v3 ->
(
forall d:Z,
Zis_gcd u3 v3 d ->
Zis_gcd a b d) ->
Euclid.
We get Euclid's algorithm by applying euclid_rec on
1,0,a,0,1,b when b>=0 and 1,0,a,0,-1,-b when b<0.
Existence of Bezout's coefficients for the gcd of a and b
gcd of ca and cb is c gcd(a,b).
Bezout's theorem: a and b are relatively prime if and
only if there exist u and v such that ua+vb = 1.
Gauss's theorem: if a divides bc and if a and b are
relatively prime, then a divides c.
Theorem Gauss :
forall a b c:Z, (
a |
b *
c) ->
rel_prime a b -> (
a |
c).
If a is relatively prime to b and c, then it is to bc
After factorization by a gcd, the original numbers are relatively prime.
The sole divisors of a prime number p are -1, 1, p and -p.
Lemma prime_divisors :
forall p:Z,
prime p ->
forall a:Z, (
a |
p) ->
a = -1 \/
a = 1 \/
a =
p \/
a = -
p.
A prime number is relatively prime with any number it does not divide
As a consequence, a prime number is relatively prime with smaller numbers
If a prime p divides ab then it divides either a or b
We could obtain a Zgcd function via Euclid algorithm. But we propose
here a binary version of Zgcd, faster and executable within Coq.
Algorithm:
gcd 0 b = b
gcd a 0 = a
gcd (2a) (2b) = 2(gcd a b)
gcd (2a+1) (2b) = gcd (2a+1) b
gcd (2a) (2b+1) = gcd a (2b+1)
gcd (2a+1) (2b+1) = gcd (b-a) (2*a+1)
or gcd (a-b) (2*b+1), depending on whether a<b
Open Scope positive_scope.
Fixpoint Pgcdn (
n:
nat) (
a b :
positive) {
struct n } :
positive :=
match n with
|
O => 1
|
S n =>
match a,b
with
|
xH,
_ => 1
|
_,
xH => 1
|
xO a,
xO b =>
xO (
Pgcdn n a b)
|
a,
xO b =>
Pgcdn n a b
|
xO a,
b =>
Pgcdn n a b
|
xI a',
xI b' =>
match Pcompare a' b' Eq with
|
Eq =>
a
|
Lt =>
Pgcdn n (
b'-a')
a
|
Gt =>
Pgcdn n (
a'-b')
b
end
end
end.
Definition Pgcd (
a b:
positive) :=
Pgcdn (
Psize a +
Psize b)%nat
a b.
Close Scope positive_scope.
Definition Zgcd (
a b :
Z) :
Z :=
match a,b
with
|
Z0,
_ =>
Zabs b
|
_,
Z0 =>
Zabs a
|
Zpos a,
Zpos b =>
Zpos (
Pgcd a b)
|
Zpos a,
Zneg b =>
Zpos (
Pgcd a b)
|
Zneg a,
Zpos b =>
Zpos (
Pgcd a b)
|
Zneg a,
Zneg b =>
Zpos (
Pgcd a b)
end.
Lemma Zgcd_is_pos :
forall a b, 0 <=
Zgcd a b.
Lemma Zis_gcd_even_odd :
forall a b g,
Zis_gcd (
Zpos a) (
Zpos (
xI b))
g ->
Zis_gcd (
Zpos (
xO a)) (
Zpos (
xI b))
g.
Lemma Pgcdn_correct :
forall n a b, (
Psize a +
Psize b<=n)%nat ->
Zis_gcd (
Zpos a) (
Zpos b) (
Zpos (
Pgcdn n a b)).
Lemma Pgcd_correct :
forall a b,
Zis_gcd (
Zpos a) (
Zpos b) (
Zpos (
Pgcd a b)).
Lemma Zgcd_is_gcd :
forall a b,
Zis_gcd a b (
Zgcd a b).
Theorem Zgcd_spec :
forall x y :
Z, {
z :
Z |
Zis_gcd x y z /\ 0 <=
z}.
Theorem Zdivide_Zgcd:
forall p q r :
Z,
(
p |
q) -> (
p |
r) -> (
p |
Zgcd q r).
Theorem Zis_gcd_gcd:
forall a b c :
Z,
0 <=
c ->
Zis_gcd a b c ->
Zgcd a b =
c.
Theorem Zgcd_inv_0_l:
forall x y,
Zgcd x y = 0 ->
x = 0.
Theorem Zgcd_inv_0_r:
forall x y,
Zgcd x y = 0 ->
y = 0.
Theorem Zgcd_div_swap0 :
forall a b :
Z,
0 <
Zgcd a b ->
0 <
b ->
(
a /
Zgcd a b) *
b =
a * (
b/Zgcd
a b).
Theorem Zgcd_div_swap :
forall a b c :
Z,
0 <
Zgcd a b ->
0 <
b ->
(
c *
a) /
Zgcd a b *
b =
c *
a * (
b/Zgcd
a b).
Theorem Zgcd_1_rel_prime :
forall a b,
Zgcd a b = 1 <->
rel_prime a b.
Definition rel_prime_dec:
forall a b,
{
rel_prime a b }+{ ~
rel_prime a b }.
Definition prime_dec_aux:
forall p m,
{
forall n, 1 <
n <
m ->
rel_prime n p } +
{
exists n, 1 <
n <
m /\ ~
rel_prime n p }.
Definition prime_dec:
forall p, {
prime p }+{ ~
prime p }.
Theorem not_prime_divide:
forall p, 1 <
p -> ~
prime p ->
exists n, 1 <
n <
p /\ (
n |
p).
A Generalized Gcd that also computes Bezout coefficients.
The algorithm is the same as for Zgcd.
Open Scope positive_scope.
Fixpoint Pggcdn (
n:
nat) (
a b :
positive) {
struct n } : (
positive*(positive*positive)) :=
match n with
|
O => (1,(a,b))
|
S n =>
match a,b
with
|
xH,
b => (1,(1,b))
|
a,
xH => (1,(a,1))
|
xO a,
xO b =>
let (
g,p) :=
Pggcdn n a b in
(
xO g,p)
|
a,
xO b =>
let (
g,p) :=
Pggcdn n a b in
let (
aa,bb) :=
p in
(
g,(aa,
xO bb))
|
xO a,
b =>
let (
g,p) :=
Pggcdn n a b in
let (
aa,bb) :=
p in
(
g,(xO
aa,
bb))
|
xI a',
xI b' =>
match Pcompare a' b' Eq with
|
Eq => (
a,(1,1))
|
Lt =>
let (
g,p) :=
Pggcdn n (
b'-a')
a in
let (
ba,aa) :=
p in
(
g,(aa,
aa +
xO ba))
|
Gt =>
let (
g,p) :=
Pggcdn n (
a'-b')
b in
let (
ab,bb) :=
p in
(
g,(bb+xO
ab,
bb))
end
end
end.
Definition Pggcd (
a b:
positive) :=
Pggcdn (
Psize a +
Psize b)%nat
a b.
Open Scope Z_scope.
Definition Zggcd (
a b :
Z) :
Z*(Z*Z) :=
match a,b
with
|
Z0,
_ => (
Zabs b,(0,
Zsgn b))
|
_,
Z0 => (
Zabs a,(Zsgn
a, 0))
|
Zpos a,
Zpos b =>
let (
g,p) :=
Pggcd a b in
let (
aa,bb) :=
p in
(
Zpos g, (
Zpos aa,
Zpos bb))
|
Zpos a,
Zneg b =>
let (
g,p) :=
Pggcd a b in
let (
aa,bb) :=
p in
(
Zpos g, (
Zpos aa,
Zneg bb))
|
Zneg a,
Zpos b =>
let (
g,p) :=
Pggcd a b in
let (
aa,bb) :=
p in
(
Zpos g, (
Zneg aa,
Zpos bb))
|
Zneg a,
Zneg b =>
let (
g,p) :=
Pggcd a b in
let (
aa,bb) :=
p in
(
Zpos g, (
Zneg aa,
Zneg bb))
end.
Lemma Pggcdn_gcdn :
forall n a b,
fst (
Pggcdn n a b) =
Pgcdn n a b.
Lemma Pggcd_gcd :
forall a b,
fst (
Pggcd a b) =
Pgcd a b.
Lemma Zggcd_gcd :
forall a b,
fst (
Zggcd a b) =
Zgcd a b.
Open Scope positive_scope.
Lemma Pggcdn_correct_divisors :
forall n a b,
let (
g,p) :=
Pggcdn n a b in
let (
aa,bb):=p
in
(
a=g*aa) /\ (
b=g*bb).
Lemma Pggcd_correct_divisors :
forall a b,
let (
g,p) :=
Pggcd a b in
let (
aa,bb):=p
in
(
a=g*aa) /\ (
b=g*bb).
Close Scope positive_scope.
Lemma Zggcd_correct_divisors :
forall a b,
let (
g,p) :=
Zggcd a b in
let (
aa,bb):=p
in
(
a=g*aa) /\ (
b=g*bb).
Theorem Zggcd_opp:
forall x y,
Zggcd (-x)
y =
let (
p1,p) :=
Zggcd x y in
let (
p2,p3) :=
p in
(
p1,(-p2,p3)).