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) {
struct a} :
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.