# 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.
Set Implicit Arguments.
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.
Module ZnZ.
Class Ops (t:Type) := 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 }.
Section Specs.
Context {t : Type}{ops : Ops t}.
Notation "[| x |]" := (to_Z x) (at level 0, x at level 99).
Let wB := base digits.
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).
Class Specs := MkSpecs {
spec_to_Z : forall x, 0 <= [| x |] < wB;
spec_of_pos : forall p,
Zpos p = ( Z.of_N (fst (of_pos p)))* wB + [|( snd (of_pos p))|];
spec_zdigits : [| zdigits |] = Zpos digits;
spec_more_than_1_digit: 1 < Zpos digits;
spec_0 : [| zero |] = 0;
spec_1 : [| one |] = 1;
spec_m1 : [| minus_one |] = wB - 1;
spec_compare : forall x y, compare x y = ( [| x |] ?= [| y |] );
spec_eq0 : forall x, eq0 x = true -> [| x |] = 0;
spec_opp_c : forall x, [-| opp_c x |] = - [| x |];
spec_opp : forall x, [| opp x |] = ( - [| x |] ) mod wB;
spec_opp_carry : forall x, [| opp_carry x |] = wB - [| x |] - 1;
spec_succ_c : forall x, [+| succ_c x |] = [| x |] + 1;
spec_add_c : forall x y, [+| add_c x y |] = [| x |] + [| y |];
spec_add_carry_c : forall x y, [+| add_carry_c x y |] = [| x |] + [| y |] + 1;
spec_succ : forall x, [| succ x |] = ( [| x |] + 1) mod wB;
spec_add : forall x y, [| add x y |] = ( [| x |] + [| y |] ) mod wB;
spec_add_carry :
forall x y, [| add_carry x y |] = ( [| x |] + [| y |] + 1) mod wB;
spec_pred_c : forall x, [-| pred_c x |] = [| x |] - 1;
spec_sub_c : forall x y, [-| sub_c x y |] = [| x |] - [| y |];
spec_sub_carry_c : forall x y, [-| sub_carry_c x y |] = [| x |] - [| y |] - 1;
spec_pred : forall x, [| pred x |] = ( [| x |] - 1) mod wB;
spec_sub : forall x y, [| sub x y |] = ( [| x |] - [| y |] ) mod wB;
spec_sub_carry :
forall x y, [| sub_carry x y |] = ( [| x |] - [| y |] - 1) mod wB;
spec_mul_c : forall x y, [|| mul_c x y ||] = [| x |] * [| y |];
spec_mul : forall x y, [| mul x y |] = ( [| x |] * [| y |] ) mod wB;
spec_square_c : forall x, [|| square_c x ||] = [| x |] * [| x |];
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 |];
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 |];
spec_div : forall a b, 0 < [| b |] ->
let (q,r) := div a b in
[| a |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |];
spec_modulo_gt : forall a b, [| a |] > [| b |] -> 0 < [| b |] ->
[| modulo_gt a b |] = [| a |] mod [| b |];
spec_modulo : forall a b, 0 < [| b |] ->
[| modulo a b |] = [| a |] mod [| b |];
spec_gcd_gt : forall a b, [| a |] > [| b |] ->
Zis_gcd [| a |] [| b |] [| gcd_gt a b |];
spec_gcd : forall a b, Zis_gcd [| a |] [| b |] [| gcd a b |];
spec_head00: forall x, [| x |] = 0 -> [| head0 x |] = Zpos digits;
spec_head0 : forall x, 0 < [| x |] ->
wB / 2 <= 2 ^ ( [| head0 x |] ) * [| x |] < wB;
spec_tail00: forall x, [| x |] = 0 -> [| tail0 x |] = Zpos digits;
spec_tail0 : forall x, 0 < [| x |] ->
exists y , 0 <= y /\ [| x |] = (2 * y + 1) * (2 ^ [| tail0 x |] ) ;
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;
spec_pos_mod : forall w p,
[| pos_mod p w |] = [| w |] mod (2 ^ [| p |] );
spec_is_even : forall x,
if is_even x then [| x |] mod 2 = 0 else [| x |] mod 2 = 1;
spec_sqrt2 : forall x y,
wB / 4 <= [| x |] ->
let (s,r) := sqrt2 x y in
[|| WW x y ||] = [| s |] ^ 2 + [+| r |] /\
[+| r |] <= 2 * [| s |];
spec_sqrt : forall x,
[| sqrt x |] ^ 2 <= [| x |] < ( [| sqrt x |] + 1) ^ 2
}.
End Specs.
Generic construction of double words
Section WW.
Context {t : Type}{ops : Ops t}{specs : Specs ops}.
Let wB := base digits.
Definition WO' (eq0:t->bool) zero h :=
if eq0 h then W0 else WW h zero.
Definition WO := Eval lazy beta delta [WO'] in
let eq0 := ZnZ.eq0 in
let zero := ZnZ.zero in
WO' eq0 zero.
Definition OW' (eq0:t->bool) zero l :=
if eq0 l then W0 else WW zero l.
Definition OW := Eval lazy beta delta [OW'] in
let eq0 := ZnZ.eq0 in
let zero := ZnZ.zero in
OW' eq0 zero.
Definition WW' (eq0:t->bool) zero h l :=
if eq0 h then OW' eq0 zero l else WW h l.
Definition WW := Eval lazy beta delta [WW' OW'] in
let eq0 := ZnZ.eq0 in
let zero := ZnZ.zero in
WW' eq0 zero.
Lemma spec_WO : forall h,
zn2z_to_Z wB to_Z (WO h) = ( to_Z h )* wB.
Lemma spec_OW : forall l,
zn2z_to_Z wB to_Z (OW l) = to_Z l.
Lemma spec_WW : forall h l,
zn2z_to_Z wB to_Z (WW h l) = ( to_Z h )* wB + to_Z l.
End WW.
Injecting Z numbers into a cyclic structure
Section Of_Z.
Context {t : Type}{ops : Ops t}{specs : Specs ops}.
Notation "[| x |]" := (to_Z x) (at level 0, x at level 99).
Theorem of_pos_correct:
forall p, Zpos p < base digits -> [|( snd (of_pos p))|] = Zpos p.
Definition of_Z z :=
match z with
| Zpos p => snd (of_pos p)
| _ => zero
end.
Theorem of_Z_correct:
forall p, 0 <= p < base digits -> [| of_Z p |] = p.
End Of_Z.
End ZnZ.
A modular specification grouping the earlier records.
Module Type CyclicType.
Parameter t : Type.
Declare Instance ops : ZnZ.Ops t.
Declare Instance specs : ZnZ.Specs ops.
End CyclicType.
A Cyclic structure can be seen as a ring
Module CyclicRing (Import Cyclic : CyclicType).
Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99).
Definition eq (n m : t) := [| n |] = [| m |].
Local Infix "==" := eq (at level 70).
Local Notation "0" := ZnZ.zero.
Local Notation "1" := ZnZ.one.
Local Infix "+" := ZnZ.add.
Local Infix "-" := ZnZ.sub.
Local Notation "- x" := (ZnZ.opp x).
Local Infix "*" := ZnZ.mul.
Local Notation wB := (base ZnZ.digits).
Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul
ZnZ.spec_opp ZnZ.spec_sub
: cyclic.
Ltac zify := unfold eq 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 + - y == x - y.
Lemma add_opp_diag_r : forall x, x + - x == 0.
Lemma CyclicRing : ring_theory 0 1 ZnZ.add ZnZ.mul ZnZ.sub ZnZ.opp eq.
Definition eqb x y :=
match 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.