summaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
blob: c7d83acc334439088c1e00b0fd71e27dcefec11a (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
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
(************************************************************************)
(*  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             *)
(************************************************************************)

(*i $Id: DoubleMul.v 10964 2008-05-22 11:08:13Z letouzey $ i*)

Set Implicit Arguments.

Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.

Open Local Scope Z_scope.

Section DoubleMul.
 Variable w : Type.
 Variable w_0 : w.
 Variable w_1 : w.
 Variable w_WW : w -> w -> zn2z w.
 Variable w_W0 : w -> zn2z w.
 Variable w_0W : w -> zn2z w.
 Variable w_compare : w -> w -> comparison.
 Variable w_succ : w -> w.
 Variable w_add_c : w -> w -> carry w.
 Variable w_add : w -> w -> w.
 Variable w_sub: w -> w -> w.
 Variable w_mul_c : w -> w -> zn2z w.
 Variable w_mul : w -> w -> w.
 Variable w_square_c : w -> zn2z w.
 Variable ww_add_c : zn2z w -> zn2z w -> carry (zn2z w).
 Variable ww_add   : zn2z w -> zn2z w -> zn2z w.
 Variable ww_add_carry : zn2z w -> zn2z w -> zn2z w.
 Variable ww_sub_c : zn2z w -> zn2z w -> carry (zn2z w).
 Variable ww_sub   : zn2z w -> zn2z w -> zn2z w.

 (* ** Multiplication ** *)

 (*   (xh*B+xl) (yh*B + yl)
   xh*yh         = hh  = |hhh|hhl|B2
   xh*yl +xl*yh  = cc  =     |cch|ccl|B
   xl*yl         = ll  =         |llh|lll 
  *)

 Definition double_mul_c (cross:w->w->w->w->zn2z w -> zn2z w -> w*zn2z w) x y :=
  match x, y with
  | W0, _ => W0
  | _, W0 => W0
  | WW xh xl, WW yh yl =>
    let hh := w_mul_c xh yh in
    let ll := w_mul_c xl yl in
    let (wc,cc) := cross xh xl yh yl hh ll in
    match cc with 
    | W0 => WW (ww_add hh (w_W0 wc)) ll
    | WW cch ccl =>
      match ww_add_c (w_W0 ccl) ll with
      | C0 l => WW (ww_add hh (w_WW wc cch)) l
      | C1 l => WW (ww_add_carry hh (w_WW wc cch)) l
      end
    end
  end.

 Definition ww_mul_c :=
  double_mul_c 
    (fun xh xl yh yl hh ll=> 
      match ww_add_c (w_mul_c xh yl) (w_mul_c xl yh) with
      | C0 cc => (w_0, cc)
      | C1 cc => (w_1, cc)
      end).

 Definition w_2 := w_add w_1 w_1.

 Definition kara_prod xh xl yh yl hh ll :=
    match ww_add_c hh ll with 
      C0 m =>
         match w_compare xl xh with
           Eq => (w_0, m)
         | Lt => 
           match w_compare yl yh with
             Eq => (w_0, m)
           | Lt => (w_0, ww_sub m (w_mul_c (w_sub xh xl) (w_sub yh yl)))
           | Gt => match ww_add_c m (w_mul_c (w_sub xh xl) (w_sub yl yh)) with
                      C1 m1 => (w_1, m1) | C0 m1 => (w_0, m1)
                   end
           end
         | Gt => 
           match w_compare yl yh with
             Eq => (w_0, m)
           | Lt => match ww_add_c m (w_mul_c (w_sub xl xh)  (w_sub yh yl)) with
                      C1 m1 => (w_1, m1) | C0 m1 => (w_0, m1)
                   end
           | Gt => (w_0, ww_sub m (w_mul_c (w_sub xl xh)  (w_sub yl yh)))
           end
         end
    | C1 m =>
         match w_compare xl xh with
           Eq => (w_1, m)
         | Lt => 
           match w_compare yl yh with
             Eq => (w_1, m)
           | Lt => match ww_sub_c m (w_mul_c (w_sub xh xl) (w_sub yh yl)) with
                    C0 m1 => (w_1, m1) | C1 m1 => (w_0, m1)
                   end 
           | Gt => match ww_add_c m (w_mul_c (w_sub xh xl) (w_sub yl yh)) with
                      C1 m1 => (w_2, m1) | C0 m1 => (w_1, m1)
                   end
           end
         | Gt => 
           match w_compare yl yh with
             Eq => (w_1, m)
           | Lt => match ww_add_c m (w_mul_c (w_sub xl xh) (w_sub yh yl)) with
                      C1 m1 => (w_2, m1) | C0 m1 => (w_1, m1)
                   end
           | Gt => match ww_sub_c m (w_mul_c (w_sub xl xh) (w_sub yl yh)) with
                     C1 m1 => (w_0, m1) | C0 m1 => (w_1, m1)
                   end
           end
         end
    end.

 Definition ww_karatsuba_c :=  double_mul_c kara_prod.

 Definition ww_mul x y :=
  match x, y with
  | W0, _ => W0
  | _, W0 => W0  
  | WW xh xl, WW yh yl => 
    let ccl := w_add (w_mul xh yl) (w_mul xl yh) in
    ww_add (w_W0 ccl) (w_mul_c xl yl)
  end.

 Definition ww_square_c x  :=
  match x with
  | W0 => W0
  | WW xh xl =>
    let hh := w_square_c xh in
    let ll := w_square_c xl in
    let xhxl := w_mul_c xh xl in
    let (wc,cc) :=
      match ww_add_c xhxl xhxl with
      | C0 cc => (w_0, cc)
      | C1 cc => (w_1, cc)
      end in
    match cc with
    | W0 => WW (ww_add hh (w_W0 wc)) ll
    | WW cch ccl =>
      match ww_add_c (w_W0 ccl) ll with
      | C0 l => WW (ww_add hh (w_WW wc cch)) l
      | C1 l => WW (ww_add_carry hh (w_WW wc cch)) l
      end
    end
  end.

 Section DoubleMulAddn1.
  Variable w_mul_add : w -> w -> w -> w * w.

  Fixpoint double_mul_add_n1 (n:nat) : word w n -> w -> w -> w * word w n :=
   match n return word w n -> w -> w -> w * word w n with 
   | O => w_mul_add 
   | S n1 => 
     let mul_add := double_mul_add_n1 n1 in
     fun x y r =>
     match x with
     | W0 => (w_0,extend w_0W n1 r)
     | WW xh xl =>
       let (rl,l) := mul_add xl y r in
       let (rh,h) := mul_add xh y rl in
       (rh, double_WW w_WW n1 h l)
     end
   end.

 End DoubleMulAddn1.

 Section DoubleMulAddmn1.
  Variable wn: Type.
  Variable extend_n : w -> wn.
  Variable wn_0W : wn -> zn2z wn.
  Variable wn_WW : wn -> wn -> zn2z wn.
  Variable w_mul_add_n1 : wn -> w -> w -> w*wn.
  Fixpoint double_mul_add_mn1 (m:nat) : 
	word wn m -> w -> w -> w*word wn m :=
   match m return word wn m -> w -> w -> w*word wn m with 
   | O => w_mul_add_n1 
   | S m1 => 
     let mul_add := double_mul_add_mn1 m1 in
     fun x y r =>
     match x with
     | W0 => (w_0,extend wn_0W m1 (extend_n r))
     | WW xh xl =>
       let (rl,l) := mul_add xl y r in
       let (rh,h) := mul_add xh y rl in
       (rh, double_WW wn_WW m1 h l)
     end
   end.

 End DoubleMulAddmn1.

 Definition w_mul_add x y r :=
  match w_mul_c x y with
  | W0 => (w_0, r)
  | WW h l =>
    match w_add_c l r with
    | C0 lr => (h,lr)
    | C1 lr => (w_succ h, lr) 
    end
  end.

  
 (*Section DoubleProof. *)
  Variable w_digits : positive.
  Variable w_to_Z : w -> Z.

  Notation wB  := (base w_digits).
  Notation wwB := (base (ww_digits w_digits)).
  Notation "[| x |]" := (w_to_Z x)  (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 "[-| c |]" :=
   (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99).

  Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
  Notation "[+[ c ]]" := 
   (interp_carry 1 wwB (ww_to_Z w_digits w_to_Z) c) 
   (at level 0, x at level 99).
  Notation "[-[ c ]]" := 
   (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) 
   (at level 0, x at level 99).

  Notation "[|| x ||]" :=
    (zn2z_to_Z wwB (ww_to_Z w_digits w_to_Z) x)  (at level 0, x at level 99).

  Notation "[! n | x !]" := (double_to_Z w_digits w_to_Z n x)
    (at level 0, x at level 99).

  Variable spec_more_than_1_digit: 1 < Zpos w_digits.
  Variable spec_w_0   : [|w_0|] = 0.
  Variable spec_w_1   : [|w_1|] = 1.

  Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.

  Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
  Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB.
  Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
  Variable spec_w_compare :
     forall x y,
       match w_compare x y with
       | Eq => [|x|] = [|y|]
       | Lt => [|x|] < [|y|]
       | Gt => [|x|] > [|y|]
       end.
  Variable spec_w_succ : forall x, [|w_succ x|] = ([|x|] + 1) mod wB.
  Variable spec_w_add_c  : forall x y, [+|w_add_c x y|] = [|x|] + [|y|].
  Variable spec_w_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB.
  Variable spec_w_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB.

  Variable spec_w_mul_c : forall x y, [[ w_mul_c x y ]] = [|x|] * [|y|].
  Variable spec_w_mul : forall x y, [|w_mul x y|] = ([|x|] * [|y|]) mod wB.
  Variable spec_w_square_c : forall x, [[ w_square_c x]] = [|x|] * [|x|].

  Variable spec_ww_add_c  : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]].
  Variable spec_ww_add : forall x y, [[ww_add x y]] = ([[x]] + [[y]]) mod wwB.
  Variable spec_ww_add_carry :
	 forall x y, [[ww_add_carry x y]] = ([[x]] + [[y]] + 1) mod wwB.
  Variable spec_ww_sub : forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB.
  Variable spec_ww_sub_c : forall x y, [-[ww_sub_c x y]] = [[x]] - [[y]].
 
 
  Lemma spec_ww_to_Z : forall x, 0 <= [[x]] < wwB.
  Proof. intros x;apply spec_ww_to_Z;auto. Qed.

  Lemma spec_ww_to_Z_wBwB : forall x, 0 <= [[x]] < wB^2.
  Proof. rewrite <- wwB_wBwB;apply spec_ww_to_Z. Qed.

  Hint Resolve spec_ww_to_Z spec_ww_to_Z_wBwB : mult.
  Ltac zarith := auto with zarith mult.

  Lemma wBwB_lex: forall a b c d,
      a * wB^2 + [[b]] <= c * wB^2 + [[d]] -> 
      a <= c.
  Proof.   
   intros a b c d H; apply beta_lex with [[b]] [[d]] (wB^2);zarith.
  Qed.

  Lemma wBwB_lex_inv: forall a b c d, 
      a < c -> 
      a * wB^2 + [[b]] < c * wB^2 + [[d]]. 
  Proof.
   intros a b c d H; apply beta_lex_inv; zarith.
  Qed.

  Lemma sum_mul_carry : forall xh xl yh yl wc cc,
   [|wc|]*wB^2 + [[cc]] = [|xh|] * [|yl|] + [|xl|] * [|yh|] -> 
   0 <= [|wc|] <= 1.
  Proof.
   intros.
   apply (sum_mul_carry [|xh|] [|xl|] [|yh|] [|yl|] [|wc|][[cc]] wB);zarith.
   apply wB_pos.
  Qed.

  Theorem mult_add_ineq: forall xH yH crossH, 
               0 <= [|xH|] * [|yH|] + [|crossH|] < wwB.
  Proof.
   intros;rewrite wwB_wBwB;apply mult_add_ineq;zarith.
  Qed.
 
  Hint Resolve mult_add_ineq : mult.
 
  Lemma spec_mul_aux : forall xh xl yh yl wc (cc:zn2z w) hh ll,
   [[hh]] = [|xh|] * [|yh|] ->
   [[ll]] = [|xl|] * [|yl|] ->
   [|wc|]*wB^2 + [[cc]] = [|xh|] * [|yl|] + [|xl|] * [|yh|] ->
    [||match cc with
      | W0 => WW (ww_add hh (w_W0 wc)) ll
      | WW cch ccl =>
          match ww_add_c (w_W0 ccl) ll with
          | C0 l => WW (ww_add hh (w_WW wc cch)) l
          | C1 l => WW (ww_add_carry hh (w_WW wc cch)) l
          end
      end||] = ([|xh|] * wB + [|xl|]) * ([|yh|] * wB + [|yl|]).
  Proof.
   intros;assert (U1 := wB_pos w_digits).
   replace (([|xh|] * wB + [|xl|]) * ([|yh|] * wB + [|yl|])) with 
   ([|xh|]*[|yh|]*wB^2 + ([|xh|]*[|yl|] + [|xl|]*[|yh|])*wB + [|xl|]*[|yl|]).
   2:ring. rewrite <- H1;rewrite <- H;rewrite <- H0.  
   assert (H2 := sum_mul_carry _ _ _ _ _ _ H1).
   destruct cc as [ | cch ccl]; simpl zn2z_to_Z; simpl ww_to_Z.
   rewrite spec_ww_add;rewrite spec_w_W0;rewrite Zmod_small;
    rewrite wwB_wBwB. ring.
   rewrite <- (Zplus_0_r ([|wc|]*wB));rewrite H;apply mult_add_ineq3;zarith.
   simpl ww_to_Z in H1. assert (U:=spec_to_Z cch).
   assert ([|wc|]*wB + [|cch|] <= 2*wB - 3).
    destruct (Z_le_gt_dec ([|wc|]*wB + [|cch|]) (2*wB - 3));trivial.
    assert ([|xh|] * [|yl|] + [|xl|] * [|yh|] <= (2*wB - 4)*wB + 2).
     ring_simplify ((2*wB - 4)*wB + 2).
     assert (H4 := Zmult_lt_b _ _ _ (spec_to_Z xh) (spec_to_Z yl)).
     assert (H5 := Zmult_lt_b _ _ _ (spec_to_Z xl) (spec_to_Z yh)).
     omega.
   generalize H3;clear H3;rewrite <- H1.
   rewrite Zplus_assoc; rewrite Zpower_2; rewrite Zmult_assoc;
     rewrite <- Zmult_plus_distr_l.
    assert (((2 * wB - 4) + 2)*wB <= ([|wc|] * wB + [|cch|])*wB).
     apply Zmult_le_compat;zarith.
    rewrite Zmult_plus_distr_l in H3. 
    intros. assert (U2 := spec_to_Z ccl);omega.
   generalize (spec_ww_add_c (w_W0 ccl) ll);destruct (ww_add_c (w_W0 ccl) ll)
   as [l|l];unfold interp_carry;rewrite spec_w_W0;try rewrite Zmult_1_l;
   simpl zn2z_to_Z;
   try rewrite spec_ww_add;try rewrite spec_ww_add_carry;rewrite spec_w_WW;
   rewrite Zmod_small;rewrite wwB_wBwB;intros.
   rewrite H4;ring. rewrite H;apply mult_add_ineq2;zarith.
   rewrite Zplus_assoc;rewrite Zmult_plus_distr_l.
   rewrite Zmult_1_l;rewrite <- Zplus_assoc;rewrite H4;ring.
   repeat rewrite <- Zplus_assoc;rewrite H;apply mult_add_ineq2;zarith.
  Qed.

  Lemma spec_double_mul_c : forall cross:w->w->w->w->zn2z w -> zn2z w -> w*zn2z w,
     (forall xh xl yh yl hh ll,
        [[hh]] = [|xh|]*[|yh|] ->
        [[ll]] = [|xl|]*[|yl|] ->
        let (wc,cc) :=  cross xh xl yh yl hh ll in 
        [|wc|]*wwB + [[cc]] = [|xh|]*[|yl|] + [|xl|]*[|yh|]) -> 
     forall x y, [||double_mul_c cross x y||] = [[x]] * [[y]].
  Proof.
   intros cross Hcross x y;destruct x as [ |xh xl];simpl;trivial.
   destruct y as [ |yh yl];simpl. rewrite Zmult_0_r;trivial.
   assert (H1:= spec_w_mul_c xh yh);assert (H2:= spec_w_mul_c xl yl).
   generalize (Hcross _ _ _ _ _ _ H1 H2).
   destruct (cross xh xl yh yl (w_mul_c xh yh) (w_mul_c xl yl)) as (wc,cc).
   intros;apply spec_mul_aux;trivial.
   rewrite <- wwB_wBwB;trivial.
  Qed.

  Lemma spec_ww_mul_c : forall x y, [||ww_mul_c x y||] = [[x]] * [[y]]. 
  Proof.
   intros x y;unfold ww_mul_c;apply spec_double_mul_c.
   intros xh xl yh yl hh ll H1 H2.
   generalize (spec_ww_add_c (w_mul_c xh yl) (w_mul_c xl yh));
   destruct (ww_add_c (w_mul_c xh yl) (w_mul_c xl yh)) as [c|c];
   unfold interp_carry;repeat rewrite spec_w_mul_c;intros H;
   (rewrite spec_w_0 || rewrite spec_w_1);rewrite H;ring.
  Qed.

  Lemma spec_w_2: [|w_2|] = 2.
  unfold w_2; rewrite spec_w_add; rewrite spec_w_1; simpl.
  apply Zmod_small; split; auto with zarith.
  rewrite <- (Zpower_1_r 2); unfold base; apply Zpower_lt_monotone; auto with zarith.
  Qed.

  Lemma kara_prod_aux : forall xh xl yh yl,
   xh*yh + xl*yl - (xh-xl)*(yh-yl) = xh*yl + xl*yh.
  Proof. intros;ring. Qed.

  Lemma spec_kara_prod : forall xh xl yh yl hh ll,
   [[hh]] = [|xh|]*[|yh|] ->
   [[ll]] = [|xl|]*[|yl|] ->
   let (wc,cc) := kara_prod xh xl yh yl hh ll in
   [|wc|]*wwB + [[cc]] = [|xh|]*[|yl|] + [|xl|]*[|yh|].
  Proof.
   intros xh xl yh yl hh ll H H0; rewrite <- kara_prod_aux; 
     rewrite <- H; rewrite <- H0; unfold kara_prod.
   assert (Hxh := (spec_to_Z xh)); assert (Hxl := (spec_to_Z xl)); 
     assert (Hyh := (spec_to_Z yh)); assert (Hyl := (spec_to_Z yl)).
   generalize (spec_ww_add_c hh ll); case (ww_add_c hh ll);
     intros z Hz; rewrite <- Hz; unfold interp_carry; assert (Hz1 := (spec_ww_to_Z z)).
   generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh;
    try rewrite Hxlh; try rewrite spec_w_0; try (ring; fail).
   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh.
   rewrite Hylh; rewrite spec_w_0; try (ring; fail).
   rewrite spec_w_0; try (ring; fail). 
   repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   split; auto with zarith.
   simpl in Hz; rewrite Hz; rewrite H; rewrite H0.
   rewrite kara_prod_aux; apply Zplus_le_0_compat; apply Zmult_le_0_compat; auto with zarith.
   apply Zle_lt_trans with ([[z]]-0); auto with zarith.
   unfold Zminus; apply Zplus_le_compat_l; apply Zle_left_rev; simpl; rewrite Zopp_involutive.
   apply Zmult_le_0_compat; auto with zarith.
   match goal with |- context[ww_add_c ?x ?y] =>
     generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_0;
     intros z1 Hz2
   end.
   simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2;
     repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh.
   rewrite Hylh; rewrite spec_w_0; try (ring; fail).
   match goal with |- context[ww_add_c ?x ?y] =>
     generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_0;
     intros z1 Hz2
   end.
   simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2;
     repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   rewrite spec_w_0; try (ring; fail).
   repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   split.
   match goal with |- context[(?x - ?y) * (?z - ?t)] =>
     replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring]
   end.
   simpl in Hz; rewrite Hz; rewrite H; rewrite H0.
   rewrite kara_prod_aux; apply Zplus_le_0_compat; apply Zmult_le_0_compat; auto with zarith.
   apply Zle_lt_trans with ([[z]]-0); auto with zarith.
   unfold Zminus; apply Zplus_le_compat_l; apply Zle_left_rev; simpl; rewrite Zopp_involutive.
   apply Zmult_le_0_compat; auto with zarith.
   (** there is a carry in hh + ll **)
   rewrite Zmult_1_l.
   generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh;
    try rewrite Hxlh; try rewrite spec_w_1; try (ring; fail).
   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
     try rewrite Hylh; try rewrite spec_w_1; try (ring; fail).
   match goal with |- context[ww_sub_c ?x ?y] =>
     generalize (spec_ww_sub_c x y); case (ww_sub_c x y); try rewrite spec_w_1;
     intros z1 Hz2
   end.
   simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   rewrite spec_w_0; rewrite Zmult_0_l; rewrite Zplus_0_l.
   generalize Hz2; clear Hz2; unfold interp_carry.
   repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   match goal with |- context[ww_add_c ?x ?y] =>
     generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_1;
     intros z1 Hz2
   end.
   simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   rewrite spec_w_2; unfold interp_carry in Hz2.
   apply trans_equal with (wwB + (1 * wwB + [[z1]])).
   ring.
   rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
     try rewrite Hylh; try rewrite spec_w_1; try (ring; fail).
   match goal with |- context[ww_add_c ?x ?y] =>
     generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_1;
     intros z1 Hz2
   end.
   simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   rewrite spec_w_2; unfold interp_carry in Hz2.
   apply trans_equal with (wwB + (1 * wwB + [[z1]])).
   ring.
   rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   match goal with |- context[ww_sub_c ?x ?y] =>
     generalize (spec_ww_sub_c x y); case (ww_sub_c x y); try rewrite spec_w_1;
     intros z1 Hz2
   end.
   simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
   rewrite spec_w_0; rewrite Zmult_0_l; rewrite Zplus_0_l.
   match goal with |- context[(?x - ?y) * (?z - ?t)] =>
     replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring]
   end.
   generalize Hz2; clear Hz2; unfold interp_carry.
   repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
   repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
  Qed.

  Lemma sub_carry : forall xh xl yh yl z, 
    0 <= z -> 
    [|xh|]*[|yl|] + [|xl|]*[|yh|] = wwB + z ->
    z < wwB.
  Proof.
   intros xh xl yh yl z Hle Heq.
   destruct (Z_le_gt_dec wwB z);auto with zarith.
   generalize (Zmult_lt_b _ _ _ (spec_to_Z xh) (spec_to_Z yl)).
   generalize (Zmult_lt_b _ _ _ (spec_to_Z xl) (spec_to_Z yh)).
   rewrite <- wwB_wBwB;intros H1 H2.
   assert (H3 := wB_pos w_digits).
   assert (2*wB <= wwB). 
    rewrite wwB_wBwB; rewrite Zpower_2; apply Zmult_le_compat;zarith.
   omega.
  Qed.

  Ltac Spec_ww_to_Z x :=
   let H:= fresh "H" in
   assert (H:= spec_ww_to_Z x).

  Ltac Zmult_lt_b x y := 
   let H := fresh "H" in
   assert (H := Zmult_lt_b _ _ _ (spec_to_Z x) (spec_to_Z y)).

  Lemma spec_ww_karatsuba_c : forall x y, [||ww_karatsuba_c x y||]=[[x]]*[[y]].
  Proof.
   intros x y; unfold ww_karatsuba_c;apply spec_double_mul_c.
   intros; apply spec_kara_prod; auto.
  Qed.

  Lemma spec_ww_mul : forall x y, [[ww_mul x y]] = [[x]]*[[y]] mod wwB.
  Proof.
   assert (U:= lt_0_wB w_digits).
   assert (U1:= lt_0_wwB w_digits).
   intros x y; case x; auto; intros xh xl.
   case y; auto.
   simpl; rewrite Zmult_0_r; rewrite Zmod_small; auto with zarith.
   intros yh yl;simpl.
   repeat (rewrite spec_ww_add || rewrite spec_w_W0 || rewrite spec_w_mul_c
    || rewrite spec_w_add || rewrite spec_w_mul).
   rewrite <- Zplus_mod; auto with zarith.
   repeat (rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r).
   rewrite <- Zmult_mod_distr_r; auto with zarith.
   rewrite <- Zpower_2; rewrite <- wwB_wBwB; auto with zarith.
   rewrite Zplus_mod; auto with zarith.
   rewrite Zmod_mod; auto with zarith.
   rewrite <- Zplus_mod; auto with zarith.
   match goal with |- ?X mod _ = _ =>
     rewrite <- Z_mod_plus with (a := X) (b := [|xh|] * [|yh|])
   end; auto with zarith.
   f_equal; auto; rewrite wwB_wBwB; ring.
  Qed.

  Lemma spec_ww_square_c : forall x, [||ww_square_c x||] = [[x]]*[[x]].
  Proof.
   destruct x as [ |xh xl];simpl;trivial.
   case_eq match ww_add_c (w_mul_c xh xl) (w_mul_c xh xl) with
          | C0 cc => (w_0, cc)
          | C1 cc => (w_1, cc)
          end;intros wc cc Heq.
   apply (spec_mul_aux xh xl xh xl wc cc);trivial.
   generalize Heq (spec_ww_add_c (w_mul_c xh xl) (w_mul_c xh xl));clear Heq.
   rewrite spec_w_mul_c;destruct (ww_add_c (w_mul_c xh xl) (w_mul_c xh xl));
   unfold interp_carry;try rewrite Zmult_1_l;intros Heq Heq';inversion Heq;
   rewrite (Zmult_comm [|xl|]);subst.
   rewrite spec_w_0;rewrite Zmult_0_l;rewrite Zplus_0_l;trivial.
   rewrite spec_w_1;rewrite Zmult_1_l;rewrite <- wwB_wBwB;trivial.
  Qed.

  Section DoubleMulAddn1Proof.

   Variable w_mul_add : w -> w -> w -> w * w.
   Variable spec_w_mul_add : forall x y r,
    let (h,l):= w_mul_add x y r in
    [|h|]*wB+[|l|] = [|x|]*[|y|] + [|r|]. 

   Lemma spec_double_mul_add_n1 : forall n x y r,
     let (h,l) := double_mul_add_n1 w_mul_add n x y r in
     [|h|]*double_wB w_digits n + [!n|l!] = [!n|x!]*[|y|]+[|r|].
   Proof.
    induction n;intros x y r;trivial.
    exact (spec_w_mul_add x y r).
    unfold double_mul_add_n1;destruct x as[ |xh xl]; 
     fold(double_mul_add_n1 w_mul_add).
    rewrite spec_w_0;rewrite spec_extend;simpl;trivial.
    assert(H:=IHn xl y r);destruct (double_mul_add_n1 w_mul_add n xl y r)as(rl,l).
   assert(U:=IHn xh y rl);destruct(double_mul_add_n1 w_mul_add n xh y rl)as(rh,h).
    rewrite <- double_wB_wwB. rewrite spec_double_WW;simpl;trivial.
    rewrite Zmult_plus_distr_l;rewrite <- Zplus_assoc;rewrite <- H.
    rewrite Zmult_assoc;rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l.
    rewrite U;ring.
   Qed. 
 
  End DoubleMulAddn1Proof.

  Lemma spec_w_mul_add : forall x y r, 
    let (h,l):= w_mul_add x y r in
    [|h|]*wB+[|l|] = [|x|]*[|y|] + [|r|]. 
  Proof.
   intros x y r;unfold w_mul_add;assert (H:=spec_w_mul_c x y);
   destruct (w_mul_c x y) as [ |h l];simpl;rewrite <- H.
   rewrite spec_w_0;trivial.
   assert (U:=spec_w_add_c l r);destruct (w_add_c l r) as [lr|lr];unfold
   interp_carry in U;try rewrite Zmult_1_l in H;simpl.
   rewrite U;ring. rewrite spec_w_succ. rewrite Zmod_small.
   rewrite <- Zplus_assoc;rewrite <- U;ring.
   simpl in H;assert (H1:= Zmult_lt_b _ _ _ (spec_to_Z x) (spec_to_Z y)).
   rewrite <- H in H1.
   assert (H2:=spec_to_Z h);split;zarith.
   case H1;clear H1;intro H1;clear H1.
   replace (wB ^ 2 - 2 * wB) with ((wB - 2)*wB). 2:ring.
   intros H0;assert (U1:= wB_pos w_digits).
   assert (H1 := beta_lex _ _ _ _ _ H0 (spec_to_Z l));zarith.
  Qed.

(* End DoubleProof. *)

End DoubleMul.