# 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.

let z := [|x|] + [|y|] in
if Z_lt_le_dec z wB then C0 z else C1 (z-wB).

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_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.

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
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.