# Type Z viewed modulo 2^d implements CyclicAxioms.

This library has been deprecated since Coq version 8.17.

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 Zpow_facts.
Require Import DoubleType.
Require Import CyclicAxioms.
Require Import Lia.

Local Open Scope Z_scope.

Section ZModulo.

Variable digits : positive.
Hypothesis digits_ne_1 : digits <> 1%positive.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition wB := base digits.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition t := Z.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition zdigits := Zpos digits.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition to_Z x := x mod wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Notation "[| x |]" := (to_Z x) (at level 0, x at level 99).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Notation "[+| c |]" :=
(interp_carry 1 wB to_Z c) (at level 0, c at level 99).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Notation "[-| c |]" :=
(interp_carry (-1) wB to_Z c) (at level 0, c at level 99).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Notation "[|| x ||]" :=
(zn2z_to_Z wB to_Z x) (at level 0, x at level 99).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_more_than_1_digit: 1 < Zpos digits.
Let digits_gt_1 := spec_more_than_1_digit.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma wB_pos : wB > 0.
#[local]
Hint Resolve wB_pos : core.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_to_Z_1 : forall x, 0 <= [|x|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_to_Z_2 : forall x, [|x|] < wB.
#[local]
Hint Resolve spec_to_Z_1 spec_to_Z_2 : core.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_to_Z : forall x, 0 <= [|x|] < wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition of_pos x :=
let (q,r) := Z.pos_div_eucl x wB in (N_of_Z q, r).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_of_pos : forall p,
Zpos p = (Z.of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_zdigits : [|zdigits|] = Zpos digits.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition zero := 0.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition one := 1.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition minus_one := wB - 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_0 : [|zero|] = 0.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_1 : [|one|] = 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_Bm1 : [|minus_one|] = wB - 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition compare x y := Z.compare [|x|] [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_compare : forall x y,
compare x y = Z.compare [|x|] [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition eq0 x :=
match [|x|] with Z0 => true | _ => false end.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_eq0 : forall x, eq0 x = true -> [|x|] = 0.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition opp_c x :=
if eq0 x then C0 0 else C1 (- x).
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition opp x := - x.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition opp_carry x := - x - 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_opp_c : forall x, [-|opp_c x|] = -[|x|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition succ_c x :=
let y := Z.succ x in
if eq0 y then C1 0 else C0 y.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
let z := [|x|] + [|y|] in
if Z_lt_le_dec z wB then C0 z else C1 (z-wB).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
let z := [|x|]+[|y|]+1 in
if Z_lt_le_dec z wB then C0 z else C1 (z-wB).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition succ := Z.succ.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition add_carry x y := x + y + 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma Zmod_equal :
forall x y z, z>0 -> (x-y) mod z = 0 -> x mod z = y mod z.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_succ_c : forall x, [+|succ_c x|] = [|x|] + 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
forall x y, [|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition pred_c x :=
if eq0 x then C1 (wB-1) else C0 (x-1).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition sub_c x y :=
let z := [|x|]-[|y|] in
if Z_lt_le_dec z 0 then C1 (wB+z) else C0 z.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
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.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition pred := Z.pred.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition sub := Z.sub.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition sub_carry x y := x - y - 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_pred_c : forall x, [-|pred_c x|] = [|x|] - 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_sub_carry :
forall x y, [|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
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.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition mul := Z.mul.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition square_c x := mul_c x x.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_mul_c : forall x y, [|| mul_c x y ||] = [|x|] * [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_square_c : forall x, [|| square_c x||] = [|x|] * [|x|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition div x y := Z.div_eucl [|x|] [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_div : forall a b, 0 < [|b|] ->
let (q,r) := div a b in
[|a|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition div_gt := div.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
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|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition modulo x y := [|x|] mod [|y|].
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition modulo_gt x y := [|x|] mod [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_modulo : forall a b, 0 < [|b|] ->
[|modulo a b|] = [|a|] mod [|b|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
[|modulo_gt a b|] = [|a|] mod [|b|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition gcd x y := Z.gcd [|x|] [|y|].
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition gcd_gt x y := Z.gcd [|x|] [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma Zgcd_bound : forall a b, 0<=a -> 0<=b -> Z.gcd a b <= Z.max a b.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_gcd_gt : forall a b, [|a|] > [|b|] ->
Zis_gcd [|a|] [|b|] [|gcd_gt a b|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition div21 a1 a2 b :=
Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
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|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition add_mul_div p x y :=
([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos digits) - [|p|]))).
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
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.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition pos_mod p w := [|w|] mod (2 ^ [|p|]).
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_pos_mod : forall w p,
[|pos_mod p w|] = [|w|] mod (2 ^ [|p|]).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition is_even x :=
if Z.eq_dec ([|x|] mod 2) 0 then true else false.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_is_even : forall x,
if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition sqrt x := Z.sqrt [|x|].
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_sqrt : forall x,
[|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
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.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
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|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma two_p_power2 : forall x, x>=0 -> two_p x = 2 ^ x.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
match [| x |] with
| Z0 => zdigits
| Zneg _ => 0
| (Zpos _) as p => zdigits - Z.log2 p - 1
end.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_head00: forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_head0 : forall x, 0 < [|x|] ->
wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Fixpoint Ptail p := match p with
| xO p => (Ptail p)+1
| _ => 0
end.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma Ptail_pos : forall p, 0 <= Ptail p.
#[local]
Hint Resolve Ptail_pos : core.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition tail0 x :=
match [|x|] with
| Z0 => zdigits
| Zpos p => Ptail p
| Zneg _ => 0
end.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_tail00: forall x, [|x|] = 0 -> [|tail0 x|] = Zpos digits.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_tail0 : forall x, 0 < [|x|] ->
exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]).

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition lor := Z.lor.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition land := Z.land.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition lxor := Z.lxor.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_land x y : [|land x y|] = Z.land [|x|] [|y|].

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Lemma spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|].

Let's now group everything in two records

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition zmod_ops : ZnZ.Ops Z := ZnZ.MkOps
(digits : positive)
(zdigits: t)
(to_Z : t -> Z)
(of_pos : positive -> N * 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)
(lor : t -> t -> t)
(land : t -> t -> t)
(lxor : t -> t -> t).
Existing Instance zmod_ops.

#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition 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_succ

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_tail00
spec_tail0

spec_pos_mod

spec_is_even
spec_sqrt2
spec_sqrt
spec_lor
spec_land
spec_lxor.
Existing Instance zmod_specs.

End ZModulo.

A modular version of the previous construction.

Module Type PositiveNotOne.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Parameter p : positive.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Axiom not_one : p <> 1%positive.
End PositiveNotOne.

Module ZModuloCyclicType (P:PositiveNotOne) <: CyclicType.
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition t := Z.
#[global]
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition ops : ZnZ.Ops t := zmod_ops P.p.
Existing Instance ops.
#[global]
#[deprecated(note="Cyclic.ZModulo will be moved to the test suite", since="8.17")]
Definition specs : ZnZ.Specs ops := zmod_specs P.not_one.
Existing Instance specs.
End ZModuloCyclicType.