← 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/DoubleAdd.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/DoubleAdd.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: DoubleAdd.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 DoubleAdd.
 
23
 Variable w : Type.
 
24
 Variable w_0 : w.
 
25
 Variable w_1 : w.
 
26
 Variable w_WW : w -> w -> zn2z w.
 
27
 Variable w_W0 : w -> zn2z w.
 
28
 Variable ww_1 : zn2z w.
 
29
 Variable w_succ_c : w -> carry w.
 
30
 Variable w_add_c : w -> w -> carry w.
 
31
 Variable w_add_carry_c : w -> w -> carry w.
 
32
 Variable w_succ : w -> w.
 
33
 Variable w_add : w -> w -> w.
 
34
 Variable w_add_carry : w -> w -> w.
 
35
 
 
36
 Definition ww_succ_c x :=
 
37
  match x with
 
38
  | W0 => C0 ww_1
 
39
  | WW xh xl => 
 
40
    match w_succ_c xl with
 
41
    | C0 l => C0 (WW xh l)
 
42
    | C1 l => 
 
43
      match w_succ_c xh with
 
44
      | C0 h => C0 (WW h w_0)
 
45
      | C1 h => C1 W0
 
46
      end
 
47
    end
 
48
  end.
 
49
 
 
50
 Definition ww_succ x := 
 
51
  match x with
 
52
  | W0 => ww_1
 
53
  | WW xh xl =>
 
54
    match w_succ_c xl with
 
55
    | C0 l => WW xh l
 
56
    | C1 l => w_W0 (w_succ xh) 
 
57
    end
 
58
  end.
 
59
 
 
60
 Definition ww_add_c x y :=
 
61
  match x, y with
 
62
  | W0, _ => C0 y
 
63
  | _, W0 => C0 x
 
64
  | WW xh xl, WW yh yl =>
 
65
    match w_add_c xl yl with
 
66
    | C0 l => 
 
67
      match w_add_c xh yh with
 
68
      | C0 h => C0 (WW h l)
 
69
      | C1 h => C1 (w_WW h l)
 
70
      end 
 
71
    | C1 l => 
 
72
      match w_add_carry_c xh yh with
 
73
      | C0 h => C0 (WW h l)
 
74
      | C1 h => C1 (w_WW h l)
 
75
      end
 
76
    end
 
77
  end.
 
78
 
 
79
 Variable R : Type.
 
80
 Variable f0 f1 : zn2z w -> R.
 
81
 
 
82
 Definition ww_add_c_cont x y :=
 
83
  match x, y with
 
84
  | W0, _ => f0 y
 
85
  | _, W0 => f0 x
 
86
  | WW xh xl, WW yh yl =>
 
87
    match w_add_c xl yl with
 
88
    | C0 l => 
 
89
      match w_add_c xh yh with
 
90
      | C0 h => f0 (WW h l)
 
91
      | C1 h => f1 (w_WW h l)
 
92
      end 
 
93
    | C1 l => 
 
94
      match w_add_carry_c xh yh with
 
95
      | C0 h => f0 (WW h l)
 
96
      | C1 h => f1 (w_WW h l)
 
97
      end
 
98
    end
 
99
  end.
 
100
 
 
101
 (* ww_add et ww_add_carry conserve la forme normale s'il n'y a pas
 
102
    de debordement *)
 
103
 Definition ww_add x y :=
 
104
  match x, y with
 
105
  | W0, _ => y
 
106
  | _, W0 => x
 
107
  | WW xh xl, WW yh yl =>
 
108
    match w_add_c xl yl with
 
109
    | C0 l => WW (w_add xh yh) l
 
110
    | C1 l => WW (w_add_carry xh yh) l
 
111
    end
 
112
  end.
 
113
 
 
114
 Definition ww_add_carry_c x y :=
 
115
  match x, y with
 
116
  | W0, W0 => C0 ww_1
 
117
  | W0, WW yh yl => ww_succ_c (WW yh yl)
 
118
  | WW xh xl, W0 => ww_succ_c (WW xh xl)
 
119
  | WW xh xl, WW yh yl =>
 
