aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
blob: 1e66d9b9ef3d5ee82fdd84fd31a8083295ffc067 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
(************************************************************************)

(** * 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 {

    (* Conversion functions with Z *)
    digits : positive;
    zdigits: t;
    to_Z   : t -> Z;
    of_pos : positive -> N * t; (* Euclidean division by [2^digits] *)
    head0  : t -> t; (* number of digits 0 in front of the number *)
    tail0  : t -> t; (* number of digits 0 at the bottom of the number *)

    (* Basic numbers *)
    zero : t;
    one  : t;
    minus_one : t;  (* [2^digits-1], which is equivalent to [-1] *)

    (* Comparison *)
    compare     : t -> t -> comparison;
    eq0         : t -> bool;

    (* Basic arithmetic operations *)
    opp_c       : t -> carry t;
    opp         : t -> t;
    opp_carry   : t -> t; (* the carry is known to be -1 *)

    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;

    (* Special divisions operations *)
    div21       : t -> t -> t -> t*t;
    div_gt      : t -> t -> t * t; (* specialized version of [div] *)
    div         : t -> t -> t * t;

    modulo_gt   : t -> t -> t; (* specialized version of [mod] *)
    modulo      : t -> t -> t;

    gcd_gt      : t -> t -> t; (* specialized version of [gcd] *)
    gcd         : t -> t -> t;
    (* [add_mul_div p i j] is a combination of the [(digits-p)]
       low bits of [i] above the [p] high bits of [j]:
       [add_mul_div p i j = i*2^p+j/2^(digits-p)] *)
    add_mul_div : t -> t -> t -> t;
    (* [pos_mod p i] is [i mod 2^p] *)
    pos_mod     : t -> t -> t;

    is_even     : t -> bool;
    (* square root *)
    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 {

    (* Conversion functions with Z *)
    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;

    (* Basic numbers *)
    spec_0   : [|zero|] = 0;
    spec_1   : [|one|] = 1;
    spec_m1 : [|minus_one|] = wB - 1;

    (* Comparison *)
    spec_compare : forall x y, compare x y = ([|x|] ?= [|y|]);
    (* NB: the spec of [eq0] is deliberately partial,
       see DoubleCyclic where [eq0 x = true <-> x = W0] *)
    spec_eq0 : forall x, eq0 x = true -> [|x|] = 0;
    (* Basic arithmetic operations *)
    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|];

    (* Special divisions operations *)
    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|];


    (* shift operations *)
    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|]);
    (* sqrt *)
    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.

 Implicit Arguments Specs [[t]].

 (** Generic construction of double words *)

 Section WW.

 Context {t : Type}{ops : Ops t}{specs : Specs ops}.

 Let wB := base digits.

 Definition WO h :=
  if eq0 h then W0 else WW h zero.

 Definition OW l :=
  if eq0 l then W0 else WW zero l.

 Definition WW h l :=
  if eq0 h then OW l else WW h l.

 Lemma spec_WO : forall h,
   zn2z_to_Z wB to_Z (WO h) = (to_Z h)*wB.
 Proof.
 unfold zn2z_to_Z, WO; simpl; intros.
 case_eq (eq0 h); intros.
 rewrite (spec_eq0 _ H); auto.
 rewrite spec_0; auto with zarith.
 Qed.

 Lemma spec_OW : forall l,
   zn2z_to_Z wB to_Z (OW l) = to_Z l.
 Proof.
 unfold zn2z_to_Z, OW; simpl; intros.
 case_eq (eq0 l); intros.
 rewrite (spec_eq0 _ H); auto.
 rewrite spec_0; auto with zarith.
 Qed.

 Lemma spec_WW : forall h l,
  zn2z_to_Z wB to_Z (WW h l) = (to_Z h)*wB + to_Z l.
 Proof.
 unfold WW; simpl; intros.
 case_eq (eq0 h); intros.
 rewrite (spec_eq0 _ H); auto.
 rewrite spec_OW; auto.
 simpl; auto.
 Qed.

 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.
 Proof.
 intros p Hp.
 generalize (spec_of_pos p).
 case (of_pos p); intros n w1; simpl.
 case n; simpl Npos; auto with zarith.
 intros p1 Hp1; contradict Hp; apply Zle_not_lt.
 replace (base digits) with (1 * base digits + 0) by ring.
 rewrite Hp1.
 apply Zplus_le_compat.
 apply Zmult_le_compat; auto with zarith.
 case p1; simpl; intros; red; simpl; intros; discriminate.
 unfold base; auto with zarith.
 case (spec_to_Z w1); auto with zarith.
 Qed.

 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.
 Proof.
 intros p; case p; simpl; try rewrite spec_0; auto.
 intros; rewrite of_pos_correct; auto with zarith.
 intros p1 (H1, _); contradict H1; apply Zlt_not_le; red; simpl; auto.
 Qed.

 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.
