← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 
9
(************************************************************************)
 
10
 
 
11
(*i $Id: DoubleLift.v 10964 2008-05-22 11:08:13Z letouzey $ i*)
 
12
 
 
13
Set Implicit Arguments.
 
14
 
 
15
Require Import ZArith.
 
16
Require Import BigNumPrelude.
 
17
Require Import DoubleType.
 
18
Require Import DoubleBase.
 
19
 
 
20
Open Local Scope Z_scope.
 
21
 
 
22
Section DoubleLift.
 
23
 Variable w : Type.
 
24
 Variable w_0 : w.
 
25
 Variable w_WW : w -> w -> zn2z w.
 
26
 Variable w_W0 : w ->  zn2z w.
 
27
 Variable w_0W : w ->  zn2z w.
 
28
 Variable w_compare : w -> w -> comparison.
 
29
 Variable ww_compare : zn2z w -> zn2z w -> comparison.
 
30
 Variable w_head0 : w -> w.
 
31
 Variable w_tail0 : w -> w.
 
32
 Variable w_add: w -> w -> zn2z w.
 
33
 Variable w_add_mul_div : w -> w -> w -> w.
 
34
 Variable ww_sub: zn2z w -> zn2z w -> zn2z w.
 
35
 Variable w_digits : positive.
 
36
 Variable ww_Digits : positive.
 
37
 Variable w_zdigits : w.
 
38
 Variable ww_zdigits : zn2z w.
 
39
 Variable low: zn2z w -> w.
 
40
 
 
41
 Definition ww_head0 x :=
 
42
  match x with
 
43
  | W0 => ww_zdigits
 
44
  | WW xh xl =>
 
45
    match w_compare w_0 xh with
 
46
    | Eq => w_add w_zdigits (w_head0 xl)
 
47
    | _ => w_0W (w_head0 xh)
 
48
    end
 
49
  end.
 
50
 
 
51
 
 
52
 Definition ww_tail0 x :=
 
53
  match x with
 
54
  | W0 => ww_zdigits
 
55
  | WW xh xl =>
 
56
    match w_compare w_0 xl with
 
57
    | Eq => w_add w_zdigits (w_tail0 xh)
 
58
    | _ => w_0W (w_tail0 xl)
 
59
    end
 
60
  end.
 
61
 
 
62
 
 
63
  (* 0 < p < ww_digits *)
 
64
 Definition ww_add_mul_div p x y := 
 
65
  let zdigits := w_0W w_zdigits in
 
66
  match x, y with
 
67
  | W0, W0 => W0
 
68
  | W0, WW yh yl =>
 
69
    match ww_compare p zdigits with
 
70
    | Eq => w_0W yh 
 
71
    | Lt => w_0W (w_add_mul_div (low p) w_0 yh)
 
72
    | Gt =>
 
73
      let n := low (ww_sub p zdigits) in
 
74
      w_WW (w_add_mul_div n w_0 yh) (w_add_mul_div n yh yl)
 
75
    end
 
76
  | WW xh xl, W0 =>
 
77
    match ww_compare p zdigits with
 
78
    | Eq => w_W0 xl 
 
79
    | Lt => w_WW (w_add_mul_div (low p) xh xl) (w_add_mul_div (low p) xl w_0)
 
80
    | Gt =>
 
81
      let n := low (ww_sub p zdigits) in
 
82
      w_W0 (w_add_mul_div n xl w_0) 
 
83
    end
 
84
  | WW xh xl, WW yh yl =>
 
85
    match ww_compare p zdigits with
 
86
    | Eq => w_WW xl yh 
 
87
    | Lt => w_WW (w_add_mul_div (low p) xh xl) (w_add_mul_div (low p) xl yh)
 
88
    | Gt =>
 
89
      let n := low (ww_sub p zdigits) in
 
90
      w_WW (w_add_mul_div n xl yh) (w_add_mul_div n yh yl)
 
91
    end
 
92
  end.
 
93
 
 
94
 Section DoubleProof.
 
95
  Variable w_to_Z : w -> Z.
 
96
 
 
97
  Notation wB  := (base w_digits).
 
98
  Notation wwB := (base (ww_digits w_digits)).
 
99
  Notation "[| x |]" := (w_to_Z x)  (at level 0, x at level 99).
 
100
  Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
 
101
 
 
102
  Variable spec_w_0   : [|w_0|] = 0.
 
