Library Coq.micromega.ZifyUint63
Require
Import
ZArith
.
Require
Import
Uint63
.
Require
Import
ZifyBool
.
Import
ZifyClasses
.
Lemma
to_Z_bounded
:
forall
x
, (0
<=
to_Z
x
<
9223372036854775808)%
Z
.
#[
global
]
Instance
Inj_int_Z
:
InjTyp
int
Z
:=
mkinj
_
_
to_Z
(
fun
x
=> 0
<=
x
<
9223372036854775808)%
Z
to_Z_bounded
.
Add
Zify
InjTyp
Inj_int_Z
.
#[
global
]
Instance
Op_max_int
:
CstOp
max_int
:=
{
TCst
:= 9223372036854775807 ;
TCstInj
:=
eq_refl
}.
Add
Zify
CstOp
Op_max_int
.
#[
global
]
Instance
Op_digits
:
CstOp
digits
:=
{
TCst
:= 63 ;
TCstInj
:=
eq_refl
}.
Add
Zify
CstOp
Op_digits
.
#[
global
]
Instance
Op_size
:
CstOp
size
:=
{
TCst
:= 63 ;
TCstInj
:=
eq_refl
}.
Add
Zify
CstOp
Op_size
.
#[
global
]
Instance
Op_wB
:
CstOp
wB
:=
{
TCst
:= 2
^
63 ;
TCstInj
:=
eq_refl
}.
Add
Zify
CstOp
Op_wB
.
Lemma
ltb_lt
:
forall
n
m
,
(
n
<?
m
)%
uint63
=
(
φ
(
n
)
%
uint63
<?
φ
(
m
)
%
uint63
)%
Z
.
#[
global
]
Instance
Op_ltb
:
BinOp
ltb
:=
{|
TBOp
:=
Z.ltb
;
TBOpInj
:=
ltb_lt
|}.
Add
Zify
BinOp
Op_ltb
.
Lemma
leb_le
:
forall
n
m
,
(
n
<=?
m
)%
uint63
=
(
φ
(
n
)
%
uint63
<=?
φ
(
m
)
%
uint63
)%
Z
.
#[
global
]
Instance
Op_leb
:
BinOp
leb
:=
{|
TBOp
:=
Z.leb
;
TBOpInj
:=
leb_le
|}.
Add
Zify
BinOp
Op_leb
.
Lemma
eqb_eq
:
forall
n
m
,
(
n
=?
m
)%
uint63
=
(
φ
(
n
)
%
uint63
=?
φ
(
m
)
%
uint63
)%
Z
.
#[
global
]
Instance
Op_eqb
:
BinOp
eqb
:=
{|
TBOp
:=
Z.eqb
;
TBOpInj
:=
eqb_eq
|}.
Add
Zify
BinOp
Op_eqb
.
Lemma
eq_int_inj
:
forall
n
m
:
int
,
n
=
m
<->
(
φ
n
=
φ
m
)%
uint63
.
#[
global
]
Instance
Op_eq
:
BinRel
(@
eq
int
) :=
{|
TR
:= @
eq
Z
;
TRInj
:=
eq_int_inj
|}.
Add
Zify
BinRel
Op_eq
.
#[
global
]
Instance
Op_add
:
BinOp
add
:=
{|
TBOp
:=
fun
x
y
=>
(
x
+
y
)
mod
9223372036854775808%
Z
;
TBOpInj
:=
add_spec
|}%
Z
.
Add
Zify
BinOp
Op_add
.
#[
global
]
Instance
Op_sub
:
BinOp
sub
:=
{|
TBOp
:=
fun
x
y
=>
(
x
-
y
)
mod
9223372036854775808%
Z
;
TBOpInj
:=
sub_spec
|}%
Z
.
Add
Zify
BinOp
Op_sub
.
#[
global
]
Instance
Op_opp
:
UnOp
Uint63.opp
:=
{|
TUOp
:= (
fun
x
=>
(
-
x
)
mod
9223372036854775808)%
Z
;
TUOpInj
:= (
sub_spec
0) |}%
Z
.
Add
Zify
UnOp
Op_opp
.
#[
global
]
Instance
Op_oppcarry
:
UnOp
oppcarry
:=
{|
TUOp
:= (
fun
x
=> 2
^
63
-
x
-
1)%
Z
;
TUOpInj
:=
oppcarry_spec
|}%
Z
.
Add
Zify
UnOp
Op_oppcarry
.
#[
global
]
Instance
Op_succ
:
UnOp
succ
:=
{|
TUOp
:= (
fun
x
=>
(
x
+
1
)
mod
2
^
63)%
Z
;
TUOpInj
:=
succ_spec
|}%
Z
.
Add
Zify
UnOp
Op_succ
.
#[
global
]
Instance
Op_pred
:
UnOp
Uint63.pred
:=
{|
TUOp
:= (
fun
x
=>
(
x
-
1
)
mod
2
^
63)%
Z
;
TUOpInj
:=
pred_spec
|}%
Z
.
Add
Zify
UnOp
Op_pred
.
#[
global
]
Instance
Op_mul
:
BinOp
mul
:=
{|
TBOp
:=
fun
x
y
=>
(
x
*
y
)
mod
9223372036854775808%
Z
;
TBOpInj
:=
mul_spec
|}%
Z
.
Add
Zify
BinOp
Op_mul
.
#[
global
]
Instance
Op_gcd
:
BinOp
gcd
:=
{|
TBOp
:= (
fun
x
y
=>
Zgcd_alt.Zgcdn
(2
*
63)%
nat
y
x
) ;
TBOpInj
:=
to_Z_gcd
|}.
Add
Zify
BinOp
Op_gcd
.
#[
global
]
Instance
Op_mod
:
BinOp
Uint63.mod
:=
{|
TBOp
:=
Z.modulo
;
TBOpInj
:=
mod_spec
|}.
Add
Zify
BinOp
Op_mod
.
#[
global
]
Instance
Op_subcarry
:
BinOp
subcarry
:=
{|
TBOp
:= (
fun
x
y
=>
(
x
-
y
-
1
)
mod
2
^
63)%
Z
;
TBOpInj
:=
subcarry_spec
|}.
Add
Zify
BinOp
Op_subcarry
.
#[
global
]
Instance
Op_addcarry
:
BinOp
addcarry
:=
{|
TBOp
:= (
fun
x
y
=>
(
x
+
y
+
1
)
mod
2
^
63)%
Z
;
TBOpInj
:=
addcarry_spec
|}.
Add
Zify
BinOp
Op_addcarry
.
#[
global
]
Instance
Op_lsr
:
BinOp
lsr
:=
{|
TBOp
:= (
fun
x
y
=>
x
/
2
^
y
)%
Z
;
TBOpInj
:=
lsr_spec
|}.
Add
Zify
BinOp
Op_lsr
.
#[
global
]
Instance
Op_lsl
:
BinOp
lsl
:=
{|
TBOp
:= (
fun
x
y
=>
(
x
*
2
^
y
)
mod
2
^
63)%
Z
;
TBOpInj
:=
lsl_spec
|}.
Add
Zify
BinOp
Op_lsl
.
#[
global
]
Instance
Op_lor
:
BinOp
Uint63.lor
:=
{|
TBOp
:=
Z.lor
;
TBOpInj
:=
lor_spec'
|}.
Add
Zify
BinOp
Op_lor
.
#[
global
]
Instance
Op_land
:
BinOp
Uint63.land
:=
{|
TBOp
:=
Z.land
;
TBOpInj
:=
land_spec'
|}.
Add
Zify
BinOp
Op_land
.
#[
global
]
Instance
Op_lxor
:
BinOp
Uint63.lxor
:=
{|
TBOp
:=
Z.lxor
;
TBOpInj
:=
lxor_spec'
|}.
Add
Zify
BinOp
Op_lxor
.
#[
global
]
Instance
Op_div
:
BinOp
div
:=
{|
TBOp
:=
Z.div
;
TBOpInj
:=
div_spec
|}.
Add
Zify
BinOp
Op_div
.
#[
global
]
Instance
Op_bit
:
BinOp
bit
:=
{|
TBOp
:=
Z.testbit
;
TBOpInj
:=
bitE
|}.
Add
Zify
BinOp
Op_bit
.
#[
global
]
Instance
Op_of_Z
:
UnOp
of_Z
:=
{
TUOp
:= (
fun
x
=>
x
mod
9223372036854775808)%
Z
;
TUOpInj
:=
of_Z_spec
}.
Add
Zify
UnOp
Op_of_Z
.
#[
global
]
Instance
Op_to_Z
:
UnOp
to_Z
:=
{
TUOp
:=
fun
x
=>
x
;
TUOpInj
:=
fun
x
:
int
=>
eq_refl
}.
Add
Zify
UnOp
Op_to_Z
.
#[
global
]
Instance
Op_is_zero
:
UnOp
is_zero
:=
{
TUOp
:= (
Z.eqb
0) ;
TUOpInj
:=
is_zeroE
}.
Add
Zify
UnOp
Op_is_zero
.
Lemma
is_evenE
:
forall
x
,
is_even
x
=
Z.even
φ
(
x
)
%
uint63
.
#[
global
]
Instance
Op_is_even
:
UnOp
is_even
:=
{
TUOp
:=
Z.even
;
TUOpInj
:=
is_evenE
}.
Add
Zify
UnOp
Op_is_even
.
Ltac
Zify.zify_convert_to_euclidean_division_equations_flag
::=
constr
:(
true
).