Proof.
intros. zify. rewrite Zplus_0_l.
apply Zmod_small. apply ZnZ.spec_to_Z.
Qed.

Lemma add_comm : forall x y, x + y == y + x.
Proof.
intros. zify. now rewrite Zplus_comm.
Qed.

Lemma add_assoc : forall x y z, x + (y + z) == x + y + z.
Proof.
intros. zify. now rewrite Zplus_mod_idemp_r, Zplus_mod_idemp_l, Zplus_assoc.
Qed.

Lemma mul_1_l : forall x, 1 * x == x.
Proof.
intros. zify. rewrite Zmult_1_l.
apply Zmod_small. apply ZnZ.spec_to_Z.
Qed.

Lemma mul_comm : forall x y, x * y == y * x.
Proof.
intros. zify. now rewrite Zmult_comm.
Qed.

Lemma mul_assoc : forall x y z, x * (y * z) == x * y * z.
Proof.
intros. zify. now rewrite Zmult_mod_idemp_r, Zmult_mod_idemp_l, Zmult_assoc.
Qed.

Lemma mul_add_distr_r : forall x y z, (x+y)*z == x*z + y*z.
Proof.
intros. zify. now rewrite <- Zplus_mod, Zmult_mod_idemp_l, Zmult_plus_distr_l.
Qed.

Lemma add_opp_r : forall x y, x + - y == x-y.
Proof.
intros. zify. rewrite <- Zminus_mod_idemp_r. unfold Zminus.
destruct (Z_eq_dec ([|y|] mod wB) 0) as [EQ|NEQ].
rewrite Z_mod_zero_opp_full, EQ, 2 Zplus_0_r; auto.
rewrite Z_mod_nz_opp_full by auto.
rewrite <- Zplus_mod_idemp_r, <- Zminus_mod_idemp_l.
rewrite Z_mod_same_full. simpl. now rewrite Zplus_mod_idemp_r.
Qed.

Lemma add_opp_diag_r : forall x, x + - x == 0.
Proof.
intros. red. rewrite add_opp_r. zify. now rewrite Zminus_diag, Zmod_0_l.
Qed.

Lemma CyclicRing : ring_theory 0 1 ZnZ.add ZnZ.mul ZnZ.sub ZnZ.opp eq.
Proof.
constructor.
exact add_0_l. exact add_comm. exact add_assoc.
exact mul_1_l. exact mul_comm. exact mul_assoc.
exact mul_add_distr_r.
symmetry. apply add_opp_r.
exact add_opp_diag_r.
Qed.

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.
Proof.
 intros. unfold eqb, eq.
 rewrite ZnZ.spec_compare.
 case Zcompare_spec; intuition; try discriminate.
Qed.

(* POUR HUGO:
Lemma eqb_eq : forall x y, eqb x y = true <-> x == y.
Proof.
 intros. unfold eqb, eq. generalize (ZnZ.spec_compare x y).
 case (ZnZ.compare x y); intuition; try discriminate.
 (* BUG ?! using destruct instead of case won't work:
   it gives 3 subcases, but ZnZ.compare x y is still there in them! *)
Qed.
*)

Lemma eqb_correct : forall x y, eqb x y = true -> x==y.
Proof. now apply eqb_eq. Qed.

End CyclicRing.