103
  Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.
 
104
  Variable spec_to_w_Z  : forall x, 0 <= [[x]] < wwB.
 
105
  Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
 
106
  Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB.
 
107
  Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
 
108
  Variable spec_compare : forall x y,
 
109
       match w_compare x y with
 
110
       | Eq => [|x|] = [|y|]
 
111
       | Lt => [|x|] < [|y|]
 
112
       | Gt => [|x|] > [|y|]
 
113
       end.
 
114
  Variable spec_ww_compare : forall x y,
 
115
       match ww_compare x y with
 
116
       | Eq => [[x]] = [[y]]
 
117
       | Lt => [[x]] < [[y]]
 
118
       | Gt => [[x]] > [[y]]
 
119
       end.
 
120
  Variable spec_ww_digits : ww_Digits = xO w_digits.
 
121
  Variable spec_w_head00  : forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_digits.
 
122
  Variable spec_w_head0  : forall x,  0 < [|x|] ->
 
123
         wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB.
 
124
  Variable spec_w_tail00  : forall x, [|x|] = 0 -> [|w_tail0 x|] = Zpos w_digits.
 
125
  Variable spec_w_tail0 : forall x, 0 < [|x|] -> 
 
126
         exists y, 0 <= y /\ [|x|] = (2* y + 1) * (2 ^ [|w_tail0 x|]).
 
127
  Variable spec_w_add_mul_div : forall x y p,
 
128
       [|p|] <= Zpos w_digits ->
 
129
       [| w_add_mul_div p x y |] =
 
