# 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.
Set Implicit Arguments.
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 t := Z.
Definition zdigits := Zpos digits.
Definition to_Z x := x mod wB.
Notation "[| x |]" := (to_Z x) (at level 0, x at level 99).
Notation "[+| c |]" :=
(interp_carry 1 wB to_Z c) (at level 0, x at level 99).
Notation "[-| c |]" :=
(interp_carry (-1) wB to_Z c) (at level 0, x at level 99).
Notation "[|| x ||]" :=
(zn2z_to_Z wB 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 of_pos x :=
let (q,r) := Z.pos_div_eucl x wB in ( N_of_Z q , r ).
Lemma spec_of_pos : forall p,
Zpos p = ( Z.of_N (fst (of_pos p)))* wB + [|( snd (of_pos p))|].
Lemma spec_zdigits : [| zdigits |] = Zpos digits.
Definition zero := 0.
Definition one := 1.
Definition minus_one := wB - 1.
Lemma spec_0 : [| zero |] = 0.
Lemma spec_1 : [| one |] = 1.
Lemma spec_Bm1 : [| minus_one |] = wB - 1.
Definition compare x y := Z.compare [| x |] [| y |].
Lemma spec_compare : forall x y,
compare x y = Z.compare [| x |] [| y |].
Definition eq0 x :=
match [| x |] with Z0 => true | _ => false end.
Lemma spec_eq0 : forall x, eq0 x = true -> [| x |] = 0.
Definition opp_c x :=
if eq0 x then C0 0 else C1 (- x).
Definition opp x := - x.
Definition opp_carry x := - x - 1.
Lemma spec_opp_c : forall x, [-| opp_c x |] = - [| x |].
Lemma spec_opp : forall x, [| opp x |] = ( - [| x |] ) mod wB.
Lemma spec_opp_carry : forall x, [| opp_carry x |] = wB - [| x |] - 1.
Definition succ_c x :=
let y := Z.succ x in
if eq0 y then C1 0 else C0 y.
Definition add_c x y :=
let z := [| x |] + [| y |] in
if Z_lt_le_dec z wB then C0 z else C1 (z - wB).
Definition 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 succ := Z.succ.
Definition add := Z.add.
Definition 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, [+| succ_c x |] = [| x |] + 1.
Lemma spec_add_c : forall x y, [+| add_c x y |] = [| x |] + [| y |].
Lemma spec_add_carry_c : forall x y, [+| add_carry_c x y |] = [| x |] + [| y |] + 1.
Lemma spec_succ : forall x, [| succ x |] = ( [| x |] + 1) mod wB.
Lemma spec_add : forall x y, [| add x y |] = ( [| x |] + [| y |] ) mod wB.
Lemma spec_add_carry :
forall x y, [| add_carry x y |] = ( [| x |] + [| y |] + 1) mod wB.
Definition pred_c x :=
if eq0 x then C1 (wB -1) else C0 (x -1).
Definition sub_c x y :=
let z := [| x |] - [| y |] in
if Z_lt_le_dec z 0 then C1 (wB + z) else C0 z.
Definition 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 pred := Z.pred.
Definition sub := Z.sub.
Definition sub_carry x y := x - y - 1.
Lemma spec_pred_c : forall x, [-| pred_c x |] = [| x |] - 1.
Lemma spec_sub_c : forall x y, [-| sub_c x y |] = [| x |] - [| y |].
Lemma spec_sub_carry_c : forall x y, [-| sub_carry_c x y |] = [| x |] - [| y |] - 1.
Lemma spec_pred : forall x, [| pred x |] = ( [| x |] - 1) mod wB.
Lemma spec_sub : forall x y, [| sub x y |] = ( [| x |] - [| y |] ) mod wB.
Lemma spec_sub_carry :
forall x y, [| sub_carry x y |] = ( [| x |] - [| y |] - 1) mod wB.
Definition mul_c x y :=
let (h,l) := Z.div_eucl ([| x |] * [| y |]) wB in
if eq0 h then if eq0 l then W0 else WW h l else WW h l.
Definition mul := Z.mul.
Definition square_c x := mul_c x x.
Lemma spec_mul_c : forall x y, [|| mul_c x y ||] = [| x |] * [| y |].
Lemma spec_mul : forall x y, [| mul x y |] = ( [| x |] * [| y |] ) mod wB.
Lemma spec_square_c : forall x, [|| square_c x ||] = [| x |] * [| x |].
Definition div x y := Z.div_eucl [| x |] [| y |].
Lemma spec_div : forall a b, 0 < [| b |] ->
let (q,r) := div a b in
[| a |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |].
Definition div_gt := div.
Lemma spec_div_gt : forall a b, [| a |] > [| b |] -> 0 < [| b |] ->
let (q,r) := div_gt a b in
[| a |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |].
Definition modulo x y := [| x |] mod [| y |].
Definition modulo_gt x y := [| x |] mod [| y |].
Lemma spec_modulo : forall a b, 0 < [| b |] ->
[| modulo a b |] = [| a |] mod [| b |].
Lemma spec_modulo_gt : forall a b, [| a |] > [| b |] -> 0 < [| b |] ->
[| modulo_gt a b |] = [| a |] mod [| b |].
Definition gcd x y := Z.gcd [| x |] [| y |].
Definition gcd_gt x y := Z.gcd [| x |] [| y |].
Lemma Zgcd_bound : forall a b, 0<= a -> 0<= b -> Z.gcd a b <= Z.max a b.
Lemma spec_gcd : forall a b, Zis_gcd [| a |] [| b |] [| gcd a b |].
Lemma spec_gcd_gt : forall a b, [| a |] > [| b |] ->
Zis_gcd [| a |] [| b |] [| gcd_gt a b |].
Definition div21 a1 a2 b :=
Z.div_eucl ([| a1 |] * wB + [| a2 |]) [| b |].
Lemma spec_div21 : forall a1 a2 b,
wB /2 <= [| b |] ->
[| a1 |] < [| b |] ->
let (q,r) := div21 a1 a2 b in
[| a1 |] * wB + [| a2 |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |].
Definition add_mul_div p x y :=
([| x |] * (2 ^ [| p |] ) + [| y |] / (2 ^ ( ( Zpos digits ) - [| p |] ) )).
Lemma spec_add_mul_div : forall x y p,
[| p |] <= Zpos digits ->
[| add_mul_div p x y |] =
( [| x |] * (2 ^ [| p |] ) +
[| y |] / (2 ^ ( ( Zpos digits ) - [| p |] ) ) ) mod wB.
Definition pos_mod p w := [| w |] mod (2 ^ [| p |] ).
Lemma spec_pos_mod : forall w p,
[| pos_mod p w |] = [| w |] mod (2 ^ [| p |] ).
Definition is_even x :=
if Z.eq_dec ([| x |] mod 2) 0 then true else false.
Lemma spec_is_even : forall x,
if is_even x then [| x |] mod 2 = 0 else [| x |] mod 2 = 1.
Definition sqrt x := Z.sqrt [| x |].
Lemma spec_sqrt : forall x,
[| sqrt x |] ^ 2 <= [| x |] < ( [| sqrt x |] + 1) ^ 2.
Definition sqrt2 x y :=
let z := [| x |] * wB + [| y |] in
match z with
| Z0 => (0, C0 0)
| Zpos p =>
let (s,r) := Z.sqrtrem (Zpos 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) := 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 head0 x := match [| x |] with
| Z0 => zdigits
| Zpos p => zdigits - log_inf p - 1
| _ => 0
end.
Lemma spec_head00: forall x, [| x |] = 0 -> [| head0 x |] = Zpos 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 ^ ( [| 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 tail0 x :=
match [| x |] with
| Z0 => zdigits
| Zpos p => Ptail p
| Zneg _ => 0
end.
Lemma spec_tail00: forall x, [| x |] = 0 -> [| tail0 x |] = Zpos digits.
Lemma spec_tail0 : forall x, 0 < [| x |] ->
exists y , 0 <= y /\ [| x |] = (2 * y + 1) * (2 ^ [| tail0 x |] ).
Let's now group everything in two records
Instance zmod_ops : ZnZ.Ops Z := ZnZ.MkOps
(digits : positive)
(zdigits: t)
(to_Z : t -> Z)
(of_pos : positive -> N * t)
(head0 : t -> t)
(tail0 : t -> t)
(zero : t)
(one : t)
(minus_one : t)
(compare : t -> t -> comparison)
(eq0 : t -> bool)
(opp_c : t -> carry t)
(opp : t -> t)
(opp_carry : t -> t)
(succ_c : t -> carry t)
(add_c : t -> t -> carry t)
(add_carry_c : t -> t -> carry t)
(succ : t -> t)
(add : t -> t -> t)
(add_carry : t -> t -> t)
(pred_c : t -> carry t)
(sub_c : t -> t -> carry t)
(sub_carry_c : t -> t -> carry t)
(pred : t -> t)
(sub : t -> t -> t)
(sub_carry : t -> t -> t)
(mul_c : t -> t -> zn2z t)
(mul : t -> t -> t)
(square_c : t -> zn2z t)
(div21 : t -> t -> t -> t * t)
(div_gt : t -> t -> t * t)
(div : t -> t -> t * t)
(modulo_gt : t -> t -> t)
(modulo : t -> t -> t)
(gcd_gt : t -> t -> t)
(gcd : t -> t -> t)
(add_mul_div : t -> t -> t -> t)
(pos_mod : t -> t -> t)
(is_even : t -> bool)
(sqrt2 : t -> t -> t * carry t)
(sqrt : t -> t).
Instance zmod_specs : ZnZ.Specs zmod_ops := ZnZ.MkSpecs
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_modulo_gt
spec_modulo
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 t := Z.
Instance ops : ZnZ.Ops t := zmod_ops P.p.
Instance specs : ZnZ.Specs ops := zmod_specs P.not_one.
End ZModuloCyclicType.