120
    match w_add_carry_c xl yl with
 
121
    | C0 l => 
 
122
      match w_add_c xh yh with
 
123
      | C0 h => C0 (WW h l)
 
124
      | C1 h => C1 (WW h l)
 
125
      end
 
126
    | C1 l => 
 
127
      match w_add_carry_c xh yh with
 
128
      | C0 h => C0 (WW h l)
 
129
      | C1 h => C1 (w_WW h l)
 
130
      end
 
131
    end
 
132
  end.
 
133
 
 
134
 Definition ww_add_carry x y := 
 
135
  match x, y with
 
136
  | W0, W0 => ww_1
 
137
  | W0, WW yh yl => ww_succ (WW yh yl)
 
138
  | WW xh xl, W0 => ww_succ (WW xh xl)
 
139
  | WW xh xl, WW yh yl =>
 
140
    match w_add_carry_c xl yl with
 
141
    | C0 l => WW (w_add xh yh) l
 
142
    | C1 l => WW (w_add_carry xh yh) l
 
143
    end
 
144
  end.
 
145
 
 
146
 (*Section DoubleProof.*)
 
147
  Variable w_digits : positive.
 
148
  Variable w_to_Z : w -> Z.
 
149
 
 
150
 
 
151
  Notation wB  := (base w_digits).
 
152
  Notation wwB := (base (ww_digits w_digits)).
 
153
  Notation "[| x |]" := (w_to_Z x)  (at level 0, x at level 99).
 
154
  Notation "[+| c |]" :=
 
155
   (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99).
 
156
  Notation "[-| c |]" :=
 
157
   (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99).
 
158
 
 
159
  Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
 
160
  Notation "[+[ c ]]" := 
 
161
   (interp_carry 1 wwB (ww_to_Z w_digits w_to_Z) c) 
 
162
   (at level 0, x at level 99).
 
163
  Notation "[-[ c ]]" := 
 
164
   (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) 
 
165
   (at level 0, x at level 99).
 
166
 
 
167
  Variable spec_w_0   : [|w_0|] = 0.
 
168
  Variable spec_w_1   : [|w_1|] = 1.
 
169
  Variable spec_ww_1   : [[ww_1]] = 1.
 
170
  Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.
 
171
  Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
 
172
  Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB.
 
173
  Variable spec_w_succ_c : forall x, [+|w_succ_c x|] = [|x|] + 1.
 
174
  Variable spec_w_add_c  : forall x y, [+|w_add_c x y|] = [|x|] + [|y|].
 
175
  Variable spec_w_add_carry_c : 
 
176
         forall x y, [+|w_add_carry_c x y|] = [|x|] + [|y|] + 1.
 
177
  Variable spec_w_succ : forall x, [|w_succ x|] = ([|x|] + 1) mod wB.
 
178
  Variable spec_w_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB.
 
179
  Variable spec_w_add_carry :
 
180
         forall x y, [|w_add_carry x y|] = ([|x|] + [|y|] + 1) mod wB.
 
181
 
 
182
  Lemma spec_ww_succ_c : forall x, [+[ww_succ_c x]] = [[x]] + 1.
 
183
  Proof.
 
184
   destruct x as [ |xh xl];simpl. apply spec_ww_1.
 
185
   generalize (spec_w_succ_c xl);destruct (w_succ_c xl) as [l|l];
 
186
    intro H;unfold interp_carry in H. simpl;rewrite H;ring.
 
187
   rewrite <- Zplus_assoc;rewrite <- H;rewrite Zmult_1_l.
 
188
   assert ([|l|] = 0). generalize (spec_to_Z xl)(spec_to_Z l);omega.
 
189
   rewrite H0;generalize (spec_w_succ_c xh);destruct (w_succ_c xh) as [h|h];
 
190
    intro H1;unfold interp_carry in H1. 
 
191
   simpl;rewrite H1;rewrite spec_w_0;ring.
 
192
   unfold interp_carry;simpl ww_to_Z;rewrite wwB_wBwB.
 
