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: NMake_gen.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
13
(*S NMake_gen.ml : this file generates NMake.v *)
16
(*s The two parameters that control the generation: *)
18
let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ
19
process before relying on a generic construct *)
20
let gen_proof = true (* should we generate proofs ? *)
27
let pz n = if n == 0 then "w_0" else "W0"
28
let rec gen2 n = if n == 0 then "1" else if n == 1 then "2"
29
else "2 * " ^ (gen2 (n - 1))
31
if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")"
33
(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to
34
/dev/null, but for being compatible with earlier ocaml and not
35
relying on system-dependent stuff like open_out "/dev/null",
36
let's use instead a magical hack *)
38
(* Standard printer, with a final newline *)
39
let pr s = Printf.printf (s^^"\n")
40
(* Printing to /dev/null *)
41
let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ())
42
: ('a, out_channel, unit) format -> 'a)
43
(* Proof printer : prints iff gen_proof is true *)
44
let pp = if gen_proof then pr else pn
45
(* Printer for admitted parts : prints iff gen_proof is false *)
46
let pa = if not gen_proof then pr else pn
47
(* Same as before, but without the final newline *)
48
let pr0 = Printf.printf
49
let pp0 = if gen_proof then pr0 else pn
52
(*s The actual printing *)
56
pr "(************************************************************************)";
57
pr "(* v * The Coq Proof Assistant / The Coq Development Team *)";
58
pr "(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)";
59
pr "(* \\VV/ **************************************************************)";
60
pr "(* // * This file is distributed under the terms of the *)";
61
pr "(* * GNU Lesser General Public License Version 2.1 *)";
62
pr "(************************************************************************)";
63
pr "(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)";
64
pr "(************************************************************************)";
68
pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)";
70
pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)";
72
pr "Require Import BigNumPrelude.";
73
pr "Require Import ZArith.";
74
pr "Require Import CyclicAxioms.";
75
pr "Require Import DoubleType.";
76
pr "Require Import DoubleMul.";
77
pr "Require Import DoubleDivn1.";
78
pr "Require Import DoubleCyclic.";
79
pr "Require Import Nbasic.";
80
pr "Require Import Wf_nat.";
81
pr "Require Import StreamMemo.";
82
pr "Require Import NSig.";
84
pr "Module Make (Import W0:CyclicType) <: NType.";
87
pr " Definition w0 := W0.w.";
89
pr " Definition w%i := zn2z w%i." i (i-1)
93
pr " Definition w0_op := W0.w_op.";
95
pr " Definition w%i_op := mk_zn2z_op w%i_op." i (i-1)
97
for i = 4 to size + 3 do
98
pr " Definition w%i_op := mk_zn2z_op_karatsuba w%i_op." i (i-1)
102
pr " Section Make_op.";
103
pr " Variable mk : forall w', znz_op w' -> znz_op (zn2z w').";
105
pr " Fixpoint make_op_aux (n:nat) : znz_op (word w%i (S n)):=" size;
106
pr " match n return znz_op (word w%i (S n)) with" size;
107
pr " | O => w%i_op" (size+1);
109
pr " match n1 return znz_op (word w%i (S (S n1))) with" size;
110
pr " | O => w%i_op" (size+2);
112
pr " match n2 return znz_op (word w%i (S (S (S n2)))) with" size;
113
pr " | O => w%i_op" (size+3);
114
pr " | S n3 => mk _ (mk _ (mk _ (make_op_aux n3)))";
121
pr " Definition omake_op := make_op_aux mk_zn2z_op_karatsuba.";
124
pr " Definition make_op_list := dmemo_list _ omake_op.";
126
pr " Definition make_op n := dmemo_get _ omake_op n make_op_list.";
128
pr " Lemma make_op_omake: forall n, make_op n = omake_op n.";
129
pr " intros n; unfold make_op, make_op_list.";
130
pr " refine (dmemo_get_correct _ _ _).";
134
pr " Inductive %s_ :=" t;
136
pr " | %s%i : w%i -> %s_" c i i t
138
pr " | %sn : forall n, word w%i (S n) -> %s_." c size t;
140
pr " Definition %s := %s_." t t;
142
pr " Definition w_0 := w0_op.(znz_0).";
146
pr " Definition one%i := w%i_op.(znz_1)." i i
151
pr " Definition zero := %s0 w_0." c;
152
pr " Definition one := %s0 one0." c;
155
pr " Definition to_Z x :=";
158
pr " | %s%i wx => w%i_op.(znz_to_Z) wx" c i i
160
pr " | %sn n wx => (make_op n).(znz_to_Z) wx" c;
164
pr " Open Scope Z_scope.";
165
pr " Notation \"[ x ]\" := (to_Z x).";
168
pr " Definition to_N x := Zabs_N (to_Z x).";
171
pr " Definition eq x y := (to_Z x = to_Z y).";
174
pp " (* Regular make op (no karatsuba) *)";
175
pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) : ";
176
pp " znz_op (word ww n) :=";
177
pp " match n return znz_op (word ww n) with ";
179
pp " | S n1 => mk_zn2z_op (nmake_op ww ww_op n1) ";
182
pp " (* Simplification by rewriting for nmake_op *)";
183
pp " Theorem nmake_op_S: forall ww (w_op: znz_op ww) x, ";
184
pp " nmake_op _ w_op (S x) = mk_zn2z_op (nmake_op _ w_op x).";
190
pr " (* Eval and extend functions for each level *)";
192
pp " Let nmake_op%i := nmake_op _ w%i_op." i i;
193
pp " Let eval%in n := znz_to_Z (nmake_op%i n)." i i;
195
pr " Let extend%i := DoubleBase.extend (WW w_0)." i
197
pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i;
202
pp " Theorem digits_doubled:forall n ww (w_op: znz_op ww), ";
203
pp " znz_digits (nmake_op _ w_op n) = ";
204
pp " DoubleBase.double_digits (znz_digits w_op) n.";
206
pp " intros n; elim n; auto; clear n.";
207
pp " intros n Hrec ww ww_op; simpl DoubleBase.double_digits.";
208
pp " rewrite <- Hrec; auto.";
211
pp " Theorem nmake_double: forall n ww (w_op: znz_op ww), ";
212
pp " znz_to_Z (nmake_op _ w_op n) =";
213
pp " @DoubleBase.double_to_Z _ (znz_digits w_op) (znz_to_Z w_op) n.";
215
pp " intros n; elim n; auto; clear n.";
216
pp " intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z.";
217
pp " rewrite <- Hrec; auto.";
218
pp " unfold DoubleBase.double_wB; rewrite <- digits_doubled; auto.";
223
pp " Theorem digits_nmake:forall n ww (w_op: znz_op ww), ";
224
pp " znz_digits (nmake_op _ w_op (S n)) = ";
225
pp " xO (znz_digits (nmake_op _ w_op n)).";
232
pp " Theorem znz_nmake_op: forall ww ww_op n xh xl,";
233
pp " znz_to_Z (nmake_op ww ww_op (S n)) (WW xh xl) =";
234
pp " znz_to_Z (nmake_op ww ww_op n) xh *";
235
pp " base (znz_digits (nmake_op ww ww_op n)) +";
236
pp " znz_to_Z (nmake_op ww ww_op n) xl.";
242
pp " Theorem make_op_S: forall n,";
243
pp " make_op (S n) = mk_zn2z_op_karatsuba (make_op n).";
245
pp " do 2 rewrite make_op_omake.";
246
pp " pattern n; apply lt_wf_ind; clear n.";
247
pp " intros n; case n; clear n.";
248
pp " intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 2);
249
pp " intros n; case n; clear n.";
250
pp " intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 3);
251
pp " intros n; case n; clear n.";
252
pp " intros _; unfold omake_op, make_op_aux, w%i_op, w%i_op; apply refl_equal." (size + 3) (size + 2);
253
pp " intros n Hrec.";
254
pp " change (omake_op (S (S (S (S n))))) with";
255
pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op (S n))))).";
256
pp " change (omake_op (S (S (S n)))) with";
257
pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op n)))).";
258
pp " rewrite Hrec; auto with arith.";
263
for i = 1 to size + 2 do
264
pp " Let znz_to_Z_%i: forall x y," i;
265
pp " znz_to_Z w%i_op (WW x y) = " i;
266
pp " znz_to_Z w%i_op x * base (znz_digits w%i_op) + znz_to_Z w%i_op y." (i-1) (i-1) (i-1);
273
pp " Let znz_to_Z_n: forall n x y,";
274
pp " znz_to_Z (make_op (S n)) (WW x y) = ";
275
pp " znz_to_Z (make_op n) x * base (znz_digits (make_op n)) + znz_to_Z (make_op n) y.";
277
pp " intros n x y; rewrite make_op_S; auto.";
281
pp " Let w0_spec: znz_spec w0_op := W0.w_spec.";
283
pp " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec." i i (i-1)
285
for i = 4 to size + 3 do
286
pp " Let w%i_spec : znz_spec w%i_op := mk_znz2_karatsuba_spec w%i_spec." i i (i-1)
290
pp " Let wn_spec: forall n, znz_spec (make_op n).";
291
pp " intros n; elim n; clear n.";
292
pp " exact w%i_spec." (size + 1);
293
pp " intros n Hrec; rewrite make_op_S.";
294
pp " exact (mk_znz2_karatsuba_spec Hrec).";
299
pr " Definition w%i_eq0 := w%i_op.(znz_eq0)." i i;
300
pr " Let spec_w%i_eq0: forall x, if w%i_eq0 x then [%s%i x] = 0 else True." i i c i;
303
pp " intros x; unfold w%i_eq0, to_Z; generalize (spec_eq0 w%i_spec x);" i i;
304
pp " case znz_eq0; auto.";
312
pp " Theorem digits_w%i: znz_digits w%i_op = znz_digits (nmake_op _ w0_op %i)." i i i;
316
pp " rewrite digits_nmake; rewrite <- digits_w%i; auto." (i - 1);
319
pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) n." i i i i;
321
pp " intros n; exact (nmake_double n w%i w%i_op)." i i;
327
for j = 0 to (size - i) do
328
pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i j (i + j) i j;
335
pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1);
337
pp " unfold nmake_op; auto.";
341
pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1);
343
pp " rewrite digits_nmake.";
344
pp " rewrite digits_w%in%i." i (j - 1);
349
pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j;
352
pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i
355
pp " intros x; case x.";
357
pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (i + j);
358
pp " rewrite digits_w%in%i." i (j - 1);
359
pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (j - 1);
360
pp " unfold eval%in, nmake_op%i." i i;
361
pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (j - 1);
364
if i + j <> size then
366
pp " Let spec_extend%in%i: forall x, [%s%i x] = [%s%i (extend%i %i x)]." i (i + j + 1) c i c (i + j + 1) i j;
369
pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." i (i + j);
370
pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1);
371
pp " rewrite (spec_0 w%i_spec); auto." (i + j);
375
pp " intros x; change (extend%i %i x) with (WW (znz_0 w%i_op) (extend%i %i x))." i j (i + j) i (j - 1);
376
pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1);
377
pp " rewrite (spec_0 w%i_spec)." (i + j);
378
pp " generalize (spec_extend%in%i x); unfold to_Z." i (i + j);
379
pp " intros HH; rewrite <- HH; auto.";
386
pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i (size - i + 1) (size + 1) i (size - i + 1);
388
pp " apply trans_equal with (xO (znz_digits w%i_op))." size;
390
pp " rewrite digits_nmake.";
391
pp " rewrite digits_w%in%i." i (size - i);
396
pp " Let spec_eval%in%i: forall x, [%sn 0 x] = eval%in %i x." i (size - i + 1) c i (size - i + 1);
398
pp " intros x; case x.";
400
pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 1);
401
pp " rewrite digits_w%in%i." i (size - i);
402
pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (size - i);
403
pp " unfold eval%in, nmake_op%i." i i;
404
pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size - i);
408
pp " Let spec_eval%in%i: forall x, [%sn 1 x] = eval%in %i x." i (size - i + 2) c i (size - i + 2);
409
pp " intros x; case x.";
411
pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 2);
412
pp " rewrite digits_w%in%i." i (size + 1 - i);
413
pp " generalize (spec_eval%in%i); unfold to_Z; change (make_op 0) with (w%i_op); intros HH; repeat rewrite HH." i (size + 1 - i) (size + 1);
414
pp " unfold eval%in, nmake_op%i." i i;
415
pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size + 1 - i);
420
pp " Let digits_w%in: forall n," size;
421
pp " znz_digits (make_op n) = znz_digits (nmake_op _ w%i_op (S n))." size;
422
pp " intros n; elim n; clear n.";
423
pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size;
424
pp " rewrite nmake_op_S; apply sym_equal; auto.";
425
pp " intros n Hrec.";
426
pp " replace (znz_digits (make_op (S n))) with (xO (znz_digits (make_op n))).";
428
pp " rewrite nmake_op_S; apply sym_equal; auto.";
429
pp " rewrite make_op_S; apply sym_equal; auto.";
433
pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size;
434
pp " intros n; elim n; clear n.";
435
pp " exact spec_eval%in1." size;
436
pp " intros n Hrec x; case x; clear x.";
437
pp " unfold to_Z, eval%in, nmake_op%i." size size;
438
pp " rewrite make_op_S; rewrite nmake_op_S; auto.";
440
pp " unfold to_Z in Hrec |- *.";
441
pp " rewrite znz_to_Z_n.";
442
pp " rewrite digits_w%in." size;
443
pp " repeat rewrite Hrec.";
444
pp " unfold eval%in, nmake_op%i." size size;
445
pp " apply sym_equal; rewrite nmake_op_S; auto.";
449
pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ;
450
pp " intros n; elim n; clear n.";
451
pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." size size;
453
pp " change (make_op 0) with w%i_op." (size + 1);
454
pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto." (size + 1) size;
455
pp " intros n Hrec x.";
456
pp " change (extend%i (S n) x) with (WW W0 (extend%i n x))." size size;
457
pp " unfold to_Z in Hrec |- *; rewrite znz_to_Z_n; auto.";
458
pp " rewrite <- Hrec.";
459
pp " replace (znz_to_Z (make_op n) W0) with 0; auto.";
460
pp " case n; auto; intros; rewrite make_op_S; auto.";
464
pr " Theorem spec_pos: forall x, 0 <= [x].";
467
pp " intros x; case x; clear x.";
469
pp " intros x; case (spec_to_Z w%i_spec x); auto." i;
471
pp " intros n x; case (spec_to_Z (wn_spec n) x); auto.";
475
pp " Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx]." c c;
476
pp " intros n; elim n; auto.";
477
pp " intros n1 Hrec wx; simpl extend; rewrite <- Hrec; auto.";
479
pp " case n1; auto; intros n2; repeat rewrite make_op_S; auto.";
481
pp " Hint Rewrite spec_extendn_0: extr.";
483
pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c;
485
pp " intros n x; unfold to_Z.";
486
pp " rewrite znz_to_Z_n.";
487
pp " rewrite <- (Zplus_0_l (znz_to_Z (make_op n) x)).";
488
pp " apply (f_equal2 Zplus); auto.";
490
pp " intros n1; rewrite make_op_S; auto.";
492
pp " Hint Rewrite spec_extendn_0: extr.";
494
pp " Let spec_extend_tr: forall m n (w: word _ (S n)),";
495
pp " [%sn (m + n) (extend_tr w m)] = [%sn n w]." c c;
497
pp " induction m; auto.";
498
pp " intros n x; simpl extend_tr.";
499
pp " simpl plus; rewrite spec_extendn0_0; auto.";
501
pp " Hint Rewrite spec_extend_tr: extr.";
503
pp " Let spec_cast_l: forall n m x1,";
504
pp " [%sn (Max.max n m)" c;
505
pp " (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))] =";
508
pp " intros n m x1; case (diff_r n m); simpl castm.";
509
pp " rewrite spec_extend_tr; auto.";
511
pp " Hint Rewrite spec_cast_l: extr.";
513
pp " Let spec_cast_r: forall n m x1,";
514
pp " [%sn (Max.max n m)" c;
515
pp " (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))] =";
518
pp " intros n m x1; case (diff_l n m); simpl castm.";
519
pp " rewrite spec_extend_tr; auto.";
521
pp " Hint Rewrite spec_cast_r: extr.";
525
pr " Section LevelAndIter.";
527
pr " Variable res: Type.";
528
pr " Variable xxx: res.";
529
pr " Variable P: Z -> Z -> res -> Prop.";
530
pr " (* Abstraction function for each level *)";
532
pr " Variable f%i: w%i -> w%i -> res." i i i;
533
pr " Variable f%in: forall n, w%i -> word w%i (S n) -> res." i i i;
534
pr " Variable fn%i: forall n, word w%i (S n) -> w%i -> res." i i i;
535
pp " Variable Pf%i: forall x y, P [%s%i x] [%s%i y] (f%i x y)." i c i c i i;
538
pp " Variable Pf%in: forall n x y, P [%s%i x] (eval%in (S n) y) (f%in n x y)." i c i i i;
539
pp " Variable Pfn%i: forall n x y, P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i i c i i;
543
pp " Variable Pf%in: forall n x y, Z_of_nat n <= %i -> P [%s%i x] (eval%in (S n) y) (f%in n x y)." i (size - i) c i i i;
544
pp " Variable Pfn%i: forall n x y, Z_of_nat n <= %i -> P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i (size - i) i c i i;
548
pr " Variable fnn: forall n, word w%i (S n) -> word w%i (S n) -> res." size size;
549
pp " Variable Pfnn: forall n x y, P [%sn n x] [%sn n y] (fnn n x y)." c c;
550
pr " Variable fnm: forall n m, word w%i (S n) -> word w%i (S m) -> res." size size;
551
pp " Variable Pfnm: forall n m x y, P [%sn n x] [%sn m y] (fnm n m x y)." c c;
553
pr " (* Special zero functions *)";
554
pr " Variable f0t: t_ -> res.";
555
pp " Variable Pf0t: forall x, P 0 [x] (f0t x).";
556
pr " Variable ft0: t_ -> res.";
557
pp " Variable Pft0: forall x, P [x] 0 (ft0 x).";
561
pr " (* We level the two arguments before applying *)";
562
pr " (* the functions at each leval *)";
563
pr " Definition same_level (x y: t_): res :=";
564
pr0 " Eval lazy zeta beta iota delta [";
569
pr " DoubleBase.extend DoubleBase.extend_aux";
571
pr " match x, y with";
573
for j = 0 to i - 1 do
574
pr " | %s%i wx, %s%i wy => f%i wx (extend%i %i wy)" c i c j i j (i - j -1);
576
pr " | %s%i wx, %s%i wy => f%i wx wy" c i c i i;
577
for j = i + 1 to size do
578
pr " | %s%i wx, %s%i wy => f%i (extend%i %i wx) wy" c i c j j i (j - i - 1);
581
pr " | %s%i wx, %sn m wy => fnn m (extend%i m wx) wy" c size c size
583
pr " | %s%i wx, %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c i c size i (size - i - 1);
587
pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n wy)" c c size size
589
pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n (extend%i %i wy))" c c i size i (size - i - 1);
591
pr " | %sn n wx, Nn m wy =>" c;
592
pr " let mn := Max.max n m in";
593
pr " let d := diff n m in";
595
pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
596
pr " (castm (diff_l n m) (extend_tr wy (fst d)))";
600
pp " Lemma spec_same_level: forall x y, P [x] [y] (same_level x y).";
602
pp " intros x; case x; clear x; unfold same_level.";
604
pp " intros x y; case y; clear y.";
605
for j = 0 to i - 1 do
606
pp " intros y; rewrite spec_extend%in%i; apply Pf%i." j i i;
608
pp " intros y; apply Pf%i." i;
609
for j = i + 1 to size do
610
pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j;
613
pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size
615
pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size;
617
pp " intros n x y; case y; clear y.";
620
pp " intros y; rewrite (spec_extend%in n); apply Pfnn." size
622
pp " intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size;
624
pp " intros m y; rewrite <- (spec_cast_l n m x); ";
625
pp " rewrite <- (spec_cast_r n m y); apply Pfnn.";
629
pr " (* We level the two arguments before applying *)";
630
pr " (* the functions at each level (special zero case) *)";
631
pr " Definition same_level0 (x y: t_): res :=";
632
pr0 " Eval lazy zeta beta iota delta [";
637
pr " DoubleBase.extend DoubleBase.extend_aux";
641
pr " | %s%i wx =>" c i;
643
pr " if w0_eq0 wx then f0t y else";
645
for j = 0 to i - 1 do
646
pr " | %s%i wy =>" c j;
648
pr " if w0_eq0 wy then ft0 x else";
649
pr " f%i wx (extend%i %i wy)" i j (i - j -1);
651
pr " | %s%i wy => f%i wx wy" c i i;
652
for j = i + 1 to size do
653
pr " | %s%i wy => f%i (extend%i %i wx) wy" c j j i (j - i - 1);
656
pr " | %sn m wy => fnn m (extend%i m wx) wy" c size
658
pr " | %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c size i (size - i - 1);
661
pr " | %sn n wx =>" c;
664
pr " | %s%i wy =>" c i;
666
pr " if w0_eq0 wy then ft0 x else";
668
pr " fnn n wx (extend%i n wy)" size
670
pr " fnn n wx (extend%i n (extend%i %i wy))" size i (size - i - 1);
672
pr " | %sn m wy =>" c;
673
pr " let mn := Max.max n m in";
674
pr " let d := diff n m in";
676
pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
677
pr " (castm (diff_l n m) (extend_tr wy (fst d)))";
682
pp " Lemma spec_same_level0: forall x y, P [x] [y] (same_level0 x y).";
684
pp " intros x; case x; clear x; unfold same_level0.";
689
pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H.";
690
pp " intros y; rewrite H; apply Pf0t.";
693
pp " intros y; case y; clear y.";
694
for j = 0 to i - 1 do
698
pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H.";
699
pp " rewrite H; apply Pft0.";
702
pp " rewrite spec_extend%in%i; apply Pf%i." j i i;
704
pp " intros y; apply Pf%i." i;
705
for j = i + 1 to size do
706
pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j;
709
pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size
711
pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size;
713
pp " intros n x y; case y; clear y.";
718
pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H.";
719
pp " rewrite H; apply Pft0.";
723
pp " rewrite (spec_extend%in n); apply Pfnn." size
725
pp " rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size;
727
pp " intros m y; rewrite <- (spec_cast_l n m x); ";
728
pp " rewrite <- (spec_cast_r n m y); apply Pfnn.";
732
pr " (* We iter the smaller argument with the bigger *)";
733
pr " Definition iter (x y: t_): res := ";
734
pr0 " Eval lazy zeta beta iota delta [";
739
pr " DoubleBase.extend DoubleBase.extend_aux";
741
pr " match x, y with";
743
for j = 0 to i - 1 do
744
pr " | %s%i wx, %s%i wy => fn%i %i wx wy" c i c j j (i - j - 1);
746
pr " | %s%i wx, %s%i wy => f%i wx wy" c i c i i;
747
for j = i + 1 to size do
748
pr " | %s%i wx, %s%i wy => f%in %i wx wy" c i c j i (j - i - 1);
751
pr " | %s%i wx, %sn m wy => f%in m wx wy" c size c size
753
pr " | %s%i wx, %sn m wy => f%in m (extend%i %i wx) wy" c i c size i (size - i - 1);
757
pr " | %sn n wx, %s%i wy => fn%i n wx wy" c c size size
759
pr " | %sn n wx, %s%i wy => fn%i n wx (extend%i %i wy)" c c i size i (size - i - 1);
761
pr " | %sn n wx, %sn m wy => fnm n m wx wy" c c;
765
pp " Ltac zg_tac := try";
766
pp " (red; simpl Zcompare; auto;";
767
pp " let t := fresh \"H\" in (intros t; discriminate t)).";
768
pp " Lemma spec_iter: forall x y, P [x] [y] (iter x y).";
770
pp " intros x; case x; clear x; unfold iter.";
772
pp " intros x y; case y; clear y.";
773
for j = 0 to i - 1 do
774
pp " intros y; rewrite spec_eval%in%i; apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1);
776
pp " intros y; apply Pf%i." i;
777
for j = i + 1 to size do
778
pp " intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1);
781
pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size
783
pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
785
pp " intros n x y; case y; clear y.";
788
pp " intros y; rewrite spec_eval%in; apply Pfn%i." size size
790
pp " intros y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
792
pp " intros m y; apply Pfnm.";
797
pr " (* We iter the smaller argument with the bigger (zero case) *)";
798
pr " Definition iter0 (x y: t_): res :=";
799
pr0 " Eval lazy zeta beta iota delta [";
804
pr " DoubleBase.extend DoubleBase.extend_aux";
808
pr " | %s%i wx =>" c i;
810
pr " if w0_eq0 wx then f0t y else";
812
for j = 0 to i - 1 do
813
pr " | %s%i wy =>" c j;
815
pr " if w0_eq0 wy then ft0 x else";
816
pr " fn%i %i wx wy" j (i - j - 1);
818
pr " | %s%i wy => f%i wx wy" c i i;
819
for j = i + 1 to size do
820
pr " | %s%i wy => f%in %i wx wy" c j i (j - i - 1);
823
pr " | %sn m wy => f%in m wx wy" c size
825
pr " | %sn m wy => f%in m (extend%i %i wx) wy" c size i (size - i - 1);
828
pr " | %sn n wx =>" c;
831
pr " | %s%i wy =>" c i;
833
pr " if w0_eq0 wy then ft0 x else";
835
pr " fn%i n wx wy" size
837
pr " fn%i n wx (extend%i %i wy)" size i (size - i - 1);
839
pr " | %sn m wy => fnm n m wx wy" c;
844
pp " Lemma spec_iter0: forall x y, P [x] [y] (iter0 x y).";
846
pp " intros x; case x; clear x; unfold iter0.";
851
pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H.";
852
pp " intros y; rewrite H; apply Pf0t.";
855
pp " intros y; case y; clear y.";
856
for j = 0 to i - 1 do
860
pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H.";
861
pp " rewrite H; apply Pft0.";
864
pp " rewrite spec_eval%in%i; apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1);
866
pp " intros y; apply Pf%i." i;
867
for j = i + 1 to size do
868
pp " intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1);
871
pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size
873
pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
875
pp " intros n x y; case y; clear y.";
880
pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H.";
881
pp " rewrite H; apply Pft0.";
885
pp " rewrite spec_eval%in; apply Pfn%i." size size
887
pp " rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
889
pp " intros m y; apply Pfnm.";
894
pr " End LevelAndIter.";
898
pr " (***************************************************************)";
900
pr " (* Reduction *)";
902
pr " (***************************************************************)";
905
pr " Definition reduce_0 (x:w) := %s0 x." c;
906
pr " Definition reduce_1 :=";
907
pr " Eval lazy beta iota delta[reduce_n1] in";
908
pr " reduce_n1 _ _ zero w0_eq0 %s0 %s1." c c;
910
pr " Definition reduce_%i :=" i;
911
pr " Eval lazy beta iota delta[reduce_n1] in";
912
pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i %s%i."
915
pr " Definition reduce_%i :=" (size+1);
916
pr " Eval lazy beta iota delta[reduce_n1] in";
917
pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i (%sn 0)."
920
pr " Definition reduce_n n := ";
921
pr " Eval lazy beta iota delta[reduce_n] in";
922
pr " reduce_n _ _ zero reduce_%i %sn n." (size + 1) c;
925
pp " Let spec_reduce_0: forall x, [reduce_0 x] = [%s0 x]." c;
927
pp " intros x; unfold to_Z, reduce_0.";
932
for i = 1 to size + 1 do
933
if i == size + 1 then
934
pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%sn 0 x]." i i c
936
pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x]." i i c i;
938
pp " intros x; case x; unfold reduce_%i." i;
939
pp " exact (spec_0 w0_spec).";
941
pp " generalize (spec_w%i_eq0 x1); " (i - 1);
942
pp " case w%i_eq0; intros H1; auto." (i - 1);
944
pp " rewrite spec_reduce_%i." (i - 1);
945
pp " unfold to_Z; rewrite znz_to_Z_%i." i;
946
pp " unfold to_Z in H1; rewrite H1; auto.";
951
pp " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x]." c;
953
pp " intros n; elim n; simpl reduce_n.";
954
pp " intros x; rewrite <- spec_reduce_%i; auto." (size + 1);
955
pp " intros n1 Hrec x; case x.";
956
pp " unfold to_Z; rewrite make_op_S; auto.";
957
pp " exact (spec_0 w0_spec).";
958
pp " intros x1 y1; case x1; auto.";
960
pp " rewrite spec_extendn0_0; auto.";
964
pr " (***************************************************************)";
966
pr " (* Successor *)";
968
pr " (***************************************************************)";
972
pr " Definition w%i_succ_c := w%i_op.(znz_succ_c)." i i
977
pr " Definition w%i_succ := w%i_op.(znz_succ)." i i
981
pr " Definition succ x :=";
983
for i = 0 to size-1 do
984
pr " | %s%i wx =>" c i;
985
pr " match w%i_succ_c wx with" i;
986
pr " | C0 r => %s%i r" c i;
987
pr " | C1 r => %s%i (WW one%i r)" c (i+1) i;
990
pr " | %s%i wx =>" c size;
991
pr " match w%i_succ_c wx with" size;
992
pr " | C0 r => %s%i r" c size;
993
pr " | C1 r => %sn 0 (WW one%i r)" c size ;
995
pr " | %sn n wx =>" c;
996
pr " let op := make_op n in";
997
pr " match op.(znz_succ_c) wx with";
998
pr " | C0 r => %sn n r" c;
999
pr " | C1 r => %sn (S n) (WW op.(znz_1) r)" c;
1004
pr " Theorem spec_succ: forall n, [succ n] = [n] + 1.";
1007
pp " intros n; case n; unfold succ, to_Z.";
1008
for i = 0 to size do
1009
pp " intros n1; generalize (spec_succ_c w%i_spec n1);" i;
1010
pp " unfold succ, to_Z, w%i_succ_c; case znz_succ_c; auto." i;
1011
pp " intros ww H; rewrite <- H.";
1012
pp " (rewrite znz_to_Z_%i; unfold interp_carry;" (i + 1);
1013
pp " apply f_equal2 with (f := Zplus); auto;";
1014
pp " apply f_equal2 with (f := Zmult); auto;";
1015
pp " exact (spec_1 w%i_spec))." i;
1017
pp " intros k n1; generalize (spec_succ_c (wn_spec k) n1).";
1018
pp " unfold succ, to_Z; case znz_succ_c; auto.";
1019
pp " intros ww H; rewrite <- H.";
1020
pp " (rewrite (znz_to_Z_n k); unfold interp_carry;";
1021
pp " apply f_equal2 with (f := Zplus); auto;";
1022
pp " apply f_equal2 with (f := Zmult); auto;";
1023
pp " exact (spec_1 (wn_spec k))).";
1028
pr " (***************************************************************)";
1030
pr " (* Adddition *)";
1032
pr " (***************************************************************)";
1035
for i = 0 to size do
1036
pr " Definition w%i_add_c := znz_add_c w%i_op." i i;
1037
pr " Definition w%i_add x y :=" i;
1038
pr " match w%i_add_c x y with" i;
1039
pr " | C0 r => %s%i r" c i;
1041
pr " | C1 r => %sn 0 (WW one%i r)" c size
1043
pr " | C1 r => %s%i (WW one%i r)" c (i + 1) i;
1047
pr " Definition addn n (x y : word w%i (S n)) :=" size;
1048
pr " let op := make_op n in";
1049
pr " match op.(znz_add_c) x y with";
1050
pr " | C0 r => %sn n r" c;
1051
pr " | C1 r => %sn (S n) (WW op.(znz_1) r) end." c;
1055
for i = 0 to size do
1056
pp " Let spec_w%i_add: forall x y, [w%i_add x y] = [%s%i x] + [%s%i y]." i i c i c i;
1058
pp " intros n m; unfold to_Z, w%i_add, w%i_add_c." i i;
1059
pp " generalize (spec_add_c w%i_spec n m); case znz_add_c; auto." i;
1060
pp " intros ww H; rewrite <- H.";
1061
pp " rewrite znz_to_Z_%i; unfold interp_carry;" (i + 1);
1062
pp " apply f_equal2 with (f := Zplus); auto;";
1063
pp " apply f_equal2 with (f := Zmult); auto;";
1064
pp " exact (spec_1 w%i_spec)." i;
1066
pp " Hint Rewrite spec_w%i_add: addr." i;
1069
pp " Let spec_wn_add: forall n x y, [addn n x y] = [%sn n x] + [%sn n y]." c c;
1071
pp " intros k n m; unfold to_Z, addn.";
1072
pp " generalize (spec_add_c (wn_spec k) n m); case znz_add_c; auto.";
1073
pp " intros ww H; rewrite <- H.";
1074
pp " rewrite (znz_to_Z_n k); unfold interp_carry;";
1075
pp " apply f_equal2 with (f := Zplus); auto;";
1076
pp " apply f_equal2 with (f := Zmult); auto;";
1077
pp " exact (spec_1 (wn_spec k)).";
1079
pp " Hint Rewrite spec_wn_add: addr.";
1081
pr " Definition add := Eval lazy beta delta [same_level] in";
1082
pr0 " (same_level t_ ";
1083
for i = 0 to size do
1089
pr " Theorem spec_add: forall x y, [add x y] = [x] + [y].";
1093
pp " generalize (spec_same_level t_ (fun x y res => [res] = x + y)).";
1094
pp " unfold same_level; intros HH; apply HH; clear HH.";
1095
for i = 0 to size do
1096
pp " exact spec_w%i_add." i;
1098
pp " exact spec_wn_add.";
1102
pr " (***************************************************************)";
1104
pr " (* Predecessor *)";
1106
pr " (***************************************************************)";
1109
for i = 0 to size do
1110
pr " Definition w%i_pred_c := w%i_op.(znz_pred_c)." i i
1114
pr " Definition pred x :=";
1116
for i = 0 to size do
1117
pr " | %s%i wx =>" c i;
1118
pr " match w%i_pred_c wx with" i;
1119
pr " | C0 r => reduce_%i r" i;
1120
pr " | C1 r => zero";
1123
pr " | %sn n wx =>" c;
1124
pr " let op := make_op n in";
1125
pr " match op.(znz_pred_c) wx with";
1126
pr " | C0 r => reduce_n n r";
1127
pr " | C1 r => zero";
1132
pr " Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.";
1135
pp " intros x; case x; unfold pred.";
1136
for i = 0 to size do
1137
pp " intros x1 H1; unfold w%i_pred_c; " i;
1138
pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i;
1139
pp " rewrite spec_reduce_%i; auto." i;
1140
pp " unfold interp_carry; unfold to_Z.";
1141
pp " case (spec_to_Z w%i_spec x1); intros HH1 HH2." i;
1142
pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4 HH5." i;
1143
pp " assert (znz_to_Z w%i_op x1 - 1 < 0); auto with zarith." i;
1144
pp " unfold to_Z in H1; auto with zarith.";
1146
pp " intros n x1 H1; ";
1147
pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.";
1148
pp " rewrite spec_reduce_n; auto.";
1149
pp " unfold interp_carry; unfold to_Z.";
1150
pp " case (spec_to_Z (wn_spec n) x1); intros HH1 HH2.";
1151
pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4 HH5.";
1152
pp " assert (znz_to_Z (make_op n) x1 - 1 < 0); auto with zarith.";
1153
pp " unfold to_Z in H1; auto with zarith.";
1157
pp " Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0.";
1159
pp " intros x; case x; unfold pred.";
1160
for i = 0 to size do
1161
pp " intros x1 H1; unfold w%i_pred_c; " i;
1162
pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i;
1163
pp " unfold interp_carry; unfold to_Z.";
1164
pp " unfold to_Z in H1; auto with zarith.";
1165
pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4; auto with zarith." i;
1166
pp " intros; exact (spec_0 w0_spec).";
1168
pp " intros n x1 H1; ";
1169
pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.";
1170
pp " unfold interp_carry; unfold to_Z.";
1171
pp " unfold to_Z in H1; auto with zarith.";
1172
pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith.";
1173
pp " intros; exact (spec_0 w0_spec).";
1178
pr " (***************************************************************)";
1180
pr " (* Subtraction *)";
1182
pr " (***************************************************************)";
1185
for i = 0 to size do
1186
pr " Definition w%i_sub_c := w%i_op.(znz_sub_c)." i i
1190
for i = 0 to size do
1191
pr " Definition w%i_sub x y :=" i;
1192
pr " match w%i_sub_c x y with" i;
1193
pr " | C0 r => reduce_%i r" i;
1194
pr " | C1 r => zero";
1199
pr " Definition subn n (x y : word w%i (S n)) :=" size;
1200
pr " let op := make_op n in";
1201
pr " match op.(znz_sub_c) x y with";
1202
pr " | C0 r => %sn n r" c;
1203
pr " | C1 r => N0 w_0";
1207
for i = 0 to size do
1208
pp " Let spec_w%i_sub: forall x y, [%s%i y] <= [%s%i x] -> [w%i_sub x y] = [%s%i x] - [%s%i y]." i c i c i i c i c i;
1210
pp " intros n m; unfold w%i_sub, w%i_sub_c." i i;
1211
pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; " i;
1213
pp " intros x; auto."
1215
pp " intros x; try rewrite spec_reduce_%i; auto." i;
1216
pp " unfold interp_carry; unfold zero, w_0, to_Z.";
1217
pp " rewrite (spec_0 w0_spec).";
1218
pp " case (spec_to_Z w%i_spec x); intros; auto with zarith." i;
1223
pp " Let spec_wn_sub: forall n x y, [%sn n y] <= [%sn n x] -> [subn n x y] = [%sn n x] - [%sn n y]." c c c c;
1225
pp " intros k n m; unfold subn.";
1226
pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; ";
1227
pp " intros x; auto.";
1228
pp " unfold interp_carry, to_Z.";
1229
pp " case (spec_to_Z (wn_spec k) x); intros; auto with zarith.";
1233
pr " Definition sub := Eval lazy beta delta [same_level] in";
1234
pr0 " (same_level t_ ";
1235
for i = 0 to size do
1241
pr " Theorem spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y].";
1245
pp " generalize (spec_same_level t_ (fun x y res => y <= x -> [res] = x - y)).";
1246
pp " unfold same_level; intros HH; apply HH; clear HH.";
1247
for i = 0 to size do
1248
pp " exact spec_w%i_sub." i;
1250
pp " exact spec_wn_sub.";
1254
for i = 0 to size do
1255
pp " Let spec_w%i_sub0: forall x y, [%s%i x] < [%s%i y] -> [w%i_sub x y] = 0." i c i c i i;
1257
pp " intros n m; unfold w%i_sub, w%i_sub_c." i i;
1258
pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; " i;
1259
pp " intros x; unfold interp_carry.";
1260
pp " unfold to_Z; case (spec_to_Z w%i_spec x); intros; auto with zarith." i;
1261
pp " intros; unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto.";
1266
pp " Let spec_wn_sub0: forall n x y, [%sn n x] < [%sn n y] -> [subn n x y] = 0." c c;
1268
pp " intros k n m; unfold subn.";
1269
pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; ";
1270
pp " intros x; unfold interp_carry.";
1271
pp " unfold to_Z; case (spec_to_Z (wn_spec k) x); intros; auto with zarith.";
1272
pp " intros; unfold to_Z, w_0; rewrite (spec_0 (w0_spec)); auto.";
1276
pr " Theorem spec_sub0: forall x y, [x] < [y] -> [sub x y] = 0.";
1280
pp " generalize (spec_same_level t_ (fun x y res => x < y -> [res] = 0)).";
1281
pp " unfold same_level; intros HH; apply HH; clear HH.";
1282
for i = 0 to size do
1283
pp " exact spec_w%i_sub0." i;
1285
pp " exact spec_wn_sub0.";
1290
pr " (***************************************************************)";
1292
pr " (* Comparison *)";
1294
pr " (***************************************************************)";
1297
for i = 0 to size do
1298
pr " Definition compare_%i := w%i_op.(znz_compare)." i i;
1299
pr " Definition comparen_%i :=" i;
1300
pr " compare_mn_1 w%i w%i %s compare_%i (compare_%i %s) compare_%i." i i (pz i) i i (pz i) i
1304
pr " Definition comparenm n m wx wy :=";
1305
pr " let mn := Max.max n m in";
1306
pr " let d := diff n m in";
1307
pr " let op := make_op mn in";
1308
pr " op.(znz_compare)";
1309
pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
1310
pr " (castm (diff_l n m) (extend_tr wy (fst d))).";
1313
pr " Definition compare := Eval lazy beta delta [iter] in ";
1315
for i = 0 to size do
1317
pr " (fun n x y => opp_compare (comparen_%i (S n) y x))" i;
1318
pr " (fun n => comparen_%i (S n))" i;
1323
pr " Definition lt n m := compare n m = Lt.";
1324
pr " Definition le n m := compare n m <> Gt.";
1325
pr " Definition min n m := match compare n m with Gt => m | _ => n end.";
1326
pr " Definition max n m := match compare n m with Lt => m | _ => n end.";
1329
for i = 0 to size do
1330
pp " Let spec_compare_%i: forall x y," i;
1331
pp " match compare_%i x y with " i;
1332
pp " Eq => [%s%i x] = [%s%i y]" c i c i;
1333
pp " | Lt => [%s%i x] < [%s%i y]" c i c i;
1334
pp " | Gt => [%s%i x] > [%s%i y]" c i c i;
1337
pp " unfold compare_%i, to_Z; exact (spec_compare w%i_spec)." i i;
1341
pp " Let spec_comparen_%i:" i;
1342
pp " forall (n : nat) (x : word w%i n) (y : w%i)," i i;
1343
pp " match comparen_%i n x y with" i;
1344
pp " | Eq => eval%in n x = [%s%i y]" i c i;
1345
pp " | Lt => eval%in n x < [%s%i y]" i c i;
1346
pp " | Gt => eval%in n x > [%s%i y]" i c i;
1348
pp " intros n x y.";
1349
pp " unfold comparen_%i, to_Z; rewrite spec_double_eval%in." i i;
1350
pp " apply spec_compare_mn_1.";
1351
pp " exact (spec_0 w%i_spec)." i;
1352
pp " intros x1; exact (spec_compare w%i_spec %s x1)." i (pz i);
1353
pp " exact (spec_to_Z w%i_spec)." i;
1354
pp " exact (spec_compare w%i_spec)." i;
1355
pp " exact (spec_compare w%i_spec)." i;
1356
pp " exact (spec_to_Z w%i_spec)." i;
1361
pp " Let spec_opp_compare: forall c (u v: Z),";
1362
pp " match c with Eq => u = v | Lt => u < v | Gt => u > v end ->";
1363
pp " match opp_compare c with Eq => v = u | Lt => v < u | Gt => v > u end.";
1365
pp " intros c u v; case c; unfold opp_compare; auto with zarith.";
1370
pr " Theorem spec_compare: forall x y,";
1371
pr " match compare x y with ";
1372
pr " Eq => [x] = [y]";
1373
pr " | Lt => [x] < [y]";
1374
pr " | Gt => [x] > [y]";
1378
pp " refine (spec_iter _ (fun x y res => ";
1379
pp " match res with ";
1381
pp " | Lt => x < y";
1382
pp " | Gt => x > y";
1384
for i = 0 to size do
1386
pp " (fun n x y => opp_compare (comparen_%i (S n) y x))" i;
1387
pp " (fun n => comparen_%i (S n)) _ _ _" i;
1389
pp " comparenm _).";
1391
for i = 0 to size - 1 do
1392
pp " exact spec_compare_%i." i;
1393
pp " intros n x y H;apply spec_opp_compare; apply spec_comparen_%i." i;
1394
pp " intros n x y H; exact (spec_comparen_%i (S n) x y)." i;
1396
pp " exact spec_compare_%i." size;
1397
pp " intros n x y;apply spec_opp_compare; apply spec_comparen_%i." size;
1398
pp " intros n; exact (spec_comparen_%i (S n))." size;
1399
pp " intros n m x y; unfold comparenm.";
1400
pp " rewrite <- (spec_cast_l n m x); rewrite <- (spec_cast_r n m y).";
1401
pp " unfold to_Z; apply (spec_compare (wn_spec (Max.max n m))).";
1405
pr " Definition eq_bool x y :=";
1406
pr " match compare x y with";
1413
pr " Theorem spec_eq_bool: forall x y,";
1414
pr " if eq_bool x y then [x] = [y] else [x] <> [y].";
1417
pp " intros x y; unfold eq_bool.";
1418
pp " generalize (spec_compare x y); case compare; auto with zarith.";
1424
pr " (***************************************************************)";
1426
pr " (* Multiplication *)";
1428
pr " (***************************************************************)";
1431
for i = 0 to size do
1432
pr " Definition w%i_mul_c := w%i_op.(znz_mul_c)." i i
1436
for i = 0 to size do
1437
pr " Definition w%i_mul_add :=" i;
1438
pr " Eval lazy beta delta [w_mul_add] in";
1439
pr " @w_mul_add w%i %s w%i_succ w%i_add_c w%i_mul_c." i (pz i) i i i
1443
for i = 0 to size do
1444
pr " Definition w%i_0W := znz_0W w%i_op." i i
1448
for i = 0 to size do
1449
pr " Definition w%i_WW := znz_WW w%i_op." i i
1453
for i = 0 to size do
1454
pr " Definition w%i_mul_add_n1 :=" i;
1455
pr " @double_mul_add_n1 w%i %s w%i_WW w%i_0W w%i_mul_add." i (pz i) i i i
1459
for i = 0 to size - 1 do
1460
pr " Let to_Z%i n :=" i;
1461
pr " match n return word w%i (S n) -> t_ with" i;
1462
for j = 0 to size - i do
1463
if (i + j) == size then
1465
pr " | %i%s => fun x => %sn 0 x" j "%nat" c;
1466
pr " | %i%s => fun x => %sn 1 x" (j + 1) "%nat" c
1469
pr " | %i%s => fun x => %s%i x" j "%nat" c (i + j + 1)
1471
pr " | _ => fun _ => N0 w_0";
1477
for i = 0 to size - 1 do
1478
pp "Theorem to_Z%i_spec:" i;
1479
pp " forall n x, Z_of_nat n <= %i -> [to_Z%i n x] = znz_to_Z (nmake_op _ w%i_op (S n)) x." (size + 1 - i) i i;
1480
for j = 1 to size + 2 - i do
1481
pp " intros n; case n; clear n.";
1482
pp " unfold to_Z%i." i;
1483
pp " intros x H; rewrite spec_eval%in%i; auto." i j;
1486
pp " repeat rewrite inj_S; unfold Zsucc; auto with zarith.";
1492
for i = 0 to size do
1493
pr " Definition w%i_mul n x y :=" i;
1494
pr " let (w,r) := w%i_mul_add_n1 (S n) x y %s in" i (pz i);
1497
pr " if w%i_eq0 w then %sn n r" i c;
1498
pr " else %sn (S n) (WW (extend%i n w) r)." c i;
1502
pr " if w%i_eq0 w then to_Z%i n r" i i;
1503
pr " else to_Z%i (S n) (WW (extend%i n w) r)." i i;
1508
pr " Definition mulnm n m x y :=";
1509
pr " let mn := Max.max n m in";
1510
pr " let d := diff n m in";
1511
pr " let op := make_op mn in";
1512
pr " reduce_n (S mn) (op.(znz_mul_c)";
1513
pr " (castm (diff_r n m) (extend_tr x (snd d)))";
1514
pr " (castm (diff_l n m) (extend_tr y (fst d)))).";
1517
pr " Definition mul := Eval lazy beta delta [iter0] in ";
1519
for i = 0 to size do
1520
pr " (fun x y => reduce_%i (w%i_mul_c x y)) " (i + 1) i;
1521
pr " (fun n x y => w%i_mul n y x)" i;
1525
pr " (fun _ => N0 w_0)";
1526
pr " (fun _ => N0 w_0)";
1529
for i = 0 to size do
1530
pp " Let spec_w%i_mul_add: forall x y z," i;
1531
pp " let (q,r) := w%i_mul_add x y z in" i;
1532
pp " znz_to_Z w%i_op q * (base (znz_digits w%i_op)) + znz_to_Z w%i_op r =" i i i;
1533
pp " znz_to_Z w%i_op x * znz_to_Z w%i_op y + znz_to_Z w%i_op z :=" i i i ;
1534
pp " (spec_mul_add w%i_spec)." i;
1538
for i = 0 to size do
1539
pp " Theorem spec_w%i_mul_add_n1: forall n x y z," i;
1540
pp " let (q,r) := w%i_mul_add_n1 n x y z in" i;
1541
pp " znz_to_Z w%i_op q * (base (znz_digits (nmake_op _ w%i_op n))) +" i i;
1542
pp " znz_to_Z (nmake_op _ w%i_op n) r =" i;
1543
pp " znz_to_Z (nmake_op _ w%i_op n) x * znz_to_Z w%i_op y +" i i;
1544
pp " znz_to_Z w%i_op z." i;
1546
pp " intros n x y z; unfold w%i_mul_add_n1." i;
1547
pp " rewrite nmake_double.";
1548
pp " rewrite digits_doubled.";
1549
pp " change (base (DoubleBase.double_digits (znz_digits w%i_op) n)) with" i;
1550
pp " (DoubleBase.double_wB (znz_digits w%i_op) n)." i;
1551
pp " apply spec_double_mul_add_n1; auto.";
1552
if i == 0 then pp " exact (spec_0 w%i_spec)." i;
1553
pp " exact (spec_WW w%i_spec)." i;
1554
pp " exact (spec_0W w%i_spec)." i;
1555
pp " exact (spec_mul_add w%i_spec)." i;
1560
pp " Lemma nmake_op_WW: forall ww ww1 n x y,";
1561
pp " znz_to_Z (nmake_op ww ww1 (S n)) (WW x y) =";
1562
pp " znz_to_Z (nmake_op ww ww1 n) x * base (znz_digits (nmake_op ww ww1 n)) +";
1563
pp " znz_to_Z (nmake_op ww ww1 n) y.";
1568
for i = 0 to size do
1569
pp " Lemma extend%in_spec: forall n x1," i;
1570
pp " znz_to_Z (nmake_op _ w%i_op (S n)) (extend%i n x1) = " i i;
1571
pp " znz_to_Z w%i_op x1." i;
1573
pp " intros n1 x2; rewrite nmake_double.";
1574
pp " unfold extend%i." i;
1575
pp " rewrite DoubleBase.spec_extend; auto.";
1577
pp " intros l; simpl; unfold w_0; rewrite (spec_0 w0_spec); ring.";
1582
pp " Lemma spec_muln:";
1583
pp " forall n (x: word _ (S n)) y,";
1584
pp " [%sn (S n) (znz_mul_c (make_op n) x y)] = [%sn n x] * [%sn n y]." c c c;
1586
pp " intros n x y; unfold to_Z.";
1587
pp " rewrite <- (spec_mul_c (wn_spec n)).";
1588
pp " rewrite make_op_S.";
1589
pp " case znz_mul_c; auto.";
1592
pr " Theorem spec_mul: forall x y, [mul x y] = [x] * [y].";
1595
for i = 0 to size do
1596
pp " assert(F%i: " i;
1597
pp " forall n x y,";
1599
pp0 " Z_of_nat n <= %i -> " (size - i);
1600
pp " [w%i_mul n x y] = eval%in (S n) x * [%s%i y])." i i c i;
1602
pp " intros n x y; unfold w%i_mul." i
1604
pp " intros n x y H; unfold w%i_mul." i;
1605
pp " generalize (spec_w%i_mul_add_n1 (S n) x y %s)." i (pz i);
1606
pp " case w%i_mul_add_n1; intros x1 y1." i;
1607
pp " change (znz_to_Z (nmake_op _ w%i_op (S n)) x) with (eval%in (S n) x)." i i;
1608
pp " change (znz_to_Z w%i_op y) with ([%s%i y])." i c i;
1610
pp " unfold w_0; rewrite (spec_0 w0_spec); rewrite Zplus_0_r."
1612
pp " change (znz_to_Z w%i_op W0) with 0; rewrite Zplus_0_r." i;
1613
pp " intros H1; rewrite <- H1; clear H1.";
1614
pp " generalize (spec_w%i_eq0 x1); case w%i_eq0; intros HH." i i;
1615
pp " unfold to_Z in HH; rewrite HH.";
1618
pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i; auto." i i i;
1619
pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i." i i i
1623
pp " rewrite to_Z%i_spec; auto with zarith." i;
1624
pp " rewrite to_Z%i_spec; try (rewrite inj_S; auto with zarith)." i
1626
pp " rewrite nmake_op_WW; rewrite extend%in_spec; auto." i;
1628
pp " refine (spec_iter0 t_ (fun x y res => [res] = x * y)";
1629
for i = 0 to size do
1630
pp " (fun x y => reduce_%i (w%i_mul_c x y)) " (i + 1) i;
1631
pp " (fun n x y => w%i_mul n y x)" i;
1632
pp " w%i_mul _ _ _" i;
1635
pp " (fun _ => N0 w_0) _";
1636
pp " (fun _ => N0 w_0) _";
1638
for i = 0 to size do
1639
pp " intros x y; rewrite spec_reduce_%i." (i + 1);
1640
pp " unfold w%i_mul_c, to_Z." i;
1641
pp " generalize (spec_mul_c w%i_spec x y)." i;
1642
pp " intros HH; rewrite <- HH; clear HH; auto.";
1645
pp " intros n x y; rewrite F%i; auto with zarith." i;
1646
pp " intros n x y; rewrite F%i; auto with zarith. " i;
1650
pp " intros n x y H; rewrite F%i; auto with zarith." i;
1651
pp " intros n x y H; rewrite F%i; auto with zarith. " i;
1654
pp " intros n m x y; unfold mulnm.";
1655
pp " rewrite spec_reduce_n.";
1656
pp " rewrite <- (spec_cast_l n m x).";
1657
pp " rewrite <- (spec_cast_r n m y).";
1658
pp " rewrite spec_muln; rewrite spec_cast_l; rewrite spec_cast_r; auto.";
1659
pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring.";
1660
pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring.";
1664
pr " (***************************************************************)";
1668
pr " (***************************************************************)";
1671
for i = 0 to size do
1672
pr " Definition w%i_square_c := w%i_op.(znz_square_c)." i i
1676
pr " Definition square x :=";
1678
pr " | %s0 wx => reduce_1 (w0_square_c wx)" c;
1679
for i = 1 to size - 1 do
1680
pr " | %s%i wx => %s%i (w%i_square_c wx)" c i c (i+1) i
1682
pr " | %s%i wx => %sn 0 (w%i_square_c wx)" c size c size;
1683
pr " | %sn n wx =>" c;
1684
pr " let op := make_op n in";
1685
pr " %sn (S n) (op.(znz_square_c) wx)" c;
1689
pr " Theorem spec_square: forall x, [square x] = [x] * [x].";
1692
pp " intros x; case x; unfold square; clear x.";
1693
pp " intros x; rewrite spec_reduce_1; unfold to_Z.";
1694
pp " exact (spec_square_c w%i_spec x)." 0;
1695
for i = 1 to size do
1696
pp " intros x; unfold to_Z.";
1697
pp " exact (spec_square_c w%i_spec x)." i;
1699
pp " intros n x; unfold to_Z.";
1700
pp " rewrite make_op_S.";
1701
pp " exact (spec_square_c (wn_spec n) x).";
1706
pr " (***************************************************************)";
1710
pr " (***************************************************************)";
1713
pr " Fixpoint power_pos (x:%s) (p:positive) {struct p} : %s :=" t t;
1716
pr " | xO p => square (power_pos x p)";
1717
pr " | xI p => mul (square (power_pos x p)) x";
1721
pr " Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.";
1724
pp " intros x n; generalize x; elim n; clear n x; simpl power_pos.";
1725
pp " intros; rewrite spec_mul; rewrite spec_square; rewrite H.";
1726
pp " rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith.";
1727
pp " rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.";
1728
pp " rewrite Zpower_2; rewrite Zpower_1_r; auto.";
1729
pp " intros; rewrite spec_square; rewrite H.";
1730
pp " rewrite Zpos_xO; auto with zarith.";
1731
pp " rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.";
1732
pp " rewrite Zpower_2; auto.";
1733
pp " intros; rewrite Zpower_1_r; auto.";
1738
pr " (***************************************************************)";
1740
pr " (* Square root *)";
1742
pr " (***************************************************************)";
1745
for i = 0 to size do
1746
pr " Definition w%i_sqrt := w%i_op.(znz_sqrt)." i i
1750
pr " Definition sqrt x :=";
1752
for i = 0 to size do
1753
pr " | %s%i wx => reduce_%i (w%i_sqrt wx)" c i i i;
1755
pr " | %sn n wx =>" c;
1756
pr " let op := make_op n in";
1757
pr " reduce_n n (op.(znz_sqrt) wx)";
1761
pr " Theorem spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.";
1764
pp " intros x; unfold sqrt; case x; clear x.";
1765
for i = 0 to size do
1766
pp " intros x; rewrite spec_reduce_%i; exact (spec_sqrt w%i_spec x)." i i;
1768
pp " intros n x; rewrite spec_reduce_n; exact (spec_sqrt (wn_spec n) x).";
1773
pr " (***************************************************************)";
1775
pr " (* Division *)";
1777
pr " (***************************************************************)";
1780
for i = 0 to size do
1781
pr " Definition w%i_div_gt := w%i_op.(znz_div_gt)." i i
1785
pp " Let spec_divn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := ";
1786
pp " (spec_double_divn1 ";
1787
pp " ww_op.(znz_zdigits) ww_op.(znz_0)";
1788
pp " (znz_WW ww_op) ww_op.(znz_head0)";
1789
pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)";
1790
pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)";
1791
pp " (spec_to_Z ww_spec) ";
1792
pp " (spec_zdigits ww_spec)";
1793
pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)";
1794
pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) ";
1795
pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec)).";
1798
for i = 0 to size do
1799
pr " Definition w%i_divn1 n x y :=" i;
1800
pr " let (u, v) :=";
1801
pr " double_divn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i;
1802
pr " (znz_WW w%i_op) w%i_op.(znz_head0)" i i;
1803
pr " w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i;
1804
pr " w%i_op.(znz_compare) w%i_op.(znz_sub) (S n) x y in" i i;
1806
pr " (%sn _ u, %s%i v)." c c i
1808
pr " (to_Z%i _ u, %s%i v)." i c i;
1812
for i = 0 to size do
1813
pp " Lemma spec_get_end%i: forall n x y," i;
1814
pp " eval%in n x <= [%s%i y] -> " i c i;
1815
pp " [%s%i (DoubleBase.get_low %s n x)] = eval%in n x." c i (pz i) i;
1817
pp " intros n x y H.";
1818
pp " rewrite spec_double_eval%in; unfold to_Z." i;
1819
pp " apply DoubleBase.spec_get_low.";
1820
pp " exact (spec_0 w%i_spec)." i;
1821
pp " exact (spec_to_Z w%i_spec)." i;
1822
pp " apply Zle_lt_trans with [%s%i y]; auto." c i;
1823
pp " rewrite <- spec_double_eval%in; auto." i;
1824
pp " unfold to_Z; case (spec_to_Z w%i_spec y); auto." i;
1829
for i = 0 to size do
1830
pr " Let div_gt%i x y := let (u,v) := (w%i_div_gt x y) in (reduce_%i u, reduce_%i v)." i i i i;
1835
pr " Let div_gtnm n m wx wy :=";
1836
pr " let mn := Max.max n m in";
1837
pr " let d := diff n m in";
1838
pr " let op := make_op mn in";
1839
pr " let (q, r):= op.(znz_div_gt)";
1840
pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
1841
pr " (castm (diff_l n m) (extend_tr wy (fst d))) in";
1842
pr " (reduce_n mn q, reduce_n mn r).";
1845
pr " Definition div_gt := Eval lazy beta delta [iter] in";
1847
for i = 0 to size do
1849
pr " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i);
1855
pr " Theorem spec_div_gt: forall x y,";
1856
pr " [x] > [y] -> 0 < [y] ->";
1857
pr " let (q,r) := div_gt x y in";
1858
pr " [q] = [x] / [y] /\\ [r] = [x] mod [y].";
1862
pp " forall x y, [x] > [y] -> 0 < [y] ->";
1863
pp " let (q,r) := div_gt x y in";
1864
pp " [x] = [q] * [y] + [r] /\\ 0 <= [r] < [y]).";
1865
pp " refine (spec_iter (t_*t_) (fun x y res => x > y -> 0 < y ->";
1866
pp " let (q,r) := res in";
1867
pp " x = [q] * y + [r] /\\ 0 <= [r] < y)";
1868
for i = 0 to size do
1870
pp " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i);
1871
pp " w%i_divn1 _ _ _" i;
1874
for i = 0 to size do
1875
pp " intros x y H1 H2; unfold div_gt%i, w%i_div_gt." i i;
1876
pp " generalize (spec_div_gt w%i_spec x y H1 H2); case znz_div_gt." i;
1877
pp " intros xx yy; repeat rewrite spec_reduce_%i; auto." i;
1879
pp " intros n x y H2 H3; unfold div_gt%i, w%i_div_gt." i i
1881
pp " intros n x y H1 H2 H3; unfold div_gt%i, w%i_div_gt." i i;
1882
pp " generalize (spec_div_gt w%i_spec x " i;
1883
pp " (DoubleBase.get_low %s (S n) y))." (pz i);
1886
pp0 "unfold w%i; " (i-j);
1888
pp "case znz_div_gt.";
1889
pp " intros xx yy H4; repeat rewrite spec_reduce_%i." i;
1890
pp " generalize (spec_get_end%i (S n) y x); unfold to_Z; intros H5." i;
1891
pp " unfold to_Z in H2; rewrite H5 in H4; auto with zarith.";
1893
pp " intros n x y H2 H3."
1895
pp " intros n x y H1 H2 H3.";
1897
pp " (spec_divn1 w%i w%i_op w%i_spec (S n) x y H3)." i i i;
1898
pp0 " unfold w%i_divn1; " i;
1900
pp0 "unfold w%i; " (i-j);
1902
pp "case double_divn1.";
1903
pp " intros xx yy H4.";
1906
pp " repeat rewrite <- spec_double_eval%in in H4; auto." i;
1907
pp " rewrite spec_eval%in; auto." i;
1911
pp " rewrite to_Z%i_spec; auto with zarith." i;
1912
pp " repeat rewrite <- spec_double_eval%in in H4; auto." i;
1915
pp " intros n m x y H1 H2; unfold div_gtnm.";
1916
pp " generalize (spec_div_gt (wn_spec (Max.max n m))";
1917
pp " (castm (diff_r n m)";
1918
pp " (extend_tr x (snd (diff n m))))";
1919
pp " (castm (diff_l n m)";
1920
pp " (extend_tr y (fst (diff n m))))).";
1921
pp " case znz_div_gt.";
1922
pp " intros xx yy HH.";
1923
pp " repeat rewrite spec_reduce_n.";
1924
pp " rewrite <- (spec_cast_l n m x).";
1925
pp " rewrite <- (spec_cast_r n m y).";
1926
pp " unfold to_Z; apply HH.";
1927
pp " rewrite <- (spec_cast_l n m x) in H1; auto.";
1928
pp " rewrite <- (spec_cast_r n m y) in H1; auto.";
1929
pp " rewrite <- (spec_cast_r n m y) in H2; auto.";
1930
pp " intros x y H1 H2; generalize (FO x y H1 H2); case div_gt.";
1931
pp " intros q r (H3, H4); split.";
1932
pp " apply (Zdiv_unique [x] [y] [q] [r]); auto.";
1933
pp " rewrite Zmult_comm; auto.";
1934
pp " apply (Zmod_unique [x] [y] [q] [r]); auto.";
1935
pp " rewrite Zmult_comm; auto.";
1939
pr " Definition div_eucl x y :=";
1940
pr " match compare x y with";
1941
pr " | Eq => (one, zero)";
1942
pr " | Lt => (zero, x)";
1943
pr " | Gt => div_gt x y";
1947
pr " Theorem spec_div_eucl: forall x y,";
1949
pr " let (q,r) := div_eucl x y in";
1950
pr " ([q], [r]) = Zdiv_eucl [x] [y].";
1953
pp " assert (F0: [zero] = 0).";
1954
pp " exact (spec_0 w0_spec).";
1955
pp " assert (F1: [one] = 1).";
1956
pp " exact (spec_1 w0_spec).";
1957
pp " intros x y H; generalize (spec_compare x y);";
1958
pp " unfold div_eucl; case compare; try rewrite F0;";
1959
pp " try rewrite F1; intros; auto with zarith.";
1960
pp " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))";
1961
pp " (Z_mod_same [y] (Zlt_gt _ _ H));";
1962
pp " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.";
1963
pp " assert (F2: 0 <= [x] < [y]).";
1964
pp " generalize (spec_pos x); auto.";
1965
pp " generalize (Zdiv_small _ _ F2)";
1966
pp " (Zmod_small _ _ F2);";
1967
pp " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.";
1968
pp " generalize (spec_div_gt _ _ H0 H); auto.";
1969
pp " unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt.";
1970
pp " intros a b c d (H1, H2); subst; auto.";
1974
pr " Definition div x y := fst (div_eucl x y).";
1977
pr " Theorem spec_div:";
1978
pr " forall x y, 0 < [y] -> [div x y] = [x] / [y].";
1981
pp " intros x y H1; unfold div; generalize (spec_div_eucl x y H1);";
1982
pp " case div_eucl; simpl fst.";
1983
pp " intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; ";
1984
pp " injection H; auto.";
1988
pr " (***************************************************************)";
1992
pr " (***************************************************************)";
1995
for i = 0 to size do
1996
pr " Definition w%i_mod_gt := w%i_op.(znz_mod_gt)." i i
2000
for i = 0 to size do
2001
pr " Definition w%i_modn1 :=" i;
2002
pr " double_modn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i;
2003
pr " w%i_op.(znz_head0) w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i i;
2004
pr " w%i_op.(znz_compare) w%i_op.(znz_sub)." i i;
2008
pr " Let mod_gtnm n m wx wy :=";
2009
pr " let mn := Max.max n m in";
2010
pr " let d := diff n m in";
2011
pr " let op := make_op mn in";
2012
pr " reduce_n mn (op.(znz_mod_gt)";
2013
pr " (castm (diff_r n m) (extend_tr wx (snd d)))";
2014
pr " (castm (diff_l n m) (extend_tr wy (fst d)))).";
2017
pr " Definition mod_gt := Eval lazy beta delta[iter] in";
2019
for i = 0 to size do
2020
pr " (fun x y => reduce_%i (w%i_mod_gt x y))" i i;
2021
pr " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i);
2022
pr " (fun n x y => reduce_%i (w%i_modn1 (S n) x y))" i i;
2027
pp " Let spec_modn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := ";
2028
pp " (spec_double_modn1 ";
2029
pp " ww_op.(znz_zdigits) ww_op.(znz_0)";
2030
pp " (znz_WW ww_op) ww_op.(znz_head0)";
2031
pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)";
2032
pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)";
2033
pp " (spec_to_Z ww_spec) ";
2034
pp " (spec_zdigits ww_spec)";
2035
pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)";
2036
pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) ";
2037
pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec)).";
2040
pr " Theorem spec_mod_gt:";
2041
pr " forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y].";
2044
pp " refine (spec_iter _ (fun x y res => x > y -> 0 < y ->";
2045
pp " [res] = x mod y)";
2046
for i = 0 to size do
2047
pp " (fun x y => reduce_%i (w%i_mod_gt x y))" i i;
2048
pp " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i);
2049
pp " (fun n x y => reduce_%i (w%i_modn1 (S n) x y)) _ _ _" i i;
2052
for i = 0 to size do
2053
pp " intros x y H1 H2; rewrite spec_reduce_%i." i;
2054
pp " exact (spec_mod_gt w%i_spec x y H1 H2)." i;
2056
pp " intros n x y H2 H3; rewrite spec_reduce_%i." i
2058
pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i;
2059
pp " unfold w%i_mod_gt." i;
2060
pp " rewrite <- (spec_get_end%i (S n) y x); auto with zarith." i;
2061
pp " unfold to_Z; apply (spec_mod_gt w%i_spec); auto." i;
2062
pp " rewrite <- (spec_get_end%i (S n) y x) in H2; auto with zarith." i;
2063
pp " rewrite <- (spec_get_end%i (S n) y x) in H3; auto with zarith." i;
2065
pp " intros n x y H2 H3; rewrite spec_reduce_%i." i
2067
pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i;
2068
pp " unfold w%i_modn1, to_Z; rewrite spec_double_eval%in." i i;
2069
pp " apply (spec_modn1 _ _ w%i_spec); auto." i;
2071
pp " intros n m x y H1 H2; unfold mod_gtnm.";
2072
pp " repeat rewrite spec_reduce_n.";
2073
pp " rewrite <- (spec_cast_l n m x).";
2074
pp " rewrite <- (spec_cast_r n m y).";
2075
pp " unfold to_Z; apply (spec_mod_gt (wn_spec (Max.max n m))).";
2076
pp " rewrite <- (spec_cast_l n m x) in H1; auto.";
2077
pp " rewrite <- (spec_cast_r n m y) in H1; auto.";
2078
pp " rewrite <- (spec_cast_r n m y) in H2; auto.";
2082
pr " Definition modulo x y := ";
2083
pr " match compare x y with";
2086
pr " | Gt => mod_gt x y";
2090
pr " Theorem spec_modulo:";
2091
pr " forall x y, 0 < [y] -> [modulo x y] = [x] mod [y].";
2094
pp " assert (F0: [zero] = 0).";
2095
pp " exact (spec_0 w0_spec).";
2096
pp " assert (F1: [one] = 1).";
2097
pp " exact (spec_1 w0_spec).";
2098
pp " intros x y H; generalize (spec_compare x y);";
2099
pp " unfold modulo; case compare; try rewrite F0;";
2100
pp " try rewrite F1; intros; try split; auto with zarith.";
2101
pp " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith.";
2102
pp " apply sym_equal; apply Zmod_small; auto with zarith.";
2103
pp " generalize (spec_pos x); auto with zarith.";
2104
pp " apply spec_mod_gt; auto.";
2108
pr " (***************************************************************)";
2112
pr " (***************************************************************)";
2115
pr " Definition digits x :=";
2117
for i = 0 to size do
2118
pr " | %s%i _ => w%i_op.(znz_digits)" c i i;
2120
pr " | %sn n _ => (make_op n).(znz_digits)" c;
2124
pr " Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x).";
2127
pp " intros x; case x; clear x.";
2128
for i = 0 to size do
2129
pp " intros x; unfold to_Z, digits;";
2130
pp " generalize (spec_to_Z w%i_spec x); unfold base; intros H; exact H." i;
2132
pp " intros n x; unfold to_Z, digits;";
2133
pp " generalize (spec_to_Z (wn_spec n) x); unfold base; intros H; exact H.";
2137
pr " Definition gcd_gt_body a b cont :=";
2138
pr " match compare b zero with";
2140
pr " let r := mod_gt a b in";
2141
pr " match compare r zero with";
2142
pr " | Gt => cont r (mod_gt b r)";
2149
pp " Theorem Zspec_gcd_gt_body: forall a b cont p,";
2150
pp " [a] > [b] -> [a] < 2 ^ p ->";
2151
pp " (forall a1 b1, [a1] < 2 ^ (p - 1) -> [a1] > [b1] ->";
2152
pp " Zis_gcd [a1] [b1] [cont a1 b1]) -> ";
2153
pp " Zis_gcd [a] [b] [gcd_gt_body a b cont].";
2155
pp " assert (F1: [zero] = 0).";
2156
pp " unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto.";
2157
pp " intros a b cont p H2 H3 H4; unfold gcd_gt_body.";
2158
pp " generalize (spec_compare b zero); case compare; try rewrite F1.";
2159
pp " intros HH; rewrite HH; apply Zis_gcd_0.";
2160
pp " intros HH; absurd (0 <= [b]); auto with zarith.";
2161
pp " case (spec_digits b); auto with zarith.";
2162
pp " intros H5; generalize (spec_compare (mod_gt a b) zero); ";
2163
pp " case compare; try rewrite F1.";
2164
pp " intros H6; rewrite <- (Zmult_1_r [b]).";
2165
pp " rewrite (Z_div_mod_eq [a] [b]); auto with zarith.";
2166
pp " rewrite <- spec_mod_gt; auto with zarith.";
2167
pp " rewrite H6; rewrite Zplus_0_r.";
2168
pp " apply Zis_gcd_mult; apply Zis_gcd_1.";
2169
pp " intros; apply False_ind.";
2170
pp " case (spec_digits (mod_gt a b)); auto with zarith.";
2171
pp " intros H6; apply DoubleDiv.Zis_gcd_mod; auto with zarith.";
2172
pp " apply DoubleDiv.Zis_gcd_mod; auto with zarith.";
2173
pp " rewrite <- spec_mod_gt; auto with zarith.";
2174
pp " assert (F2: [b] > [mod_gt a b]).";
2175
pp " case (Z_mod_lt [a] [b]); auto with zarith.";
2176
pp " repeat rewrite <- spec_mod_gt; auto with zarith.";
2177
pp " assert (F3: [mod_gt a b] > [mod_gt b (mod_gt a b)]).";
2178
pp " case (Z_mod_lt [b] [mod_gt a b]); auto with zarith.";
2179
pp " rewrite <- spec_mod_gt; auto with zarith.";
2180
pp " repeat rewrite <- spec_mod_gt; auto with zarith.";
2181
pp " apply H4; auto with zarith.";
2182
pp " apply Zmult_lt_reg_r with 2; auto with zarith.";
2183
pp " apply Zle_lt_trans with ([b] + [mod_gt a b]); auto with zarith.";
2184
pp " apply Zle_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith.";
2185
pp " apply Zplus_le_compat_r.";
2186
pp " pattern [b] at 1; rewrite <- (Zmult_1_l [b]).";
2187
pp " apply Zmult_le_compat_r; auto with zarith.";
2188
pp " case (Zle_lt_or_eq 0 ([a]/[b])); auto with zarith.";
2189
pp " intros HH; rewrite (Z_div_mod_eq [a] [b]) in H2;";
2190
pp " try rewrite <- HH in H2; auto with zarith.";
2191
pp " case (Z_mod_lt [a] [b]); auto with zarith.";
2192
pp " rewrite Zmult_comm; rewrite spec_mod_gt; auto with zarith.";
2193
pp " rewrite <- Z_div_mod_eq; auto with zarith.";
2194
pp " pattern 2 at 2; rewrite <- (Zpower_1_r 2).";
2195
pp " rewrite <- Zpower_exp; auto with zarith.";
2196
pp " ring_simplify (p - 1 + 1); auto.";
2197
pp " case (Zle_lt_or_eq 0 p); auto with zarith.";
2198
pp " generalize H3; case p; simpl Zpower; auto with zarith.";
2199
pp " intros HH; generalize H3; rewrite <- HH; simpl Zpower; auto with zarith.";
2203
pr " Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) {struct p} : t :=";
2204
pr " gcd_gt_body a b";
2207
pr " | xH => cont a b";
2208
pr " | xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b";
2209
pr " | xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b";
2213
pp " Theorem Zspec_gcd_gt_aux: forall p n a b cont,";
2214
pp " [a] > [b] -> [a] < 2 ^ (Zpos p + n) ->";
2215
pp " (forall a1 b1, [a1] < 2 ^ n -> [a1] > [b1] ->";
2216
pp " Zis_gcd [a1] [b1] [cont a1 b1]) ->";
2217
pp " Zis_gcd [a] [b] [gcd_gt_aux p cont a b].";
2218
pp " intros p; elim p; clear p.";
2219
pp " intros p Hrec n a b cont H2 H3 H4.";
2220
pp " unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xI p) + n); auto.";
2221
pp " intros a1 b1 H6 H7.";
2222
pp " apply Hrec with (Zpos p + n); auto.";
2223
pp " replace (Zpos p + (Zpos p + n)) with";
2224
pp " (Zpos (xI p) + n - 1); auto.";
2225
pp " rewrite Zpos_xI; ring.";
2226
pp " intros a2 b2 H9 H10.";
2227
pp " apply Hrec with n; auto.";
2228
pp " intros p Hrec n a b cont H2 H3 H4.";
2229
pp " unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xO p) + n); auto.";
2230
pp " intros a1 b1 H6 H7.";
2231
pp " apply Hrec with (Zpos p + n - 1); auto.";
2232
pp " replace (Zpos p + (Zpos p + n - 1)) with";
2233
pp " (Zpos (xO p) + n - 1); auto.";
2234
pp " rewrite Zpos_xO; ring.";
2235
pp " intros a2 b2 H9 H10.";
2236
pp " apply Hrec with (n - 1); auto.";
2237
pp " replace (Zpos p + (n - 1)) with";
2238
pp " (Zpos p + n - 1); auto with zarith.";
2239
pp " intros a3 b3 H12 H13; apply H4; auto with zarith.";
2240
pp " apply Zlt_le_trans with (1 := H12).";
2241
pp " case (Zle_or_lt 1 n); intros HH.";
2242
pp " apply Zpower_le_monotone; auto with zarith.";
2243
pp " apply Zle_trans with 0; auto with zarith.";
2244
pp " assert (HH1: n - 1 < 0); auto with zarith.";
2245
pp " generalize HH1; case (n - 1); auto with zarith.";
2246
pp " intros p1 HH2; discriminate.";
2247
pp " intros n a b cont H H2 H3.";
2248
pp " simpl gcd_gt_aux.";
2249
pp " apply Zspec_gcd_gt_body with (n + 1); auto with zarith.";
2250
pp " rewrite Zplus_comm; auto.";
2251
pp " intros a1 b1 H5 H6; apply H3; auto.";
2252
pp " replace n with (n + 1 - 1); auto; try ring.";
2256
pr " Definition gcd_cont a b :=";
2257
pr " match compare one b with";
2263
pr " Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b.";
2266
pr " Theorem spec_gcd_gt: forall a b,";
2267
pr " [a] > [b] -> [gcd_gt a b] = Zgcd [a] [b].";
2270
pp " intros a b H2.";
2271
pp " case (spec_digits (gcd_gt a b)); intros H3 H4.";
2272
pp " case (spec_digits a); intros H5 H6.";
2273
pp " apply sym_equal; apply Zis_gcd_gcd; auto with zarith.";
2274
pp " unfold gcd_gt; apply Zspec_gcd_gt_aux with 0; auto with zarith.";
2275
pp " intros a1 a2; rewrite Zpower_0_r.";
2276
pp " case (spec_digits a2); intros H7 H8;";
2277
pp " intros; apply False_ind; auto with zarith.";
2281
pr " Definition gcd a b :=";
2282
pr " match compare a b with";
2284
pr " | Lt => gcd_gt b a";
2285
pr " | Gt => gcd_gt a b";
2289
pr " Theorem spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].";
2293
pp " case (spec_digits a); intros H1 H2.";
2294
pp " case (spec_digits b); intros H3 H4.";
2295
pp " unfold gcd; generalize (spec_compare a b); case compare.";
2296
pp " intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto.";
2297
pp " apply Zis_gcd_refl.";
2298
pp " intros; apply trans_equal with (Zgcd [b] [a]).";
2299
pp " apply spec_gcd_gt; auto with zarith.";
2300
pp " apply Zis_gcd_gcd; auto with zarith.";
2301
pp " apply Zgcd_is_pos.";
2302
pp " apply Zis_gcd_sym; apply Zgcd_is_gcd.";
2303
pp " intros; apply spec_gcd_gt; auto.";
2308
pr " (***************************************************************)";
2310
pr " (* Conversion *)";
2312
pr " (***************************************************************)";
2315
pr " Definition pheight p := ";
2316
pr " Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (plength p))).";
2319
pr " Theorem pheight_correct: forall p, ";
2320
pr " Zpos p < 2 ^ (Zpos (znz_digits w0_op) * 2 ^ (Z_of_nat (pheight p))).";
2322
pr " intros p; unfold pheight.";
2323
pr " assert (F1: forall x, Z_of_nat (Peano.pred (nat_of_P x)) = Zpos x - 1).";
2325
pr " assert (Zsucc (Z_of_nat (Peano.pred (nat_of_P x))) = Zpos x); auto with zarith.";
2326
pr " rewrite <- inj_S.";
2327
pr " rewrite <- (fun x => S_pred x 0); auto with zarith.";
2328
pr " rewrite Zpos_eq_Z_of_nat_o_nat_of_P; auto.";
2329
pr " apply lt_le_trans with 1%snat; auto with zarith." "%";
2330
pr " exact (le_Pmult_nat x 1).";
2331
pr " rewrite F1; clear F1.";
2332
pr " assert (F2:= (get_height_correct (znz_digits w0_op) (plength p))).";
2333
pr " apply Zlt_le_trans with (Zpos (Psucc p)).";
2334
pr " rewrite Zpos_succ_morphism; auto with zarith.";
2335
pr " apply Zle_trans with (1 := plength_pred_correct (Psucc p)).";
2336
pr " rewrite Ppred_succ.";
2337
pr " apply Zpower_le_monotone; auto with zarith.";
2341
pr " Definition of_pos x :=";
2342
pr " let h := pheight x in";
2344
for i = 0 to size do
2345
pr " | %i%snat => reduce_%i (snd (w%i_op.(znz_of_pos) x))" i "%" i i;
2348
pr " let n := minus h %i in" (size + 1);
2349
pr " reduce_n n (snd ((make_op n).(znz_of_pos) x))";
2353
pr " Theorem spec_of_pos: forall x,";
2354
pr " [of_pos x] = Zpos x.";
2357
pp " assert (F := spec_more_than_1_digit w0_spec).";
2358
pp " intros x; unfold of_pos; case_eq (pheight x).";
2359
for i = 0 to size do
2361
pp " intros n; case n; clear n.";
2362
pp " intros H1; rewrite spec_reduce_%i; unfold to_Z." i;
2363
pp " apply (znz_of_pos_correct w%i_spec)." i;
2364
pp " apply Zlt_le_trans with (1 := pheight_correct x).";
2365
pp " rewrite H1; simpl Z_of_nat; change (2^%i) with (%s)." i (gen2 i);
2367
pp " apply Zpower_le_monotone; split; auto with zarith.";
2370
pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.";
2371
pp " repeat rewrite <- Zpos_xO.";
2372
pp " refine (Zle_refl _).";
2376
pp " intros H1; rewrite spec_reduce_n; unfold to_Z.";
2377
pp " simpl minus; rewrite <- minus_n_O.";
2378
pp " apply (znz_of_pos_correct (wn_spec n)).";
2379
pp " apply Zlt_le_trans with (1 := pheight_correct x).";
2381
pp " apply Zpower_le_monotone; auto with zarith.";
2382
pp " split; auto with zarith.";
2384
pp " elim n; clear n H1.";
2385
pp " simpl Z_of_nat; change (2^%i) with (%s)." (size + 1) (gen2 (size + 1));
2386
pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc.";
2387
pp " repeat rewrite <- Zpos_xO.";
2388
pp " refine (Zle_refl _).";
2389
pp " intros n Hrec.";
2390
pp " rewrite make_op_S.";
2391
pp " change (@znz_digits (word _ (S (S n))) (mk_zn2z_op_karatsuba (make_op n))) with";
2392
pp " (xO (znz_digits (make_op n))).";
2393
pp " rewrite (fun x y => (Zpos_xO (@znz_digits x y))).";
2394
pp " rewrite inj_S; unfold Zsucc.";
2395
pp " rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith.";
2396
pp " rewrite Zpower_1_r.";
2397
pp " assert (tmp: forall x y z, x * (y * z) = y * (x * z));";
2398
pp " [intros; ring | rewrite tmp; clear tmp].";
2399
pp " apply Zmult_le_compat_l; auto with zarith.";
2403
pr " Definition of_N x :=";
2405
pr " | BinNat.N0 => zero";
2406
pr " | Npos p => of_pos p";
2410
pr " Theorem spec_of_N: forall x,";
2411
pr " [of_N x] = Z_of_N x.";
2414
pp " intros x; case x.";
2416
pp " unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto.";
2417
pp " intros p; exact (spec_of_pos p).";
2421
pr " (***************************************************************)";
2425
pr " (***************************************************************)";
2429
pr " Definition head0 w := match w with";
2430
for i = 0 to size do
2431
pr " | %s%i w=> reduce_%i (w%i_op.(znz_head0) w)" c i i i;
2433
pr " | %sn n w=> reduce_n n ((make_op n).(znz_head0) w)" c;
2437
pr " Theorem spec_head00: forall x, [x] = 0 ->[head0 x] = Zpos (digits x).";
2440
pp " intros x; case x; unfold head0; clear x.";
2441
for i = 0 to size do
2442
pp " intros x; rewrite spec_reduce_%i; exact (spec_head00 w%i_spec x)." i i;
2444
pp " intros n x; rewrite spec_reduce_n; exact (spec_head00 (wn_spec n) x).";
2448
pr " Theorem spec_head0: forall x, 0 < [x] ->";
2449
pr " 2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x).";
2452
pp " assert (F0: forall x, (x - 1) + 1 = x).";
2453
pp " intros; ring. ";
2454
pp " intros x; case x; unfold digits, head0; clear x.";
2455
for i = 0 to size do
2456
pp " intros x Hx; rewrite spec_reduce_%i." i;
2457
pp " assert (F1:= spec_more_than_1_digit w%i_spec)." i;
2458
pp " generalize (spec_head0 w%i_spec x Hx)." i;
2460
pp " pattern (Zpos (znz_digits w%i_op)) at 1; " i;
2461
pp " rewrite <- (fun x => (F0 (Zpos x))).";
2462
pp " rewrite Zpower_exp; auto with zarith.";
2463
pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith.";
2465
pp " intros n x Hx; rewrite spec_reduce_n.";
2466
pp " assert (F1:= spec_more_than_1_digit (wn_spec n)).";
2467
pp " generalize (spec_head0 (wn_spec n) x Hx).";
2469
pp " pattern (Zpos (znz_digits (make_op n))) at 1; ";
2470
pp " rewrite <- (fun x => (F0 (Zpos x))).";
2471
pp " rewrite Zpower_exp; auto with zarith.";
2472
pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith.";
2478
pr " Definition tail0 w := match w with";
2479
for i = 0 to size do
2480
pr " | %s%i w=> reduce_%i (w%i_op.(znz_tail0) w)" c i i i;
2482
pr " | %sn n w=> reduce_n n ((make_op n).(znz_tail0) w)" c;
2487
pr " Theorem spec_tail00: forall x, [x] = 0 ->[tail0 x] = Zpos (digits x).";
2490
pp " intros x; case x; unfold tail0; clear x.";
2491
for i = 0 to size do
2492
pp " intros x; rewrite spec_reduce_%i; exact (spec_tail00 w%i_spec x)." i i;
2494
pp " intros n x; rewrite spec_reduce_n; exact (spec_tail00 (wn_spec n) x).";
2499
pr " Theorem spec_tail0: forall x,";
2500
pr " 0 < [x] -> exists y, 0 <= y /\\ [x] = (2 * y + 1) * 2 ^ [tail0 x].";
2503
pp " intros x; case x; clear x; unfold tail0.";
2504
for i = 0 to size do
2505
pp " intros x Hx; rewrite spec_reduce_%i; exact (spec_tail0 w%i_spec x Hx)." i i;
2507
pp " intros n x Hx; rewrite spec_reduce_n; exact (spec_tail0 (wn_spec n) x Hx).";
2512
(* Number of digits *)
2513
pr " Definition %sdigits x :=" c;
2515
pr " | %s0 _ => %s0 w0_op.(znz_zdigits)" c c;
2516
for i = 1 to size do
2517
pr " | %s%i _ => reduce_%i w%i_op.(znz_zdigits)" c i i i;
2519
pr " | %sn n _ => reduce_n n (make_op n).(znz_zdigits)" c;
2523
pr " Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x).";
2526
pp " intros x; case x; clear x; unfold Ndigits, digits.";
2527
for i = 0 to size do
2528
pp " intros _; try rewrite spec_reduce_%i; exact (spec_zdigits w%i_spec)." i i;
2530
pp " intros n _; try rewrite spec_reduce_n; exact (spec_zdigits (wn_spec n)).";
2536
for i = 0 to size do
2537
pr " Definition shiftr%i n x := w%i_op.(znz_add_mul_div) (w%i_op.(znz_sub) w%i_op.(znz_zdigits) n) w%i_op.(znz_0) x." i i i i i;
2539
pr " Definition shiftrn n p x := (make_op n).(znz_add_mul_div) ((make_op n).(znz_sub) (make_op n).(znz_zdigits) p) (make_op n).(znz_0) x.";
2542
pr " Definition shiftr := Eval lazy beta delta [same_level] in ";
2543
pr " same_level _ (fun n x => %s0 (shiftr0 n x))" c;
2544
for i = 1 to size do
2545
pr " (fun n x => reduce_%i (shiftr%i n x))" i i;
2547
pr " (fun n p x => reduce_n n (shiftrn n p x)).";
2551
pr " Theorem spec_shiftr: forall n x,";
2552
pr " [n] <= [Ndigits x] -> [shiftr n x] = [x] / 2 ^ [n].";
2555
pp " assert (F0: forall x y, x - (x - y) = y).";
2556
pp " intros; ring.";
2557
pp " assert (F2: forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z).";
2558
pp " intros x y z HH HH1 HH2.";
2559
pp " split; auto with zarith.";
2560
pp " apply Zle_lt_trans with (2 := HH2); auto with zarith.";
2561
pp " apply Zdiv_le_upper_bound; auto with zarith.";
2562
pp " pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith.";
2563
pp " apply Zmult_le_compat_l; auto.";
2564
pp " apply Zpower_le_monotone; auto with zarith.";
2565
pp " rewrite Zpower_0_r; ring.";
2566
pp " assert (F3: forall x y, 0 <= y -> y <= x -> 0 <= x - y < 2 ^ x).";
2567
pp " intros xx y HH HH1.";
2568
pp " split; auto with zarith.";
2569
pp " apply Zle_lt_trans with xx; auto with zarith.";
2570
pp " apply Zpower2_lt_lin; auto with zarith.";
2571
pp " assert (F4: forall ww ww1 ww2 ";
2572
pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)";
2573
pp " xx yy xx1 yy1,";
2574
pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_zdigits ww1_op) ->";
2575
pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->";
2576
pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->";
2577
pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->";
2578
pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->";
2579
pp " znz_to_Z ww_op";
2580
pp " (znz_add_mul_div ww_op (znz_sub ww_op (znz_zdigits ww_op) yy1)";
2581
pp " (znz_0 ww_op) xx1) = znz_to_Z ww1_op xx / 2 ^ znz_to_Z ww2_op yy).";
2582
pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy.";
2583
pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2.";
2584
pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4.";
2585
pp " rewrite <- Hx.";
2586
pp " rewrite <- Hy.";
2587
pp " generalize (spec_add_mul_div Hw";
2588
pp " (znz_0 ww_op) xx1";
2589
pp " (znz_sub ww_op (znz_zdigits ww_op) ";
2592
pp " rewrite (spec_0 Hw).";
2593
pp " rewrite Zmult_0_l; rewrite Zplus_0_l.";
2594
pp " rewrite (CyclicAxioms.spec_sub Hw).";
2595
pp " rewrite Zmod_small; auto with zarith.";
2596
pp " rewrite (spec_zdigits Hw).";
2598
pp " rewrite Zmod_small; auto with zarith.";
2599
pp " unfold base; rewrite (spec_zdigits Hw) in Hl1 |- *;";
2600
pp " auto with zarith.";
2601
pp " assert (F5: forall n m, (n <= m)%snat ->" "%";
2602
pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m))).";
2603
pp " intros n m HH; elim HH; clear m HH; auto with zarith.";
2604
pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec).";
2605
pp " rewrite make_op_S.";
2606
pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end.";
2607
pp " rewrite Zpos_xO.";
2608
pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith.";
2609
pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size;
2610
pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0))).";
2611
pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size;
2612
pp " rewrite Zpos_xO.";
2613
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size;
2614
pp " apply F5; auto with arith.";
2615
pp " intros x; case x; clear x; unfold shiftr, same_level.";
2616
for i = 0 to size do
2617
pp " intros x y; case y; clear y.";
2618
for j = 0 to i - 1 do
2619
pp " intros y; unfold shiftr%i, Ndigits." i;
2620
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
2621
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i;
2622
pp " rewrite (spec_zdigits w%i_spec)." i;
2623
pp " rewrite (spec_zdigits w%i_spec)." j;
2624
pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)"));
2625
pp " repeat rewrite (fun x => Zpos_xO (xO x)).";
2626
pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y)).";
2627
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j;
2628
pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i;
2631
pp " intros y; unfold shiftr%i, Ndigits." i;
2632
pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
2633
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i;
2634
for j = i + 1 to size do
2635
pp " intros y; unfold shiftr%i, Ndigits." j;
2636
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
2637
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i;
2638
pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j;
2642
pp " intros m y; unfold shiftrn, Ndigits.";
2643
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
2644
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size;
2645
pp " try (apply sym_equal; exact (spec_extend%in m x))." size;
2649
pp " intros m y; unfold shiftrn, Ndigits.";
2650
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
2651
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i;
2652
pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i;
2653
pp " rewrite <- (spec_extend%in m); rewrite <- spec_extend%in%i; auto." size i size;
2656
pp " intros n x y; case y; clear y;";
2657
pp " intros y; unfold shiftrn, Ndigits; try rewrite spec_reduce_n.";
2658
for i = 0 to size do
2659
pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
2660
pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i;
2661
pp " rewrite (spec_zdigits w%i_spec)." i;
2662
pp " rewrite (spec_zdigits (wn_spec n)).";
2663
pp " apply Zle_trans with (2 := F6 n).";
2664
pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)"));
2665
pp " repeat rewrite (fun x => Zpos_xO (xO x)).";
2666
pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y)).";
2667
pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i;
2669
pp " change ([Nn n (extend%i n y)] = [N%i y])." size i
2671
pp " change ([Nn n (extend%i n (extend%i %i y))] = [N%i y])." size i (size - i - 1) i;
2672
pp " rewrite <- (spec_extend%in n); auto." size;
2674
pp " try (rewrite <- spec_extend%in%i; auto)." i size;
2676
pp " generalize y; clear y; intros m y.";
2677
pp " rewrite spec_reduce_n; unfold to_Z; intros H1.";
2678
pp " apply F4 with (3:=(wn_spec (Max.max n m)))(4:=wn_spec m)(5:=wn_spec n); auto with zarith.";
2679
pp " rewrite (spec_zdigits (wn_spec m)).";
2680
pp " rewrite (spec_zdigits (wn_spec (Max.max n m))).";
2681
pp " apply F5; auto with arith.";
2682
pp " exact (spec_cast_r n m y).";
2683
pp " exact (spec_cast_l n m x).";
2687
pr " Definition safe_shiftr n x := ";
2688
pr " match compare n (Ndigits x) with";
2689
pr " | Lt => shiftr n x ";
2690
pr " | _ => %s0 w_0" c;
2695
pr " Theorem spec_safe_shiftr: forall n x,";
2696
pr " [safe_shiftr n x] = [x] / 2 ^ [n].";
2699
pp " intros n x; unfold safe_shiftr;";
2700
pp " generalize (spec_compare n (Ndigits x)); case compare; intros H.";
2701
pp " apply trans_equal with (1 := spec_0 w0_spec).";
2702
pp " apply sym_equal; apply Zdiv_small; rewrite H.";
2703
pp " rewrite spec_Ndigits; exact (spec_digits x).";
2704
pp " rewrite <- spec_shiftr; auto with zarith.";
2705
pp " apply trans_equal with (1 := spec_0 w0_spec).";
2706
pp " apply sym_equal; apply Zdiv_small.";
2707
pp " rewrite spec_Ndigits in H; case (spec_digits x); intros H1 H2.";
2709
pp " apply Zlt_le_trans with (1 := H2).";
2710
pp " apply Zpower_le_monotone; auto with zarith.";
2717
for i = 0 to size do
2718
pr " Definition shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i
2720
pr " Definition shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0).";
2721
pr " Definition shiftl := Eval lazy beta delta [same_level] in";
2722
pr " same_level _ (fun n x => %s0 (shiftl0 n x))" c;
2723
for i = 1 to size do
2724
pr " (fun n x => reduce_%i (shiftl%i n x))" i i;
2726
pr " (fun n p x => reduce_n n (shiftln n p x)).";
2731
pr " Theorem spec_shiftl: forall n x,";
2732
pr " [n] <= [head0 x] -> [shiftl n x] = [x] * 2 ^ [n].";
2735
pp " assert (F0: forall x y, x - (x - y) = y).";
2736
pp " intros; ring.";
2737
pp " assert (F2: forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z).";
2738
pp " intros x y z HH HH1 HH2.";
2739
pp " split; auto with zarith.";
2740
pp " apply Zle_lt_trans with (2 := HH2); auto with zarith.";
2741
pp " apply Zdiv_le_upper_bound; auto with zarith.";
2742
pp " pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith.";
2743
pp " apply Zmult_le_compat_l; auto.";
2744
pp " apply Zpower_le_monotone; auto with zarith.";
2745
pp " rewrite Zpower_0_r; ring.";
2746
pp " assert (F3: forall x y, 0 <= y -> y <= x -> 0 <= x - y < 2 ^ x).";
2747
pp " intros xx y HH HH1.";
2748
pp " split; auto with zarith.";
2749
pp " apply Zle_lt_trans with xx; auto with zarith.";
2750
pp " apply Zpower2_lt_lin; auto with zarith.";
2751
pp " assert (F4: forall ww ww1 ww2 ";
2752
pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)";
2753
pp " xx yy xx1 yy1,";
2754
pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_head0 ww1_op xx) ->";
2755
pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->";
2756
pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->";
2757
pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->";
2758
pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->";
2759
pp " znz_to_Z ww_op";
2760
pp " (znz_add_mul_div ww_op yy1";
2761
pp " xx1 (znz_0 ww_op)) = znz_to_Z ww1_op xx * 2 ^ znz_to_Z ww2_op yy).";
2762
pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy.";
2763
pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2.";
2764
pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4.";
2765
pp " rewrite <- Hx.";
2766
pp " rewrite <- Hy.";
2767
pp " generalize (spec_add_mul_div Hw xx1 (znz_0 ww_op) yy1).";
2768
pp " rewrite (spec_0 Hw).";
2769
pp " assert (F1: znz_to_Z ww1_op (znz_head0 ww1_op xx) <= Zpos (znz_digits ww1_op)).";
2770
pp " case (Zle_lt_or_eq _ _ HH1); intros HH5.";
2771
pp " apply Zlt_le_weak.";
2772
pp " case (CyclicAxioms.spec_head0 Hw1 xx).";
2773
pp " rewrite <- Hx; auto.";
2774
pp " intros _ Hu; unfold base in Hu.";
2775
pp " case (Zle_or_lt (Zpos (znz_digits ww1_op))";
2776
pp " (znz_to_Z ww1_op (znz_head0 ww1_op xx))); auto; intros H1.";
2777
pp " absurd (2 ^ (Zpos (znz_digits ww1_op)) <= 2 ^ (znz_to_Z ww1_op (znz_head0 ww1_op xx))).";
2778
pp " apply Zlt_not_le.";
2779
pp " case (spec_to_Z Hw1 xx); intros HHx3 HHx4.";
2780
pp " rewrite <- (Zmult_1_r (2 ^ znz_to_Z ww1_op (znz_head0 ww1_op xx))).";
2781
pp " apply Zle_lt_trans with (2 := Hu).";
2782
pp " apply Zmult_le_compat_l; auto with zarith.";
2783
pp " apply Zpower_le_monotone; auto with zarith.";
2784
pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith.";
2785
pp " rewrite Zdiv_0_l; auto with zarith.";
2786
pp " rewrite Zplus_0_r.";
2787
pp " case (Zle_lt_or_eq _ _ HH1); intros HH5.";
2788
pp " rewrite Zmod_small; auto with zarith.";
2789
pp " intros HH; apply HH.";
2790
pp " rewrite Hy; apply Zle_trans with (1:= Hl).";
2791
pp " rewrite <- (spec_zdigits Hw). ";
2792
pp " apply Zle_trans with (2 := Hl1); auto.";
2793
pp " rewrite (spec_zdigits Hw1); auto with zarith.";
2794
pp " split; auto with zarith .";
2795
pp " apply Zlt_le_trans with (base (znz_digits ww1_op)).";
2797
pp " case (CyclicAxioms.spec_head0 Hw1 xx); auto.";
2798
pp " rewrite <- Hx; auto.";
2799
pp " intros _ Hu; rewrite Zmult_comm in Hu.";
2800
pp " apply Zle_lt_trans with (2 := Hu).";
2801
pp " apply Zmult_le_compat_l; auto with zarith.";
2802
pp " apply Zpower_le_monotone; auto with zarith.";
2803
pp " unfold base; apply Zpower_le_monotone; auto with zarith.";
2804
pp " split; auto with zarith.";
2805
pp " rewrite <- (spec_zdigits Hw); auto with zarith.";
2806
pp " rewrite <- (spec_zdigits Hw1); auto with zarith.";
2807
pp " rewrite <- HH5.";
2808
pp " rewrite Zmult_0_l.";
2809
pp " rewrite Zmod_small; auto with zarith.";
2810
pp " intros HH; apply HH.";
2811
pp " rewrite Hy; apply Zle_trans with (1 := Hl).";
2812
pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith.";
2813
pp " rewrite <- (spec_zdigits Hw); auto with zarith.";
2814
pp " rewrite <- (spec_zdigits Hw1); auto with zarith.";
2815
pp " assert (F5: forall n m, (n <= m)%snat ->" "%";
2816
pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m))).";
2817
pp " intros n m HH; elim HH; clear m HH; auto with zarith.";
2818
pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec).";
2819
pp " rewrite make_op_S.";
2820
pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end.";
2821
pp " rewrite Zpos_xO.";
2822
pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith.";
2823
pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size;
2824
pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0))).";
2825
pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size;
2826
pp " rewrite Zpos_xO.";
2827
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size;
2828
pp " apply F5; auto with arith.";
2829
pp " intros x; case x; clear x; unfold shiftl, same_level.";
2830
for i = 0 to size do
2831
pp " intros x y; case y; clear y.";
2832
for j = 0 to i - 1 do
2833
pp " intros y; unfold shiftl%i, head0." i;
2834
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
2835
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i;
2836
pp " rewrite (spec_zdigits w%i_spec)." i;
2837
pp " rewrite (spec_zdigits w%i_spec)." j;
2838
pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)"));
2839
pp " repeat rewrite (fun x => Zpos_xO (xO x)).";
2840
pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y)).";
2841
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j;
2842
pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i;
2844
pp " intros y; unfold shiftl%i, head0." i;
2845
pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
2846
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i;
2847
for j = i + 1 to size do
2848
pp " intros y; unfold shiftl%i, head0." j;
2849
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
2850
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i;
2851
pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j;
2855
pp " intros m y; unfold shiftln, head0.";
2856
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
2857
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size;
2858
pp " try (apply sym_equal; exact (spec_extend%in m x))." size;
2862
pp " intros m y; unfold shiftln, head0.";
2863
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
2864
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i;
2865
pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i;
2866
pp " rewrite <- (spec_extend%in m); rewrite <- spec_extend%in%i; auto." size i size;
2869
pp " intros n x y; case y; clear y;";
2870
pp " intros y; unfold shiftln, head0; try rewrite spec_reduce_n.";
2871
for i = 0 to size do
2872
pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
2873
pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i;
2874
pp " rewrite (spec_zdigits w%i_spec)." i;
2875
pp " rewrite (spec_zdigits (wn_spec n)).";
2876
pp " apply Zle_trans with (2 := F6 n).";
2877
pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)"));
2878
pp " repeat rewrite (fun x => Zpos_xO (xO x)).";
2879
pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y)).";
2880
pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i;
2882
pp " change ([Nn n (extend%i n y)] = [N%i y])." size i
2884
pp " change ([Nn n (extend%i n (extend%i %i y))] = [N%i y])." size i (size - i - 1) i;
2885
pp " rewrite <- (spec_extend%in n); auto." size;
2887
pp " try (rewrite <- spec_extend%in%i; auto)." i size;
2889
pp " generalize y; clear y; intros m y.";
2890
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
2891
pp " apply F4 with (3:=(wn_spec (Max.max n m)))(4:=wn_spec m)(5:=wn_spec n); auto with zarith.";
2892
pp " rewrite (spec_zdigits (wn_spec m)).";
2893
pp " rewrite (spec_zdigits (wn_spec (Max.max n m))).";
2894
pp " apply F5; auto with arith.";
2895
pp " exact (spec_cast_r n m y).";
2896
pp " exact (spec_cast_l n m x).";
2901
pr " Definition double_size w := match w with";
2902
for i = 0 to size-1 do
2903
pr " | %s%i x => %s%i (WW (znz_0 w%i_op) x)" c i c (i + 1) i;
2905
pr " | %s%i x => %sn 0 (WW (znz_0 w%i_op) x)" c size c size;
2906
pr " | %sn n x => %sn (S n) (WW (znz_0 (make_op n)) x)" c c;
2910
pr " Theorem spec_double_size_digits: ";
2911
pr " forall x, digits (double_size x) = xO (digits x).";
2914
pp " intros x; case x; unfold double_size, digits; clear x; auto.";
2915
pp " intros n x; rewrite make_op_S; auto.";
2920
pr " Theorem spec_double_size: forall x, [double_size x] = [x].";
2923
pp " intros x; case x; unfold double_size; clear x.";
2924
for i = 0 to size do
2925
pp " intros x; unfold to_Z, make_op; ";
2926
pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto with zarith." (i + 1) i;
2928
pp " intros n x; unfold to_Z;";
2929
pp " generalize (znz_to_Z_n n); simpl word.";
2930
pp " intros HH; rewrite HH; clear HH.";
2931
pp " generalize (spec_0 (wn_spec n)); simpl word.";
2932
pp " intros HH; rewrite HH; clear HH; auto with zarith.";
2937
pr " Theorem spec_double_size_head0: ";
2938
pr " forall x, 2 * [head0 x] <= [head0 (double_size x)].";
2942
pp " assert (F1:= spec_pos (head0 x)).";
2943
pp " assert (F2: 0 < Zpos (digits x)).";
2945
pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH.";
2946
pp " generalize HH; rewrite <- (spec_double_size x); intros HH1.";
2947
pp " case (spec_head0 x HH); intros _ HH2.";
2948
pp " case (spec_head0 _ HH1).";
2949
pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x).";
2950
pp " intros HH3 _.";
2951
pp " case (Zle_or_lt ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4.";
2952
pp " absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto.";
2953
pp " apply Zle_not_lt.";
2954
pp " apply Zmult_le_compat_r; auto with zarith.";
2955
pp " apply Zpower_le_monotone; auto; auto with zarith.";
2956
pp " generalize (spec_pos (head0 (double_size x))); auto with zarith.";
2957
pp " assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)).";
2958
pp " case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5.";
2959
pp " apply Zmult_le_reg_r with (2 ^ 1); auto with zarith.";
2960
pp " rewrite <- (fun x y z => Zpower_exp x (y - z)); auto with zarith.";
2961
pp " assert (tmp: forall x, x - 1 + 1 = x); [intros; ring | rewrite tmp; clear tmp].";
2962
pp " apply Zle_trans with (2 := Zlt_le_weak _ _ HH2).";
2963
pp " apply Zmult_le_compat_l; auto with zarith.";
2964
pp " rewrite Zpower_1_r; auto with zarith.";
2965
pp " apply Zpower_le_monotone; auto with zarith.";
2966
pp " split; auto with zarith. ";
2967
pp " case (Zle_or_lt (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6.";
2968
pp " absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith.";
2969
pp " rewrite <- HH5; rewrite Zmult_1_r.";
2970
pp " apply Zpower_le_monotone; auto with zarith.";
2971
pp " rewrite (Zmult_comm 2).";
2972
pp " rewrite Zpower_mult; auto with zarith.";
2973
pp " rewrite Zpower_2.";
2974
pp " apply Zlt_le_trans with (2 := HH3).";
2975
pp " rewrite <- Zmult_assoc.";
2976
pp " replace (Zpos (xO (digits x)) - 1) with";
2977
pp " ((Zpos (digits x) - 1) + (Zpos (digits x))).";
2978
pp " rewrite Zpower_exp; auto with zarith.";
2979
pp " apply Zmult_lt_compat2; auto with zarith.";
2980
pp " split; auto with zarith.";
2981
pp " apply Zmult_lt_0_compat; auto with zarith.";
2982
pp " rewrite Zpos_xO; ring.";
2983
pp " apply Zlt_le_weak; auto.";
2984
pp " repeat rewrite spec_head00; auto.";
2985
pp " rewrite spec_double_size_digits.";
2986
pp " rewrite Zpos_xO; auto with zarith.";
2987
pp " rewrite spec_double_size; auto.";
2991
pr " Theorem spec_double_size_head0_pos: ";
2992
pr " forall x, 0 < [head0 (double_size x)].";
2996
pp " assert (F: 0 < Zpos (digits x)).";
2998
pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0.";
2999
pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1.";
3000
pp " apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith.";
3001
pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3.";
3002
pp " generalize F3; rewrite <- (spec_double_size x); intros F4.";
3003
pp " absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))).";
3004
pp " apply Zle_not_lt.";
3005
pp " apply Zpower_le_monotone; auto with zarith.";
3006
pp " split; auto with zarith.";
3007
pp " rewrite Zpos_xO; auto with zarith.";
3008
pp " case (spec_head0 x F3).";
3009
pp " rewrite <- F1; rewrite Zpower_0_r; rewrite Zmult_1_l; intros _ HH.";
3010
pp " apply Zle_lt_trans with (2 := HH).";
3011
pp " case (spec_head0 _ F4).";
3012
pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x).";
3013
pp " rewrite <- F0; rewrite Zpower_0_r; rewrite Zmult_1_l; auto.";
3014
pp " generalize F1; rewrite (spec_head00 _ (sym_equal F3)); auto with zarith.";
3021
pr " Definition safe_shiftl_aux_body cont n x :=";
3022
pr " match compare n (head0 x) with";
3023
pr " Gt => cont n (double_size x)";
3024
pr " | _ => shiftl n x";
3028
pr " Theorem spec_safe_shift_aux_body: forall n p x cont,";
3029
pr " 2^ Zpos p <= [head0 x] ->";
3030
pr " (forall x, 2 ^ (Zpos p + 1) <= [head0 x]->";
3031
pr " [cont n x] = [x] * 2 ^ [n]) ->";
3032
pr " [safe_shiftl_aux_body cont n x] = [x] * 2 ^ [n].";
3035
pp " intros n p x cont H1 H2; unfold safe_shiftl_aux_body.";
3036
pp " generalize (spec_compare n (head0 x)); case compare; intros H.";
3037
pp " apply spec_shiftl; auto with zarith.";
3038
pp " apply spec_shiftl; auto with zarith.";
3040
pp " rewrite spec_double_size; auto.";
3041
pp " rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith.";
3042
pp " apply Zle_trans with (2 := spec_double_size_head0 x).";
3043
pp " rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith.";
3047
pr " Fixpoint safe_shiftl_aux p cont n x {struct p} :=";
3048
pr " safe_shiftl_aux_body ";
3049
pr " (fun n x => match p with";
3050
pr " | xH => cont n x";
3051
pr " | xO p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x";
3052
pr " | xI p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x";
3056
pr " Theorem spec_safe_shift_aux: forall p q n x cont,";
3057
pr " 2 ^ (Zpos q) <= [head0 x] ->";
3058
pr " (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] ->";
3059
pr " [cont n x] = [x] * 2 ^ [n]) -> ";
3060
pr " [safe_shiftl_aux p cont n x] = [x] * 2 ^ [n].";
3063
pp " intros p; elim p; unfold safe_shiftl_aux; fold safe_shiftl_aux; clear p.";
3064
pp " intros p Hrec q n x cont H1 H2.";
3065
pp " apply spec_safe_shift_aux_body with (q); auto.";
3066
pp " intros x1 H3; apply Hrec with (q + 1)%spositive; auto." "%";
3067
pp " intros x2 H4; apply Hrec with (p + q + 1)%spositive; auto." "%";
3068
pp " rewrite <- Pplus_assoc.";
3069
pp " rewrite Zpos_plus_distr; auto.";
3070
pp " intros x3 H5; apply H2.";
3071
pp " rewrite Zpos_xI.";
3072
pp " replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1));";
3074
pp " repeat rewrite Zpos_plus_distr; ring.";
3075
pp " intros p Hrec q n x cont H1 H2.";
3076
pp " apply spec_safe_shift_aux_body with (q); auto.";
3077
pp " intros x1 H3; apply Hrec with (q); auto.";
3078
pp " apply Zle_trans with (2 := H3); auto with zarith.";
3079
pp " apply Zpower_le_monotone; auto with zarith.";
3080
pp " intros x2 H4; apply Hrec with (p + q)%spositive; auto." "%";
3081
pp " intros x3 H5; apply H2.";
3082
pp " rewrite (Zpos_xO p).";
3083
pp " replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q));";
3085
pp " repeat rewrite Zpos_plus_distr; ring.";
3086
pp " intros q n x cont H1 H2.";
3087
pp " apply spec_safe_shift_aux_body with (q); auto.";
3088
pp " rewrite Zplus_comm; auto.";
3093
pr " Definition safe_shiftl n x :=";
3094
pr " safe_shiftl_aux_body";
3095
pr " (safe_shiftl_aux_body";
3096
pr " (safe_shiftl_aux (digits n) shiftl)) n x.";
3099
pr " Theorem spec_safe_shift: forall n x,";
3100
pr " [safe_shiftl n x] = [x] * 2 ^ [n].";
3103
pp " intros n x; unfold safe_shiftl, safe_shiftl_aux_body.";
3104
pp " generalize (spec_compare n (head0 x)); case compare; intros H.";
3105
pp " apply spec_shiftl; auto with zarith.";
3106
pp " apply spec_shiftl; auto with zarith.";
3107
pp " rewrite <- (spec_double_size x).";
3108
pp " generalize (spec_compare n (head0 (double_size x))); case compare; intros H1.";
3109
pp " apply spec_shiftl; auto with zarith.";
3110
pp " apply spec_shiftl; auto with zarith.";
3111
pp " rewrite <- (spec_double_size (double_size x)).";
3112
pp " apply spec_safe_shift_aux with 1%spositive." "%";
3113
pp " apply Zle_trans with (2 := spec_double_size_head0 (double_size x)).";
3114
pp " replace (2 ^ 1) with (2 * 1).";
3115
pp " apply Zmult_le_compat_l; auto with zarith.";
3116
pp " generalize (spec_double_size_head0_pos x); auto with zarith.";
3117
pp " rewrite Zpower_1_r; ring.";
3118
pp " intros x1 H2; apply spec_shiftl.";
3119
pp " apply Zle_trans with (2 := H2).";
3120
pp " apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith.";
3121
pp " case (spec_digits n); auto with zarith.";
3122
pp " apply Zpower_le_monotone; auto with zarith.";
3127
pr " Definition is_even x :=";
3129
for i = 0 to size do
3130
pr " | %s%i wx => w%i_op.(znz_is_even) wx" c i i
3132
pr " | %sn n wx => (make_op n).(znz_is_even) wx" c;
3137
pr " Theorem spec_is_even: forall x,";
3138
pr " if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1.";
3141
pp " intros x; case x; unfold is_even, to_Z; clear x.";
3142
for i = 0 to size do
3143
pp " intros x; exact (spec_is_even w%i_spec x)." i;
3145
pp " intros n x; exact (spec_is_even (wn_spec n) x).";
3149
pr " Theorem spec_0: [zero] = 0.";
3152
pp " exact (spec_0 w0_spec).";
3156
pr " Theorem spec_1: [one] = 1.";
3159
pp " exact (spec_1 w0_spec).";
added
removed
theories/Numbers/Natural/BigN/NMake_gen.ml
