# Library Coq.Numbers.Cyclic.Abstract.CyclicAxioms

# Signature and specification of a bounded integer structure

This file specifies how to represent Z/nZ when n=2^d, d being the number of digits of these bounded integers.
Require Import ZArith.
Require Import Znumtheory.
Require Import BigNumPrelude.
Require Import DoubleType.
Local Open Scope Z_scope.
First, a description via an operator record and a spec record.
Section Z_nZ_Op.
Variable znz : Type.
Record znz_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 }.
End Z_nZ_Op.
Section Z_nZ_Spec.
Variable w : Type.
Variable w_op : znz_op w.
Let w_digits := w_op.(znz_digits).
Let w_zdigits := w_op.(znz_zdigits).
Let w_to_Z := w_op.(znz_to_Z).
Let w_of_pos := w_op.(znz_of_pos).
Let w_head0 := w_op.(znz_head0).
Let w_tail0 := w_op.(znz_tail0).
Let w0 := w_op.(znz_0).
Let w1 := w_op.(znz_1).
Let wBm1 := w_op.(znz_Bm1).
Let w_compare := w_op.(znz_compare).
Let w_eq0 := w_op.(znz_eq0).
Let w_opp_c := w_op.(znz_opp_c).
Let w_opp := w_op.(znz_opp).
Let w_opp_carry := w_op.(znz_opp_carry).
Let w_succ_c := w_op.(znz_succ_c).
Let w_add_c := w_op.(znz_add_c).
Let w_add_carry_c := w_op.(znz_add_carry_c).
Let w_succ := w_op.(znz_succ).
Let w_add := w_op.(znz_add).
Let w_add_carry := w_op.(znz_add_carry).
Let w_pred_c := w_op.(znz_pred_c).
Let w_sub_c := w_op.(znz_sub_c).
Let w_sub_carry_c := w_op.(znz_sub_carry_c).
Let w_pred := w_op.(znz_pred).
Let w_sub := w_op.(znz_sub).
Let w_sub_carry := w_op.(znz_sub_carry).
Let w_mul_c := w_op.(znz_mul_c).
Let w_mul := w_op.(znz_mul).
Let w_square_c := w_op.(znz_square_c).
Let w_div21 := w_op.(znz_div21).
Let w_div_gt := w_op.(znz_div_gt).
Let w_div := w_op.(znz_div).
Let w_mod_gt := w_op.(znz_mod_gt).
Let w_mod := w_op.(znz_mod).
Let w_gcd_gt := w_op.(znz_gcd_gt).
Let w_gcd := w_op.(znz_gcd).
Let w_add_mul_div := w_op.(znz_add_mul_div).
Let w_pos_mod := w_op.(znz_pos_mod).
Let w_is_even := w_op.(znz_is_even).
Let w_sqrt2 := w_op.(znz_sqrt2).
Let w_sqrt := w_op.(znz_sqrt).
Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99).
Let wB := base w_digits.
Notation "[+| c |]" :=
(interp_carry 1 wB w_to_Z c) (at level 0, x at level 99).
Notation "[-| c |]" :=
(interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99).
Notation "[|| x ||]" :=
(zn2z_to_Z wB w_to_Z x) (at level 0, x at level 99).
Record znz_spec := mk_znz_spec {
spec_to_Z : forall x, 0 <= [| x |] < wB;
spec_of_pos : forall p,
Zpos p = ( Z_of_N (fst (w_of_pos p)))* wB + [|( snd (w_of_pos p))|];
spec_zdigits : [| w_zdigits |] = Zpos w_digits;
spec_more_than_1_digit: 1 < Zpos w_digits;
spec_0 : [| w0 |] = 0;
spec_1 : [| w1 |] = 1;
spec_Bm1 : [| wBm1 |] = wB - 1;
spec_compare :
forall x y,
match w_compare x y with
| Eq => [| x |] = [| y |]
| Lt => [| x |] < [| y |]
| Gt => [| x |] > [| y |]
end;
spec_eq0 : forall x, w_eq0 x = true -> [| x |] = 0;
spec_opp_c : forall x, [-| w_opp_c x |] = - [| x |];
spec_opp : forall x, [| w_opp x |] = ( - [| x |] ) mod wB;
spec_opp_carry : forall x, [| w_opp_carry x |] = wB - [| x |] - 1;
spec_succ_c : forall x, [+| w_succ_c x |] = [| x |] + 1;
spec_add_c : forall x y, [+| w_add_c x y |] = [| x |] + [| y |];
spec_add_carry_c : forall x y, [+| w_add_carry_c x y |] = [| x |] + [| y |] + 1;
spec_succ : forall x, [| w_succ x |] = ( [| x |] + 1) mod wB;
spec_add : forall x y, [| w_add x y |] = ( [| x |] + [| y |] ) mod wB;
spec_add_carry :
forall x y, [| w_add_carry x y |] = ( [| x |] + [| y |] + 1) mod wB;
spec_pred_c : forall x, [-| w_pred_c x |] = [| x |] - 1;
spec_sub_c : forall x y, [-| w_sub_c x y |] = [| x |] - [| y |];
spec_sub_carry_c : forall x y, [-| w_sub_carry_c x y |] = [| x |] - [| y |] - 1;
spec_pred : forall x, [| w_pred x |] = ( [| x |] - 1) mod wB;
spec_sub : forall x y, [| w_sub x y |] = ( [| x |] - [| y |] ) mod wB;
spec_sub_carry :
forall x y, [| w_sub_carry x y |] = ( [| x |] - [| y |] - 1) mod wB;
spec_mul_c : forall x y, [|| w_mul_c x y ||] = [| x |] * [| y |];
spec_mul : forall x y, [| w_mul x y |] = ( [| x |] * [| y |] ) mod wB;
spec_square_c : forall x, [|| w_square_c x ||] = [| x |] * [| x |];
spec_div21 : forall a1 a2 b,
wB /2 <= [| b |] ->
[| a1 |] < [| b |] ->
let (q,r) := w_div21 a1 a2 b in
[| a1 |] * wB + [| a2 |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |];
spec_div_gt : forall a b, [| a |] > [| b |] -> 0 < [| b |] ->
let (q,r) := w_div_gt a b in
[| a |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |];
spec_div : forall a b, 0 < [| b |] ->
let (q,r) := w_div a b in
[| a |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |];
spec_mod_gt : forall a b, [| a |] > [| b |] -> 0 < [| b |] ->
[| w_mod_gt a b |] = [| a |] mod [| b |];
spec_mod : forall a b, 0 < [| b |] ->
[| w_mod a b |] = [| a |] mod [| b |];
spec_gcd_gt : forall a b, [| a |] > [| b |] ->
Zis_gcd [| a |] [| b |] [| w_gcd_gt a b |];
spec_gcd : forall a b, Zis_gcd [| a |] [| b |] [| w_gcd a b |];
spec_head00: forall x, [| x |] = 0 -> [| w_head0 x |] = Zpos w_digits;
spec_head0 : forall x, 0 < [| x |] ->
wB / 2 <= 2 ^ ( [| w_head0 x |] ) * [| x |] < wB;
spec_tail00: forall x, [| x |] = 0 -> [| w_tail0 x |] = Zpos w_digits;
spec_tail0 : forall x, 0 < [| x |] ->
exists y , 0 <= y /\ [| x |] = (2 * y + 1) * (2 ^ [| w_tail0 x |] ) ;
spec_add_mul_div : forall x y p,
[| p |] <= Zpos w_digits ->
[| w_add_mul_div p x y |] =
( [| x |] * (2 ^ [| p |] ) +
[| y |] / (2 ^ ( ( Zpos w_digits ) - [| p |] ) ) ) mod wB;
spec_pos_mod : forall w p,
[| w_pos_mod p w |] = [| w |] mod (2 ^ [| p |] );
spec_is_even : forall x,
if w_is_even x then [| x |] mod 2 = 0 else [| x |] mod 2 = 1;
spec_sqrt2 : forall x y,
wB / 4 <= [| x |] ->
let (s,r) := w_sqrt2 x y in
[|| WW x y ||] = [| s |] ^ 2 + [+| r |] /\
[+| r |] <= 2 * [| s |];
spec_sqrt : forall x,
[| w_sqrt x |] ^ 2 <= [| x |] < ( [| w_sqrt x |] + 1) ^ 2
}.
End Z_nZ_Spec.
Generic construction of double words
Section WW.
Variable w : Type.
Variable w_op : znz_op w.
Variable op_spec : znz_spec w_op.
Let wB := base w_op.(znz_digits).
Let w_to_Z := w_op.(znz_to_Z).
Let w_eq0 := w_op.(znz_eq0).
Let w_0 := w_op.(znz_0).
Definition znz_W0 h :=
if w_eq0 h then W0 else WW h w_0.
Definition znz_0W l :=
if w_eq0 l then W0 else WW w_0 l.
Definition znz_WW h l :=
if w_eq0 h then znz_0W l else WW h l.
Lemma spec_W0 : forall h,
zn2z_to_Z wB w_to_Z (znz_W0 h) = ( w_to_Z h )* wB.
Lemma spec_0W : forall l,
zn2z_to_Z wB w_to_Z (znz_0W l) = w_to_Z l.
Lemma spec_WW : forall h l,
zn2z_to_Z wB w_to_Z (znz_WW h l) = ( w_to_Z h )* wB + w_to_Z l.
End WW.
Injecting Z numbers into a cyclic structure
Section znz_of_pos.
Variable w : Type.
Variable w_op : znz_op w.
Variable op_spec : znz_spec w_op.
Notation "[| x |]" := (znz_to_Z w_op x) (at level 0, x at level 99).
Definition znz_of_Z (w:Type) (op:znz_op w) z :=
match z with
| Zpos p => snd (op.(znz_of_pos) p)
| _ => op.(znz_0)
end.
Theorem znz_of_pos_correct:
forall p, Zpos p < base (znz_digits w_op) -> [|( snd (znz_of_pos w_op p))|] = Zpos p.
Theorem znz_of_Z_correct:
forall p, 0 <= p < base (znz_digits w_op) -> [| znz_of_Z w_op p |] = p.
End znz_of_pos.
A modular specification grouping the earlier records.
Module Type CyclicType.
Parameter w : Type.
Parameter w_op : znz_op w.
Parameter w_spec : znz_spec w_op.
End CyclicType.
A Cyclic structure can be seen as a ring
Module CyclicRing (Import Cyclic : CyclicType).
Definition t := w.
Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
Definition eq (n m : t) := [| n |] = [| m |].
Definition zero : t := w_op.(znz_0).
Definition one := w_op.(znz_1).
Definition add := w_op.(znz_add).
Definition sub := w_op.(znz_sub).
Definition mul := w_op.(znz_mul).
Definition opp := w_op.(znz_opp).
Local Infix "==" := eq (at level 70).
Local Notation "0" := zero.
Local Notation "1" := one.
Local Infix "+" := add.
Local Infix "-" := sub.
Local Infix "*" := mul.
Local Notation "!!" := (base (znz_digits w_op)).
Hint Rewrite
w_spec.(spec_0) w_spec.(spec_1)
w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_opp) w_spec.(spec_sub)
: cyclic.
Ltac zify :=
unfold eq, zero, one, add, sub, mul, opp in *; autorewrite with cyclic.
Lemma add_0_l : forall x, 0 + x == x.
Lemma add_comm : forall x y, x + y == y + x.
Lemma add_assoc : forall x y z, x + ( y + z ) == x + y + z.
Lemma mul_1_l : forall x, 1 * x == x.
Lemma mul_comm : forall x y, x * y == y * x.
Lemma mul_assoc : forall x y z, x * ( y * z ) == x * y * z.
Lemma mul_add_distr_r : forall x y z, ( x + y )* z == x * z + y * z.
Lemma add_opp_r : forall x y, x + opp y == x - y.
Lemma add_opp_diag_r : forall x, x + opp x == 0.
Lemma CyclicRing : ring_theory 0 1 add mul sub opp eq.
Definition eqb x y :=
match w_op.(znz_compare) x y with Eq => true | _ => false end.
Lemma eqb_eq : forall x y, eqb x y = true <-> x == y.
Lemma eqb_correct : forall x y, eqb x y = true -> x == y.
End CyclicRing.