193
   assert ([|xh|] = wB - 1). generalize (spec_to_Z xh)(spec_to_Z h);omega.
 
194
   rewrite H2;ring. 
 
195
  Qed.
 
196
 
 
197
  Lemma spec_ww_add_c  : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]].
 
198
  Proof.
 
199
   destruct x as [ |xh xl];simpl;trivial.
 
200
   destruct y as [ |yh yl];simpl. rewrite Zplus_0_r;trivial.
 
201
   replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]))
 
202
   with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|])). 2:ring.
 
203
   generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l];
 
204
    intros H;unfold interp_carry in H;rewrite <- H.
 
205
   generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h];
 
206
    intros H1;unfold interp_carry in *;rewrite <- H1. trivial.
 
207
   repeat rewrite Zmult_1_l;rewrite spec_w_WW;rewrite wwB_wBwB; ring.
 
208
   rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l.
 
209
   generalize (spec_w_add_carry_c xh yh);destruct (w_add_carry_c xh yh)
 
210
    as [h|h]; intros H1;unfold interp_carry in *;rewrite <- H1.
 
211
   simpl;ring.
 
212
   repeat rewrite Zmult_1_l;rewrite wwB_wBwB;rewrite spec_w_WW;ring.
 
213
  Qed.
 
214
 
 
215
  Section Cont.
 
216
   Variable P : zn2z w -> zn2z w -> R -> Prop.
 
217
   Variable x y : zn2z w.
 
218
   Variable spec_f0 : forall r, [[r]] = [[x]] + [[y]] -> P x y (f0 r).
 
219
   Variable spec_f1 : forall r, wwB + [[r]] = [[x]] + [[y]] -> P x y (f1 r).
 
220
 
 
221
   Lemma spec_ww_add_c_cont  : P x y (ww_add_c_cont x y).
 
222
   Proof.
 
223
    destruct x as [ |xh xl];simpl;trivial.
 
224
    apply spec_f0;trivial.
 
225
    destruct y as [ |yh yl];simpl. 
 
226
    apply spec_f0;simpl;rewrite Zplus_0_r;trivial.
 
227
    generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l];
 
228
     intros H;unfold interp_carry in H.
 
229
    generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h];
 
230
     intros H1;unfold interp_carry in *. 
 
231
    apply spec_f0. simpl;rewrite H;rewrite H1;ring.
 
232
    apply spec_f1. simpl;rewrite spec_w_WW;rewrite H.
 
233
    rewrite Zplus_assoc;rewrite wwB_wBwB. rewrite Zpower_2; rewrite <- Zmult_plus_distr_l.
 
234
    rewrite Zmult_1_l in H1;rewrite H1;ring.
 
235
    generalize (spec_w_add_carry_c xh yh);destruct (w_add_carry_c xh yh)
 
236
     as [h|h]; intros H1;unfold interp_carry in *.
 
237
    apply spec_f0;simpl;rewrite H1. rewrite Zmult_plus_distr_l.
 
238
    rewrite <- Zplus_assoc;rewrite H;ring.
 
239
    apply spec_f1.  simpl;rewrite spec_w_WW;rewrite wwB_wBwB. 
 
240
    rewrite Zplus_assoc; rewrite Zpower_2; rewrite <- Zmult_plus_distr_l. 
 
241
    rewrite Zmult_1_l in H1;rewrite H1. rewrite Zmult_plus_distr_l.
 
242
    rewrite <- Zplus_assoc;rewrite H;ring.
 
243
   Qed.
 
244
  
 
245
  End Cont.
 
246
 
 
247
  Lemma spec_ww_add_carry_c :
 
248
         forall x y, [+[ww_add_carry_c x y]] = [[x]] + [[y]] + 1.
 
249
  Proof.
 
250
   destruct x as [ |xh xl];intro y;simpl.
 
251
   exact (spec_ww_succ_c y).
 
252
   destruct y as [ |yh yl];simpl.
 
253
   rewrite Zplus_0_r;exact (spec_ww_succ_c (WW xh xl)).
 
254
   replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1) 
 
255
   with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|]+1)). 2:ring.
 