130
         ([|x|] * (2 ^ [|p|]) +
 
131
          [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB.
 
132
 Variable spec_w_add: forall x y, 
 
133
   [[w_add x y]] = [|x|] + [|y|].
 
134
 Variable spec_ww_sub: forall x y, 
 
135
   [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB.
 
136
 
 
137
 Variable spec_zdigits : [| w_zdigits |] = Zpos w_digits.
 
138
 Variable spec_low: forall x, [| low x|] = [[x]] mod wB.
 
139
 
 
140
 Variable spec_ww_zdigits : [[ww_zdigits]] = Zpos ww_Digits.
 
141
 
 
142
  Hint Resolve div_le_0 div_lt w_to_Z_wwB: lift.
 
143
  Ltac zarith := auto with zarith lift.
 
144
 
 
145
  Lemma spec_ww_head00  : forall x, [[x]] = 0 -> [[ww_head0 x]] = Zpos ww_Digits.
 
146
  Proof.
 
147
  intros x; case x; unfold ww_head0.
 
148
    intros HH; rewrite spec_ww_zdigits; auto.
 
149
  intros xh xl; simpl; intros Hx.
 
150
  case (spec_to_Z xh); intros Hx1 Hx2.
 
151
  case (spec_to_Z xl); intros Hy1 Hy2.
 
152
  assert (F1: [|xh|] = 0).
 
153
    case (Zle_lt_or_eq _ _ Hy1); auto; intros Hy3.
 
154
    absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith.
 
155
    apply Zlt_le_trans with (1 := Hy3); auto with zarith.
 
156
    pattern [|xl|] at 1; rewrite <- (Zplus_0_l [|xl|]).
 
157
    apply Zplus_le_compat_r; auto with zarith.
 
158
    case (Zle_lt_or_eq _ _ Hx1); auto; intros Hx3.
 
159
    absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith.
 
160
    rewrite <- Hy3; rewrite Zplus_0_r; auto with zarith.
 
161
    apply Zmult_lt_0_compat; auto with zarith.
 
162
  generalize (spec_compare w_0 xh); case w_compare.
 
163
    intros H; simpl.
 
164
    rewrite spec_w_add; rewrite spec_w_head00.
 
165
    rewrite spec_zdigits; rewrite spec_ww_digits.
 
166
    rewrite Zpos_xO; auto with zarith.
 
167
  rewrite F1 in Hx; auto with zarith.
 
168
  rewrite spec_w_0; auto with zarith.
 
169
  rewrite spec_w_0; auto with zarith.
 
170
  Qed.
 
171
   
 
172
  Lemma spec_ww_head0  : forall x,  0 < [[x]] ->
 
173
         wwB/ 2 <= 2 ^ [[ww_head0 x]] * [[x]] < wwB.
 
174
  Proof.
 
175
   clear spec_ww_zdigits.
 
176
   rewrite wwB_div_2;rewrite Zmult_comm;rewrite wwB_wBwB.
 
177
   assert (U:= lt_0_wB w_digits); destruct x as [ |xh xl];simpl ww_to_Z;intros H.
 
178
   unfold Zlt in H;discriminate H.
 
179
   assert (H0 := spec_compare w_0 xh);rewrite spec_w_0 in H0.
 
180
   destruct (w_compare w_0 xh).
 
181
   rewrite <- H0. simpl Zplus. rewrite <- H0 in H;simpl in H.
 
182
   case (spec_to_Z w_zdigits); 
 
183
     case (spec_to_Z (w_head0 xl)); intros HH1 HH2 HH3 HH4.
 
184
   rewrite spec_w_add.
 
185
   rewrite spec_zdigits; rewrite Zpower_exp; auto with zarith.
 
186
   case (spec_w_head0 H); intros H1 H2.
 
187
   rewrite Zpower_2; fold wB; rewrite <- Zmult_assoc; split.
 
188
     apply Zmult_le_compat_l; auto with zarith.
 
189
   apply Zmult_lt_compat_l; auto with zarith.
 
190
   assert (H1 := spec_w_head0 H0).
 
191
   rewrite spec_w_0W.
 
192
   split.
 
193
   rewrite Zmult_plus_distr_r;rewrite Zmult_assoc.
 
194
   apply Zle_trans with (2 ^ [|w_head0 xh|] * [|xh|] * wB).
 
195
   rewrite Zmult_comm; zarith.
 
196
   assert (0 <= 2 ^ [|w_head0 xh|] * [|xl|]);zarith.
 
197
   assert (H2:=spec_to_Z xl);apply Zmult_le_0_compat;zarith.
 
198
   case (spec_to_Z (w_head0 xh)); intros H2 _.
 
199
   generalize ([|w_head0 xh|]) H1 H2;clear H1 H2;
 
200
     intros p H1 H2.
 
201
   assert (Eq1 : 2^p < wB).
 
202
     rewrite <- (Zmult_1_r (2^p));apply Zle_lt_trans with (2^p*[|xh|]);zarith.
 
203
   assert (Eq2: p < Zpos w_digits).
 
204
    destruct (Zle_or_lt (Zpos w_digits) p);trivial;contradict  Eq1.
 
205
   apply Zle_not_lt;unfold base;apply Zpower_le_monotone;zarith.
 
206
   assert (Zpos w_digits = p + (Zpos w_digits - p)). ring.
 
207
   rewrite Zpower_2.
 
208
   unfold base at 2;rewrite H3;rewrite Zpower_exp;zarith.
 
209
   rewrite <- Zmult_assoc; apply Zmult_lt_compat_l; zarith.
 
210
   rewrite <- (Zplus_0_r (2^(Zpos w_digits - p)*wB));apply beta_lex_inv;zarith.
 
211
   apply Zmult_lt_reg_r with (2 ^ p); zarith.
 
212
   rewrite <- Zpower_exp;zarith. 
 
213
   rewrite Zmult_comm;ring_simplify (Zpos w_digits - p + p);fold wB;zarith.
 
214
   assert (H1 := spec_to_Z xh);zarith.
 
215
  Qed.
 
216
 
 
217
  Lemma spec_ww_tail00  : forall x, [[x]] = 0 -> [[ww_tail0 x]] = Zpos ww_Digits.
 
218
  Proof.
 
219
  intros x; case x; unfold ww_tail0.
 
220
    intros HH; rewrite spec_ww_zdigits; auto.
 
221
  intros xh xl; simpl; intros Hx.
 
222
  case (spec_to_Z xh); intros Hx1 Hx2.
 
223
  case (spec_to_Z xl); intros Hy1 Hy2.
 
224
  assert (F1: [|xh|] = 0).
 
225
    case (Zle_lt_or_eq _ _ Hy1); auto; intros Hy3.
 
226
    absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith.
 
227
    apply Zlt_le_trans with (1 := Hy3); auto with zarith.
 
228
    pattern [|xl|] at 1; rewrite <- (Zplus_0_l [|xl|]).
 
229
    apply Zplus_le_compat_r; auto with zarith.
 
230
    case (Zle_lt_or_eq _ _ Hx1); auto; intros Hx3.
 
231
    absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith.
 
232
    rewrite <- Hy3; rewrite Zplus_0_r; auto with zarith.
 
233
    apply Zmult_lt_0_compat; auto with zarith.
 
234
  assert (F2: [|xl|] = 0).
 
235
    rewrite F1 in Hx; auto with zarith.
 
236
  generalize (spec_compare w_0 xl); case w_compare.
 
237
    intros H; simpl.
 
238
    rewrite spec_w_add; rewrite spec_w_tail00; auto.
 
239
    rewrite spec_zdigits; rewrite spec_ww_digits.
 
240
    rewrite Zpos_xO; auto with zarith.
 
241
  rewrite spec_w_0; auto with zarith.
 
242
  rewrite spec_w_0; auto with zarith.
 
243
  Qed.
 
244
 
 
245
  Lemma spec_ww_tail0  : forall x,  0 < [[x]] ->
 
246
         exists y, 0 <= y /\ [[x]] = (2 * y + 1) * 2 ^ [[ww_tail0 x]].
 
247
  Proof.
 
248
   clear spec_ww_zdigits.
 
249
   destruct x as [ |xh xl];simpl ww_to_Z;intros H.
 
250
   unfold Zlt in H;discriminate H.
 
251
   assert (H0 := spec_compare w_0 xl);rewrite spec_w_0 in H0.
 
252
   destruct (w_compare w_0 xl).
 
253
   rewrite <- H0; rewrite Zplus_0_r.
 
254
   case (spec_to_Z (w_tail0 xh)); intros HH1 HH2.
 
255
   generalize H; rewrite <- H0; rewrite Zplus_0_r; clear H; intros H.
 
256
   case (@spec_w_tail0 xh).
 
257
     apply Zmult_lt_reg_r with wB; auto with zarith.
 
258
     unfold base; auto with zarith.
 
259
   intros z (Hz1, Hz2); exists z; split; auto.
 
260
   rewrite spec_w_add; rewrite (fun x => Zplus_comm [|x|]).
 
261
   rewrite spec_zdigits; rewrite Zpower_exp; auto with zarith.
 
262
   rewrite Zmult_assoc; rewrite <- Hz2; auto.
 
263
 
 
264
   case (spec_to_Z (w_tail0 xh)); intros HH1 HH2.
 
265
   case (spec_w_tail0 H0); intros z (Hz1, Hz2).
 
266
   assert (Hp: [|w_tail0 xl|] < Zpos w_digits).
 
267
     case (Zle_or_lt (Zpos w_digits) [|w_tail0 xl|]); auto; intros H1.
 
268
     absurd (2 ^  (Zpos w_digits) <= 2 ^ [|w_tail0 xl|]).
 
269
       apply Zlt_not_le.
 
270
       case (spec_to_Z xl); intros HH3 HH4.
 
271
       apply Zle_lt_trans with (2 := HH4).
 
272
       apply Zle_trans with (1 * 2 ^ [|w_tail0 xl|]); auto with zarith.
 
273
       rewrite Hz2.
 
274
       apply Zmult_le_compat_r; auto with zarith.
 
275
     apply Zpower_le_monotone; auto with zarith.
 
276
   exists ([|xh|] * (2 ^ ((Zpos w_digits - [|w_tail0 xl|]) - 1)) + z); split.
 
277
     apply Zplus_le_0_compat; auto.
 
278
     apply Zmult_le_0_compat; auto with zarith.
 
279
     case (spec_to_Z xh); auto.
 
280
   rewrite spec_w_0W.
 
281
   rewrite (Zmult_plus_distr_r 2); rewrite <- Zplus_assoc.
 
282
   rewrite Zmult_plus_distr_l; rewrite <- Hz2.
 
283
   apply f_equal2 with (f := Zplus); auto.
 
284
   rewrite (Zmult_comm 2).
 
285
   repeat rewrite <- Zmult_assoc.
 
286
   apply f_equal2 with (f := Zmult); auto.
 
287
   case (spec_to_Z (w_tail0 xl)); intros HH3 HH4.
 
288
   pattern 2 at 2; rewrite <- Zpower_1_r.
 
289
   lazy beta; repeat rewrite <- Zpower_exp; auto with zarith.
 
290
   unfold base; apply f_equal with (f := Zpower 2); auto with zarith.
 
291
 
 
292
   contradict H0; case (spec_to_Z xl); auto with zarith.
 
293
  Qed.
 
294
 
 
295
  Hint Rewrite Zdiv_0_l Zmult_0_l Zplus_0_l Zmult_0_r Zplus_0_r
 
296
    spec_w_W0 spec_w_0W spec_w_WW spec_w_0  
 
297
    (wB_div w_digits w_to_Z spec_to_Z) 
 
298
    (wB_div_plus w_digits w_to_Z spec_to_Z) : w_rewrite.
 
299
  Ltac w_rewrite := autorewrite with w_rewrite;trivial.
 
300
 
 
301
  Lemma spec_ww_add_mul_div_aux : forall xh xl yh yl p,
 
302
   let zdigits := w_0W w_zdigits in
 
303
    [[p]] <= Zpos (xO w_digits) ->
 
304
      [[match ww_compare p zdigits with
 
305
        | Eq => w_WW xl yh
 
306
        | Lt => w_WW (w_add_mul_div (low p) xh xl) 
 
307
                     (w_add_mul_div (low p) xl yh)
 
308
        | Gt =>
 
309
              let n := low (ww_sub p zdigits) in
 
310
            w_WW (w_add_mul_div n xl yh) (w_add_mul_div n yh yl)
 
311
        end]] =  
 
312
      ([[WW xh xl]] * (2^[[p]]) +
 
313
       [[WW yh yl]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB.
 
314
  Proof.
 
315
   clear spec_ww_zdigits.
 
316
   intros xh xl yh yl p zdigits;assert (HwwB := wwB_pos w_digits).
 
317
   case (spec_to_w_Z p); intros Hv1 Hv2.
 
318
   replace (Zpos (xO w_digits)) with (Zpos w_digits + Zpos w_digits).
 
319
   2 : rewrite Zpos_xO;ring.
 
320
   replace (Zpos w_digits + Zpos w_digits - [[p]]) with 
 
321
     (Zpos w_digits + (Zpos w_digits - [[p]])). 2:ring.
 
322
   intros Hp; assert (Hxh := spec_to_Z xh);assert (Hxl:=spec_to_Z xl);
 
323
   assert (Hx := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl));
 
324
   simpl in Hx;assert (Hyh := spec_to_Z yh);assert (Hyl:=spec_to_Z yl);
 
325
   assert (Hy:=spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW yh yl));simpl in Hy.
 
326
   generalize (spec_ww_compare p zdigits); case ww_compare; intros H1.
 
327
   rewrite H1; unfold zdigits; rewrite spec_w_0W.
 
328
   rewrite spec_zdigits; rewrite Zminus_diag; rewrite Zplus_0_r.
 
329
   simpl ww_to_Z; w_rewrite;zarith.
 
330
   fold wB.
 
331
   rewrite Zmult_plus_distr_l;rewrite <- Zmult_assoc;rewrite <- Zplus_assoc.
 
332
   rewrite <- Zpower_2.
 
333
   rewrite <- wwB_wBwB;apply Zmod_unique with [|xh|]. 
 
334
   exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xl yh)). ring.
 
335
   simpl ww_to_Z; w_rewrite;zarith.
 
336
   assert (HH0: [|low p|] = [[p]]).
 
337
     rewrite spec_low.
 
338
     apply Zmod_small.
 
339
     case (spec_to_w_Z p); intros HH1 HH2; split; auto.
 
340
     generalize H1; unfold zdigits; rewrite spec_w_0W;
 
341
      rewrite spec_zdigits; intros tmp.
 
342
     apply Zlt_le_trans with (1 := tmp).
 
343
     unfold base.
 
344
     apply Zpower2_le_lin; auto with zarith.
 
345
   2: generalize H1; unfold zdigits; rewrite spec_w_0W;
 
346
      rewrite spec_zdigits; auto with zarith.
 
347
   generalize H1; unfold zdigits; rewrite spec_w_0W;
 
348
      rewrite spec_zdigits; auto; clear H1; intros H1.
 
349
   assert (HH: [|low p|] <= Zpos w_digits).
 
350
     rewrite HH0; auto with zarith.
 
351
   repeat rewrite spec_w_add_mul_div with (1 := HH).
 
352
   rewrite HH0.
 
353
   rewrite Zmult_plus_distr_l.
 
354
   pattern ([|xl|] * 2 ^ [[p]]) at 2;
 
355
   rewrite shift_unshift_mod with (n:= Zpos w_digits);fold wB;zarith.
 
356
   replace ([|xh|] * wB * 2^[[p]]) with ([|xh|] * 2^[[p]] * wB). 2:ring. 
 
357
   rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. rewrite <- Zplus_assoc.
 
358
   unfold base at 5;rewrite <- Zmod_shift_r;zarith.
 
359
   unfold base;rewrite Zmod_shift_r with (b:= Zpos (ww_digits w_digits));
 
360
   fold wB;fold wwB;zarith.
 
361
   rewrite wwB_wBwB;rewrite Zpower_2; rewrite  Zmult_mod_distr_r;zarith.
 
362
   unfold ww_digits;rewrite Zpos_xO;zarith. apply Z_mod_lt;zarith.
 
363
   split;zarith. apply Zdiv_lt_upper_bound;zarith.
 
364
   rewrite <- Zpower_exp;zarith.
 
365
   ring_simplify ([[p]] + (Zpos w_digits - [[p]]));fold wB;zarith.
 
366
   assert (Hv: [[p]] > Zpos w_digits).
 
367
     generalize H1; clear H1.
 
368
     unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto.
 
369
   clear H1.
 
370
   assert (HH0: [|low (ww_sub p zdigits)|] = [[p]] - Zpos w_digits).
 
371
     rewrite spec_low.
 
372
     rewrite spec_ww_sub.
 
373
     unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits.
 
374
     rewrite <- Zmod_div_mod; auto with zarith.
 
375
     rewrite Zmod_small; auto with zarith.
 
376
     split; auto with zarith.
 
377
     apply Zle_lt_trans with (Zpos w_digits); auto with zarith.
 
378
     unfold base; apply Zpower2_lt_lin; auto with zarith.
 
379
     exists wB; unfold base.
 
380
     unfold ww_digits; rewrite (Zpos_xO w_digits).
 
381
     rewrite <- Zpower_exp; auto with zarith.
 
382
     apply f_equal with (f := fun x => 2 ^ x); auto with zarith.
 
383
   assert (HH: [|low (ww_sub p zdigits)|] <= Zpos w_digits).
 
384
     rewrite HH0; auto with zarith.
 
385
   replace (Zpos w_digits + (Zpos w_digits - [[p]])) with
 
386
       (Zpos w_digits - ([[p]] - Zpos w_digits)); zarith.
 
387
   lazy zeta; simpl ww_to_Z; w_rewrite;zarith.
 
388
   repeat rewrite spec_w_add_mul_div;zarith.
 
389
   rewrite HH0.
 
390
   pattern wB at 5;replace wB with 
 
391
    (2^(([[p]] - Zpos w_digits) 
 
392
         + (Zpos w_digits - ([[p]] - Zpos w_digits)))).
 
393
   rewrite Zpower_exp;zarith. rewrite Zmult_assoc.
 
394
   rewrite Z_div_plus_l;zarith.
 
395
   rewrite shift_unshift_mod with (a:= [|yh|]) (p:= [[p]] - Zpos w_digits)
 
396
    (n := Zpos w_digits);zarith. fold wB.
 
397
   set (u := [[p]] - Zpos w_digits).
 
398
   replace [[p]] with (u + Zpos w_digits);zarith.
 
399
   rewrite Zpower_exp;zarith. rewrite Zmult_assoc. fold wB.
 
400
   repeat rewrite Zplus_assoc. rewrite <- Zmult_plus_distr_l.
 
401
   repeat rewrite <- Zplus_assoc.
 
402
   unfold base;rewrite Zmod_shift_r with (b:= Zpos (ww_digits w_digits));
 
403
   fold wB;fold wwB;zarith.
 
404
   unfold base;rewrite Zmod_shift_r with (a:= Zpos w_digits) 
 
405
   (b:= Zpos w_digits);fold wB;fold wwB;zarith.
 
406
   rewrite wwB_wBwB; rewrite Zpower_2; rewrite  Zmult_mod_distr_r;zarith.
 
407
   rewrite Zmult_plus_distr_l.
 
408
   replace ([|xh|] * wB * 2 ^ u) with 
 
409
     ([|xh|]*2^u*wB). 2:ring.
 
410
   repeat rewrite <- Zplus_assoc. 
 
411
   rewrite (Zplus_comm ([|xh|] * 2 ^ u * wB)).
 
412
   rewrite Z_mod_plus;zarith. rewrite Z_mod_mult;zarith.
 
413
   unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith.
 
414
   unfold u; split;zarith. 
 
415
   split;zarith. unfold u; apply Zdiv_lt_upper_bound;zarith.
 
416
   rewrite <- Zpower_exp;zarith.
 
417
   fold u. 
 
418
   ring_simplify (u + (Zpos w_digits - u)); fold 
 
419
   wB;zarith. unfold ww_digits;rewrite Zpos_xO;zarith.
 
420
   unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith.
 
421
   unfold u; split;zarith.
 
422
   unfold u; split;zarith.
 
423
   apply Zdiv_lt_upper_bound;zarith.
 
424
   rewrite <- Zpower_exp;zarith.
 
425
   fold u. 
 
426
   ring_simplify (u + (Zpos w_digits - u)); fold wB; auto with zarith.
 
427
   unfold u;zarith.
 
428
   unfold u;zarith.
 
429
   set (u := [[p]] - Zpos w_digits).
 
430
   ring_simplify (u + (Zpos w_digits - u)); fold wB; auto with zarith.
 
431
  Qed.
 
432
 
 
433
  Lemma spec_ww_add_mul_div : forall x y p,
 
434
       [[p]] <= Zpos (xO w_digits) ->
 
435
       [[ ww_add_mul_div p x y ]] =
 
436
         ([[x]] * (2^[[p]]) +
 
437
          [[y]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB.
 
438
  Proof.
 
439
   clear spec_ww_zdigits.
 
440
   intros x y p H.
 
441
   destruct x as [ |xh xl];
 
442
   [assert (H1 := @spec_ww_add_mul_div_aux w_0 w_0)
 
443
   |assert (H1 := @spec_ww_add_mul_div_aux xh xl)];
 
444
   (destruct y as [ |yh yl];
 
445
    [generalize (H1 w_0 w_0 p H) | generalize (H1 yh yl p H)];
 
446
    clear H1;w_rewrite);simpl ww_add_mul_div.
 
447
   replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial].
 
448
   intros Heq;rewrite <- Heq;clear Heq; auto.
 
449
   generalize (spec_ww_compare p (w_0W w_zdigits)); 
 
450
     case ww_compare; intros H1; w_rewrite.
 
451
   rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith.
 
452
   generalize H1; w_rewrite; rewrite spec_zdigits; clear H1; intros H1.
 
453
   assert (HH0: [|low p|] = [[p]]).
 
454
     rewrite spec_low.
 
455
     apply Zmod_small.
 
456
     case (spec_to_w_Z p); intros HH1 HH2; split; auto.
 
457
     apply Zlt_le_trans with (1 := H1).
 
458
     unfold base; apply Zpower2_le_lin; auto with zarith.
 
459
   rewrite HH0; auto with zarith.
 
460
   replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial].
 
461
   intros Heq;rewrite <- Heq;clear Heq.
 
462
   generalize (spec_ww_compare p (w_0W w_zdigits)); 
 
463
     case ww_compare; intros H1; w_rewrite.
 
464
   rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith.
 
465
   rewrite Zpos_xO in H;zarith.
 
466
   assert (HH: [|low (ww_sub p (w_0W w_zdigits)) |] = [[p]] - Zpos w_digits).
 
467
     generalize H1; clear H1.
 
468
     rewrite spec_low.
 
469
     rewrite spec_ww_sub; w_rewrite; intros H1.
 
470
     rewrite <- Zmod_div_mod; auto with zarith.
 
471
     rewrite Zmod_small; auto with zarith.
 
472
     split; auto with zarith.
 
473
     apply Zle_lt_trans with (Zpos w_digits); auto with zarith.
 
474
     unfold base; apply Zpower2_lt_lin; auto with zarith.
 
475
     unfold base; auto with zarith.
 
476
     unfold base; auto with zarith.
 
477
     exists wB; unfold base.
 
478
     unfold ww_digits; rewrite (Zpos_xO w_digits).
 
479
     rewrite <- Zpower_exp; auto with zarith.
 
480
     apply f_equal with (f := fun x => 2 ^ x); auto with zarith.
 
481
  case (spec_to_Z xh); auto with zarith.
 
482
  Qed.
 
483
 
 
484
 End DoubleProof.
 
485
 
 
486
End DoubleLift.
 
487