Library Coq.Numbers.Cyclic.Int63.Cyclic63
Int63 numbers defines indeed a cyclic structure : Z/(2^31)Z
Author: Arnaud Spiwack (+ Pierre Letouzey)
Require
Import
CyclicAxioms
.
Require
Export
ZArith
.
Require
Export
Int63
.
Import
Zpow_facts
.
Import
Utf8
.
Import
Lia
.
Local Open
Scope
int63_scope
.
{2 Operators }
Definition
Pdigits
:=
Eval
compute
in
P_of_succ_nat
(
size
-
1).
Fixpoint
positive_to_int_rec
(
n
:
nat
) (
p
:
positive
) :=
match
n
,
p
with
|
O
,
_
=>
(
Npos
p
,
0
)
|
S
n
,
xH
=>
(
0%
N
,
1
)
|
S
n
,
xO
p
=>
let
(
N
,
i
) :=
positive_to_int_rec
n
p
in
(
N
,
i
<<
1
)
|
S
n
,
xI
p
=>
let
(
N
,
i
) :=
positive_to_int_rec
n
p
in
(
N
,
(
i
<<
1
)
+
1
)
end
.
Definition
positive_to_int
:=
positive_to_int_rec
size
.
Definition
mulc_WW
x
y
:=
let
(
h
,
l
) :=
mulc
x
y
in
if
is_zero
h
then
if
is_zero
l
then
W0
else
WW
h
l
else
WW
h
l
.
Notation
"
n '*c' m" := (
mulc_WW
n
m
) (
at
level
40,
no
associativity
) :
int63_scope
.
Definition
pos_mod
p
x
:=
if
p
<=
digits
then
let
p
:=
digits
-
p
in
(
x
<<
p
)
>>
p
else
x
.
Notation
pos_mod_int
:=
pos_mod
.
Import
ZnZ
.
Instance
int_ops
:
ZnZ.Ops
int
:=
{|
digits
:=
Pdigits
;
zdigits
:=
Int63.digits
;
to_Z
:=
Int63.to_Z
;
of_pos
:=
positive_to_int
;
head0
:=
Int63.head0
;
tail0
:=
Int63.tail0
;
zero
:= 0;
one
:= 1;
minus_one
:=
Int63.max_int
;
compare
:=
Int63.compare
;
eq0
:=
Int63.is_zero
;
opp_c
:=
Int63.oppc
;
opp
:=
Int63.opp
;
opp_carry
:=
Int63.oppcarry
;
succ_c
:=
Int63.succc
;
add_c
:=
Int63.addc
;
add_carry_c
:=
Int63.addcarryc
;
succ
:=
Int63.succ
;
add
:=
Int63.add
;
add_carry
:=
Int63.addcarry
;
pred_c
:=
Int63.predc
;
sub_c
:=
Int63.subc
;
sub_carry_c
:=
Int63.subcarryc
;
pred
:=
Int63.pred
;
sub
:=
Int63.sub
;
sub_carry
:=
Int63.subcarry
;
mul_c
:=
mulc_WW
;
mul
:=
Int63.mul
;
square_c
:=
fun
x
=>
mulc_WW
x
x
;
div21
:=
diveucl_21
;
div_gt
:=
diveucl
;
div
:=
diveucl
;
modulo_gt
:=
Int63.mod
;
modulo
:=
Int63.mod
;
gcd_gt
:=
Int63.gcd
;
gcd
:=
Int63.gcd
;
add_mul_div
:=
Int63.addmuldiv
;
pos_mod
:=
pos_mod_int
;
is_even
:=
Int63.is_even
;
sqrt2
:=
Int63.sqrt2
;
sqrt
:=
Int63.sqrt
;
ZnZ.lor
:=
Int63.lor
;
ZnZ.land
:=
Int63.land
;
ZnZ.lxor
:=
Int63.lxor
|}.
Local Open
Scope
Z_scope
.
Lemma
is_zero_spec_aux
:
forall
x
:
int
,
is_zero
x
=
true
->
φ
x
=
0%
Z
.
Lemma
positive_to_int_spec
:
forall
p
:
positive
,
Zpos
p
=
Z_of_N
(
fst
(
positive_to_int
p
))
*
wB
+
to_Z
(
snd
(
positive_to_int
p
)).
Lemma
mulc_WW_spec
:
forall
x
y
,
Φ
(
x
*
c
y
)
=
φ
x
*
φ
y
.
Lemma
squarec_spec
:
forall
x
,
Φ
(
x
*
c
x
)
=
φ
x
*
φ
x
.
Lemma
diveucl_spec_aux
:
forall
a
b
, 0
<
φ
b
->
let
(
q
,
r
) :=
diveucl
a
b
in
φ
a
=
φ
q
*
φ
b
+
φ
r
/\
0
<=
φ
r
<
φ
b
.
Lemma
shift_unshift_mod_2
:
forall
n
p
a
, 0
<=
p
<=
n
->
((
a
*
2
^
(
n
-
p
)
)
mod
(
2
^
n
)
/
2
^
(
n
-
p
)
)
mod
(
2
^
n
)
=
a
mod
2
^
p
.
Lemma
div_le_0
:
forall
p
x
, 0
<=
x
->
0
<=
x
/
2
^
p
.
Lemma
div_lt
:
forall
p
x
y
, 0
<=
x
<
y
->
x
/
2
^
p
<
y
.
Lemma
P
(
A
B
C
:
Prop
) :
A
→
(
B
→
C
)
→
(
A
→
B
)
→
C
.
Lemma
shift_unshift_mod_3
:
forall
n
p
a
:
Z
,
0
<=
p
<=
n
->
(
a
*
2
^
(
n
-
p
)
)
mod
2
^
n
/
2
^
(
n
-
p
)
=
a
mod
2
^
p
.
Lemma
pos_mod_spec
w
p
:
φ(
pos_mod
p
w
)
=
φ(
w
)
mod
(
2
^
φ(
p
)
)
.
{2 Specification and proof}
Global Instance
int_specs
:
ZnZ.Specs
int_ops
:= {
spec_to_Z
:=
to_Z_bounded
;
spec_of_pos
:=
positive_to_int_spec
;
spec_zdigits
:=
refl_equal
_
;
spec_more_than_1_digit
:=
refl_equal
_
;
spec_0
:=
to_Z_0
;
spec_1
:=
to_Z_1
;
spec_m1
:=
refl_equal
_
;
spec_compare
:=
compare_spec
;
spec_eq0
:=
is_zero_spec_aux
;
spec_opp_c
:=
oppc_spec
;
spec_opp
:=
opp_spec
;
spec_opp_carry
:=
oppcarry_spec
;
spec_succ_c
:=
succc_spec
;
spec_add_c
:=
addc_spec
;
spec_add_carry_c
:=
addcarryc_spec
;
spec_succ
:=
succ_spec
;
spec_add
:=
add_spec
;
spec_add_carry
:=
addcarry_spec
;
spec_pred_c
:=
predc_spec
;
spec_sub_c
:=
subc_spec
;
spec_sub_carry_c
:=
subcarryc_spec
;
spec_pred
:=
pred_spec
;
spec_sub
:=
sub_spec
;
spec_sub_carry
:=
subcarry_spec
;
spec_mul_c
:=
mulc_WW_spec
;
spec_mul
:=
mul_spec
;
spec_square_c
:=
squarec_spec
;
spec_div21
:=
diveucl_21_spec_aux
;
spec_div_gt
:=
fun
a
b
_
=>
diveucl_spec_aux
a
b
;
spec_div
:=
diveucl_spec_aux
;
spec_modulo_gt
:=
fun
a
b
_
_
=>
mod_spec
a
b
;
spec_modulo
:=
fun
a
b
_
=>
mod_spec
a
b
;
spec_gcd_gt
:=
fun
a
b
_
=>
gcd_spec
a
b
;
spec_gcd
:=
gcd_spec
;
spec_head00
:=
head00_spec
;
spec_head0
:=
head0_spec
;
spec_tail00
:=
tail00_spec
;
spec_tail0
:=
tail0_spec
;
spec_add_mul_div
:=
addmuldiv_spec
;
spec_pos_mod
:=
pos_mod_spec
;
spec_is_even
:=
is_even_spec
;
spec_sqrt2
:=
sqrt2_spec
;
spec_sqrt
:=
sqrt_spec
;
spec_land
:=
land_spec'
;
spec_lor
:=
lor_spec'
;
spec_lxor
:=
lxor_spec'
}.
Module
Int63Cyclic
<:
CyclicType
.
Definition
t
:=
int
.
Definition
ops
:=
int_ops
.
Definition
specs
:=
int_specs
.
End
Int63Cyclic
.