# Library Coq.Numbers.Cyclic.ZModulo.ZModulo

# Type Z viewed modulo a particular constant corresponds to Z/nZ

as defined abstractly in CyclicAxioms.
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.
Local Open 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 |] ).
Let's now group everything in two records
Definition zmod_op := mk_znz_op
(znz_digits : positive)
(znz_zdigits: znz)
(znz_to_Z : znz -> Z)
(znz_of_pos : positive -> N * znz)
(znz_head0 : znz -> znz)
(znz_tail0 : znz -> znz)
(znz_0 : znz)
(znz_1 : znz)
(znz_Bm1 : znz)
(znz_compare : znz -> znz -> comparison)
(znz_eq0 : znz -> bool)
(znz_opp_c : znz -> carry znz)
(znz_opp : znz -> znz)
(znz_opp_carry : znz -> znz)
(znz_succ_c : znz -> carry znz)
(znz_add_c : znz -> znz -> carry znz)
(znz_add_carry_c : znz -> znz -> carry znz)
(znz_succ : znz -> znz)
(znz_add : znz -> znz -> znz)
(znz_add_carry : znz -> znz -> znz)
(znz_pred_c : znz -> carry znz)
(znz_sub_c : znz -> znz -> carry znz)
(znz_sub_carry_c : znz -> znz -> carry znz)
(znz_pred : znz -> znz)
(znz_sub : znz -> znz -> znz)
(znz_sub_carry : znz -> znz -> znz)
(znz_mul_c : znz -> znz -> zn2z znz)
(znz_mul : znz -> znz -> znz)
(znz_square_c : znz -> zn2z znz)
(znz_div21 : znz -> znz -> znz -> znz * znz)
(znz_div_gt : znz -> znz -> znz * znz)
(znz_div : znz -> znz -> znz * znz)
(znz_mod_gt : znz -> znz -> znz)
(znz_mod : znz -> znz -> znz)
(znz_gcd_gt : znz -> znz -> znz)
(znz_gcd : znz -> znz -> znz)
(znz_add_mul_div : znz -> znz -> znz -> znz)
(znz_pos_mod : znz -> znz -> znz)
(znz_is_even : znz -> bool)
(znz_sqrt2 : znz -> znz -> znz * carry znz)
(znz_sqrt : znz -> znz).
Definition zmod_spec := mk_znz_spec zmod_op
spec_to_Z
spec_of_pos
spec_zdigits
spec_more_than_1_digit
spec_0
spec_1
spec_Bm1
spec_compare
spec_eq0
spec_opp_c
spec_opp
spec_opp_carry
spec_succ_c
spec_add_c
spec_add_carry_c
spec_succ
spec_add
spec_add_carry
spec_pred_c
spec_sub_c
spec_sub_carry_c
spec_pred
spec_sub
spec_sub_carry
spec_mul_c
spec_mul
spec_square_c
spec_div21
spec_div_gt
spec_div
spec_mod_gt
spec_mod
spec_gcd_gt
spec_gcd
spec_head00
spec_head0
spec_tail00
spec_tail0
spec_add_mul_div
spec_pos_mod
spec_is_even
spec_sqrt2
spec_sqrt.
End ZModulo.
A modular version of the previous construction.
Module Type PositiveNotOne.
Parameter p : positive.
Axiom not_one : p <> 1%positive.
End PositiveNotOne.
Module ZModuloCyclicType (P:PositiveNotOne) <: CyclicType.
Definition w := Z.
Definition w_op := zmod_op P.p.
Definition w_spec := zmod_spec P.not_one.
End ZModuloCyclicType.