256
   generalize (spec_w_add_carry_c xl yl);destruct (w_add_carry_c xl yl) 
 
257
    as [l|l];intros H;unfold interp_carry in H;rewrite <- H.
 
258
   generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h];
 
259
    intros H1;unfold interp_carry in H1;rewrite <- H1. trivial.
 
260
   unfold interp_carry;repeat rewrite Zmult_1_l;simpl;rewrite wwB_wBwB;ring.
 
261
   rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l.
 
262
   generalize (spec_w_add_carry_c xh yh);destruct (w_add_carry_c xh yh) 
 
263
    as [h|h];intros H1;unfold interp_carry in H1;rewrite <- H1. trivial.  
 
264
   unfold interp_carry;rewrite spec_w_WW;
 
265
   repeat rewrite Zmult_1_l;simpl;rewrite wwB_wBwB;ring.
 
266
  Qed.
 
267
 
 
268
  Lemma spec_ww_succ : forall x, [[ww_succ x]] = ([[x]] + 1) mod wwB.
 
269
  Proof.
 
270
   destruct x as [ |xh xl];simpl.
 
271
   rewrite spec_ww_1;rewrite Zmod_small;trivial.
 
272
   split;[intro;discriminate|apply wwB_pos].
 
273
   rewrite <- Zplus_assoc;generalize (spec_w_succ_c xl);
 
274
   destruct (w_succ_c xl) as[l|l];intro H;unfold interp_carry in H;rewrite <-H.
 
275
   rewrite Zmod_small;trivial.
 
276
   rewrite wwB_wBwB;apply beta_mult;apply spec_to_Z.
 
277
   assert ([|l|] = 0). clear spec_ww_1 spec_w_1 spec_w_0.
 
278
    assert (H1:= spec_to_Z l); assert (H2:= spec_to_Z xl); omega.
 
279
   rewrite H0;rewrite Zplus_0_r;rewrite <- Zmult_plus_distr_l;rewrite wwB_wBwB.
 
280
   rewrite Zpower_2; rewrite Zmult_mod_distr_r;try apply lt_0_wB.
 
281
   rewrite spec_w_W0;rewrite spec_w_succ;trivial.
 
282
  Qed.
 
283
 
 
284
  Lemma spec_ww_add : forall x y, [[ww_add x y]] = ([[x]] + [[y]]) mod wwB.
 
285
  Proof.
 
286
   destruct x as [ |xh xl];intros y;simpl.
 
287
   rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial.
 
288
   destruct y as [ |yh yl].
 
289
   change [[W0]] with 0;rewrite Zplus_0_r.
 
290
   rewrite Zmod_small;trivial. 
 
291
    exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl)).
 
292
   simpl. replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|])) 
 
293
   with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|])). 2:ring.
 
294
   generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l];
 
295
   unfold interp_carry;intros H;simpl;rewrite <- H.
 
296
   rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add;trivial.
 
297
   rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l.
 
298
   rewrite(mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add_carry;trivial.
 
299
  Qed.
 
300
 
 
301
  Lemma spec_ww_add_carry :
 
302
         forall x y, [[ww_add_carry x y]] = ([[x]] + [[y]] + 1) mod wwB.
 
303
  Proof.
 
304
   destruct x as [ |xh xl];intros y;simpl.
 
305
   exact (spec_ww_succ y).
 
306
   destruct y as [ |yh yl].
 
307
   change [[W0]] with 0;rewrite Zplus_0_r. exact (spec_ww_succ (WW xh xl)).
 
308
   simpl;replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1) 
 
309
   with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|]+1)). 2:ring.
 
310
   generalize (spec_w_add_carry_c xl yl);destruct (w_add_carry_c xl yl) 
 
311
   as [l|l];unfold interp_carry;intros H;rewrite <- H;simpl ww_to_Z.
 
312
   rewrite(mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add;trivial.
 
313
   rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l.
 
314
   rewrite(mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_w_add_carry;trivial.
 
315
  Qed. 
 
316
 
 
317
(* End DoubleProof. *)
 
318
End DoubleAdd.