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, c at level 99).

 Notation "[-| c |]" :=
   (interp_carry (-1) wB to_Z c) (at level 0, c 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|]).

 Definition lor := Z.lor.
 Definition land := Z.land.
 Definition lxor := Z.lxor.

 Lemma spec_lor x y : [|lor x y|] = Z.lor [|x|] [|y|].

 Lemma spec_land x y : [|land x y|] = Z.land [|x|] [|y|].

 Lemma spec_lxor x y : [|lxor x y|] = Z.lxor [|x|] [|y|].

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)
    (lor : t -> t -> t)
    (land : t -> t -> t)
    (lxor : t -> 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
    spec_lor
    spec_land
    spec_lxor.

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.