summaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/BigN/NMake_gen.ml
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml')
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml929
1 files changed, 219 insertions, 710 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 04c7b96d..b8552a39 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -8,14 +8,14 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NMake_gen.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
(*S NMake_gen.ml : this file generates NMake.v *)
(*s The two parameters that control the generation: *)
-let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ
+let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ
process before relying on a generic construct *)
let gen_proof = true (* should we generate proofs ? *)
@@ -27,18 +27,18 @@ let c = "N"
let pz n = if n == 0 then "w_0" else "W0"
let rec gen2 n = if n == 0 then "1" else if n == 1 then "2"
else "2 * " ^ (gen2 (n - 1))
-let rec genxO n s =
+let rec genxO n s =
if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")"
-(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to
- /dev/null, but for being compatible with earlier ocaml and not
- relying on system-dependent stuff like open_out "/dev/null",
+(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to
+ /dev/null, but for being compatible with earlier ocaml and not
+ relying on system-dependent stuff like open_out "/dev/null",
let's use instead a magical hack *)
(* Standard printer, with a final newline *)
let pr s = Printf.printf (s^^"\n")
(* Printing to /dev/null *)
-let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ())
+let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ())
: ('a, out_channel, unit) format -> 'a)
(* Proof printer : prints iff gen_proof is true *)
let pp = if gen_proof then pr else pn
@@ -51,7 +51,7 @@ let pp0 = if gen_proof then pr0 else pn
(*s The actual printing *)
-let _ =
+let _ =
pr "(************************************************************************)";
pr "(* v * The Coq Proof Assistant / The Coq Development Team *)";
@@ -67,21 +67,13 @@ let _ =
pr "";
pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)";
pr "";
- pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)";
+ pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)";
pr "";
- pr "Require Import BigNumPrelude.";
- pr "Require Import ZArith.";
- pr "Require Import CyclicAxioms.";
- pr "Require Import DoubleType.";
- pr "Require Import DoubleMul.";
- pr "Require Import DoubleDivn1.";
- pr "Require Import DoubleCyclic.";
- pr "Require Import Nbasic.";
- pr "Require Import Wf_nat.";
- pr "Require Import StreamMemo.";
- pr "Require Import NSig.";
+ pr "Require Import BigNumPrelude ZArith CyclicAxioms";
+ pr " DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic";
+ pr " Wf_nat StreamMemo.";
pr "";
- pr "Module Make (Import W0:CyclicType) <: NType.";
+ pr "Module Make (Import W0:CyclicType).";
pr "";
pr " Definition w0 := W0.w.";
@@ -132,7 +124,7 @@ let _ =
pr "";
pr " Inductive %s_ :=" t;
- for i = 0 to size do
+ for i = 0 to size do
pr " | %s%i : w%i -> %s_" c i i t
done;
pr " | %sn : forall n, word w%i (S n) -> %s_." c size t;
@@ -167,20 +159,20 @@ let _ =
pr " Definition to_N x := Zabs_N (to_Z x).";
pr "";
-
+
pr " Definition eq x y := (to_Z x = to_Z y).";
pr "";
pp " (* Regular make op (no karatsuba) *)";
- pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) : ";
+ pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) :";
pp " znz_op (word ww n) :=";
- pp " match n return znz_op (word ww n) with ";
+ pp " match n return znz_op (word ww n) with";
pp " O => ww_op";
- pp " | S n1 => mk_zn2z_op (nmake_op ww ww_op n1) ";
+ pp " | S n1 => mk_zn2z_op (nmake_op ww ww_op n1)";
pp " end.";
pp "";
pp " (* Simplification by rewriting for nmake_op *)";
- pp " Theorem nmake_op_S: forall ww (w_op: znz_op ww) x, ";
+ pp " Theorem nmake_op_S: forall ww (w_op: znz_op ww) x,";
pp " nmake_op _ w_op (S x) = mk_zn2z_op (nmake_op _ w_op x).";
pp " auto.";
pp " Qed.";
@@ -191,7 +183,7 @@ let _ =
for i = 0 to size do
pp " Let nmake_op%i := nmake_op _ w%i_op." i i;
pp " Let eval%in n := znz_to_Z (nmake_op%i n)." i i;
- if i == 0 then
+ if i == 0 then
pr " Let extend%i := DoubleBase.extend (WW w_0)." i
else
pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i;
@@ -199,8 +191,8 @@ let _ =
pr "";
- pp " Theorem digits_doubled:forall n ww (w_op: znz_op ww), ";
- pp " znz_digits (nmake_op _ w_op n) = ";
+ pp " Theorem digits_doubled:forall n ww (w_op: znz_op ww),";
+ pp " znz_digits (nmake_op _ w_op n) =";
pp " DoubleBase.double_digits (znz_digits w_op) n.";
pp " Proof.";
pp " intros n; elim n; auto; clear n.";
@@ -208,7 +200,7 @@ let _ =
pp " rewrite <- Hrec; auto.";
pp " Qed.";
pp "";
- pp " Theorem nmake_double: forall n ww (w_op: znz_op ww), ";
+ pp " Theorem nmake_double: forall n ww (w_op: znz_op ww),";
pp " znz_to_Z (nmake_op _ w_op n) =";
pp " @DoubleBase.double_to_Z _ (znz_digits w_op) (znz_to_Z w_op) n.";
pp " Proof.";
@@ -220,8 +212,8 @@ let _ =
pp "";
- pp " Theorem digits_nmake:forall n ww (w_op: znz_op ww), ";
- pp " znz_digits (nmake_op _ w_op (S n)) = ";
+ pp " Theorem digits_nmake:forall n ww (w_op: znz_op ww),";
+ pp " znz_digits (nmake_op _ w_op (S n)) =";
pp " xO (znz_digits (nmake_op _ w_op n)).";
pp " Proof.";
pp " auto.";
@@ -257,30 +249,30 @@ let _ =
pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op n)))).";
pp " rewrite Hrec; auto with arith.";
pp " Qed.";
- pp " ";
+ pp "";
for i = 1 to size + 2 do
pp " Let znz_to_Z_%i: forall x y," i;
- pp " znz_to_Z w%i_op (WW x y) = " i;
+ pp " znz_to_Z w%i_op (WW x y) =" i;
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);
pp " Proof.";
pp " auto.";
- pp " Qed. ";
+ pp " Qed.";
pp "";
done;
pp " Let znz_to_Z_n: forall n x y,";
- pp " znz_to_Z (make_op (S n)) (WW x y) = ";
+ pp " znz_to_Z (make_op (S n)) (WW x y) =";
pp " znz_to_Z (make_op n) x * base (znz_digits (make_op n)) + znz_to_Z (make_op n) y.";
pp " Proof.";
pp " intros n x y; rewrite make_op_S; auto.";
- pp " Qed. ";
+ pp " Qed.";
pp "";
pp " Let w0_spec: znz_spec w0_op := W0.w_spec.";
for i = 1 to 3 do
- pp " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec." i i (i-1)
+ pp " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec." i i (i-1)
done;
for i = 4 to size + 3 do
pp " Let w%i_spec : znz_spec w%i_op := mk_znz2_karatsuba_spec w%i_spec." i i (i-1)
@@ -309,14 +301,14 @@ let _ =
for i = 0 to size do
- pp " Theorem digits_w%i: znz_digits w%i_op = znz_digits (nmake_op _ w0_op %i)." i i i;
+ pp " Theorem digits_w%i: znz_digits w%i_op = znz_digits (nmake_op _ w0_op %i)." i i i;
if i == 0 then
pp " auto."
else
pp " rewrite digits_nmake; rewrite <- digits_w%i; auto." (i - 1);
pp " Qed.";
pp "";
- 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;
+ 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;
pp " Proof.";
pp " intros n; exact (nmake_double n w%i w%i_op)." i i;
pp " Qed.";
@@ -325,7 +317,7 @@ let _ =
for i = 0 to size do
for j = 0 to (size - i) do
- 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;
+ 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;
pp " Proof.";
if j == 0 then
if i == 0 then
@@ -346,7 +338,7 @@ let _ =
end;
pp " Qed.";
pp "";
- pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j;
+ pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j;
pp " Proof.";
if j == 0 then
pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i
@@ -363,7 +355,7 @@ let _ =
pp " Qed.";
if i + j <> size then
begin
- 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;
+ 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;
if j == 0 then
begin
pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." i (i + j);
@@ -393,7 +385,7 @@ let _ =
pp " Qed.";
pp "";
- pp " Let spec_eval%in%i: forall x, [%sn 0 x] = eval%in %i x." i (size - i + 1) c i (size - i + 1);
+ pp " Let spec_eval%in%i: forall x, [%sn 0 x] = eval%in %i x." i (size - i + 1) c i (size - i + 1);
pp " Proof.";
pp " intros x; case x.";
pp " auto.";
@@ -405,7 +397,7 @@ let _ =
pp " Qed.";
pp "";
- pp " Let spec_eval%in%i: forall x, [%sn 1 x] = eval%in %i x." i (size - i + 2) c i (size - i + 2);
+ pp " Let spec_eval%in%i: forall x, [%sn 1 x] = eval%in %i x." i (size - i + 2) c i (size - i + 2);
pp " intros x; case x.";
pp " auto.";
pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 2);
@@ -430,7 +422,7 @@ let _ =
pp " Qed.";
pp "";
- pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size;
+ pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size;
pp " intros n; elim n; clear n.";
pp " exact spec_eval%in1." size;
pp " intros n Hrec x; case x; clear x.";
@@ -446,7 +438,7 @@ let _ =
pp " Qed.";
pp "";
- pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ;
+ pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ;
pp " intros n; elim n; clear n.";
pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." size size;
pp " unfold to_Z.";
@@ -478,7 +470,6 @@ let _ =
pp " unfold to_Z.";
pp " case n1; auto; intros n2; repeat rewrite make_op_S; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_extendn_0: extr.";
pp "";
pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c;
pp " Proof.";
@@ -489,7 +480,6 @@ let _ =
pp " case n; auto.";
pp " intros n1; rewrite make_op_S; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_extendn_0: extr.";
pp "";
pp " Let spec_extend_tr: forall m n (w: word _ (S n)),";
pp " [%sn (m + n) (extend_tr w m)] = [%sn n w]." c c;
@@ -498,7 +488,6 @@ let _ =
pp " intros n x; simpl extend_tr.";
pp " simpl plus; rewrite spec_extendn0_0; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_extend_tr: extr.";
pp "";
pp " Let spec_cast_l: forall n m x1,";
pp " [%sn (Max.max n m)" c;
@@ -508,7 +497,6 @@ let _ =
pp " intros n m x1; case (diff_r n m); simpl castm.";
pp " rewrite spec_extend_tr; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_cast_l: extr.";
pp "";
pp " Let spec_cast_r: forall n m x1,";
pp " [%sn (Max.max n m)" c;
@@ -518,7 +506,6 @@ let _ =
pp " intros n m x1; case (diff_l n m); simpl castm.";
pp " rewrite spec_extend_tr; auto.";
pp " Qed.";
- pp " Hint Rewrite spec_cast_r: extr.";
pp "";
@@ -578,14 +565,14 @@ let _ =
pr " | %s%i wx, %s%i wy => f%i (extend%i %i wx) wy" c i c j j i (j - i - 1);
done;
if i == size then
- pr " | %s%i wx, %sn m wy => fnn m (extend%i m wx) wy" c size c size
- else
+ pr " | %s%i wx, %sn m wy => fnn m (extend%i m wx) wy" c size c size
+ else
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);
done;
for i = 0 to size do
if i == size then
- pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n wy)" c c size size
- else
+ pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n wy)" c c size size
+ else
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);
done;
pr " | %sn n wx, Nn m wy =>" c;
@@ -611,17 +598,17 @@ let _ =
done;
if i == size then
pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size
- else
+ else
pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size;
done;
pp " intros n x y; case y; clear y.";
for i = 0 to size do
if i == size then
pp " intros y; rewrite (spec_extend%in n); apply Pfnn." size
- else
+ else
pp " intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size;
done;
- pp " intros m y; rewrite <- (spec_cast_l n m x); ";
+ pp " intros m y; rewrite <- (spec_cast_l n m x);";
pp " rewrite <- (spec_cast_r n m y); apply Pfnn.";
pp " Qed.";
pp "";
@@ -644,7 +631,7 @@ let _ =
pr " match y with";
for j = 0 to i - 1 do
pr " | %s%i wy =>" c j;
- if j == 0 then
+ if j == 0 then
pr " if w0_eq0 wy then ft0 x else";
pr " f%i wx (extend%i %i wy)" i j (i - j -1);
done;
@@ -653,8 +640,8 @@ let _ =
pr " | %s%i wy => f%i (extend%i %i wx) wy" c j j i (j - i - 1);
done;
if i == size then
- pr " | %sn m wy => fnn m (extend%i m wx) wy" c size
- else
+ pr " | %sn m wy => fnn m (extend%i m wx) wy" c size
+ else
pr " | %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c size i (size - i - 1);
pr" end";
done;
@@ -665,8 +652,8 @@ let _ =
if i == 0 then
pr " if w0_eq0 wy then ft0 x else";
if i == size then
- pr " fnn n wx (extend%i n wy)" size
- else
+ pr " fnn n wx (extend%i n wy)" size
+ else
pr " fnn n wx (extend%i n (extend%i %i wy))" size i (size - i - 1);
done;
pr " | %sn m wy =>" c;
@@ -707,7 +694,7 @@ let _ =
done;
if i == size then
pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size
- else
+ else
pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size;
done;
pp " intros n x y; case y; clear y.";
@@ -721,16 +708,16 @@ let _ =
end;
if i == size then
pp " rewrite (spec_extend%in n); apply Pfnn." size
- else
+ else
pp " rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size;
done;
- pp " intros m y; rewrite <- (spec_cast_l n m x); ";
+ pp " intros m y; rewrite <- (spec_cast_l n m x);";
pp " rewrite <- (spec_cast_r n m y); apply Pfnn.";
pp " Qed.";
pp "";
pr " (* We iter the smaller argument with the bigger *)";
- pr " Definition iter (x y: t_): res := ";
+ pr " Definition iter (x y: t_): res :=";
pr0 " Eval lazy zeta beta iota delta [";
for i = 0 to size do
pr0 "extend%i " i;
@@ -748,14 +735,14 @@ let _ =
pr " | %s%i wx, %s%i wy => f%in %i wx wy" c i c j i (j - i - 1);
done;
if i == size then
- pr " | %s%i wx, %sn m wy => f%in m wx wy" c size c size
- else
+ pr " | %s%i wx, %sn m wy => f%in m wx wy" c size c size
+ else
pr " | %s%i wx, %sn m wy => f%in m (extend%i %i wx) wy" c i c size i (size - i - 1);
done;
for i = 0 to size do
if i == size then
- pr " | %sn n wx, %s%i wy => fn%i n wx wy" c c size size
- else
+ pr " | %sn n wx, %s%i wy => fn%i n wx wy" c c size size
+ else
pr " | %sn n wx, %s%i wy => fn%i n wx (extend%i %i wy)" c c i size i (size - i - 1);
done;
pr " | %sn n wx, %sn m wy => fnm n m wx wy" c c;
@@ -765,6 +752,7 @@ let _ =
pp " Ltac zg_tac := try";
pp " (red; simpl Zcompare; auto;";
pp " let t := fresh \"H\" in (intros t; discriminate t)).";
+ pp "";
pp " Lemma spec_iter: forall x y, P [x] [y] (iter x y).";
pp " Proof.";
pp " intros x; case x; clear x; unfold iter.";
@@ -779,14 +767,14 @@ let _ =
done;
if i == size then
pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size
- else
+ else
pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
done;
pp " intros n x y; case y; clear y.";
for i = 0 to size do
if i == size then
pp " intros y; rewrite spec_eval%in; apply Pfn%i." size size
- else
+ else
pp " intros y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
done;
pp " intros m y; apply Pfnm.";
@@ -820,8 +808,8 @@ let _ =
pr " | %s%i wy => f%in %i wx wy" c j i (j - i - 1);
done;
if i == size then
- pr " | %sn m wy => f%in m wx wy" c size
- else
+ pr " | %sn m wy => f%in m wx wy" c size
+ else
pr " | %sn m wy => f%in m (extend%i %i wx) wy" c size i (size - i - 1);
pr " end";
done;
@@ -832,8 +820,8 @@ let _ =
if i == 0 then
pr " if w0_eq0 wy then ft0 x else";
if i == size then
- pr " fn%i n wx wy" size
- else
+ pr " fn%i n wx wy" size
+ else
pr " fn%i n wx (extend%i %i wy)" size i (size - i - 1);
done;
pr " | %sn m wy => fnm n m wx wy" c;
@@ -869,7 +857,7 @@ let _ =
done;
if i == size then
pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size
- else
+ else
pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size;
done;
pp " intros n x y; case y; clear y.";
@@ -883,7 +871,7 @@ let _ =
end;
if i == size then
pp " rewrite spec_eval%in; apply Pfn%i." size size
- else
+ else
pp " rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size;
done;
pp " intros m y; apply Pfnm.";
@@ -897,27 +885,27 @@ let _ =
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Reduction *)";
+ pr " (** * Reduction *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
- pr " Definition reduce_0 (x:w) := %s0 x." c;
+ pr " Definition reduce_0 (x:w) := %s0 x." c;
pr " Definition reduce_1 :=";
pr " Eval lazy beta iota delta[reduce_n1] in";
pr " reduce_n1 _ _ zero w0_eq0 %s0 %s1." c c;
for i = 2 to size do
pr " Definition reduce_%i :=" i;
pr " Eval lazy beta iota delta[reduce_n1] in";
- pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i %s%i."
+ pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i %s%i."
(i-1) (i-1) c i
done;
pr " Definition reduce_%i :=" (size+1);
pr " Eval lazy beta iota delta[reduce_n1] in";
- pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i (%sn 0)."
- size size c;
+ pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i (%sn 0)."
+ size size c;
- pr " Definition reduce_n n := ";
+ pr " Definition reduce_n n :=";
pr " Eval lazy beta iota delta[reduce_n] in";
pr " reduce_n _ _ zero reduce_%i %sn n." (size + 1) c;
pr "";
@@ -927,7 +915,7 @@ let _ =
pp " intros x; unfold to_Z, reduce_0.";
pp " auto.";
pp " Qed.";
- pp " ";
+ pp "";
for i = 1 to size + 1 do
if i == size + 1 then
@@ -938,14 +926,14 @@ let _ =
pp " intros x; case x; unfold reduce_%i." i;
pp " exact (spec_0 w0_spec).";
pp " intros x1 y1.";
- pp " generalize (spec_w%i_eq0 x1); " (i - 1);
+ pp " generalize (spec_w%i_eq0 x1);" (i - 1);
pp " case w%i_eq0; intros H1; auto." (i - 1);
- if i <> 1 then
+ if i <> 1 then
pp " rewrite spec_reduce_%i." (i - 1);
pp " unfold to_Z; rewrite znz_to_Z_%i." i;
pp " unfold to_Z in H1; rewrite H1; auto.";
pp " Qed.";
- pp " ";
+ pp "";
done;
pp " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x]." c;
@@ -959,11 +947,11 @@ let _ =
pp " rewrite Hrec.";
pp " rewrite spec_extendn0_0; auto.";
pp " Qed.";
- pp " ";
+ pp "";
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Successor *)";
+ pr " (** * Successor *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
@@ -983,19 +971,19 @@ let _ =
for i = 0 to size-1 do
pr " | %s%i wx =>" c i;
pr " match w%i_succ_c wx with" i;
- pr " | C0 r => %s%i r" c i;
+ pr " | C0 r => %s%i r" c i;
pr " | C1 r => %s%i (WW one%i r)" c (i+1) i;
pr " end";
done;
pr " | %s%i wx =>" c size;
pr " match w%i_succ_c wx with" size;
- pr " | C0 r => %s%i r" c size;
+ pr " | C0 r => %s%i r" c size;
pr " | C1 r => %sn 0 (WW one%i r)" c size ;
pr " end";
pr " | %sn n wx =>" c;
pr " let op := make_op n in";
pr " match op.(znz_succ_c) wx with";
- pr " | C0 r => %sn n r" c;
+ pr " | C0 r => %sn n r" c;
pr " | C1 r => %sn (S n) (WW op.(znz_1) r)" c;
pr " end";
pr " end.";
@@ -1027,13 +1015,13 @@ let _ =
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Adddition *)";
+ pr " (** * Adddition *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
for i = 0 to size do
- pr " Definition w%i_add_c := znz_add_c w%i_op." i i;
+ pr " Definition w%i_add_c := znz_add_c w%i_op." i i;
pr " Definition w%i_add x y :=" i;
pr " match w%i_add_c x y with" i;
pr " | C0 r => %s%i r" c i;
@@ -1057,26 +1045,24 @@ let _ =
pp " Proof.";
pp " intros n m; unfold to_Z, w%i_add, w%i_add_c." i i;
pp " generalize (spec_add_c w%i_spec n m); case znz_add_c; auto." i;
- pp " intros ww H; rewrite <- H.";
+ pp " intros ww H; rewrite <- H.";
pp " rewrite znz_to_Z_%i; unfold interp_carry;" (i + 1);
pp " apply f_equal2 with (f := Zplus); auto;";
pp " apply f_equal2 with (f := Zmult); auto;";
pp " exact (spec_1 w%i_spec)." i;
pp " Qed.";
- pp " Hint Rewrite spec_w%i_add: addr." i;
pp "";
done;
pp " Let spec_wn_add: forall n x y, [addn n x y] = [%sn n x] + [%sn n y]." c c;
pp " Proof.";
pp " intros k n m; unfold to_Z, addn.";
pp " generalize (spec_add_c (wn_spec k) n m); case znz_add_c; auto.";
- pp " intros ww H; rewrite <- H.";
+ pp " intros ww H; rewrite <- H.";
pp " rewrite (znz_to_Z_n k); unfold interp_carry;";
pp " apply f_equal2 with (f := Zplus); auto;";
pp " apply f_equal2 with (f := Zmult); auto;";
pp " exact (spec_1 (wn_spec k)).";
pp " Qed.";
- pp " Hint Rewrite spec_wn_add: addr.";
pr " Definition add := Eval lazy beta delta [same_level] in";
pr0 " (same_level t_ ";
@@ -1101,7 +1087,7 @@ let _ =
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Predecessor *)";
+ pr " (** * Predecessor *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
@@ -1116,25 +1102,25 @@ let _ =
for i = 0 to size do
pr " | %s%i wx =>" c i;
pr " match w%i_pred_c wx with" i;
- pr " | C0 r => reduce_%i r" i;
+ pr " | C0 r => reduce_%i r" i;
pr " | C1 r => zero";
pr " end";
done;
pr " | %sn n wx =>" c;
pr " let op := make_op n in";
pr " match op.(znz_pred_c) wx with";
- pr " | C0 r => reduce_n n r";
+ pr " | C0 r => reduce_n n r";
pr " | C1 r => zero";
pr " end";
pr " end.";
pr "";
- pr " Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.";
+ pr " Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1.";
pa " Admitted.";
pp " Proof.";
pp " intros x; case x; unfold pred.";
for i = 0 to size do
- pp " intros x1 H1; unfold w%i_pred_c; " i;
+ pp " intros x1 H1; unfold w%i_pred_c;" i;
pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i;
pp " rewrite spec_reduce_%i; auto." i;
pp " unfold interp_carry; unfold to_Z.";
@@ -1143,7 +1129,7 @@ let _ =
pp " assert (znz_to_Z w%i_op x1 - 1 < 0); auto with zarith." i;
pp " unfold to_Z in H1; auto with zarith.";
done;
- pp " intros n x1 H1; ";
+ pp " intros n x1 H1;";
pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.";
pp " rewrite spec_reduce_n; auto.";
pp " unfold interp_carry; unfold to_Z.";
@@ -1152,32 +1138,31 @@ let _ =
pp " assert (znz_to_Z (make_op n) x1 - 1 < 0); auto with zarith.";
pp " unfold to_Z in H1; auto with zarith.";
pp " Qed.";
- pp " ";
-
+ pp "";
+
pp " Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0.";
pp " Proof.";
pp " intros x; case x; unfold pred.";
for i = 0 to size do
- pp " intros x1 H1; unfold w%i_pred_c; " i;
+ pp " intros x1 H1; unfold w%i_pred_c;" i;
pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i;
pp " unfold interp_carry; unfold to_Z.";
pp " unfold to_Z in H1; auto with zarith.";
pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4; auto with zarith." i;
pp " intros; exact (spec_0 w0_spec).";
done;
- pp " intros n x1 H1; ";
+ pp " intros n x1 H1;";
pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.";
pp " unfold interp_carry; unfold to_Z.";
pp " unfold to_Z in H1; auto with zarith.";
pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith.";
pp " intros; exact (spec_0 w0_spec).";
pp " Qed.";
- pr " ";
-
+ pr "";
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Subtraction *)";
+ pr " (** * Subtraction *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
@@ -1187,7 +1172,7 @@ let _ =
done;
pr "";
- for i = 0 to size do
+ for i = 0 to size do
pr " Definition w%i_sub x y :=" i;
pr " match w%i_sub_c x y with" i;
pr " | C0 r => reduce_%i r" i;
@@ -1208,8 +1193,8 @@ let _ =
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;
pp " Proof.";
pp " intros n m; unfold w%i_sub, w%i_sub_c." i i;
- pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; " i;
- if i == 0 then
+ pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c;" i;
+ if i == 0 then
pp " intros x; auto."
else
pp " intros x; try rewrite spec_reduce_%i; auto." i;
@@ -1219,11 +1204,11 @@ let _ =
pp " Qed.";
pp "";
done;
-
+
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;
pp " Proof.";
pp " intros k n m; unfold subn.";
- pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; ";
+ pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c;";
pp " intros x; auto.";
pp " unfold interp_carry, to_Z.";
pp " case (spec_to_Z (wn_spec k) x); intros; auto with zarith.";
@@ -1238,7 +1223,7 @@ let _ =
pr "subn).";
pr "";
- pr " Theorem spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y].";
+ pr " Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y].";
pa " Admitted.";
pp " Proof.";
pp " unfold sub.";
@@ -1255,7 +1240,7 @@ let _ =
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;
pp " Proof.";
pp " intros n m; unfold w%i_sub, w%i_sub_c." i i;
- pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; " i;
+ pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c;" i;
pp " intros x; unfold interp_carry.";
pp " unfold to_Z; case (spec_to_Z w%i_spec x); intros; auto with zarith." i;
pp " intros; unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto.";
@@ -1266,7 +1251,7 @@ let _ =
pp " Let spec_wn_sub0: forall n x y, [%sn n x] < [%sn n y] -> [subn n x y] = 0." c c;
pp " Proof.";
pp " intros k n m; unfold subn.";
- pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; ";
+ pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c;";
pp " intros x; unfold interp_carry.";
pp " unfold to_Z; case (spec_to_Z (wn_spec k) x); intros; auto with zarith.";
pp " intros; unfold to_Z, w_0; rewrite (spec_0 (w0_spec)); auto.";
@@ -1289,7 +1274,7 @@ let _ =
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Comparison *)";
+ pr " (** * Comparison *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
@@ -1299,7 +1284,7 @@ let _ =
pr " Definition comparen_%i :=" i;
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
done;
- pr "";
+ pr "";
pr " Definition comparenm n m wx wy :=";
pr " let mn := Max.max n m in";
@@ -1310,8 +1295,8 @@ let _ =
pr " (castm (diff_l n m) (extend_tr wy (fst d))).";
pr "";
- pr " Definition compare := Eval lazy beta delta [iter] in ";
- pr " (iter _ ";
+ pr " Definition compare := Eval lazy beta delta [iter] in";
+ pr " (iter _";
for i = 0 to size do
pr " compare_%i" i;
pr " (fun n x y => opp_compare (comparen_%i (S n) y x))" i;
@@ -1320,15 +1305,9 @@ let _ =
pr " comparenm).";
pr "";
- pr " Definition lt n m := compare n m = Lt.";
- pr " Definition le n m := compare n m <> Gt.";
- pr " Definition min n m := match compare n m with Gt => m | _ => n end.";
- pr " Definition max n m := match compare n m with Lt => m | _ => n end.";
- pr "";
-
for i = 0 to size do
pp " Let spec_compare_%i: forall x y," i;
- pp " match compare_%i x y with " i;
+ pp " match compare_%i x y with" i;
pp " Eq => [%s%i x] = [%s%i y]" c i c i;
pp " | Lt => [%s%i x] < [%s%i y]" c i c i;
pp " | Gt => [%s%i x] > [%s%i y]" c i c i;
@@ -1337,7 +1316,7 @@ let _ =
pp " unfold compare_%i, to_Z; exact (spec_compare w%i_spec)." i i;
pp " Qed.";
pp "";
-
+
pp " Let spec_comparen_%i:" i;
pp " forall (n : nat) (x : word w%i n) (y : w%i)," i i;
pp " match comparen_%i n x y with" i;
@@ -1367,16 +1346,16 @@ let _ =
pp "";
- pr " Theorem spec_compare: forall x y,";
- pr " match compare x y with ";
+ pr " Theorem spec_compare_aux: forall x y,";
+ pr " match compare x y with";
pr " Eq => [x] = [y]";
pr " | Lt => [x] < [y]";
pr " | Gt => [x] > [y]";
pr " end.";
pa " Admitted.";
pp " Proof.";
- pp " refine (spec_iter _ (fun x y res => ";
- pp " match res with ";
+ pp " refine (spec_iter _ (fun x y res =>";
+ pp " match res with";
pp " Eq => x = y";
pp " | Lt => x < y";
pp " | Gt => x > y";
@@ -1387,12 +1366,12 @@ let _ =
pp " (fun n => comparen_%i (S n)) _ _ _" i;
done;
pp " comparenm _).";
-
+
for i = 0 to size - 1 do
pp " exact spec_compare_%i." i;
pp " intros n x y H;apply spec_opp_compare; apply spec_comparen_%i." i;
pp " intros n x y H; exact (spec_comparen_%i (S n) x y)." i;
- done;
+ done;
pp " exact spec_compare_%i." size;
pp " intros n x y;apply spec_opp_compare; apply spec_comparen_%i." size;
pp " intros n; exact (spec_comparen_%i (S n))." size;
@@ -1402,28 +1381,9 @@ let _ =
pp " Qed.";
pr "";
- pr " Definition eq_bool x y :=";
- pr " match compare x y with";
- pr " | Eq => true";
- pr " | _ => false";
- pr " end.";
- pr "";
-
-
- pr " Theorem spec_eq_bool: forall x y,";
- pr " if eq_bool x y then [x] = [y] else [x] <> [y].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x y; unfold eq_bool.";
- pp " generalize (spec_compare x y); case compare; auto with zarith.";
- pp " Qed.";
- pr "";
-
-
-
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Multiplication *)";
+ pr " (** * Multiplication *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
@@ -1461,7 +1421,7 @@ let _ =
pr " match n return word w%i (S n) -> t_ with" i;
for j = 0 to size - i do
if (i + j) == size then
- begin
+ begin
pr " | %i%s => fun x => %sn 0 x" j "%nat" c;
pr " | %i%s => fun x => %sn 1 x" (j + 1) "%nat" c
end
@@ -1471,7 +1431,7 @@ let _ =
pr " | _ => fun _ => N0 w_0";
pr " end.";
pr "";
- done;
+ done;
for i = 0 to size - 1 do
@@ -1486,7 +1446,7 @@ let _ =
pp " repeat rewrite inj_S; unfold Zsucc; auto with zarith.";
pp " Qed.";
pp "";
- done;
+ done;
for i = 0 to size do
@@ -1497,8 +1457,8 @@ let _ =
pr " if w%i_eq0 w then %sn n r" i c;
pr " else %sn (S n) (WW (extend%i n w) r)." c i;
end
- else
- begin
+ else
+ begin
pr " if w%i_eq0 w then to_Z%i n r" i i;
pr " else to_Z%i (S n) (WW (extend%i n w) r)." i i;
end;
@@ -1514,10 +1474,10 @@ let _ =
pr " (castm (diff_l n m) (extend_tr y (fst d)))).";
pr "";
- pr " Definition mul := Eval lazy beta delta [iter0] in ";
- pr " (iter0 t_ ";
+ pr " Definition mul := Eval lazy beta delta [iter0] in";
+ pr " (iter0 t_";
for i = 0 to size do
- pr " (fun x y => reduce_%i (w%i_mul_c x y)) " (i + 1) i;
+ pr " (fun x y => reduce_%i (w%i_mul_c x y))" (i + 1) i;
pr " (fun n x y => w%i_mul n y x)" i;
pr " w%i_mul" i;
done;
@@ -1556,7 +1516,7 @@ let _ =
pp " Qed.";
pp "";
done;
-
+
pp " Lemma nmake_op_WW: forall ww ww1 n x y,";
pp " znz_to_Z (nmake_op ww ww1 (S n)) (WW x y) =";
pp " znz_to_Z (nmake_op ww ww1 n) x * base (znz_digits (nmake_op ww ww1 n)) +";
@@ -1564,21 +1524,21 @@ let _ =
pp " auto.";
pp " Qed.";
pp "";
-
+
for i = 0 to size do
pp " Lemma extend%in_spec: forall n x1," i;
- pp " znz_to_Z (nmake_op _ w%i_op (S n)) (extend%i n x1) = " i i;
+ pp " znz_to_Z (nmake_op _ w%i_op (S n)) (extend%i n x1) =" i i;
pp " znz_to_Z w%i_op x1." i;
pp " Proof.";
pp " intros n1 x2; rewrite nmake_double.";
pp " unfold extend%i." i;
pp " rewrite DoubleBase.spec_extend; auto.";
- if i == 0 then
+ if i == 0 then
pp " intros l; simpl; unfold w_0; rewrite (spec_0 w0_spec); ring.";
pp " Qed.";
pp "";
done;
-
+
pp " Lemma spec_muln:";
pp " forall n (x: word _ (S n)) y,";
pp " [%sn (S n) (znz_mul_c (make_op n) x y)] = [%sn n x] * [%sn n y]." c c c;
@@ -1588,12 +1548,13 @@ let _ =
pp " rewrite make_op_S.";
pp " case znz_mul_c; auto.";
pp " Qed.";
+ pr "";
pr " Theorem spec_mul: forall x y, [mul x y] = [x] * [y].";
pa " Admitted.";
pp " Proof.";
for i = 0 to size do
- pp " assert(F%i: " i;
+ pp " assert(F%i:" i;
pp " forall n x y,";
if i <> size then
pp0 " Z_of_nat n <= %i -> " (size - i);
@@ -1614,7 +1575,7 @@ let _ =
pp " generalize (spec_w%i_eq0 x1); case w%i_eq0; intros HH." i i;
pp " unfold to_Z in HH; rewrite HH.";
if i == size then
- begin
+ begin
pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i; auto." i i i;
pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i." i i i
end
@@ -1627,7 +1588,7 @@ let _ =
done;
pp " refine (spec_iter0 t_ (fun x y res => [res] = x * y)";
for i = 0 to size do
- pp " (fun x y => reduce_%i (w%i_mul_c x y)) " (i + 1) i;
+ pp " (fun x y => reduce_%i (w%i_mul_c x y))" (i + 1) i;
pp " (fun n x y => w%i_mul n y x)" i;
pp " w%i_mul _ _ _" i;
done;
@@ -1643,12 +1604,12 @@ let _ =
if i == size then
begin
pp " intros n x y; rewrite F%i; auto with zarith." i;
- pp " intros n x y; rewrite F%i; auto with zarith. " i;
+ pp " intros n x y; rewrite F%i; auto with zarith." i;
end
else
begin
pp " intros n x y H; rewrite F%i; auto with zarith." i;
- pp " intros n x y H; rewrite F%i; auto with zarith. " i;
+ pp " intros n x y H; rewrite F%i; auto with zarith." i;
end;
done;
pp " intros n m x y; unfold mulnm.";
@@ -1663,7 +1624,7 @@ let _ =
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Square *)";
+ pr " (** * Square *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
@@ -1702,42 +1663,9 @@ let _ =
pp "Qed.";
pr "";
-
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Power *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
- pr " Fixpoint power_pos (x:%s) (p:positive) {struct p} : %s :=" t t;
- pr " match p with";
- pr " | xH => x";
- pr " | xO p => square (power_pos x p)";
- pr " | xI p => mul (square (power_pos x p)) x";
- pr " end.";
- pr "";
-
- pr " Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x n; generalize x; elim n; clear n x; simpl power_pos.";
- pp " intros; rewrite spec_mul; rewrite spec_square; rewrite H.";
- pp " rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith.";
- pp " rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.";
- pp " rewrite Zpower_2; rewrite Zpower_1_r; auto.";
- pp " intros; rewrite spec_square; rewrite H.";
- pp " rewrite Zpos_xO; auto with zarith.";
- pp " rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.";
- pp " rewrite Zpower_2; auto.";
- pp " intros; rewrite Zpower_1_r; auto.";
- pp " Qed.";
- pp "";
- pr "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (* Square root *)";
+ pr " (** * Square root *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
@@ -1772,26 +1700,26 @@ let _ =
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Division *)";
+ pr " (** * Division *)";
pr " (* *)";
pr " (***************************************************************)";
- pr "";
+ pr "";
for i = 0 to size do
pr " Definition w%i_div_gt := w%i_op.(znz_div_gt)." i i
done;
pr "";
- pp " Let spec_divn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := ";
- pp " (spec_double_divn1 ";
+ pp " Let spec_divn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) :=";
+ pp " (spec_double_divn1";
pp " ww_op.(znz_zdigits) ww_op.(znz_0)";
pp " (znz_WW ww_op) ww_op.(znz_head0)";
pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)";
pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)";
- pp " (spec_to_Z ww_spec) ";
+ pp " (spec_to_Z ww_spec)";
pp " (spec_zdigits ww_spec)";
pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)";
- pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) ";
+ pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec)";
pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec)).";
pp "";
@@ -1811,7 +1739,7 @@ let _ =
for i = 0 to size do
pp " Lemma spec_get_end%i: forall n x y," i;
- pp " eval%in n x <= [%s%i y] -> " i c i;
+ pp " eval%in n x <= [%s%i y] ->" i c i;
pp " [%s%i (DoubleBase.get_low %s n x)] = eval%in n x." c i (pz i) i;
pp " Proof.";
pp " intros n x y H.";
@@ -1843,8 +1771,8 @@ let _ =
pr "";
pr " Definition div_gt := Eval lazy beta delta [iter] in";
- pr " (iter _ ";
- for i = 0 to size do
+ pr " (iter _";
+ for i = 0 to size do
pr " div_gt%i" i;
pr " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i);
pr " w%i_divn1" i;
@@ -1862,10 +1790,10 @@ let _ =
pp " forall x y, [x] > [y] -> 0 < [y] ->";
pp " let (q,r) := div_gt x y in";
pp " [x] = [q] * [y] + [r] /\\ 0 <= [r] < [y]).";
- pp " refine (spec_iter (t_*t_) (fun x y res => x > y -> 0 < y ->";
+ pp " refine (spec_iter (t_*t_) (fun x y res => x > y -> 0 < y ->";
pp " let (q,r) := res in";
pp " x = [q] * y + [r] /\\ 0 <= [r] < y)";
- for i = 0 to size do
+ for i = 0 to size do
pp " div_gt%i" i;
pp " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i);
pp " w%i_divn1 _ _ _" i;
@@ -1879,11 +1807,11 @@ let _ =
pp " intros n x y H2 H3; unfold div_gt%i, w%i_div_gt." i i
else
pp " intros n x y H1 H2 H3; unfold div_gt%i, w%i_div_gt." i i;
- pp " generalize (spec_div_gt w%i_spec x " i;
+ pp " generalize (spec_div_gt w%i_spec x" i;
pp " (DoubleBase.get_low %s (S n) y))." (pz i);
- pp0 " ";
+ pp0 "";
for j = 0 to i do
- pp0 "unfold w%i; " (i-j);
+ pp0 "unfold w%i; " (i-j);
done;
pp "case znz_div_gt.";
pp " intros xx yy H4; repeat rewrite spec_reduce_%i." i;
@@ -1897,7 +1825,7 @@ let _ =
pp " (spec_divn1 w%i w%i_op w%i_spec (S n) x y H3)." i i i;
pp0 " unfold w%i_divn1; " i;
for j = 0 to i do
- pp0 "unfold w%i; " (i-j);
+ pp0 "unfold w%i; " (i-j);
done;
pp "case double_divn1.";
pp " intros xx yy H4.";
@@ -1936,61 +1864,12 @@ let _ =
pp " Qed.";
pr "";
- pr " Definition div_eucl x y :=";
- pr " match compare x y with";
- pr " | Eq => (one, zero)";
- pr " | Lt => (zero, x)";
- pr " | Gt => div_gt x y";
- pr " end.";
- pr "";
-
- pr " Theorem spec_div_eucl: forall x y,";
- pr " 0 < [y] ->";
- pr " let (q,r) := div_eucl x y in";
- pr " ([q], [r]) = Zdiv_eucl [x] [y].";
- pa " Admitted.";
- pp " Proof.";
- pp " assert (F0: [zero] = 0).";
- pp " exact (spec_0 w0_spec).";
- pp " assert (F1: [one] = 1).";
- pp " exact (spec_1 w0_spec).";
- pp " intros x y H; generalize (spec_compare x y);";
- pp " unfold div_eucl; case compare; try rewrite F0;";
- pp " try rewrite F1; intros; auto with zarith.";
- pp " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))";
- pp " (Z_mod_same [y] (Zlt_gt _ _ H));";
- pp " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.";
- pp " assert (F2: 0 <= [x] < [y]).";
- pp " generalize (spec_pos x); auto.";
- pp " generalize (Zdiv_small _ _ F2)";
- pp " (Zmod_small _ _ F2);";
- pp " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.";
- pp " generalize (spec_div_gt _ _ H0 H); auto.";
- pp " unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt.";
- pp " intros a b c d (H1, H2); subst; auto.";
- pp " Qed.";
- pr "";
-
- pr " Definition div x y := fst (div_eucl x y).";
- pr "";
-
- pr " Theorem spec_div:";
- pr " forall x y, 0 < [y] -> [div x y] = [x] / [y].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x y H1; unfold div; generalize (spec_div_eucl x y H1);";
- pp " case div_eucl; simpl fst.";
- pp " intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; ";
- pp " injection H; auto.";
- pp " Qed.";
- pr "";
-
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Modulo *)";
+ pr " (** * Modulo *)";
pr " (* *)";
pr " (***************************************************************)";
- pr "";
+ pr "";
for i = 0 to size do
pr " Definition w%i_mod_gt := w%i_op.(znz_mod_gt)." i i
@@ -2015,7 +1894,7 @@ let _ =
pr "";
pr " Definition mod_gt := Eval lazy beta delta[iter] in";
- pr " (iter _ ";
+ pr " (iter _";
for i = 0 to size do
pr " (fun x y => reduce_%i (w%i_mod_gt x y))" i i;
pr " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i);
@@ -2024,16 +1903,16 @@ let _ =
pr " mod_gtnm).";
pr "";
- pp " Let spec_modn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := ";
- pp " (spec_double_modn1 ";
+ pp " Let spec_modn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) :=";
+ pp " (spec_double_modn1";
pp " ww_op.(znz_zdigits) ww_op.(znz_0)";
pp " (znz_WW ww_op) ww_op.(znz_head0)";
pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)";
pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)";
- pp " (spec_to_Z ww_spec) ";
+ pp " (spec_to_Z ww_spec)";
pp " (spec_zdigits ww_spec)";
pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)";
- pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) ";
+ pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec)";
pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec)).";
pp "";
@@ -2063,7 +1942,7 @@ let _ =
pp " rewrite <- (spec_get_end%i (S n) y x) in H3; auto with zarith." i;
if i == size then
pp " intros n x y H2 H3; rewrite spec_reduce_%i." i
- else
+ else
pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i;
pp " unfold w%i_modn1, to_Z; rewrite spec_double_eval%in." i i;
pp " apply (spec_modn1 _ _ w%i_spec); auto." i;
@@ -2079,39 +1958,9 @@ let _ =
pp " Qed.";
pr "";
- pr " Definition modulo x y := ";
- pr " match compare x y with";
- pr " | Eq => zero";
- pr " | Lt => x";
- pr " | Gt => mod_gt x y";
- pr " end.";
+ pr " (** digits: a measure for gcd *)";
pr "";
- pr " Theorem spec_modulo:";
- pr " forall x y, 0 < [y] -> [modulo x y] = [x] mod [y].";
- pa " Admitted.";
- pp " Proof.";
- pp " assert (F0: [zero] = 0).";
- pp " exact (spec_0 w0_spec).";
- pp " assert (F1: [one] = 1).";
- pp " exact (spec_1 w0_spec).";
- pp " intros x y H; generalize (spec_compare x y);";
- pp " unfold modulo; case compare; try rewrite F0;";
- pp " try rewrite F1; intros; try split; auto with zarith.";
- pp " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith.";
- pp " apply sym_equal; apply Zmod_small; auto with zarith.";
- pp " generalize (spec_pos x); auto with zarith.";
- pp " apply spec_mod_gt; auto.";
- pp " Qed.";
- pr "";
-
- pr " (***************************************************************)";
- pr " (* *)";
- pr " (* Gcd *)";
- pr " (* *)";
- pr " (***************************************************************)";
- pr "";
-
pr " Definition digits x :=";
pr " match x with";
for i = 0 to size do
@@ -2134,189 +1983,18 @@ let _ =
pp " Qed.";
pr "";
- pr " Definition gcd_gt_body a b cont :=";
- pr " match compare b zero with";
- pr " | Gt =>";
- pr " let r := mod_gt a b in";
- pr " match compare r zero with";
- pr " | Gt => cont r (mod_gt b r)";
- pr " | _ => b";
- pr " end";
- pr " | _ => a";
- pr " end.";
- pr "";
-
- pp " Theorem Zspec_gcd_gt_body: forall a b cont p,";
- pp " [a] > [b] -> [a] < 2 ^ p ->";
- pp " (forall a1 b1, [a1] < 2 ^ (p - 1) -> [a1] > [b1] ->";
- pp " Zis_gcd [a1] [b1] [cont a1 b1]) -> ";
- pp " Zis_gcd [a] [b] [gcd_gt_body a b cont].";
- pp " Proof.";
- pp " assert (F1: [zero] = 0).";
- pp " unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto.";
- pp " intros a b cont p H2 H3 H4; unfold gcd_gt_body.";
- pp " generalize (spec_compare b zero); case compare; try rewrite F1.";
- pp " intros HH; rewrite HH; apply Zis_gcd_0.";
- pp " intros HH; absurd (0 <= [b]); auto with zarith.";
- pp " case (spec_digits b); auto with zarith.";
- pp " intros H5; generalize (spec_compare (mod_gt a b) zero); ";
- pp " case compare; try rewrite F1.";
- pp " intros H6; rewrite <- (Zmult_1_r [b]).";
- pp " rewrite (Z_div_mod_eq [a] [b]); auto with zarith.";
- pp " rewrite <- spec_mod_gt; auto with zarith.";
- pp " rewrite H6; rewrite Zplus_0_r.";
- pp " apply Zis_gcd_mult; apply Zis_gcd_1.";
- pp " intros; apply False_ind.";
- pp " case (spec_digits (mod_gt a b)); auto with zarith.";
- pp " intros H6; apply DoubleDiv.Zis_gcd_mod; auto with zarith.";
- pp " apply DoubleDiv.Zis_gcd_mod; auto with zarith.";
- pp " rewrite <- spec_mod_gt; auto with zarith.";
- pp " assert (F2: [b] > [mod_gt a b]).";
- pp " case (Z_mod_lt [a] [b]); auto with zarith.";
- pp " repeat rewrite <- spec_mod_gt; auto with zarith.";
- pp " assert (F3: [mod_gt a b] > [mod_gt b (mod_gt a b)]).";
- pp " case (Z_mod_lt [b] [mod_gt a b]); auto with zarith.";
- pp " rewrite <- spec_mod_gt; auto with zarith.";
- pp " repeat rewrite <- spec_mod_gt; auto with zarith.";
- pp " apply H4; auto with zarith.";
- pp " apply Zmult_lt_reg_r with 2; auto with zarith.";
- pp " apply Zle_lt_trans with ([b] + [mod_gt a b]); auto with zarith.";
- pp " apply Zle_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith.";
- pp " apply Zplus_le_compat_r.";
- pp " pattern [b] at 1; rewrite <- (Zmult_1_l [b]).";
- pp " apply Zmult_le_compat_r; auto with zarith.";
- pp " case (Zle_lt_or_eq 0 ([a]/[b])); auto with zarith.";
- pp " intros HH; rewrite (Z_div_mod_eq [a] [b]) in H2;";
- pp " try rewrite <- HH in H2; auto with zarith.";
- pp " case (Z_mod_lt [a] [b]); auto with zarith.";
- pp " rewrite Zmult_comm; rewrite spec_mod_gt; auto with zarith.";
- pp " rewrite <- Z_div_mod_eq; auto with zarith.";
- pp " pattern 2 at 2; rewrite <- (Zpower_1_r 2).";
- pp " rewrite <- Zpower_exp; auto with zarith.";
- pp " ring_simplify (p - 1 + 1); auto.";
- pp " case (Zle_lt_or_eq 0 p); auto with zarith.";
- pp " generalize H3; case p; simpl Zpower; auto with zarith.";
- pp " intros HH; generalize H3; rewrite <- HH; simpl Zpower; auto with zarith.";
- pp " Qed.";
- pp "";
-
- pr " Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) {struct p} : t :=";
- pr " gcd_gt_body a b";
- pr " (fun a b =>";
- pr " match p with";
- pr " | xH => cont a b";
- pr " | xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b";
- pr " | xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b";
- pr " end).";
- pr "";
-
- pp " Theorem Zspec_gcd_gt_aux: forall p n a b cont,";
- pp " [a] > [b] -> [a] < 2 ^ (Zpos p + n) ->";
- pp " (forall a1 b1, [a1] < 2 ^ n -> [a1] > [b1] ->";
- pp " Zis_gcd [a1] [b1] [cont a1 b1]) ->";
- pp " Zis_gcd [a] [b] [gcd_gt_aux p cont a b].";
- pp " intros p; elim p; clear p.";
- pp " intros p Hrec n a b cont H2 H3 H4.";
- pp " unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xI p) + n); auto.";
- pp " intros a1 b1 H6 H7.";
- pp " apply Hrec with (Zpos p + n); auto.";
- pp " replace (Zpos p + (Zpos p + n)) with";
- pp " (Zpos (xI p) + n - 1); auto.";
- pp " rewrite Zpos_xI; ring.";
- pp " intros a2 b2 H9 H10.";
- pp " apply Hrec with n; auto.";
- pp " intros p Hrec n a b cont H2 H3 H4.";
- pp " unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xO p) + n); auto.";
- pp " intros a1 b1 H6 H7.";
- pp " apply Hrec with (Zpos p + n - 1); auto.";
- pp " replace (Zpos p + (Zpos p + n - 1)) with";
- pp " (Zpos (xO p) + n - 1); auto.";
- pp " rewrite Zpos_xO; ring.";
- pp " intros a2 b2 H9 H10.";
- pp " apply Hrec with (n - 1); auto.";
- pp " replace (Zpos p + (n - 1)) with";
- pp " (Zpos p + n - 1); auto with zarith.";
- pp " intros a3 b3 H12 H13; apply H4; auto with zarith.";
- pp " apply Zlt_le_trans with (1 := H12).";
- pp " case (Zle_or_lt 1 n); intros HH.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " apply Zle_trans with 0; auto with zarith.";
- pp " assert (HH1: n - 1 < 0); auto with zarith.";
- pp " generalize HH1; case (n - 1); auto with zarith.";
- pp " intros p1 HH2; discriminate.";
- pp " intros n a b cont H H2 H3.";
- pp " simpl gcd_gt_aux.";
- pp " apply Zspec_gcd_gt_body with (n + 1); auto with zarith.";
- pp " rewrite Zplus_comm; auto.";
- pp " intros a1 b1 H5 H6; apply H3; auto.";
- pp " replace n with (n + 1 - 1); auto; try ring.";
- pp " Qed.";
- pp "";
-
- pr " Definition gcd_cont a b :=";
- pr " match compare one b with";
- pr " | Eq => one";
- pr " | _ => a";
- pr " end.";
- pr "";
-
- pr " Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b.";
- pr "";
-
- pr " Theorem spec_gcd_gt: forall a b,";
- pr " [a] > [b] -> [gcd_gt a b] = Zgcd [a] [b].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros a b H2.";
- pp " case (spec_digits (gcd_gt a b)); intros H3 H4.";
- pp " case (spec_digits a); intros H5 H6.";
- pp " apply sym_equal; apply Zis_gcd_gcd; auto with zarith.";
- pp " unfold gcd_gt; apply Zspec_gcd_gt_aux with 0; auto with zarith.";
- pp " intros a1 a2; rewrite Zpower_0_r.";
- pp " case (spec_digits a2); intros H7 H8;";
- pp " intros; apply False_ind; auto with zarith.";
- pp " Qed.";
- pr "";
-
- pr " Definition gcd a b :=";
- pr " match compare a b with";
- pr " | Eq => a";
- pr " | Lt => gcd_gt b a";
- pr " | Gt => gcd_gt a b";
- pr " end.";
- pr "";
-
- pr " Theorem spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros a b.";
- pp " case (spec_digits a); intros H1 H2.";
- pp " case (spec_digits b); intros H3 H4.";
- pp " unfold gcd; generalize (spec_compare a b); case compare.";
- pp " intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto.";
- pp " apply Zis_gcd_refl.";
- pp " intros; apply trans_equal with (Zgcd [b] [a]).";
- pp " apply spec_gcd_gt; auto with zarith.";
- pp " apply Zis_gcd_gcd; auto with zarith.";
- pp " apply Zgcd_is_pos.";
- pp " apply Zis_gcd_sym; apply Zgcd_is_gcd.";
- pp " intros; apply spec_gcd_gt; auto.";
- pp " Qed.";
- pr "";
-
-
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Conversion *)";
+ pr " (** * Conversion *)";
pr " (* *)";
pr " (***************************************************************)";
pr "";
- pr " Definition pheight p := ";
+ pr " Definition pheight p :=";
pr " Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (plength p))).";
pr "";
- pr " Theorem pheight_correct: forall p, ";
+ pr " Theorem pheight_correct: forall p,";
pr " Zpos p < 2 ^ (Zpos (znz_digits w0_op) * 2 ^ (Z_of_nat (pheight p))).";
pr " Proof.";
pr " intros p; unfold pheight.";
@@ -2400,30 +2078,12 @@ let _ =
pp " Qed.";
pr "";
- pr " Definition of_N x :=";
- pr " match x with";
- pr " | BinNat.N0 => zero";
- pr " | Npos p => of_pos p";
- pr " end.";
- pr "";
-
- pr " Theorem spec_of_N: forall x,";
- pr " [of_N x] = Z_of_N x.";
- pa " Admitted.";
- pp " Proof.";
- pp " intros x; case x.";
- pp " simpl of_N.";
- pp " unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto.";
- pp " intros p; exact (spec_of_pos p).";
- pp " Qed.";
- pr "";
-
pr " (***************************************************************)";
pr " (* *)";
- pr " (* Shift *)";
+ pr " (** * Shift *)";
pr " (* *)";
pr " (***************************************************************)";
- pr "";
+ pr "";
(* Head0 *)
pr " Definition head0 w := match w with";
@@ -2443,21 +2103,21 @@ let _ =
done;
pp " intros n x; rewrite spec_reduce_n; exact (spec_head00 (wn_spec n) x).";
pp " Qed.";
- pr " ";
+ pr "";
pr " Theorem spec_head0: forall x, 0 < [x] ->";
pr " 2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x).";
pa " Admitted.";
pp " Proof.";
pp " assert (F0: forall x, (x - 1) + 1 = x).";
- pp " intros; ring. ";
+ pp " intros; ring.";
pp " intros x; case x; unfold digits, head0; clear x.";
for i = 0 to size do
pp " intros x Hx; rewrite spec_reduce_%i." i;
pp " assert (F1:= spec_more_than_1_digit w%i_spec)." i;
pp " generalize (spec_head0 w%i_spec x Hx)." i;
pp " unfold base.";
- pp " pattern (Zpos (znz_digits w%i_op)) at 1; " i;
+ pp " pattern (Zpos (znz_digits w%i_op)) at 1;" i;
pp " rewrite <- (fun x => (F0 (Zpos x))).";
pp " rewrite Zpower_exp; auto with zarith.";
pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith.";
@@ -2466,7 +2126,7 @@ let _ =
pp " assert (F1:= spec_more_than_1_digit (wn_spec n)).";
pp " generalize (spec_head0 (wn_spec n) x Hx).";
pp " unfold base.";
- pp " pattern (Zpos (znz_digits (make_op n))) at 1; ";
+ pp " pattern (Zpos (znz_digits (make_op n))) at 1;";
pp " rewrite <- (fun x => (F0 (Zpos x))).";
pp " rewrite Zpower_exp; auto with zarith.";
pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith.";
@@ -2493,7 +2153,7 @@ let _ =
done;
pp " intros n x; rewrite spec_reduce_n; exact (spec_tail00 (wn_spec n) x).";
pp " Qed.";
- pr " ";
+ pr "";
pr " Theorem spec_tail0: forall x,";
@@ -2513,7 +2173,7 @@ let _ =
pr " Definition %sdigits x :=" c;
pr " match x with";
pr " | %s0 _ => %s0 w0_op.(znz_zdigits)" c c;
- for i = 1 to size do
+ for i = 1 to size do
pr " | %s%i _ => reduce_%i w%i_op.(znz_zdigits)" c i i i;
done;
pr " | %sn n _ => reduce_n n (make_op n).(znz_zdigits)" c;
@@ -2534,22 +2194,22 @@ let _ =
(* Shiftr *)
for i = 0 to size do
- 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;
+ pr " Definition unsafe_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;
done;
- 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.";
+ pr " Definition unsafe_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.";
pr "";
- pr " Definition shiftr := Eval lazy beta delta [same_level] in ";
- pr " same_level _ (fun n x => %s0 (shiftr0 n x))" c;
+ pr " Definition unsafe_shiftr := Eval lazy beta delta [same_level] in";
+ pr " same_level _ (fun n x => %s0 (unsafe_shiftr0 n x))" c;
for i = 1 to size do
- pr " (fun n x => reduce_%i (shiftr%i n x))" i i;
+ pr " (fun n x => reduce_%i (unsafe_shiftr%i n x))" i i;
done;
- pr " (fun n p x => reduce_n n (shiftrn n p x)).";
+ pr " (fun n p x => reduce_n n (unsafe_shiftrn n p x)).";
pr "";
- pr " Theorem spec_shiftr: forall n x,";
- pr " [n] <= [Ndigits x] -> [shiftr n x] = [x] / 2 ^ [n].";
+ pr " Theorem spec_unsafe_shiftr: forall n x,";
+ pr " [n] <= [Ndigits x] -> [unsafe_shiftr n x] = [x] / 2 ^ [n].";
pa " Admitted.";
pp " Proof.";
pp " assert (F0: forall x y, x - (x - y) = y).";
@@ -2568,7 +2228,7 @@ let _ =
pp " split; auto with zarith.";
pp " apply Zle_lt_trans with xx; auto with zarith.";
pp " apply Zpower2_lt_lin; auto with zarith.";
- pp " assert (F4: forall ww ww1 ww2 ";
+ pp " assert (F4: forall ww ww1 ww2";
pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)";
pp " xx yy xx1 yy1,";
pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_zdigits ww1_op) ->";
@@ -2586,7 +2246,7 @@ let _ =
pp " rewrite <- Hy.";
pp " generalize (spec_add_mul_div Hw";
pp " (znz_0 ww_op) xx1";
- pp " (znz_sub ww_op (znz_zdigits ww_op) ";
+ pp " (znz_sub ww_op (znz_zdigits ww_op)";
pp " yy1)";
pp " ).";
pp " rewrite (spec_0 Hw).";
@@ -2612,11 +2272,11 @@ let _ =
pp " rewrite Zpos_xO.";
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size;
pp " apply F5; auto with arith.";
- pp " intros x; case x; clear x; unfold shiftr, same_level.";
+ pp " intros x; case x; clear x; unfold unsafe_shiftr, same_level.";
for i = 0 to size do
pp " intros x y; case y; clear y.";
for j = 0 to i - 1 do
- pp " intros y; unfold shiftr%i, Ndigits." i;
+ pp " intros y; unfold unsafe_shiftr%i, Ndigits." i;
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i;
pp " rewrite (spec_zdigits w%i_spec)." i;
@@ -2628,25 +2288,25 @@ let _ =
pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i;
done;
- pp " intros y; unfold shiftr%i, Ndigits." i;
+ pp " intros y; unfold unsafe_shiftr%i, Ndigits." i;
pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i;
for j = i + 1 to size do
- pp " intros y; unfold shiftr%i, Ndigits." j;
+ pp " intros y; unfold unsafe_shiftr%i, Ndigits." j;
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i;
pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j;
done;
if i == size then
begin
- pp " intros m y; unfold shiftrn, Ndigits.";
+ pp " intros m y; unfold unsafe_shiftrn, Ndigits.";
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size;
pp " try (apply sym_equal; exact (spec_extend%in m x))." size;
end
- else
+ else
begin
- pp " intros m y; unfold shiftrn, Ndigits.";
+ pp " intros m y; unfold unsafe_shiftrn, Ndigits.";
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i;
pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i;
@@ -2654,7 +2314,7 @@ let _ =
end
done;
pp " intros n x y; case y; clear y;";
- pp " intros y; unfold shiftrn, Ndigits; try rewrite spec_reduce_n.";
+ pp " intros y; unfold unsafe_shiftrn, Ndigits; try rewrite spec_reduce_n.";
for i = 0 to size do
pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i;
@@ -2684,52 +2344,23 @@ let _ =
pp " Qed.";
pr "";
- pr " Definition safe_shiftr n x := ";
- pr " match compare n (Ndigits x) with";
- pr " | Lt => shiftr n x ";
- pr " | _ => %s0 w_0" c;
- pr " end.";
- pr "";
-
-
- pr " Theorem spec_safe_shiftr: forall n x,";
- pr " [safe_shiftr n x] = [x] / 2 ^ [n].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros n x; unfold safe_shiftr;";
- pp " generalize (spec_compare n (Ndigits x)); case compare; intros H.";
- pp " apply trans_equal with (1 := spec_0 w0_spec).";
- pp " apply sym_equal; apply Zdiv_small; rewrite H.";
- pp " rewrite spec_Ndigits; exact (spec_digits x).";
- pp " rewrite <- spec_shiftr; auto with zarith.";
- pp " apply trans_equal with (1 := spec_0 w0_spec).";
- pp " apply sym_equal; apply Zdiv_small.";
- pp " rewrite spec_Ndigits in H; case (spec_digits x); intros H1 H2.";
- pp " split; auto.";
- pp " apply Zlt_le_trans with (1 := H2).";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " Qed.";
- pr "";
-
- pr "";
-
- (* Shiftl *)
+ (* Unsafe_Shiftl *)
for i = 0 to size do
- pr " Definition shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i
+ pr " Definition unsafe_shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i
done;
- pr " Definition shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0).";
- pr " Definition shiftl := Eval lazy beta delta [same_level] in";
- pr " same_level _ (fun n x => %s0 (shiftl0 n x))" c;
+ pr " Definition unsafe_shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0).";
+ pr " Definition unsafe_shiftl := Eval lazy beta delta [same_level] in";
+ pr " same_level _ (fun n x => %s0 (unsafe_shiftl0 n x))" c;
for i = 1 to size do
- pr " (fun n x => reduce_%i (shiftl%i n x))" i i;
+ pr " (fun n x => reduce_%i (unsafe_shiftl%i n x))" i i;
done;
- pr " (fun n p x => reduce_n n (shiftln n p x)).";
+ pr " (fun n p x => reduce_n n (unsafe_shiftln n p x)).";
pr "";
pr "";
- pr " Theorem spec_shiftl: forall n x,";
- pr " [n] <= [head0 x] -> [shiftl n x] = [x] * 2 ^ [n].";
+ pr " Theorem spec_unsafe_shiftl: forall n x,";
+ pr " [n] <= [head0 x] -> [unsafe_shiftl n x] = [x] * 2 ^ [n].";
pa " Admitted.";
pp " Proof.";
pp " assert (F0: forall x y, x - (x - y) = y).";
@@ -2748,7 +2379,7 @@ let _ =
pp " split; auto with zarith.";
pp " apply Zle_lt_trans with xx; auto with zarith.";
pp " apply Zpower2_lt_lin; auto with zarith.";
- pp " assert (F4: forall ww ww1 ww2 ";
+ pp " assert (F4: forall ww ww1 ww2";
pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)";
pp " xx yy xx1 yy1,";
pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_head0 ww1_op xx) ->";
@@ -2788,7 +2419,7 @@ let _ =
pp " rewrite Zmod_small; auto with zarith.";
pp " intros HH; apply HH.";
pp " rewrite Hy; apply Zle_trans with (1:= Hl).";
- pp " rewrite <- (spec_zdigits Hw). ";
+ pp " rewrite <- (spec_zdigits Hw).";
pp " apply Zle_trans with (2 := Hl1); auto.";
pp " rewrite (spec_zdigits Hw1); auto with zarith.";
pp " split; auto with zarith .";
@@ -2826,11 +2457,11 @@ let _ =
pp " rewrite Zpos_xO.";
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size;
pp " apply F5; auto with arith.";
- pp " intros x; case x; clear x; unfold shiftl, same_level.";
+ pp " intros x; case x; clear x; unfold unsafe_shiftl, same_level.";
for i = 0 to size do
pp " intros x y; case y; clear y.";
for j = 0 to i - 1 do
- pp " intros y; unfold shiftl%i, head0." i;
+ pp " intros y; unfold unsafe_shiftl%i, head0." i;
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i;
pp " rewrite (spec_zdigits w%i_spec)." i;
@@ -2841,25 +2472,25 @@ let _ =
pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j;
pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i;
done;
- pp " intros y; unfold shiftl%i, head0." i;
+ pp " intros y; unfold unsafe_shiftl%i, head0." i;
pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i;
for j = i + 1 to size do
- pp " intros y; unfold shiftl%i, head0." j;
+ pp " intros y; unfold unsafe_shiftl%i, head0." j;
pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j;
pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i;
pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j;
done;
if i == size then
begin
- pp " intros m y; unfold shiftln, head0.";
+ pp " intros m y; unfold unsafe_shiftln, head0.";
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size;
pp " try (apply sym_equal; exact (spec_extend%in m x))." size;
end
- else
+ else
begin
- pp " intros m y; unfold shiftln, head0.";
+ pp " intros m y; unfold unsafe_shiftln, head0.";
pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1.";
pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i;
pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i;
@@ -2867,7 +2498,7 @@ let _ =
end
done;
pp " intros n x y; case y; clear y;";
- pp " intros y; unfold shiftln, head0; try rewrite spec_reduce_n.";
+ pp " intros y; unfold unsafe_shiftln, head0; try rewrite spec_reduce_n.";
for i = 0 to size do
pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i;
pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i;
@@ -2907,7 +2538,7 @@ let _ =
pr " end.";
pr "";
- pr " Theorem spec_double_size_digits: ";
+ pr " Theorem spec_double_size_digits:";
pr " forall x, digits (double_size x) = xO (digits x).";
pa " Admitted.";
pp " Proof.";
@@ -2922,7 +2553,7 @@ let _ =
pp " Proof.";
pp " intros x; case x; unfold double_size; clear x.";
for i = 0 to size do
- pp " intros x; unfold to_Z, make_op; ";
+ pp " intros x; unfold to_Z, make_op;";
pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto with zarith." (i + 1) i;
done;
pp " intros n x; unfold to_Z;";
@@ -2934,7 +2565,7 @@ let _ =
pr "";
- pr " Theorem spec_double_size_head0: ";
+ pr " Theorem spec_double_size_head0:";
pr " forall x, 2 * [head0 x] <= [head0 (double_size x)].";
pa " Admitted.";
pp " Proof.";
@@ -2963,7 +2594,7 @@ let _ =
pp " apply Zmult_le_compat_l; auto with zarith.";
pp " rewrite Zpower_1_r; auto with zarith.";
pp " apply Zpower_le_monotone; auto with zarith.";
- pp " split; auto with zarith. ";
+ pp " split; auto with zarith.";
pp " case (Zle_or_lt (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6.";
pp " absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith.";
pp " rewrite <- HH5; rewrite Zmult_1_r.";
@@ -2988,7 +2619,7 @@ let _ =
pp " Qed.";
pr "";
- pr " Theorem spec_double_size_head0_pos: ";
+ pr " Theorem spec_double_size_head0_pos:";
pr " forall x, 0 < [head0 (double_size x)].";
pa " Admitted.";
pp " Proof.";
@@ -3015,114 +2646,6 @@ let _ =
pp " Qed.";
pr "";
-
- (* Safe shiftl *)
-
- pr " Definition safe_shiftl_aux_body cont n x :=";
- pr " match compare n (head0 x) with";
- pr " Gt => cont n (double_size x)";
- pr " | _ => shiftl n x";
- pr " end.";
- pr "";
-
- pr " Theorem spec_safe_shift_aux_body: forall n p x cont,";
- pr " 2^ Zpos p <= [head0 x] ->";
- pr " (forall x, 2 ^ (Zpos p + 1) <= [head0 x]->";
- pr " [cont n x] = [x] * 2 ^ [n]) ->";
- pr " [safe_shiftl_aux_body cont n x] = [x] * 2 ^ [n].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros n p x cont H1 H2; unfold safe_shiftl_aux_body.";
- pp " generalize (spec_compare n (head0 x)); case compare; intros H.";
- pp " apply spec_shiftl; auto with zarith.";
- pp " apply spec_shiftl; auto with zarith.";
- pp " rewrite H2.";
- pp " rewrite spec_double_size; auto.";
- pp " rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith.";
- pp " apply Zle_trans with (2 := spec_double_size_head0 x).";
- pp " rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith.";
- pp " Qed.";
- pr "";
-
- pr " Fixpoint safe_shiftl_aux p cont n x {struct p} :=";
- pr " safe_shiftl_aux_body ";
- pr " (fun n x => match p with";
- pr " | xH => cont n x";
- pr " | xO p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x";
- pr " | xI p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x";
- pr " end) n x.";
- pr "";
-
- pr " Theorem spec_safe_shift_aux: forall p q n x cont,";
- pr " 2 ^ (Zpos q) <= [head0 x] ->";
- pr " (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] ->";
- pr " [cont n x] = [x] * 2 ^ [n]) -> ";
- pr " [safe_shiftl_aux p cont n x] = [x] * 2 ^ [n].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros p; elim p; unfold safe_shiftl_aux; fold safe_shiftl_aux; clear p.";
- pp " intros p Hrec q n x cont H1 H2.";
- pp " apply spec_safe_shift_aux_body with (q); auto.";
- pp " intros x1 H3; apply Hrec with (q + 1)%spositive; auto." "%";
- pp " intros x2 H4; apply Hrec with (p + q + 1)%spositive; auto." "%";
- pp " rewrite <- Pplus_assoc.";
- pp " rewrite Zpos_plus_distr; auto.";
- pp " intros x3 H5; apply H2.";
- pp " rewrite Zpos_xI.";
- pp " replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1));";
- pp " auto.";
- pp " repeat rewrite Zpos_plus_distr; ring.";
- pp " intros p Hrec q n x cont H1 H2.";
- pp " apply spec_safe_shift_aux_body with (q); auto.";
- pp " intros x1 H3; apply Hrec with (q); auto.";
- pp " apply Zle_trans with (2 := H3); auto with zarith.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " intros x2 H4; apply Hrec with (p + q)%spositive; auto." "%";
- pp " intros x3 H5; apply H2.";
- pp " rewrite (Zpos_xO p).";
- pp " replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q));";
- pp " auto.";
- pp " repeat rewrite Zpos_plus_distr; ring.";
- pp " intros q n x cont H1 H2.";
- pp " apply spec_safe_shift_aux_body with (q); auto.";
- pp " rewrite Zplus_comm; auto.";
- pp " Qed.";
- pr "";
-
-
- pr " Definition safe_shiftl n x :=";
- pr " safe_shiftl_aux_body";
- pr " (safe_shiftl_aux_body";
- pr " (safe_shiftl_aux (digits n) shiftl)) n x.";
- pr "";
-
- pr " Theorem spec_safe_shift: forall n x,";
- pr " [safe_shiftl n x] = [x] * 2 ^ [n].";
- pa " Admitted.";
- pp " Proof.";
- pp " intros n x; unfold safe_shiftl, safe_shiftl_aux_body.";
- pp " generalize (spec_compare n (head0 x)); case compare; intros H.";
- pp " apply spec_shiftl; auto with zarith.";
- pp " apply spec_shiftl; auto with zarith.";
- pp " rewrite <- (spec_double_size x).";
- pp " generalize (spec_compare n (head0 (double_size x))); case compare; intros H1.";
- pp " apply spec_shiftl; auto with zarith.";
- pp " apply spec_shiftl; auto with zarith.";
- pp " rewrite <- (spec_double_size (double_size x)).";
- pp " apply spec_safe_shift_aux with 1%spositive." "%";
- pp " apply Zle_trans with (2 := spec_double_size_head0 (double_size x)).";
- pp " replace (2 ^ 1) with (2 * 1).";
- pp " apply Zmult_le_compat_l; auto with zarith.";
- pp " generalize (spec_double_size_head0_pos x); auto with zarith.";
- pp " rewrite Zpower_1_r; ring.";
- pp " intros x1 H2; apply spec_shiftl.";
- pp " apply Zle_trans with (2 := H2).";
- pp " apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith.";
- pp " case (spec_digits n); auto with zarith.";
- pp " apply Zpower_le_monotone; auto with zarith.";
- pp " Qed.";
- pr "";
-
(* even *)
pr " Definition is_even x :=";
pr " match x with";
@@ -3146,20 +2669,6 @@ let _ =
pp " Qed.";
pr "";
- pr " Theorem spec_0: [zero] = 0.";
- pa " Admitted.";
- pp " Proof.";
- pp " exact (spec_0 w0_spec).";
- pp " Qed.";
- pr "";
-
- pr " Theorem spec_1: [one] = 1.";
- pa " Admitted.";
- pp " Proof.";
- pp " exact (spec_1 w0_spec).";
- pp " Qed.";
- pr "";
-
pr "End Make.";
pr "";
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-25 17:45:57 +0000