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
.
Theorem
spec_compare
:
forall
x
y
,
compare
x
y
=
Zcompare
(
to_Z
x
) (
to_Z
y
).
Definition
eq_bool
x
y
:=
match
compare
x
y
with
|
Eq
=>
true
|
_
=>
false
end
.
Theorem
spec_eq_bool
:
forall
x
y
,
eq_bool
x
y
=
Zeq_bool
(
to_Z
x
) (
to_Z
y
).
Definition
lt
n
m
:=
to_Z
n
<
to_Z
m
.
Definition
le
n
m
:=
to_Z
n
<=
to_Z
m
.
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_min
:
forall
n
m
,
to_Z
(
min
n
m
)
=
Zmin
(
to_Z
n
) (
to_Z
m
).
Theorem
spec_max
:
forall
n
m
,
to_Z
(
max
n
m
)
=
Zmax
(
to_Z
n
) (
to_Z
m
).
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
power
x
n
:=
match
n
with
|
N0
=>
one
|
Npos
p
=>
power_pos
x
p
end
.
Theorem
spec_power
:
forall
x
n
,
to_Z
(
power
x
n
)
=
to_Z
x
^
Z_of_N
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
if
N.eq_bool
N.zero
r
then
(
Neg
q
,
zero
)
else
(
Neg
(
N.succ
q
)
,
Neg
(
N.sub
ny
r
)
)
|
Neg
nx
,
Pos
ny
=>
let
(
q
,
r
) :=
N.div_eucl
nx
ny
in
if
N.eq_bool
N.zero
r
then
(
Neg
q
,
zero
)
else
(
Neg
(
N.succ
q
)
,
Pos
(
N.sub
ny
r
)
)
|
Neg
nx
,
Neg
ny
=>
let
(
q
,
r
) :=
N.div_eucl
nx
ny
in
(
Pos
q
,
Neg
r
)
end
.
Ltac
break_nonneg
x
px
EQx
:=
let
H
:=
fresh
"H"
in
assert
(
H
:=
N.spec_pos
x
);
destruct
(
N.to_Z
x
)
as
[|
px
|
px
]
_eqn
:
EQx
;
[
clear
H
|
clear
H
|
elim
H
;
reflexivity
].
Theorem
spec_div_eucl
:
forall
x
y
,
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
(
div
x
y
)
=
to_Z
x
/
to_Z
y
.
Definition
modulo
x
y
:=
snd
(
div_eucl
x
y
).
Theorem
spec_modulo
:
forall
x
y
,
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
).
Definition
sgn
x
:=
match
compare
zero
x
with
|
Lt
=>
one
|
Eq
=>
zero
|
Gt
=>
minus_one
end
.
Lemma
spec_sgn
:
forall
x
,
to_Z
(
sgn
x
)
=
Zsgn
(
to_Z
x
).
End
Make
.