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
(************************************************************************)
11
(*i $Id: Nbasic.v 10964 2008-05-22 11:08:13Z letouzey $ i*)
13
Require Import ZArith.
14
Require Import BigNumPrelude.
16
Require Import DoubleType.
17
Require Import DoubleBase.
18
Require Import CyclicAxioms.
19
Require Import DoubleCyclic.
21
(* To compute the necessary height *)
23
Fixpoint plength (p: positive) : positive :=
26
| xO p1 => Psucc (plength p1)
27
| xI p1 => Psucc (plength p1)
30
Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z.
31
assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z).
32
intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z.
33
rewrite Zpower_exp; auto with zarith.
34
rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
35
intros p; elim p; simpl plength; auto.
36
intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI.
37
assert (tmp: (forall p, 2 * p = p + p)%Z);
38
try repeat rewrite tmp; auto with zarith.
39
intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1).
40
assert (tmp: (forall p, 2 * p = p + p)%Z);
41
try repeat rewrite tmp; auto with zarith.
42
rewrite Zpower_1_r; auto with zarith.
45
Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z.
46
intros p; case (Psucc_pred p); intros H1.
48
rewrite Zpower_1_r; auto with zarith.
49
pattern p at 1; rewrite <- H1.
50
rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith.
51
generalize (plength_correct (Ppred p)); auto with zarith.
54
Definition Pdiv p q :=
55
match Zdiv (Zpos p) (Zpos q) with
56
Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with
63
Theorem Pdiv_le: forall p q,
64
Zpos p <= Zpos q * Zpos (Pdiv p q).
67
assert (H1: Zpos q > 0); auto with zarith.
68
assert (H1b: Zpos p >= 0); auto with zarith.
69
generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b).
70
generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Zdiv.
71
intros HH _; rewrite HH; rewrite Zmult_0_r; rewrite Zmult_1_r; simpl.
72
case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith.
74
replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q).
75
2: pattern (Zpos p) at 2; rewrite H2; auto with zarith.
76
generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2;
78
intros HH _; rewrite HH; auto with zarith.
79
intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism.
80
unfold Zsucc; rewrite Zmult_plus_distr_r; auto with zarith.
81
intros r1 _ (HH,_); case HH; auto.
82
intros q1 HH; rewrite HH.
83
unfold Zge; simpl Zcompare; intros HH1; case HH1; auto.
86
Definition is_one p := match p with xH => true | _ => false end.
88
Theorem is_one_one: forall p, is_one p = true -> p = xH.
89
intros p; case p; auto; intros p1 H1; discriminate H1.
92
Definition get_height digits p :=
93
let r := Pdiv p digits in
94
if is_one r then xH else Psucc (plength (Ppred r)).
96
Theorem get_height_correct:
98
Zpos N <= Zpos digits * (2 ^ (Zpos (get_height digits N) -1)).
101
assert (H1 := Pdiv_le N digits).
102
case_eq (is_one (Pdiv N digits)); intros H2.
103
rewrite (is_one_one _ H2) in H1.
104
rewrite Zmult_1_r in H1.
105
change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto.
107
apply Zle_trans with (1 := H1).
108
apply Zmult_le_compat_l; auto with zarith.
109
rewrite Zpos_succ_morphism; unfold Zsucc.
110
rewrite Zplus_comm; rewrite Zminus_plus.
111
apply plength_pred_correct.
114
Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n.
115
fix zn2z_word_comm 2.
119
case (zn2z_word_comm w n0).
123
Fixpoint extend (n:nat) {struct n} : forall w:Type, zn2z w -> word w (S n) :=
124
match n return forall w:Type, zn2z w -> word w (S n) with
127
let aux := extend m in
128
fun w x => WW W0 (aux w x)
133
Open Scope nat_scope.
135
Fixpoint plusnS (n m: nat) {struct n} : (n + S m = S (n + m))%nat :=
136
match n return (n + S m = S (n + m))%nat with
137
| 0 => refl_equal (S m)
139
let v := S (S n1 + m) in
140
eq_ind_r (fun n => S n = v) (refl_equal v) (plusnS n1 m)
143
Fixpoint plusn0 n : n + 0 = n :=
144
match n return (n + 0 = n) with
148
eq_ind_r (fun n : nat => S n = v) (refl_equal v) (plusn0 n1)
151
Fixpoint diff (m n: nat) {struct m}: nat * nat :=
155
| S m1, S n1 => diff m1 n1
158
Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
159
match m return fst (diff m n) + n = max m n with
161
match n return (n = max 0 n) with
163
| S n0 => refl_equal _
166
match n return (fst (diff (S m1) n) + n = max (S m1) n)
170
let v := fst (diff m1 n1) + n1 in
171
let v1 := fst (diff m1 n1) + S n1 in
172
eq_ind v (fun n => v1 = S n)
173
(eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _))
178
Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
179
match m return (snd (diff m n) + m = max m n) with
181
match n return (snd (diff 0 n) + 0 = max 0 n) with
186
match n return (snd (diff (S m) n) + S m = max (S m) n) with
187
| 0 => refl_equal (snd (diff (S m) 0) + S m)
189
let v := S (max m n1) in
190
eq_ind_r (fun n => n = v)
191
(eq_ind_r (fun n => S n = v)
192
(refl_equal v) (diff_r _ _)) (plusnS _ _)
198
Definition castm (m n: nat) (H: m = n) (x: word w (S m)):
200
match H in (_ = y) return (word w (S y)) with
205
Variable v: (word w (S m)).
207
Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) :=
208
match n return (word w (S (n + m))) with
210
| S n1 => WW W0 (extend_tr n1)
215
Implicit Arguments extend_tr[w m].
216
Implicit Arguments castm[w m n].
225
Variable eq0 : w -> bool.
226
Variable reduce_n : w -> nT.
227
Variable zn2z_to_Nt : zn2z w -> nT.
229
Definition reduce_n1 (x:zn2z w) :=
233
if eq0 xh then reduce_n xl
244
Variable reduce_1n : zn2z w -> nT.
245
Variable c : forall n, word w (S n) -> nT.
247
Fixpoint reduce_n (n:nat) : word w (S n) -> nT :=
248
match n return word w (S n) -> nT with
255
| W0 => @reduce_n m xl
263
Definition opp_compare cmp :=
272
Variable wm w : Type.
274
Variable compare : w -> w -> comparison.
275
Variable compare0_m : wm -> comparison.
276
Variable compare_m : wm -> w -> comparison.
278
Fixpoint compare0_mn (n:nat) : word wm n -> comparison :=
279
match n return word wm n -> comparison with
285
match compare0_mn m xh with
286
| Eq => compare0_mn m xl
292
Variable wm_base: positive.
293
Variable wm_to_Z: wm -> Z.
294
Variable w_to_Z: w -> Z.
295
Variable w_to_Z_0: w_to_Z w_0 = 0.
296
Variable spec_compare0_m: forall x,
297
match compare0_m x with
298
Eq => w_to_Z w_0 = wm_to_Z x
299
| Lt => w_to_Z w_0 < wm_to_Z x
300
| Gt => w_to_Z w_0 > wm_to_Z x
302
Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base.
304
Let double_to_Z := double_to_Z wm_base wm_to_Z.
305
Let double_wB := double_wB wm_base.
307
Lemma base_xO: forall n, base (xO n) = (base n)^2.
309
intros n1; unfold base.
310
rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith.
313
Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n :=
314
(spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos).
317
Lemma spec_compare0_mn: forall n x,
318
match compare0_mn n x with
319
Eq => 0 = double_to_Z n x
320
| Lt => 0 < double_to_Z n x
321
| Gt => 0 > double_to_Z n x
324
intros n; elim n; clear n; auto.
325
intros x; generalize (spec_compare0_m x); rewrite w_to_Z_0; auto.
326
intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto.
328
generalize (Hrec xh); case compare0_mn; auto.
329
generalize (Hrec xl); case compare0_mn; auto.
330
simpl double_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto.
331
simpl double_to_Z; intros H1 H2; rewrite <- H2; auto.
332
case (double_to_Z_pos n xl); auto with zarith.
333
intros H1; simpl double_to_Z.
334
set (u := DoubleBase.double_wB wm_base n).
335
case (double_to_Z_pos n xl); intros H2 H3.
336
assert (0 < u); auto with zarith.
337
unfold u, DoubleBase.double_wB, base; auto with zarith.
338
change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith.
339
apply Zmult_lt_0_compat; auto with zarith.
340
case (double_to_Z_pos n xh); auto with zarith.
343
Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison :=
344
match n return word wm n -> w -> comparison with
348
| W0 => compare w_0 y
350
match compare0_mn m xh with
351
| Eq => compare_mn_1 m xl y
357
Variable spec_compare: forall x y,
358
match compare x y with
359
Eq => w_to_Z x = w_to_Z y
360
| Lt => w_to_Z x < w_to_Z y
361
| Gt => w_to_Z x > w_to_Z y
363
Variable spec_compare_m: forall x y,
364
match compare_m x y with
365
Eq => wm_to_Z x = w_to_Z y
366
| Lt => wm_to_Z x < w_to_Z y
367
| Gt => wm_to_Z x > w_to_Z y
369
Variable wm_base_lt: forall x,
370
0 <= w_to_Z x < base (wm_base).
372
Let double_wB_lt: forall n x,
373
0 <= w_to_Z x < (double_wB n).
375
intros n x; elim n; simpl; auto; clear n.
376
intros n (H0, H); split; auto.
377
apply Zlt_le_trans with (1:= H).
378
unfold double_wB, DoubleBase.double_wB; simpl.
380
set (u := base (double_digits wm_base n)).
382
unfold u, base; auto with zarith.
383
replace (u^2) with (u * u); simpl; auto with zarith.
384
apply Zle_trans with (1 * u); auto with zarith.
385
unfold Zpower_pos; simpl; ring.
389
Lemma spec_compare_mn_1: forall n x y,
390
match compare_mn_1 n x y with
391
Eq => double_to_Z n x = w_to_Z y
392
| Lt => double_to_Z n x < w_to_Z y
393
| Gt => double_to_Z n x > w_to_Z y
396
intros n; elim n; simpl; auto; clear n.
397
intros n Hrec x; case x; clear x; auto.
398
intros y; generalize (spec_compare w_0 y); rewrite w_to_Z_0; case compare; auto.
399
intros xh xl y; simpl; generalize (spec_compare0_mn n xh); case compare0_mn; intros H1b.
400
rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto.
403
case (double_wB_lt n y); intros _ H0.
404
apply Zlt_le_trans with (1:= H0).
406
case (double_to_Z_pos n xl); intros H1 H2.
407
apply Zle_trans with (double_to_Z n xh * double_wB n); auto with zarith.
408
apply Zle_trans with (1 * double_wB n); auto with zarith.
409
case (double_to_Z_pos n xh); auto with zarith.
417
Variable w wm : Type.
418
Variable incr : wm -> carry wm.
419
Variable addr : w -> wm -> carry wm.
420
Variable injr : w -> zn2z wm.
423
Fixpoint injs (n:nat): word w (S n) :=
424
match n return (word w (S n)) with
426
| S n1 => (WW W0 (injs n1))
429
Definition adds x y :=
432
| WW hy ly => match addr x ly with
434
| C1 z => match incr hy with
435
C0 z1 => C0 (WW z1 z)
436
| C1 z1 => C1 (WW z1 z)
444
Lemma spec_opp: forall u x y,
450
match opp_compare u with
456
intros u x y; case u; simpl; auto with zarith.
459
Fixpoint length_pos x :=
460
match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end.
462
Theorem length_pos_lt: forall x y,
463
(length_pos x < length_pos y)%nat -> Zpos x < Zpos y.
465
intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac];
466
intros y; case y; clear y; intros y1 H || intros H; simpl length_pos;
467
try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1));
468
try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1));
469
try (inversion H; fail);
470
try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply lt_S_n | idtac]; auto with zarith);
471
assert (0 < Zpos y1); auto with zarith; red; auto.
474
Theorem cancel_app: forall A B (f g: A -> B) x, f = g -> f x = g x.
476
intros A B f g x H; rewrite H; auto.
484
Theorem digits_zop: forall w (x: znz_op w),
485
znz_digits (mk_zn2z_op x) = xO (znz_digits x).
489
Theorem digits_kzop: forall w (x: znz_op w),
490
znz_digits (mk_zn2z_op_karatsuba x) = xO (znz_digits x).
494
Theorem make_zop: forall w (x: znz_op w),
495
znz_to_Z (mk_zn2z_op x) =
496
fun z => match z with
498
| WW xh xl => znz_to_Z x xh * base (znz_digits x)
504
Theorem make_kzop: forall w (x: znz_op w),
505
znz_to_Z (mk_zn2z_op_karatsuba x) =
506
fun z => match z with
508
| WW xh xl => znz_to_Z x xh * base (znz_digits x)
added
removed
theories/Numbers/Natural/BigN/Nbasic.v
