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.
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
Injecting Z numbers into a cyclic structure
A modular specification grouping the earlier records.
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.