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
(
NN
:
NType
) <:
ZType
.
Inductive
t_
:=
|
Pos
:
NN.t
->
t_
|
Neg
:
NN.t
->
t_
.
Definition
t
:=
t_
.
Definition
zero
:=
Pos
NN.zero
.
Definition
one
:=
Pos
NN.one
.
Definition
two
:=
Pos
NN.two
.
Definition
minus_one
:=
Neg
NN.one
.
Definition
of_Z
x
:=
match
x
with
|
Zpos
x
=>
Pos
(
NN.of_N
(
Npos
x
))
|
Z0
=>
zero
|
Zneg
x
=>
Neg
(
NN.of_N
(
Npos
x
))
end
.
Definition
to_Z
x
:=
match
x
with
|
Pos
nx
=>
NN.to_Z
nx
|
Neg
nx
=>
Z.opp
(
NN.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_2
:
to_Z
two
=
2.
Theorem
spec_m1
:
to_Z
minus_one
=
-1.
Definition
compare
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
NN.compare
nx
ny
|
Pos
nx
,
Neg
ny
=>
match
NN.compare
nx
NN.zero
with
|
Gt
=>
Gt
|
_
=>
NN.compare
ny
NN.zero
end
|
Neg
nx
,
Pos
ny
=>
match
NN.compare
NN.zero
nx
with
|
Lt
=>
Lt
|
_
=>
NN.compare
NN.zero
ny
end
|
Neg
nx
,
Neg
ny
=>
NN.compare
ny
nx
end
.
Theorem
spec_compare
:
forall
x
y
,
compare
x
y
=
Z.compare
(
to_Z
x
) (
to_Z
y
).
Definition
eqb
x
y
:=
match
compare
x
y
with
|
Eq
=>
true
|
_
=>
false
end
.
Theorem
spec_eqb
x
y
:
eqb
x
y
=
Z.eqb
(
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
ltb
(
x
y
:
t
) :
bool
:=
match
compare
x
y
with
|
Lt
=>
true
|
_
=>
false
end
.
Theorem
spec_ltb
x
y
:
ltb
x
y
=
Z.ltb
(
to_Z
x
) (
to_Z
y
).
Definition
leb
(
x
y
:
t
) :
bool
:=
match
compare
x
y
with
|
Gt
=>
false
|
_
=>
true
end
.
Theorem
spec_leb
x
y
:
leb
x
y
=
Z.leb
(
to_Z
x
) (
to_Z
y
).
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
)
=
Z.min
(
to_Z
n
) (
to_Z
m
).
Theorem
spec_max
:
forall
n
m
,
to_Z
(
max
n
m
)
=
Z.max
(
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
)
=
Z.abs
(
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
(
NN.succ
n
)
|
Neg
n
=>
match
NN.compare
NN.zero
n
with
|
Lt
=>
Neg
(
NN.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
(
NN.add
nx
ny
)
|
Pos
nx
,
Neg
ny
=>
match
NN.compare
nx
ny
with
|
Gt
=>
Pos
(
NN.sub
nx
ny
)
|
Eq
=>
zero
|
Lt
=>
Neg
(
NN.sub
ny
nx
)
end
|
Neg
nx
,
Pos
ny
=>
match
NN.compare
nx
ny
with
|
Gt
=>
Neg
(
NN.sub
nx
ny
)
|
Eq
=>
zero
|
Lt
=>
Pos
(
NN.sub
ny
nx
)
end
|
Neg
nx
,
Neg
ny
=>
Neg
(
NN.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
NN.compare
NN.zero
nx
with
|
Lt
=>
Pos
(
NN.pred
nx
)
|
_
=>
minus_one
end
|
Neg
nx
=>
Neg
(
NN.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
NN.compare
nx
ny
with
|
Gt
=>
Pos
(
NN.sub
nx
ny
)
|
Eq
=>
zero
|
Lt
=>
Neg
(
NN.sub
ny
nx
)
end
|
Pos
nx
,
Neg
ny
=>
Pos
(
NN.add
nx
ny
)
|
Neg
nx
,
Pos
ny
=>
Neg
(
NN.add
nx
ny
)
|
Neg
nx
,
Neg
ny
=>
match
NN.compare
nx
ny
with
|
Gt
=>
Neg
(
NN.sub
nx
ny
)
|
Eq
=>
zero
|
Lt
=>
Pos
(
NN.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
(
NN.mul
nx
ny
)
|
Pos
nx
,
Neg
ny
=>
Neg
(
NN.mul
nx
ny
)
|
Neg
nx
,
Pos
ny
=>
Neg
(
NN.mul
nx
ny
)
|
Neg
nx
,
Neg
ny
=>
Pos
(
NN.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
(
NN.square
nx
)
|
Neg
nx
=>
Pos
(
NN.square
nx
)
end
.
Theorem
spec_square
:
forall
x
,
to_Z
(
square
x
)
=
to_Z
x
*
to_Z
x
.
Definition
pow_pos
x
p
:=
match
x
with
|
Pos
nx
=>
Pos
(
NN.pow_pos
nx
p
)
|
Neg
nx
=>
match
p
with
|
xH
=>
x
|
xO
_
=>
Pos
(
NN.pow_pos
nx
p
)
|
xI
_
=>
Neg
(
NN.pow_pos
nx
p
)
end
end
.
Theorem
spec_pow_pos
:
forall
x
n
,
to_Z
(
pow_pos
x
n
)
=
to_Z
x
^
Zpos
n
.
Definition
pow_N
x
n
:=
match
n
with
|
N0
=>
one
|
Npos
p
=>
pow_pos
x
p
end
.
Theorem
spec_pow_N
:
forall
x
n
,
to_Z
(
pow_N
x
n
)
=
to_Z
x
^
Z.of_N
n
.
Definition
pow
x
y
:=
match
to_Z
y
with
|
Z0
=>
one
|
Zpos
p
=>
pow_pos
x
p
|
Zneg
p
=>
zero
end
.
Theorem
spec_pow
:
forall
x
y
,
to_Z
(
pow
x
y
)
=
to_Z
x
^
to_Z
y
.
Definition
log2
x
:=
match
x
with
|
Pos
nx
=>
Pos
(
NN.log2
nx
)
|
Neg
nx
=>
zero
end
.
Theorem
spec_log2
:
forall
x
,
to_Z
(
log2
x
)
=
Z.log2
(
to_Z
x
).
Definition
sqrt
x
:=
match
x
with
|
Pos
nx
=>
Pos
(
NN.sqrt
nx
)
|
Neg
nx
=>
Neg
NN.zero
end
.
Theorem
spec_sqrt
:
forall
x
,
to_Z
(
sqrt
x
)
=
Z.sqrt
(
to_Z
x
).
Definition
div_eucl
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
let
(
q
,
r
) :=
NN.div_eucl
nx
ny
in
(
Pos
q
,
Pos
r
)
|
Pos
nx
,
Neg
ny
=>
let
(
q
,
r
) :=
NN.div_eucl
nx
ny
in
if
NN.eqb
NN.zero
r
then
(
Neg
q
,
zero
)
else
(
Neg
(
NN.succ
q
)
,
Neg
(
NN.sub
ny
r
)
)
|
Neg
nx
,
Pos
ny
=>
let
(
q
,
r
) :=
NN.div_eucl
nx
ny
in
if
NN.eqb
NN.zero
r
then
(
Neg
q
,
zero
)
else
(
Neg
(
NN.succ
q
)
,
Pos
(
NN.sub
ny
r
)
)
|
Neg
nx
,
Neg
ny
=>
let
(
q
,
r
) :=
NN.div_eucl
nx
ny
in
(
Pos
q
,
Neg
r
)
end
.
Ltac
break_nonneg
x
px
EQx
:=
let
H
:=
fresh
"H"
in
assert
(
H
:=
NN.spec_pos
x
);
destruct
(
NN.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
)
=
Z.div_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
quot
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
Pos
(
NN.div
nx
ny
)
|
Pos
nx
,
Neg
ny
=>
Neg
(
NN.div
nx
ny
)
|
Neg
nx
,
Pos
ny
=>
Neg
(
NN.div
nx
ny
)
|
Neg
nx
,
Neg
ny
=>
Pos
(
NN.div
nx
ny
)
end
.
Definition
rem
x
y
:=
if
eqb
y
zero
then
x
else
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
Pos
(
NN.modulo
nx
ny
)
|
Pos
nx
,
Neg
ny
=>
Pos
(
NN.modulo
nx
ny
)
|
Neg
nx
,
Pos
ny
=>
Neg
(
NN.modulo
nx
ny
)
|
Neg
nx
,
Neg
ny
=>
Neg
(
NN.modulo
nx
ny
)
end
.
Lemma
spec_quot
:
forall
x
y
,
to_Z
(
quot
x
y
)
=
(
to_Z
x
)
÷
(
to_Z
y
)
.
Lemma
spec_rem
:
forall
x
y
,
to_Z
(
rem
x
y
)
=
Z.rem
(
to_Z
x
) (
to_Z
y
).
Definition
gcd
x
y
:=
match
x
,
y
with
|
Pos
nx
,
Pos
ny
=>
Pos
(
NN.gcd
nx
ny
)
|
Pos
nx
,
Neg
ny
=>
Pos
(
NN.gcd
nx
ny
)
|
Neg
nx
,
Pos
ny
=>
Pos
(
NN.gcd
nx
ny
)
|
Neg
nx
,
Neg
ny
=>
Pos
(
NN.gcd
nx
ny
)
end
.
Theorem
spec_gcd
:
forall
a
b
,
to_Z
(
gcd
a
b
)
=
Z.gcd
(
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
)
=
Z.sgn
(
to_Z
x
).
Definition
even
z
:=
match
z
with
|
Pos
n
=>
NN.even
n
|
Neg
n
=>
NN.even
n
end
.
Definition
odd
z
:=
match
z
with
|
Pos
n
=>
NN.odd
n
|
Neg
n
=>
NN.odd
n
end
.
Lemma
spec_even
:
forall
z
,
even
z
=
Z.even
(
to_Z
z
).
Lemma
spec_odd
:
forall
z
,
odd
z
=
Z.odd
(
to_Z
z
).
Definition
norm_pos
z
:=
match
z
with
|
Pos
_
=>
z
|
Neg
n
=>
if
NN.eqb
n
NN.zero
then
Pos
n
else
z
end
.
Definition
testbit
a
n
:=
match
norm_pos
n
,
norm_pos
a
with
|
Pos
p
,
Pos
a
=>
NN.testbit
a
p
|
Pos
p
,
Neg
a
=>
negb
(
NN.testbit
(
NN.pred
a
)
p
)
|
Neg
p
,
_
=>
false
end
.
Definition
shiftl
a
n
:=
match
norm_pos
a
,
n
with
|
Pos
a
,
Pos
n
=>
Pos
(
NN.shiftl
a
n
)
|
Pos
a
,
Neg
n
=>
Pos
(
NN.shiftr
a
n
)
|
Neg
a
,
Pos
n
=>
Neg
(
NN.shiftl
a
n
)
|
Neg
a
,
Neg
n
=>
Neg
(
NN.succ
(
NN.shiftr
(
NN.pred
a
)
n
))
end
.
Definition
shiftr
a
n
:=
shiftl
a
(
opp
n
).
Definition
lor
a
b
:=
match
norm_pos
a
,
norm_pos
b
with
|
Pos
a
,
Pos
b
=>
Pos
(
NN.lor
a
b
)
|
Neg
a
,
Pos
b
=>
Neg
(
NN.succ
(
NN.ldiff
(
NN.pred
a
)
b
))
|
Pos
a
,
Neg
b
=>
Neg
(
NN.succ
(
NN.ldiff
(
NN.pred
b
)
a
))
|
Neg
a
,
Neg
b
=>
Neg
(
NN.succ
(
NN.land
(
NN.pred
a
) (
NN.pred
b
)))
end
.
Definition
land
a
b
:=
match
norm_pos
a
,
norm_pos
b
with
|
Pos
a
,
Pos
b
=>
Pos
(
NN.land
a
b
)
|
Neg
a
,
Pos
b
=>
Pos
(
NN.ldiff
b
(
NN.pred
a
))
|
Pos
a
,
Neg
b
=>
Pos
(
NN.ldiff
a
(
NN.pred
b
))
|
Neg
a
,
Neg
b
=>
Neg
(
NN.succ
(
NN.lor
(
NN.pred
a
) (
NN.pred
b
)))
end
.
Definition
ldiff
a
b
:=
match
norm_pos
a
,
norm_pos
b
with
|
Pos
a
,
Pos
b
=>
Pos
(
NN.ldiff
a
b
)
|
Neg
a
,
Pos
b
=>
Neg
(
NN.succ
(
NN.lor
(
NN.pred
a
)
b
))
|
Pos
a
,
Neg
b
=>
Pos
(
NN.land
a
(
NN.pred
b
))
|
Neg
a
,
Neg
b
=>
Pos
(
NN.ldiff
(
NN.pred
b
) (
NN.pred
a
))
end
.
Definition
lxor
a
b
:=
match
norm_pos
a
,
norm_pos
b
with
|
Pos
a
,
Pos
b
=>
Pos
(
NN.lxor
a
b
)
|
Neg
a
,
Pos
b
=>
Neg
(
NN.succ
(
NN.lxor
(
NN.pred
a
)
b
))
|
Pos
a
,
Neg
b
=>
Neg
(
NN.succ
(
NN.lxor
a
(
NN.pred
b
)))
|
Neg
a
,
Neg
b
=>
Pos
(
NN.lxor
(
NN.pred
a
) (
NN.pred
b
))
end
.
Definition
div2
x
:=
shiftr
x
one
.
Lemma
Zlnot_alt1
:
forall
x
,
-(
x
+
1
)
=
Z.lnot
x
.
Lemma
Zlnot_alt2
:
forall
x
,
Z.lnot
(
x
-
1)
=
-
x
.
Lemma
Zlnot_alt3
:
forall
x
,
Z.lnot
(
-
x
)
=
x
-
1.
Lemma
spec_norm_pos
:
forall
x
,
to_Z
(
norm_pos
x
)
=
to_Z
x
.
Lemma
spec_norm_pos_pos
:
forall
x
y
,
norm_pos
x
=
Neg
y
->
0
<
NN.to_Z
y
.
Ltac
destr_norm_pos
x
:=
rewrite
<- (
spec_norm_pos
x
);
let
H
:=
fresh
in
let
x'
:=
fresh
x
in
assert
(
H
:=
spec_norm_pos_pos
x
);
destruct
(
norm_pos
x
)
as
[
x'
|
x'
];
specialize
(
H
x'
(
eq_refl
_
)) ||
clear
H
.
Lemma
spec_testbit
:
forall
x
p
,
testbit
x
p
=
Z.testbit
(
to_Z
x
) (
to_Z
p
).
Lemma
spec_shiftl
:
forall
x
p
,
to_Z
(
shiftl
x
p
)
=
Z.shiftl
(
to_Z
x
) (
to_Z
p
).
Lemma
spec_shiftr
:
forall
x
p
,
to_Z
(
shiftr
x
p
)
=
Z.shiftr
(
to_Z
x
) (
to_Z
p
).
Lemma
spec_land
:
forall
x
y
,
to_Z
(
land
x
y
)
=
Z.land
(
to_Z
x
) (
to_Z
y
).
Lemma
spec_lor
:
forall
x
y
,
to_Z
(
lor
x
y
)
=
Z.lor
(
to_Z
x
) (
to_Z
y
).
Lemma
spec_ldiff
:
forall
x
y
,
to_Z
(
ldiff
x
y
)
=
Z.ldiff
(
to_Z
x
) (
to_Z
y
).
Lemma
spec_lxor
:
forall
x
y
,
to_Z
(
lxor
x
y
)
=
Z.lxor
(
to_Z
x
) (
to_Z
y
).
Lemma
spec_div2
:
forall
x
,
to_Z
(
div2
x
)
=
Z.div2
(
to_Z
x
).
End
Make
.