Even if the construction provided here is not reused for building
the efficient arbitrary precision numbers, it provides a simple
implementation of CyclicAxioms, hence ensuring its coherence.
Require Import Bool.
Require Import ZArith.
Require Import Znumtheory.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import CyclicAxioms.
Open Local Scope Z_scope.
Section ZModulo.
Variable digits :
positive.
Hypothesis digits_ne_1 :
digits <> 1%positive.
Definition wB :=
base digits.
Definition znz :=
Z.
Definition znz_digits :=
digits.
Definition znz_zdigits :=
Zpos digits.
Definition znz_to_Z x :=
x mod wB.
Notation "[| x |]" := (
znz_to_Z x) (
at level 0,
x at level 99).
Notation "[+| c |]" :=
(
interp_carry 1
wB znz_to_Z c) (
at level 0,
x at level 99).
Notation "[-| c |]" :=
(
interp_carry (-1)
wB znz_to_Z c) (
at level 0,
x at level 99).
Notation "[|| x ||]" :=
(
zn2z_to_Z wB znz_to_Z x) (
at level 0,
x at level 99).
Lemma spec_more_than_1_digit: 1 <
Zpos digits.
Let digits_gt_1 :=
spec_more_than_1_digit.
Lemma wB_pos :
wB > 0.
Hint Resolve wB_pos.
Lemma spec_to_Z_1 :
forall x, 0 <= [|x|].
Lemma spec_to_Z_2 :
forall x, [|x|] <
wB.
Hint Resolve spec_to_Z_1 spec_to_Z_2.
Lemma spec_to_Z :
forall x, 0 <= [|x|] <
wB.
Definition znz_of_pos x :=
let (
q,r) :=
Zdiv_eucl_POS x wB in (
N_of_Z q,
r).
Lemma spec_of_pos :
forall p,
Zpos p = (
Z_of_N (
fst (
znz_of_pos p)))*wB + [|(snd (
znz_of_pos p))|].
Lemma spec_zdigits : [|znz_zdigits|] =
Zpos znz_digits.
Definition znz_0 := 0.
Definition znz_1 := 1.
Definition znz_Bm1 :=
wB - 1.
Lemma spec_0 : [|znz_0|] = 0.
Lemma spec_1 : [|znz_1|] = 1.
Lemma spec_Bm1 : [|znz_Bm1|] =
wB - 1.
Definition znz_compare x y :=
Zcompare [|x|] [|y|].
Lemma spec_compare :
forall x y,
match znz_compare x y with
|
Eq => [|x|] = [|y|]
|
Lt => [|x|] < [|y|]
|
Gt => [|x|] > [|y|]
end.
Definition znz_eq0 x :=
match [|x|]
with Z0 =>
true |
_ =>
false end.
Lemma spec_eq0 :
forall x,
znz_eq0 x =
true -> [|x|] = 0.
Definition znz_opp_c x :=
if znz_eq0 x then C0 0
else C1 (-
x).
Definition znz_opp x := -
x.
Definition znz_opp_carry x := -
x - 1.
Lemma spec_opp_c :
forall x, [-|znz_opp_c
x|] = -[|x|].
Lemma spec_opp :
forall x, [|znz_opp
x|] = (-[|x|])
mod wB.
Lemma spec_opp_carry :
forall x, [|znz_opp_carry
x|] =
wB - [|x|] - 1.
Definition znz_succ_c x :=
let y :=
Zsucc x in
if znz_eq0 y then C1 0
else C0 y.
Definition znz_add_c x y :=
let z := [|x|] + [|y|]
in
if Z_lt_le_dec z wB then C0 z else C1 (
z-wB).
Definition znz_add_carry_c x y :=
let z := [|x|]+[|y|]+1
in
if Z_lt_le_dec z wB then C0 z else C1 (
z-wB).
Definition znz_succ :=
Zsucc.
Definition znz_add :=
Zplus.
Definition znz_add_carry x y :=
x +
y + 1.
Lemma Zmod_equal :
forall x y z,
z>0 -> (
x-y)
mod z = 0 ->
x mod z =
y mod z.
Lemma spec_succ_c :
forall x, [+|znz_succ_c
x|] = [|x|] + 1.
Lemma spec_add_c :
forall x y, [+|znz_add_c
x y|] = [|x|] + [|y|].
Lemma spec_add_carry_c :
forall x y, [+|znz_add_carry_c
x y|] = [|x|] + [|y|] + 1.
Lemma spec_succ :
forall x, [|znz_succ
x|] = ([|x|] + 1)
mod wB.
Lemma spec_add :
forall x y, [|znz_add
x y|] = ([|x|] + [|y|])
mod wB.
Lemma spec_add_carry :
forall x y, [|znz_add_carry
x y|] = ([|x|] + [|y|] + 1)
mod wB.
Definition znz_pred_c x :=
if znz_eq0 x then C1 (
wB-1)
else C0 (
x-1).
Definition znz_sub_c x y :=
let z := [|x|]-[|y|]
in
if Z_lt_le_dec z 0
then C1 (
wB+z)
else C0 z.
Definition znz_sub_carry_c x y :=
let z := [|x|]-[|y|]-1
in
if Z_lt_le_dec z 0
then C1 (
wB+z)
else C0 z.
Definition znz_pred :=
Zpred.
Definition znz_sub :=
Zminus.
Definition znz_sub_carry x y :=
x -
y - 1.
Lemma spec_pred_c :
forall x, [-|znz_pred_c
x|] = [|x|] - 1.
Lemma spec_sub_c :
forall x y, [-|znz_sub_c
x y|] = [|x|] - [|y|].
Lemma spec_sub_carry_c :
forall x y, [-|znz_sub_carry_c
x y|] = [|x|] - [|y|] - 1.
Lemma spec_pred :
forall x, [|znz_pred
x|] = ([|x|] - 1)
mod wB.
Lemma spec_sub :
forall x y, [|znz_sub
x y|] = ([|x|] - [|y|])
mod wB.
Lemma spec_sub_carry :
forall x y, [|znz_sub_carry
x y|] = ([|x|] - [|y|] - 1)
mod wB.
Definition znz_mul_c x y :=
let (
h,l) :=
Zdiv_eucl ([|x|]*[|y|])
wB in
if znz_eq0 h then if znz_eq0 l then W0 else WW h l else WW h l.
Definition znz_mul :=
Zmult.
Definition znz_square_c x :=
znz_mul_c x x.
Lemma spec_mul_c :
forall x y, [||
znz_mul_c x y ||] = [|x|] * [|y|].
Lemma spec_mul :
forall x y, [|znz_mul
x y|] = ([|x|] * [|y|])
mod wB.
Lemma spec_square_c :
forall x, [||
znz_square_c x||] = [|x|] * [|x|].
Definition znz_div x y :=
Zdiv_eucl [|x|] [|y|].
Lemma spec_div :
forall a b, 0 < [|b|] ->
let (
q,r) :=
znz_div a b in
[|a|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|].
Definition znz_div_gt :=
znz_div.
Lemma spec_div_gt :
forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
let (
q,r) :=
znz_div_gt a b in
[|a|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|].
Definition znz_mod x y := [|x|]
mod [|y|].
Definition znz_mod_gt x y := [|x|]
mod [|y|].
Lemma spec_mod :
forall a b, 0 < [|b|] ->
[|znz_mod
a b|] = [|a|]
mod [|b|].
Lemma spec_mod_gt :
forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
[|znz_mod_gt
a b|] = [|a|]
mod [|b|].
Definition znz_gcd x y :=
Zgcd [|x|] [|y|].
Definition znz_gcd_gt x y :=
Zgcd [|x|] [|y|].
Lemma Zgcd_bound :
forall a b, 0<=a -> 0<=b ->
Zgcd a b <=
Zmax a b.
Lemma spec_gcd :
forall a b,
Zis_gcd [|a|] [|b|] [|znz_gcd
a b|].
Lemma spec_gcd_gt :
forall a b, [|a|] > [|b|] ->
Zis_gcd [|a|] [|b|] [|znz_gcd_gt
a b|].
Definition znz_div21 a1 a2 b :=
Zdiv_eucl ([|a1|]*wB+[|a2|]) [|b|].
Lemma spec_div21 :
forall a1 a2 b,
wB/2 <= [|b|] ->
[|a1|] < [|b|] ->
let (
q,r) :=
znz_div21 a1 a2 b in
[|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|].
Definition znz_add_mul_div p x y :=
([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((
Zpos znz_digits) - [|p|]))).
Lemma spec_add_mul_div :
forall x y p,
[|p|] <=
Zpos znz_digits ->
[|
znz_add_mul_div p x y |] =
([|x|] * (2 ^ [|p|]) +
[|y|] / (2 ^ ((
Zpos znz_digits) - [|p|])))
mod wB.
Definition znz_pos_mod p w := [|w|]
mod (2 ^ [|p|]).
Lemma spec_pos_mod :
forall w p,
[|znz_pos_mod
p w|] = [|w|]
mod (2 ^ [|p|]).
Definition znz_is_even x :=
if Z_eq_dec ([|x|]
mod 2) 0
then true else false.
Lemma spec_is_even :
forall x,
if znz_is_even x then [|x|]
mod 2 = 0
else [|x|]
mod 2 = 1.
Definition znz_sqrt x :=
Zsqrt_plain [|x|].
Lemma spec_sqrt :
forall x,
[|znz_sqrt
x|] ^ 2 <= [|x|] < ([|znz_sqrt
x|] + 1) ^ 2.
Definition znz_sqrt2 x y :=
let z := [|x|]*wB+[|y|]
in
match z with
|
Z0 => (0,
C0 0)
|
Zpos p =>
let (
s,r,_,_) :=
sqrtrempos p in
(
s,
if Z_lt_le_dec r wB then C0 r else C1 (
r-wB))
|
Zneg _ => (0,
C0 0)
end.
Lemma spec_sqrt2 :
forall x y,
wB/ 4 <= [|x|] ->
let (
s,r) :=
znz_sqrt2 x y in
[||WW
x y||] = [|s|] ^ 2 + [+|r|] /\
[+|r|] <= 2 * [|s|].
Lemma two_p_power2 :
forall x,
x>=0 ->
two_p x = 2 ^
x.
Definition znz_head0 x :=
match [|x|]
with
|
Z0 =>
znz_zdigits
|
Zpos p =>
znz_zdigits -
log_inf p - 1
|
_ => 0
end.
Lemma spec_head00:
forall x, [|x|] = 0 -> [|znz_head0
x|] =
Zpos znz_digits.
Lemma log_inf_bounded :
forall x p,
Zpos x < 2^p ->
log_inf x <
p.
Lemma spec_head0 :
forall x, 0 < [|x|] ->
wB/ 2 <= 2 ^ ([|znz_head0
x|]) * [|x|] <
wB.
Fixpoint Ptail p :=
match p with
|
xO p => (
Ptail p)+1
|
_ => 0
end.
Lemma Ptail_pos :
forall p, 0 <=
Ptail p.
Hint Resolve Ptail_pos.
Lemma Ptail_bounded :
forall p d,
Zpos p < 2^(Zpos
d) ->
Ptail p <
Zpos d.
Definition znz_tail0 x :=
match [|x|]
with
|
Z0 =>
znz_zdigits
|
Zpos p =>
Ptail p
|
Zneg _ => 0
end.
Lemma spec_tail00:
forall x, [|x|] = 0 -> [|znz_tail0
x|] =
Zpos znz_digits.
Lemma spec_tail0 :
forall x, 0 < [|x|] ->
exists y, 0 <=
y /\ [|x|] = (2 *
y + 1) * (2 ^ [|znz_tail0
x|]).
A modular version of the previous construction.