Library Coq.Numbers.Integer.BigZ.ZMake
Require
Import
ZArith
.
Require
Import
BigNumPrelude
.
Require
Import
NSig
.
Require
Import
ZSig
.
Open
Scope
Z_scope
.
ZMake
A generic transformation from a structure of natural numbers
NSig.NType
to a structure of integers
ZSig.ZType
.
Module
Make
(
N
:NType) <:
ZType
.
Inductive
t_
:=
|
Pos
:
N.t
->
t_
|
Neg
:
N.t
->
t_
.
Definition
t
:=
t_
.
Definition
zero
:=
Pos
N.zero
.
Definition
one
:=
Pos
N.one
.
Definition
minus_one
:=
Neg
N.one
.
Definition
of_Z
x
:=
match
x
with
|
Zpos
x
=>
Pos
(
N.of_N
(
Npos
x
))
|
Z0
=>
zero
|
Zneg
x
=>
Neg
(
N.of_N
(
Npos
x
))
end
.
Definition
to_Z
x
:=
match
x
with
|
Pos
nx
=>
N.to_Z
nx
|
Neg
nx
=>
Zopp
(
N.to_Z
nx
)
end
.
Theorem
spec_of_Z
:
forall
x
,
to_Z
(
of_Z
x
) =
x
.
Definition
eq
x
y
:= (
to_Z
x
=
to_Z
y
).
Theorem
spec_0
:
to_Z
zero
= 0.
Theorem
spec_1
:
to_Z
one
= 1.
Theorem
spec_m1
:
to_Z
minus_one
= -1.
Definition
compare
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
N.compare
nx
ny
|
Pos
nx
,
Neg
ny
=>
match
N.compare
nx
N.zero
with
|
Gt
=>
Gt
|
_
=>
N.compare
ny
N.zero
end
|
Neg
nx
,
Pos
ny
=>
match
N.compare
N.zero
nx
with
|
Lt
=>
Lt
|
_
=>
N.compare
N.zero
ny
end
|
Neg
nx
,
Neg
ny
=>
N.compare
ny
nx
end
.
Definition
lt
n
m
:=
compare
n
m
=
Lt
.
Definition
le
n
m
:=
compare
n
m
<>
Gt
.
Definition
min
n
m
:=
match
compare
n
m
with
Gt
=>
m
|
_
=>
n
end
.
Definition
max
n
m
:=
match
compare
n
m
with
Lt
=>
m
|
_
=>
n
end
.
Theorem
spec_compare
:
forall
x
y
,
match
compare
x
y
with
Eq
=>
to_Z
x
=
to_Z
y
|
Lt
=>
to_Z
x
<
to_Z
y
|
Gt
=>
to_Z
x
>
to_Z
y
end
.
Definition
eq_bool
x
y
:=
match
compare
x
y
with
|
Eq
=>
true
|
_
=>
false
end
.
Theorem
spec_eq_bool
:
forall
x
y
,
if
eq_bool
x
y
then
to_Z
x
=
to_Z
y
else
to_Z
x
<>
to_Z
y
.
Definition
cmp_sign
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Neg
ny
=>
if
N.eq_bool
ny
N.zero
then
Eq
else
Gt
|
Neg
nx
,
Pos
ny
=>
if
N.eq_bool
nx
N.zero
then
Eq
else
Lt
|
_
,
_
=>
Eq
end
.
Theorem
spec_cmp_sign
:
forall
x
y
,
match
cmp_sign
x
y
with
|
Gt
=> 0 <=
to_Z
x
/\
to_Z
y
< 0
|
Lt
=>
to_Z
x
< 0 /\ 0 <=
to_Z
y
|
Eq
=>
True
end
.
Definition
to_N
x
:=
match
x
with
|
Pos
nx
=>
nx
|
Neg
nx
=>
nx
end
.
Definition
abs
x
:=
Pos
(
to_N
x
).
Theorem
spec_abs
:
forall
x
,
to_Z
(
abs
x
) =
Zabs
(
to_Z
x
).
Definition
opp
x
:=
match
x
with
|
Pos
nx
=>
Neg
nx
|
Neg
nx
=>
Pos
nx
end
.
Theorem
spec_opp
:
forall
x
,
to_Z
(
opp
x
) = -
to_Z
x
.
Definition
succ
x
:=
match
x
with
|
Pos
n
=>
Pos
(
N.succ
n
)
|
Neg
n
=>
match
N.compare
N.zero
n
with
|
Lt
=>
Neg
(
N.pred
n
)
|
_
=>
one
end
end
.
Theorem
spec_succ
:
forall
n
,
to_Z
(
succ
n
) =
to_Z
n
+ 1.
Definition
add
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
Pos
(
N.add
nx
ny
)
|
Pos
nx
,
Neg
ny
=>
match
N.compare
nx
ny
with
|
Gt
=>
Pos
(
N.sub
nx
ny
)
|
Eq
=>
zero
|
Lt
=>
Neg
(
N.sub
ny
nx
)
end
|
Neg
nx
,
Pos
ny
=>
match
N.compare
nx
ny
with
|
Gt
=>
Neg
(
N.sub
nx
ny
)
|
Eq
=>
zero
|
Lt
=>
Pos
(
N.sub
ny
nx
)
end
|
Neg
nx
,
Neg
ny
=>
Neg
(
N.add
nx
ny
)
end
.
Theorem
spec_add
:
forall
x
y
,
to_Z
(
add
x
y
) =
to_Z
x
+
to_Z
y
.
Definition
pred
x
:=
match
x
with
|
Pos
nx
=>
match
N.compare
N.zero
nx
with
|
Lt
=>
Pos
(
N.pred
nx
)
|
_
=>
minus_one
end
|
Neg
nx
=>
Neg
(
N.succ
nx
)
end
.
Theorem
spec_pred
:
forall
x
,
to_Z
(
pred
x
) =
to_Z
x
- 1.
Definition
sub
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
match
N.compare
nx
ny
with
|
Gt
=>
Pos
(
N.sub
nx
ny
)
|
Eq
=>
zero
|
Lt
=>
Neg
(
N.sub
ny
nx
)
end
|
Pos
nx
,
Neg
ny
=>
Pos
(
N.add
nx
ny
)
|
Neg
nx
,
Pos
ny
=>
Neg
(
N.add
nx
ny
)
|
Neg
nx
,
Neg
ny
=>
match
N.compare
nx
ny
with
|
Gt
=>
Neg
(
N.sub
nx
ny
)
|
Eq
=>
zero
|
Lt
=>
Pos
(
N.sub
ny
nx
)
end
end
.
Theorem
spec_sub
:
forall
x
y
,
to_Z
(
sub
x
y
) =
to_Z
x
-
to_Z
y
.
Definition
mul
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
Pos
(
N.mul
nx
ny
)
|
Pos
nx
,
Neg
ny
=>
Neg
(
N.mul
nx
ny
)
|
Neg
nx
,
Pos
ny
=>
Neg
(
N.mul
nx
ny
)
|
Neg
nx
,
Neg
ny
=>
Pos
(
N.mul
nx
ny
)
end
.
Theorem
spec_mul
:
forall
x
y
,
to_Z
(
mul
x
y
) =
to_Z
x
*
to_Z
y
.
Definition
square
x
:=
match
x
with
|
Pos
nx
=>
Pos
(
N.square
nx
)
|
Neg
nx
=>
Pos
(
N.square
nx
)
end
.
Theorem
spec_square
:
forall
x
,
to_Z
(
square
x
) =
to_Z
x
*
to_Z
x
.
Definition
power_pos
x
p
:=
match
x
with
|
Pos
nx
=>
Pos
(
N.power_pos
nx
p
)
|
Neg
nx
=>
match
p
with
|
xH
=>
x
|
xO
_
=>
Pos
(
N.power_pos
nx
p
)
|
xI
_
=>
Neg
(
N.power_pos
nx
p
)
end
end
.
Theorem
spec_power_pos
:
forall
x
n
,
to_Z
(
power_pos
x
n
) =
to_Z
x
^
Zpos
n
.
Definition
sqrt
x
:=
match
x
with
|
Pos
nx
=>
Pos
(
N.sqrt
nx
)
|
Neg
nx
=>
Neg
N.zero
end
.
Theorem
spec_sqrt
:
forall
x
, 0 <=
to_Z
x
->
to_Z
(
sqrt
x
) ^ 2 <=
to_Z
x
< (
to_Z
(
sqrt
x
) + 1) ^ 2.
Definition
div_eucl
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
let
(
q
,
r
) :=
N.div_eucl
nx
ny
in
(
Pos
q
,
Pos
r
)
|
Pos
nx
,
Neg
ny
=>
let
(
q
,
r
) :=
N.div_eucl
nx
ny
in
match
N.compare
N.zero
r
with
|
Eq
=> (
Neg
q
,
zero
)
|
_
=> (
Neg
(
N.succ
q
),
Neg
(
N.sub
ny
r
))
end
|
Neg
nx
,
Pos
ny
=>
let
(
q
,
r
) :=
N.div_eucl
nx
ny
in
match
N.compare
N.zero
r
with
|
Eq
=> (
Neg
q
,
zero
)
|
_
=> (
Neg
(
N.succ
q
),
Pos
(
N.sub
ny
r
))
end
|
Neg
nx
,
Neg
ny
=>
let
(
q
,
r
) :=
N.div_eucl
nx
ny
in
(
Pos
q
,
Neg
r
)
end
.
Theorem
spec_div_eucl
:
forall
x
y
,
to_Z
y
<> 0 ->
let
(
q
,r) :=
div_eucl
x
y
in
(
to_Z
q
,
to_Z
r
) =
Zdiv_eucl
(
to_Z
x
) (
to_Z
y
).
Definition
div
x
y
:=
fst
(
div_eucl
x
y
).
Definition
spec_div
:
forall
x
y
,
to_Z
y
<> 0 ->
to_Z
(
div
x
y
) =
to_Z
x
/
to_Z
y
.
Qed
.
Definition
modulo
x
y
:=
snd
(
div_eucl
x
y
).
Theorem
spec_modulo
:
forall
x
y
,
to_Z
y
<> 0 ->
to_Z
(
modulo
x
y
) =
to_Z
x
mod
to_Z
y
.
Definition
gcd
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
Pos
(
N.gcd
nx
ny
)
|
Pos
nx
,
Neg
ny
=>
Pos
(
N.gcd
nx
ny
)
|
Neg
nx
,
Pos
ny
=>
Pos
(
N.gcd
nx
ny
)
|
Neg
nx
,
Neg
ny
=>
Pos
(
N.gcd
nx
ny
)
end
.
Theorem
spec_gcd
:
forall
a
b
,
to_Z
(
gcd
a
b
) =
Zgcd
(
to_Z
a
) (
to_Z
b
).
End
Make
.