Library Coq.ZArith.ZOdiv_def
Require Import BinPos BinNat Nnat ZArith_base.
Open Scope Z_scope.
Definition NPgeb (
a:
N)(
b:
positive) :=
match a with
|
N0 =>
false
|
Npos na =>
match Pcompare na b Eq with Lt =>
false |
_ =>
true end
end.
Fixpoint Pdiv_eucl (
a b:
positive) :
N * N :=
match a with
|
xH =>
match b with xH =>
(1
, 0
)%
N |
_ =>
(0
, 1
)%
N end
|
xO a' =>
let (
q,
r) :=
Pdiv_eucl a' b in
let r' := (2
* r)%
N in
if (
NPgeb r' b)
then (2
* q + 1
, (Nminus r' (
Npos b)
))%
N
else (2
* q, r')%
N
|
xI a' =>
let (
q,
r) :=
Pdiv_eucl a' b in
let r' := (2
* r + 1)%
N in
if (
NPgeb r' b)
then (2
* q + 1
, (Nminus r' (
Npos b)
))%
N
else (2
* q, r')%
N
end.
Definition ZOdiv_eucl (
a b:
Z) :
Z * Z :=
match a,
b with
|
Z0,
_ =>
(Z0, Z0)
|
_,
Z0 =>
(Z0, a)
|
Zpos na,
Zpos nb =>
let (
nq,
nr) :=
Pdiv_eucl na nb in
(Z_of_N nq, Z_of_N nr)
|
Zneg na,
Zpos nb =>
let (
nq,
nr) :=
Pdiv_eucl na nb in
(Zopp (
Z_of_N nq)
, Zopp (
Z_of_N nr)
)
|
Zpos na,
Zneg nb =>
let (
nq,
nr) :=
Pdiv_eucl na nb in
(Zopp (
Z_of_N nq)
, Z_of_N nr)
|
Zneg na,
Zneg nb =>
let (
nq,
nr) :=
Pdiv_eucl na nb in
(Z_of_N nq, Zopp (
Z_of_N nr)
)
end.
Definition ZOdiv a b :=
fst (
ZOdiv_eucl a b).
Definition ZOmod a b :=
snd (
ZOdiv_eucl a b).
Definition Ndiv_eucl (
a b:
N) :
N * N :=
match a,
b with
|
N0,
_ =>
(N0, N0)
|
_,
N0 =>
(N0, a)
|
Npos na,
Npos nb =>
Pdiv_eucl na nb
end.
Definition Ndiv a b :=
fst (
Ndiv_eucl a b).
Definition Nmod a b :=
snd (
Ndiv_eucl a b).
Theorem NPgeb_correct:
forall (
a:
N)(
b:
positive),
if NPgeb a b then a = (
Nminus a (
Npos b)
+ Npos b)%
N else True.
Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc
Zmult_plus_distr_l Zmult_plus_distr_r :
zdiv.
Hint Rewrite <-
Zplus_assoc :
zdiv.
Theorem Pdiv_eucl_correct:
forall a b,
let (
q,
r) :=
Pdiv_eucl a b in
Zpos a = Z_of_N q * Zpos b + Z_of_N r.
Theorem ZOdiv_eucl_correct:
forall a b,
let (
q,
r) :=
ZOdiv_eucl a b in a = q * b + r.
Theorem Ndiv_eucl_correct:
forall a b,
let (
q,
r) :=
Ndiv_eucl a b in a = (
q * b + r)%
N.