From 911c50439abdedd0f75856d43ff12e9615ec9980 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 8 Feb 2010 18:17:54 +0000 Subject: DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generation - Records of operations and specs in CyclicAxioms are now type classes (under a module ZnZ for qualification). We benefit from inference and from generic names: (ZnZ.mul x y) instead of (znz_mul (some_ops...) x y). - Beware of typeclasses unfolds: the line about Typeclasses Opaque w1 w2 ... is critical for decent compilation time (x2.5 without it). - Functions defined via same_level are now obtained from a generic version by (Eval ... in ...) during definition. The code obtained this way should be just as before, apart from some (minor?) details. Proofs for these functions are _way_ simplier and lighter. - The macro-generated NMake_gen.v contains only generic iterators and compare, mul, div_gt, mod_gt. I hope to be able to adapt these functions as well soon. - Spec of comparison is now fully done with respect to Zcompare - A log2 function has been added. - No more unsafe_shiftr, we detect the underflow directly with sub_c git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12713 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/BigN/NMake.v | 869 ++++++++++-- theories/Numbers/Natural/BigN/NMake_gen.ml | 1986 +++++++--------------------- theories/Numbers/Natural/BigN/Nbasic.v | 122 +- theories/Numbers/Natural/SpecViaZ/NSig.v | 3 + 4 files changed, 1301 insertions(+), 1679 deletions(-) (limited to 'theories/Numbers/Natural') diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 925b0535a..b3f7befc8 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -16,18 +16,204 @@ representation. The representation-dependent (and macro-generated) part is now in [NMake_gen]. *) -Require Import BigNumPrelude ZArith CyclicAxioms. -Require Import Nbasic Wf_nat StreamMemo NSig NMake_gen. +Require Import BigNumPrelude ZArith CyclicAxioms DoubleType + Nbasic Wf_nat StreamMemo NSig NMake_gen. -Module Make (Import W0:CyclicType) <: NType. +Module Make (W0:CyclicType) <: NType. - (** Macro-generated part *) + (** * Macro-generated part *) Include NMake_gen.Make W0. + Declare Reduction red_t := + lazy beta iota delta + [iter_t reduce same_level mk_t mk_t_S dom_t dom_op]. + + Ltac red_t := + match goal with |- ?u => let v := (eval red_t in u) in change v end. + + (** * Generic results *) + + Theorem spec_mk_t : forall n (x:dom_t n), [mk_t n x] = ZnZ.to_Z x. + Proof. + intros. change to_Z with (iter_t (fun _ x => ZnZ.to_Z x)). + unfold iter_t. + repeat (destruct n; try reflexivity). + Qed. + + Theorem spec_mk_t_S : forall n (x:zn2z (dom_t n)), + [mk_t_S n x] = zn2z_to_Z (base (ZnZ.digits (dom_op n))) ZnZ.to_Z x. + Proof. + intros. + repeat ((simpl; rewrite !make_op_S; reflexivity) || + (destruct n; [reflexivity|])). + Qed. + + Lemma spec_iter_t : forall A (P:Z->A->Prop)(f:forall n, dom_t n -> A), + (forall n x, P (ZnZ.to_Z x) (f n x)) -> forall x, P [x] (iter_t f x). + Proof. + intros A P f H; destruct x; unfold iter_t; + match goal with |- context [f ?n _] => apply (H n) end. + Qed. + + Lemma spec_iter_t_2 : forall A B (P:Z->A->B->Prop) + (f:forall n, dom_t n -> A) + (g:forall n, dom_t n -> B), + (forall n x, P (ZnZ.to_Z x) (f n x) (g n x)) -> + forall x, P [x] (iter_t f x) (iter_t g x). + Proof. + intros A B P f g H; destruct x; unfold iter_t; + match goal with |- context [f ?n _] => apply (H n) end. + Qed. + + Lemma spec_iter_t_3 : forall A B C (P:Z->A->B->C->Prop) + (f:forall n, dom_t n -> A) + (g:forall n, dom_t n -> B) + (h:forall n, dom_t n -> C), + (forall n x, P (ZnZ.to_Z x) (f n x) (g n x) (h n x)) -> + forall x, P [x] (iter_t f x) (iter_t g x) (iter_t h x). + Proof. + intros A B C P f g h H; destruct x; unfold iter_t; + match goal with |- context [f ?n _] => apply (H n) end. + Qed. + + Theorem spec_pos: forall x, 0 <= [x]. + Proof. + intros x; apply spec_iter_t with (f := fun _ _ => 0)(P := fun u _ => 0<=u). + intros n wx. now case (ZnZ.spec_to_Z wx). + Qed. + + Lemma digits_dom_op_incr : forall n m, (n<=m)%nat -> + (ZnZ.digits (dom_op n) <= ZnZ.digits (dom_op m))%positive. + Proof. + intros. + change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))). + rewrite 2 digits_dom_op. + apply Zmult_le_compat_l; auto with zarith. + apply Zpower_le_monotone2; auto with zarith. + Qed. + + (** Number of level in the tree representation of a number. + NB: This function isn't a morphism for setoid [eq]. *) + + Definition level := iter_t (fun n _ => n). + + (** Specification of [same_level] indexed by [level] *) + + Theorem spec_same_level_dep : + forall res + (P : nat -> Z -> Z -> res -> Prop) + (Pantimon : forall n m z z' r, (n <= m)%nat -> P m z z' r -> P n z z' r) + (f : forall n, dom_t n -> dom_t n -> res) + (Pf: forall n x y, P n (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)), + forall x y, P (level y) [x] [y] (same_level f x y). + Proof. + intros res P Pantimon f Pf. + set (f' := fun n x y => (n, f n x y)). + set (P' := fun z z' r => P (fst r) z z' (snd r)). + assert (FST : forall x y, (level y <= fst (same_level f' x y))%nat) + by (destruct x, y; simpl; omega with * ). + assert (SND : forall x y, same_level f x y = snd (same_level f' x y)) + by (destruct x, y; reflexivity). + intros. eapply Pantimon; [eapply FST|]. + rewrite SND. eapply (@spec_same_level _ P' f'); eauto. + Qed. + + + (** * Zero and One *) + + Theorem spec_0: [zero] = 0. + Proof. + exact ZnZ.spec_0. + Qed. + + Theorem spec_1: [one] = 1. + Proof. + exact ZnZ.spec_1. + Qed. + + (** * Successor *) + + Local Notation succn := (fun n (x:dom_t n) => + let op := dom_op n in + match ZnZ.succ_c x with + | C0 r => mk_t n r + | C1 r => mk_t_S n (WW ZnZ.one r) + end). + + Definition succ : t -> t := Eval red_t in iter_t succn. + + Lemma succ_fold : succ = iter_t succn. + Proof. red_t; reflexivity. Qed. + + Theorem spec_succ: forall n, [succ n] = [n] + 1. + Proof. + intros x. rewrite succ_fold. apply spec_iter_t. clear x. + intros n x. simpl. + generalize (ZnZ.spec_succ_c x); case ZnZ.succ_c. + intros. rewrite spec_mk_t. assumption. + intros. unfold interp_carry in *. + rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_1. assumption. + Qed. + + (** * Addition *) + + Local Notation addn := (fun n (x y : dom_t n) => + let op := dom_op n in + match ZnZ.add_c x y with + | C0 r => mk_t n r + | C1 r => mk_t_S n (WW ZnZ.one r) + end). + + Definition add : t -> t -> t := Eval red_t in same_level addn. + + Lemma add_fold : add = same_level addn. + Proof. red_t; reflexivity. Qed. + + Theorem spec_add: forall x y, [add x y] = [x] + [y]. + Proof. + intros x y. rewrite add_fold. apply spec_same_level; clear x y. + intros n x y. simpl. + generalize (ZnZ.spec_add_c x y); case ZnZ.add_c; intros z H. + rewrite spec_mk_t. assumption. + rewrite spec_mk_t_S. unfold interp_carry in H. + simpl. rewrite ZnZ.spec_1. assumption. + Qed. (** * Predecessor *) + Local Notation predn := (fun n (x:dom_t n) => + match ZnZ.pred_c x with + | C0 r => reduce n r + | C1 _ => zero + end). + + Definition pred : t -> t := Eval red_t in iter_t predn. + + Lemma pred_fold : pred = iter_t predn. + Proof. red_t; reflexivity. Qed. + + Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1. + Proof. + intros x. rewrite pred_fold. apply spec_iter_t. clear x. + intros n x H. + generalize (ZnZ.spec_pred_c x); case ZnZ.pred_c; intros y H'. + rewrite spec_reduce. assumption. + exfalso. unfold interp_carry in *. + generalize (ZnZ.spec_to_Z x) (ZnZ.spec_to_Z y); auto with zarith. + Qed. + + Theorem spec_pred0 : forall x, [x] = 0 -> [pred x] = 0. + Proof. + intros x. rewrite pred_fold. apply spec_iter_t. clear x. + intros n x H. + generalize (ZnZ.spec_pred_c x); case ZnZ.pred_c; intros y H'. + rewrite spec_reduce. + unfold interp_carry in H'. + generalize (ZnZ.spec_to_Z y); auto with zarith. + exact spec_0. + Qed. + Lemma spec_pred : forall x, [pred x] = Zmax 0 ([x]-1). Proof. intros. destruct (Zle_lt_or_eq _ _ (spec_pos x)). @@ -36,9 +222,42 @@ Module Make (Import W0:CyclicType) <: NType. rewrite <- H; apply spec_pred0; auto. Qed. - (** * Subtraction *) + Local Notation subn := (fun n (x y : dom_t n) => + let op := dom_op n in + match ZnZ.sub_c x y with + | C0 r => reduce n r + | C1 r => zero + end). + + Definition sub : t -> t -> t := Eval red_t in same_level subn. + + Lemma sub_fold : sub = same_level subn. + Proof. red_t; reflexivity. Qed. + + Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y]. + Proof. + intros x y. rewrite sub_fold. apply spec_same_level. clear x y. + intros n x y. simpl. + generalize (ZnZ.spec_sub_c x y); case ZnZ.sub_c; intros z H LE. + rewrite spec_reduce. assumption. + unfold interp_carry in H. + exfalso. + generalize (ZnZ.spec_to_Z z); auto with zarith. + Qed. + + Theorem spec_sub0 : forall x y, [x] < [y] -> [sub x y] = 0. + Proof. + intros x y. rewrite sub_fold. apply spec_same_level. clear x y. + intros n x y. simpl. + generalize (ZnZ.spec_sub_c x y); case ZnZ.sub_c; intros z H LE. + rewrite spec_reduce. + unfold interp_carry in H. + generalize (ZnZ.spec_to_Z z); auto with zarith. + exact spec_0. + Qed. + Lemma spec_sub : forall x y, [sub x y] = Zmax 0 ([x]-[y]). Proof. intros. destruct (Zle_or_lt [y] [x]). @@ -48,13 +267,7 @@ Module Make (Import W0:CyclicType) <: NType. (** * Comparison *) - Theorem spec_compare : forall x y, compare x y = Zcompare [x] [y]. - Proof. - intros x y. generalize (spec_compare_aux x y); destruct compare; - intros; symmetry; try rewrite Zcompare_Eq_iff_eq; assumption. - Qed. - - Definition eq_bool x y := + Definition eq_bool (x y : t) : bool := match compare x y with | Eq => true | _ => false @@ -65,18 +278,11 @@ Module Make (Import W0:CyclicType) <: NType. intros. unfold eq_bool, Zeq_bool. rewrite spec_compare; reflexivity. Qed. - Theorem spec_eq_bool_aux: forall x y, - if eq_bool x y then [x] = [y] else [x] <> [y]. - Proof. - intros x y; unfold eq_bool. - generalize (spec_compare_aux x y); case compare; auto with zarith. - Qed. - - Definition lt n m := [n] < [m]. - Definition le n m := [n] <= [m]. + Definition lt (n m : t) := [n] < [m]. + Definition le (n m : t) := [n] <= [m]. - Definition min n m := match compare n m with Gt => m | _ => n end. - Definition max n m := match compare n m with Lt => m | _ => n end. + Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end. + Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end. Theorem spec_max : forall n m, [max n m] = Zmax [n] [m]. Proof. @@ -88,10 +294,43 @@ Module Make (Import W0:CyclicType) <: NType. intros. unfold min, Zmin. rewrite spec_compare; destruct Zcompare; reflexivity. Qed. + (** * Square *) + + (** TODO: use reduce (original version was using it for N0 only) *) + + Local Notation squaren := + (fun n (x : dom_t n) => mk_t_S n (ZnZ.square_c x)). + + Definition square : t -> t := Eval red_t in iter_t squaren. + + Lemma square_fold : square = iter_t squaren. + Proof. red_t; reflexivity. Qed. + + Theorem spec_square: forall x, [square x] = [x] * [x]. + Proof. + intros x. rewrite square_fold. apply spec_iter_t. clear x. + intros n x. rewrite spec_mk_t_S. exact (ZnZ.spec_square_c x). + Qed. + + (** * Sqrt *) + + Local Notation sqrtn := + (fun n (x : dom_t n) => reduce n (ZnZ.sqrt x)). + + Definition sqrt : t -> t := Eval red_t in iter_t sqrtn. + + Lemma sqrt_fold : sqrt = iter_t sqrtn. + Proof. red_t; reflexivity. Qed. + + Theorem spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + Proof. + intros x. rewrite sqrt_fold. apply spec_iter_t. clear x. + intros n x; rewrite spec_reduce; exact (ZnZ.spec_sqrt x). + Qed. (** * Power *) - Fixpoint power_pos (x:t) (p:positive) {struct p} : t := + Fixpoint power_pos (x:t)(p:positive) : t := match p with | xH => x | xO p => square (power_pos x p) @@ -112,21 +351,20 @@ Module Make (Import W0:CyclicType) <: NType. intros; rewrite Zpower_1_r; auto. Qed. - Definition power x (n:N) := match n with + Definition power (x:t)(n:N) : t := match n with | BinNat.N0 => one | BinNat.Npos p => power_pos x p end. Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. Proof. - destruct n; simpl. apply (spec_1 w0_spec). + destruct n; simpl. apply ZnZ.spec_1. apply spec_power_pos. Qed. - (** * Div *) - Definition div_eucl x y := + Definition div_eucl (x y : t) : t * t := if eq_bool y zero then (zero,zero) else match compare x y with | Eq => (one, zero) @@ -138,32 +376,27 @@ Module Make (Import W0:CyclicType) <: NType. let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. Proof. - assert (F0: [zero] = 0). - exact (spec_0 w0_spec). - assert (F1: [one] = 1). - exact (spec_1 w0_spec). intros x y. unfold div_eucl. - generalize (spec_eq_bool_aux y zero). destruct eq_bool; rewrite F0. - intro H. rewrite H. destruct [x]; auto. - intro H'. - assert (0 < [y]) by (generalize (spec_pos y); auto with zarith). + rewrite spec_eq_bool, spec_compare, spec_0. + generalize (Zeq_bool_if [y] 0); case Zeq_bool. + intros ->. rewrite spec_0. destruct [x]; auto. + intros H'. + assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith). clear H'. - generalize (spec_compare_aux x y); case compare; try rewrite F0; - try rewrite F1; intros; auto with zarith. - rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H)) - (Z_mod_same [y] (Zlt_gt _ _ H)); + case Zcompare_spec; intros Cmp; + rewrite ?spec_0, ?spec_1; intros; auto with zarith. + rewrite Cmp; generalize (Z_div_same [y] (Zlt_gt _ _ H)) + (Z_mod_same [y] (Zlt_gt _ _ H)); unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto. - assert (F2: 0 <= [x] < [y]). - generalize (spec_pos x); auto. - generalize (Zdiv_small _ _ F2) - (Zmod_small _ _ F2); + assert (LeLt: 0 <= [x] < [y]) by (generalize (spec_pos x); auto). + generalize (Zdiv_small _ _ LeLt) (Zmod_small _ _ LeLt); unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto. - generalize (spec_div_gt _ _ H0 H); auto. + generalize (spec_div_gt _ _ (Zlt_gt _ _ Cmp) H); auto. unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt. intros a b c d (H1, H2); subst; auto. Qed. - Definition div x y := fst (div_eucl x y). + Definition div (x y : t) : t := fst (div_eucl x y). Theorem spec_div: forall x y, [div x y] = [x] / [y]. @@ -174,10 +407,9 @@ Module Make (Import W0:CyclicType) <: NType. injection H; auto. Qed. - (** * Modulo *) - Definition modulo x y := + Definition modulo (x y : t) : t := if eq_bool y zero then zero else match compare x y with | Eq => zero @@ -188,24 +420,45 @@ Module Make (Import W0:CyclicType) <: NType. Theorem spec_modulo: forall x y, [modulo x y] = [x] mod [y]. Proof. - assert (F0: [zero] = 0). - exact (spec_0 w0_spec). - assert (F1: [one] = 1). - exact (spec_1 w0_spec). intros x y. unfold modulo. - generalize (spec_eq_bool_aux y zero). destruct eq_bool; rewrite F0. - intro H; rewrite H. destruct [x]; auto. + rewrite spec_eq_bool, spec_compare, spec_0. + generalize (Zeq_bool_if [y] 0). case Zeq_bool. + intros ->; rewrite spec_0. destruct [x]; auto. intro H'. assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith). clear H'. - generalize (spec_compare_aux x y); case compare; try rewrite F0; - try rewrite F1; intros; try split; auto with zarith. + case Zcompare_spec; + rewrite ?spec_0, ?spec_1; intros; try split; auto with zarith. rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith. apply sym_equal; apply Zmod_small; auto with zarith. generalize (spec_pos x); auto with zarith. - apply spec_mod_gt; auto. + apply spec_mod_gt; auto with zarith. Qed. + (** * digits + + Number of digits in the representation of a numbers + (including head zero's). + NB: This function isn't a morphism for setoid [eq]. + *) + + Local Notation digitsn := (fun n _ => ZnZ.digits (dom_op n)). + + Definition digits : t -> positive := Eval red_t in iter_t digitsn. + + Lemma digits_fold : digits = iter_t digitsn. + Proof. red_t; reflexivity. Qed. + + Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x). + Proof. + intros x. rewrite digits_fold. apply spec_iter_t. clear x. + intros n x. exact (ZnZ.spec_to_Z x). + Qed. + + Lemma digits_level : forall x, digits x = ZnZ.digits (dom_op (level x)). + Proof. + destruct x; reflexivity. + Qed. (** * Gcd *) @@ -226,15 +479,12 @@ Module Make (Import W0:CyclicType) <: NType. Zis_gcd [a1] [b1] [cont a1 b1]) -> Zis_gcd [a] [b] [gcd_gt_body a b cont]. Proof. - assert (F1: [zero] = 0). - unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto. intros a b cont p H2 H3 H4; unfold gcd_gt_body. - generalize (spec_compare_aux b zero); case compare; try rewrite F1. - intros HH; rewrite HH; apply Zis_gcd_0. + rewrite ! spec_compare, spec_0. case Zcompare_spec. + intros ->; apply Zis_gcd_0. intros HH; absurd (0 <= [b]); auto with zarith. case (spec_digits b); auto with zarith. - intros H5; generalize (spec_compare_aux (mod_gt a b) zero); - case compare; try rewrite F1. + intros H5; case Zcompare_spec. intros H6; rewrite <- (Zmult_1_r [b]). rewrite (Z_div_mod_eq [a] [b]); auto with zarith. rewrite <- spec_mod_gt; auto with zarith. @@ -273,7 +523,7 @@ Module Make (Import W0:CyclicType) <: NType. intros HH; generalize H3; rewrite <- HH; simpl Zpower; auto with zarith. Qed. - Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) {struct p} : t := + Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) : t := gcd_gt_body a b (fun a b => match p with @@ -310,12 +560,7 @@ Module Make (Import W0:CyclicType) <: NType. (Zpos p + n - 1); auto with zarith. intros a3 b3 H12 H13; apply H4; auto with zarith. apply Zlt_le_trans with (1 := H12). - case (Zle_or_lt 1 n); intros HH. - apply Zpower_le_monotone; auto with zarith. - apply Zle_trans with 0; auto with zarith. - assert (HH1: n - 1 < 0); auto with zarith. - generalize HH1; case (n - 1); auto with zarith. - intros p1 HH2; discriminate. + apply Zpower_le_monotone2; auto with zarith. intros n a b cont H H2 H3. simpl gcd_gt_aux. apply Zspec_gcd_gt_body with (n + 1); auto with zarith. @@ -345,7 +590,7 @@ Module Make (Import W0:CyclicType) <: NType. intros; apply False_ind; auto with zarith. Qed. - Definition gcd a b := + Definition gcd (a b : t) : t := match compare a b with | Eq => a | Lt => gcd_gt b a @@ -357,7 +602,7 @@ Module Make (Import W0:CyclicType) <: NType. intros a b. case (spec_digits a); intros H1 H2. case (spec_digits b); intros H3 H4. - unfold gcd; generalize (spec_compare_aux a b); case compare. + unfold gcd. rewrite spec_compare. case Zcompare_spec. intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto. apply Zis_gcd_refl. intros; apply trans_equal with (Zgcd [b] [a]). @@ -365,13 +610,53 @@ Module Make (Import W0:CyclicType) <: NType. apply Zis_gcd_gcd; auto with zarith. apply Zgcd_is_pos. apply Zis_gcd_sym; apply Zgcd_is_gcd. - intros; apply spec_gcd_gt; auto. + intros; apply spec_gcd_gt; auto with zarith. Qed. - (** * Conversion *) - Definition of_N x := + Definition pheight p := + Peano.pred (nat_of_P (get_height (ZnZ.digits W0.ops) (plength p))). + + Theorem pheight_correct: forall p, + Zpos p < 2 ^ (Zpos (ZnZ.digits W0.ops) * 2 ^ (Z_of_nat (pheight p))). + Proof. + intros p; unfold pheight. + assert (F1: forall x, Z_of_nat (Peano.pred (nat_of_P x)) = Zpos x - 1). + intros x. + assert (Zsucc (Z_of_nat (Peano.pred (nat_of_P x))) = Zpos x); auto with zarith. + rewrite <- inj_S. + rewrite <- (fun x => S_pred x 0); auto with zarith. + rewrite Zpos_eq_Z_of_nat_o_nat_of_P; auto. + apply lt_le_trans with 1%nat; auto with zarith. + exact (le_Pmult_nat x 1). + rewrite F1; clear F1. + assert (F2:= (get_height_correct (ZnZ.digits W0.ops) (plength p))). + apply Zlt_le_trans with (Zpos (Psucc p)). + rewrite Zpos_succ_morphism; auto with zarith. + apply Zle_trans with (1 := plength_pred_correct (Psucc p)). + rewrite Ppred_succ. + apply Zpower_le_monotone2; auto with zarith. + Qed. + + Definition of_pos (x:positive) : t := + let n := pheight x in + reduce n (snd (ZnZ.of_pos x)). + + Theorem spec_of_pos: forall x, + [of_pos x] = Zpos x. + Proof. + intros x; unfold of_pos. + rewrite spec_reduce. + simpl. + apply ZnZ.of_pos_correct. + unfold base. + apply Zlt_le_trans with (1 := pheight_correct x). + apply Zpower_le_monotone2; auto with zarith. + rewrite digits_dom_op; auto with zarith. + Qed. + + Definition of_N (x:N) : t := match x with | BinNat.N0 => zero | Npos p => of_pos p @@ -381,37 +666,398 @@ Module Make (Import W0:CyclicType) <: NType. [of_N x] = Z_of_N x. Proof. intros x; case x. - simpl of_N. - unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto. + simpl of_N. exact spec_0. intros p; exact (spec_of_pos p). Qed. + Definition to_N (x : t) := Zabs_N (to_Z x). - (** * Shift *) + (** * [head0] and [tail0] - Definition shiftr n x := - match compare n (Ndigits x) with - | Lt => unsafe_shiftr n x - | _ => N0 w_0 - end. + Number of zero at the beginning and at the end of + the representation of the number. + NB: these functions are not morphism for setoid [eq]. + *) + + Local Notation head0n := (fun n x => reduce n (ZnZ.head0 x)). + + Definition head0 : t -> t := Eval red_t in iter_t head0n. + + Lemma head0_fold : head0 = iter_t head0n. + Proof. red_t; reflexivity. Qed. + + Theorem spec_head00: forall x, [x] = 0 -> [head0 x] = Zpos (digits x). + Proof. + intros x. rewrite head0_fold, digits_fold. + apply spec_iter_t_2 with (P:=fun z u v => z=0 -> [u] = Zpos v). clear x. + intros n x; rewrite spec_reduce; exact (ZnZ.spec_head00 x). + Qed. + + Lemma pow2_pos_minus_1 : forall z, 0 2^(z-1) = 2^z / 2. + Proof. + intros. apply Zdiv_unique with 0; auto with zarith. + change 2 with (2^1) at 2. + rewrite <- Zpower_exp; auto with zarith. + rewrite Zplus_0_r. f_equal. auto with zarith. + Qed. + + Theorem spec_head0: forall x, 0 < [x] -> + 2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x). + Proof. + intros x. rewrite pow2_pos_minus_1 by (red; auto). + rewrite head0_fold, digits_fold. + apply spec_iter_t_2 with + (P:=fun z u v => 0 2^(Zpos v) / 2 <= 2^[u] * z < 2^(Zpos v)). + clear x. intros n x. rewrite spec_reduce. + exact (ZnZ.spec_head0 x). + Qed. + + Local Notation tail0n := (fun n x => reduce n (ZnZ.tail0 x)). + + Definition tail0 : t -> t := Eval red_t in iter_t tail0n. + + Lemma tail0_fold : tail0 = iter_t tail0n. + Proof. red_t; reflexivity. Qed. + + Theorem spec_tail00: forall x, [x] = 0 -> [tail0 x] = Zpos (digits x). + Proof. + intros x. rewrite tail0_fold, digits_fold. + apply spec_iter_t_2 with (P:=fun z u v => z=0 -> [u] = Zpos v). clear x. + intros n x; rewrite spec_reduce; exact (ZnZ.spec_tail00 x). + Qed. + + Theorem spec_tail0: forall x, + 0 < [x] -> exists y, 0 <= y /\ [x] = (2 * y + 1) * 2 ^ [tail0 x]. + Proof. + intros x. rewrite tail0_fold. apply spec_iter_t. clear x. + intros n x. rewrite spec_reduce. exact (ZnZ.spec_tail0 x). + Qed. + + (** * [Ndigits] + + Same as [digits] but encoded using large integers + NB: this function is not a morphism for setoid [eq]. + *) + + Local Notation Ndigitsn := (fun n _ => reduce n (ZnZ.zdigits (dom_op n))). + + Definition Ndigits : t -> t := Eval red_t in iter_t Ndigitsn. + + Lemma Ndigits_fold : Ndigits = iter_t Ndigitsn. + Proof. red_t; reflexivity. Qed. + + Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x). + Proof. + intros x. rewrite Ndigits_fold, digits_fold. + apply spec_iter_t_2 with (P:=fun z u v => [u] = Zpos v). clear x. + intros n x. rewrite spec_reduce. apply ZnZ.spec_zdigits. + Qed. + + (** * Binary logarithm *) + + Local Notation log2n := (fun n x => + let op := dom_op n in + reduce n (ZnZ.sub_carry (ZnZ.zdigits op) (ZnZ.head0 x))). + + Definition log2 : t -> t := Eval red_t in + fun x => if eq_bool x zero then zero else iter_t log2n x. + + Lemma log2_fold : + log2 = fun x => if eq_bool x zero then zero else iter_t log2n x. + Proof. red_t; reflexivity. Qed. + + Lemma spec_log2_0 : forall x, [x] = 0 -> [log2 x] = 0. + Proof. + intros x H. rewrite log2_fold. + rewrite spec_eq_bool, H. rewrite spec_0. simpl. + exact ZnZ.spec_0. + Qed. + + Lemma head0_zdigits : forall n (x : dom_t n), + 0 < ZnZ.to_Z x -> + ZnZ.to_Z (ZnZ.head0 x) < ZnZ.to_Z (ZnZ.zdigits (dom_op n)). + Proof. + intros n x H. + destruct (ZnZ.spec_head0 x H) as (_,H0). + intros. + assert (H1 := ZnZ.spec_to_Z (ZnZ.head0 x)). + assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). + unfold base in *. + rewrite ZnZ.spec_zdigits in H2 |- *. + set (h := ZnZ.to_Z (ZnZ.head0 x)) in *; clearbody h. + set (d := ZnZ.digits (dom_op n)) in *; clearbody d. + destruct (Z_lt_le_dec h (Zpos d)); auto. exfalso. + assert (1 * 2^Zpos d <= ZnZ.to_Z x * 2^h). + apply Zmult_le_compat; auto with zarith. + apply Zpower_le_monotone2; auto with zarith. + rewrite Zmult_comm in H0. auto with zarith. + Qed. + + Lemma spec_log2 : forall x, [x]<>0 -> + 2^[log2 x] <= [x] < 2^([log2 x]+1). + Proof. + intros x H. rewrite log2_fold. + rewrite spec_eq_bool. rewrite spec_0. + generalize (Zeq_bool_if [x] 0). destruct Zeq_bool. + auto with zarith. + apply spec_iter_t. clear x H. intros n x H. simpl. + rewrite spec_reduce, ZnZ.spec_sub_carry. + assert (H0 := ZnZ.spec_to_Z x). + assert (H1 := ZnZ.spec_to_Z (ZnZ.head0 x)). + assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). + assert (H3 := head0_zdigits n x). + rewrite Zmod_small by auto with zarith. + rewrite (ZBinary.ZBinPropMod.mul_lt_mono_pos_l (2^(ZnZ.to_Z (ZnZ.head0 x)))); + auto with zarith. + rewrite (ZBinary.ZBinPropMod.mul_le_mono_pos_l _ _ (2^(ZnZ.to_Z (ZnZ.head0 x)))); + auto with zarith. + rewrite <- 2 Zpower_exp; auto with zarith. + rewrite ZBinary.ZBinPropMod.add_sub_assoc, Zplus_minus. + rewrite ZBinary.ZBinPropMod.sub_simpl_r, Zplus_minus. + rewrite ZnZ.spec_zdigits. + rewrite pow2_pos_minus_1 by (red; auto). + apply ZnZ.spec_head0; auto with zarith. + Qed. + + Lemma log2_digits_head0 : forall x, 0 < [x] -> + [log2 x] = Zpos (digits x) - [head0 x] - 1. + Proof. + intros. + rewrite log2_fold. + rewrite spec_eq_bool. rewrite spec_0. + generalize (Zeq_bool_if [x] 0). destruct Zeq_bool. + auto with zarith. + intros _. revert H. + rewrite digits_fold, head0_fold. + apply spec_iter_t_3 with (P:=fun z a b c => 0 [a] = Zpos b - [c] -1). + clear x. intros n x. rewrite 2 spec_reduce. + rewrite ZnZ.spec_sub_carry. + intros. + generalize (head0_zdigits n x H). + generalize (ZnZ.spec_to_Z (ZnZ.head0 x)). + generalize (ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). + rewrite ZnZ.spec_zdigits. intros. apply Zmod_small. + auto with zarith. + Qed. + + (** * Right shift *) + + Local Notation shiftrn := (fun n (p x : dom_t n) => + let op := dom_op n in + match ZnZ.sub_c (ZnZ.zdigits op) p with + | C0 d => reduce n (ZnZ.add_mul_div d ZnZ.zero x) + | C1 _ => zero + end). + + Definition shiftr : t -> t -> t := Eval red_t in + same_level shiftrn. + + Lemma shiftr_fold : shiftr = same_level shiftrn. + Proof. red_t; reflexivity. Qed. + + Lemma div_pow2_bound :forall x y z, + 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z. + Proof. + intros x y z HH HH1 HH2. + split; auto with zarith. + apply Zle_lt_trans with (2 := HH2); auto with zarith. + apply Zdiv_le_upper_bound; auto with zarith. + pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith. + apply Zmult_le_compat_l; auto. + apply Zpower_le_monotone2; auto with zarith. + rewrite Zpower_0_r; ring. + Qed. Theorem spec_shiftr: forall n x, - [shiftr n x] = [x] / 2 ^ [n]. - Proof. - intros n x; unfold shiftr; - generalize (spec_compare_aux n (Ndigits x)); case compare; intros H. - apply trans_equal with (1 := spec_0 w0_spec). - apply sym_equal; apply Zdiv_small; rewrite H. - rewrite spec_Ndigits; exact (spec_digits x). - rewrite <- spec_unsafe_shiftr; auto with zarith. - apply trans_equal with (1 := spec_0 w0_spec). - apply sym_equal; apply Zdiv_small. - rewrite spec_Ndigits in H; case (spec_digits x); intros H1 H2. - split; auto. - apply Zlt_le_trans with (1 := H2). - apply Zpower_le_monotone; auto with zarith. + [shiftr n x] = [x] / 2 ^ [n]. + Proof. + intros x y. rewrite shiftr_fold. apply spec_same_level. clear x y. + intros n p x. simpl. + assert (Hx := ZnZ.spec_to_Z p). + assert (Hy := ZnZ.spec_to_Z x). + generalize (ZnZ.spec_sub_c (ZnZ.zdigits (dom_op n)) p). + case ZnZ.sub_c; intros d H; unfold interp_carry in *; simpl. + (** Subtraction without underflow : [ p <= digits ] *) + rewrite spec_reduce. + rewrite ZnZ.spec_zdigits in H. + rewrite ZnZ.spec_add_mul_div by auto with zarith. + rewrite ZnZ.spec_0, Zmult_0_l, Zplus_0_l. + rewrite Zmod_small. + f_equal. f_equal. auto with zarith. + split. auto with zarith. + apply div_pow2_bound; auto with zarith. + (** Subtraction with underflow : [ digits < p ] *) + rewrite ZnZ.spec_0. symmetry. + apply Zdiv_small. + split; auto with zarith. + apply Zlt_le_trans with (base (ZnZ.digits (dom_op n))); auto with zarith. + unfold base. apply Zpower_le_monotone2; auto with zarith. + rewrite ZnZ.spec_zdigits in H. + generalize (ZnZ.spec_to_Z d); auto with zarith. + Qed. + + (** * Left shift *) + + (** First an unsafe version, working correctly only if + the representation is large enough *) + + Local Notation unsafe_shiftln := (fun n p x => + let ops := dom_op n in + reduce n (ZnZ.add_mul_div p x ZnZ.zero)). + + Definition unsafe_shiftl : t -> t -> t := Eval red_t in + same_level unsafe_shiftln. + + Lemma unsafe_shiftl_fold : unsafe_shiftl = same_level unsafe_shiftln. + Proof. red_t; reflexivity. Qed. + + Theorem spec_unsafe_shiftl_aux : forall p x K, + 0 <= K -> + [x] < 2^K -> + [p] + K <= Zpos (digits x) -> + [unsafe_shiftl p x] = [x] * 2 ^ [p]. + Proof. + intros p x. + rewrite unsafe_shiftl_fold. rewrite digits_level. + apply spec_same_level_dep. + intros n m z z' r LE H K HK H1 H2. apply (H K); auto. + transitivity (Zpos (ZnZ.digits (dom_op n))); auto. + apply digits_dom_op_incr; auto. + clear p x. + intros n p x K HK Hx Hp. lazy zeta. rewrite spec_reduce. + destruct (ZnZ.spec_to_Z x). + destruct (ZnZ.spec_to_Z p). + rewrite ZnZ.spec_add_mul_div by (omega with *). + rewrite ZnZ.spec_0, Zdiv_0_l, Zplus_0_r. + apply Zmod_small. unfold base. + split; auto with zarith. + rewrite Zmult_comm. + apply Zlt_le_trans with (2^(ZnZ.to_Z p + K)). + rewrite Zpower_exp; auto with zarith. + apply Zmult_lt_compat_l; auto with zarith. + apply Zpower_le_monotone2; auto with zarith. + Qed. + + Theorem spec_unsafe_shiftl: forall p x, + [p] <= [head0 x] -> [unsafe_shiftl p x] = [x] * 2 ^ [p]. + Proof. + intros. + destruct (Z_eq_dec [x] 0) as [EQ|NEQ]. + (* [x] = 0 *) + apply spec_unsafe_shiftl_aux with 0; auto with zarith. + now rewrite EQ. + rewrite spec_head00 in *; auto with zarith. + (* [x] <> 0 *) + apply spec_unsafe_shiftl_aux with ([log2 x] + 1); auto with zarith. + generalize (spec_pos (log2 x)); auto with zarith. + destruct (spec_log2 x); auto with zarith. + rewrite log2_digits_head0; auto with zarith. + generalize (spec_pos x); auto with zarith. Qed. + (** Then we define a function doubling the size of the representation + but without changing the value of the number. *) + + Local Notation double_size_n := + (fun n x => mk_t_S n (WW ZnZ.zero x)). + + Definition double_size : t -> t := Eval red_t in + iter_t double_size_n. + + Lemma double_size_fold : double_size = iter_t double_size_n. + Proof. red_t; reflexivity. Qed. + + Theorem spec_double_size_digits: + forall x, digits (double_size x) = xO (digits x). + Proof. + intros x; case x; unfold double_size, digits; clear x; auto. + intros n x; rewrite make_op_S; auto. + Qed. + + Theorem spec_double_size: forall x, [double_size x] = [x]. + Proof. + intros x. rewrite double_size_fold. apply spec_iter_t. clear x. + intros n x. rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_0. + auto with zarith. + Qed. + + Theorem spec_double_size_head0: + forall x, 2 * [head0 x] <= [head0 (double_size x)]. + Proof. + intros x. + assert (F1:= spec_pos (head0 x)). + assert (F2: 0 < Zpos (digits x)). + red; auto. + case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH. + generalize HH; rewrite <- (spec_double_size x); intros HH1. + case (spec_head0 x HH); intros _ HH2. + case (spec_head0 _ HH1). + rewrite (spec_double_size x); rewrite (spec_double_size_digits x). + intros HH3 _. + case (Zle_or_lt ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4. + absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto. + apply Zle_not_lt. + apply Zmult_le_compat_r; auto with zarith. + apply Zpower_le_monotone2; auto; auto with zarith. + assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)). + case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5. + apply Zmult_le_reg_r with (2 ^ 1); auto with zarith. + rewrite <- (fun x y z => Zpower_exp x (y - z)); auto with zarith. + assert (tmp: forall x, x - 1 + 1 = x); [intros; ring | rewrite tmp; clear tmp]. + apply Zle_trans with (2 := Zlt_le_weak _ _ HH2). + apply Zmult_le_compat_l; auto with zarith. + rewrite Zpower_1_r; auto with zarith. + apply Zpower_le_monotone2; auto with zarith. + case (Zle_or_lt (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6. + absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith. + rewrite <- HH5; rewrite Zmult_1_r. + apply Zpower_le_monotone2; auto with zarith. + rewrite (Zmult_comm 2). + rewrite Zpower_mult; auto with zarith. + rewrite Zpower_2. + apply Zlt_le_trans with (2 := HH3). + rewrite <- Zmult_assoc. + replace (Zpos (xO (digits x)) - 1) with + ((Zpos (digits x) - 1) + (Zpos (digits x))). + rewrite Zpower_exp; auto with zarith. + apply Zmult_lt_compat2; auto with zarith. + split; auto with zarith. + apply Zmult_lt_0_compat; auto with zarith. + rewrite Zpos_xO; ring. + apply Zlt_le_weak; auto. + repeat rewrite spec_head00; auto. + rewrite spec_double_size_digits. + rewrite Zpos_xO; auto with zarith. + rewrite spec_double_size; auto. + Qed. + + Theorem spec_double_size_head0_pos: + forall x, 0 < [head0 (double_size x)]. + Proof. + intros x. + assert (F: 0 < Zpos (digits x)). + red; auto. + case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0. + case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1. + apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith. + case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3. + generalize F3; rewrite <- (spec_double_size x); intros F4. + absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))). + apply Zle_not_lt. + apply Zpower_le_monotone2; auto with zarith. + rewrite Zpos_xO; auto with zarith. + case (spec_head0 x F3). + rewrite <- F1; rewrite Zpower_0_r; rewrite Zmult_1_l; intros _ HH. + apply Zle_lt_trans with (2 := HH). + case (spec_head0 _ F4). + rewrite (spec_double_size x); rewrite (spec_double_size_digits x). + rewrite <- F0; rewrite Zpower_0_r; rewrite Zmult_1_l; auto. + generalize F1; rewrite (spec_head00 _ (sym_equal F3)); auto with zarith. + Qed. + + (** Finally we iterate [double_size] enough before [unsafe_shiftl] + in order to get a fully correct [shiftl]. *) + Definition shiftl_aux_body cont n x := match compare n (head0 x) with Gt => cont n (double_size x) @@ -425,7 +1071,7 @@ Module Make (Import W0:CyclicType) <: NType. [shiftl_aux_body cont n x] = [x] * 2 ^ [n]. Proof. intros n p x cont H1 H2; unfold shiftl_aux_body. - generalize (spec_compare_aux n (head0 x)); case compare; intros H. + rewrite spec_compare; case Zcompare_spec; intros H. apply spec_unsafe_shiftl; auto with zarith. apply spec_unsafe_shiftl; auto with zarith. rewrite H2. @@ -435,7 +1081,7 @@ Module Make (Import W0:CyclicType) <: NType. rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith. Qed. - Fixpoint shiftl_aux p cont n x {struct p} := + Fixpoint shiftl_aux p cont n x := shiftl_aux_body (fun n x => match p with | xH => cont n x @@ -465,7 +1111,7 @@ Module Make (Import W0:CyclicType) <: NType. apply spec_shiftl_aux_body with (q); auto. intros x1 H3; apply Hrec with (q); auto. apply Zle_trans with (2 := H3); auto with zarith. - apply Zpower_le_monotone; auto with zarith. + apply Zpower_le_monotone2; auto with zarith. intros x2 H4; apply Hrec with (p + q)%positive; auto. intros x3 H5; apply H2. rewrite (Zpos_xO p). @@ -486,11 +1132,11 @@ Module Make (Import W0:CyclicType) <: NType. [shiftl n x] = [x] * 2 ^ [n]. Proof. intros n x; unfold shiftl, shiftl_aux_body. - generalize (spec_compare_aux n (head0 x)); case compare; intros H. + rewrite spec_compare; case Zcompare_spec; intros H. apply spec_unsafe_shiftl; auto with zarith. apply spec_unsafe_shiftl; auto with zarith. rewrite <- (spec_double_size x). - generalize (spec_compare_aux n (head0 (double_size x))); case compare; intros H1. + rewrite spec_compare; case Zcompare_spec; intros H1. apply spec_unsafe_shiftl; auto with zarith. apply spec_unsafe_shiftl; auto with zarith. rewrite <- (spec_double_size (double_size x)). @@ -504,21 +1150,22 @@ Module Make (Import W0:CyclicType) <: NType. apply Zle_trans with (2 := H2). apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith. case (spec_digits n); auto with zarith. - apply Zpower_le_monotone; auto with zarith. + apply Zpower_le_monotone2; auto with zarith. Qed. + (** * Parity test *) - (** * Zero and One *) + Definition is_even : t -> bool := Eval red_t in + iter_t (fun n x => ZnZ.is_even x). - Theorem spec_0: [zero] = 0. - Proof. - exact (spec_0 w0_spec). - Qed. + Lemma is_even_fold : is_even = iter_t (fun n x => ZnZ.is_even x). + Proof. red_t; reflexivity. Qed. - Theorem spec_1: [one] = 1. + Theorem spec_is_even: forall x, + if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1. Proof. - exact (spec_1 w0_spec). + intros x. rewrite is_even_fold. apply spec_iter_t. clear x. + intros n x; exact (ZnZ.spec_is_even x). Qed. - End Make. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index b8552a39b..cd8798236 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -24,7 +24,7 @@ let gen_proof = true (* should we generate proofs ? *) let t = "t" let c = "N" -let pz n = if n == 0 then "w_0" else "W0" +let pz n = if n == 0 then "ZnZ.zero" 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 = @@ -73,35 +73,52 @@ let _ = pr " DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic"; pr " Wf_nat StreamMemo."; pr ""; - pr "Module Make (Import W0:CyclicType)."; + pr "Module Make (W0:CyclicType)."; pr ""; - pr " Definition w0 := W0.w."; + pr " Implicit Arguments mk_zn2z_ops [t]."; + pr " Implicit Arguments mk_zn2z_ops_karatsuba [t]."; + pr " Implicit Arguments mk_zn2z_specs [t ops]."; + pr " Implicit Arguments mk_zn2z_specs_karatsuba [t ops]."; + pr " Implicit Arguments ZnZ.digits [t]."; + pr " Implicit Arguments ZnZ.zdigits [t]."; + pr ""; + + pr " (** * The word types *)"; + pr ""; + + pr " Local Notation w0 := W0.t."; for i = 1 to size do pr " Definition w%i := zn2z w%i." i (i-1) done; pr ""; - pr " Definition w0_op := W0.w_op."; + pr " (** * The operation type classes for the word types *)"; + pr ""; + + pr " Local Notation w0_op := W0.ops."; for i = 1 to 3 do - pr " Definition w%i_op := mk_zn2z_op w%i_op." i (i-1) + pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops w%i_op." i i (i-1) done; - for i = 4 to size + 3 do - pr " Definition w%i_op := mk_zn2z_op_karatsuba w%i_op." i (i-1) + for i = 4 to size do + pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops_karatsuba w%i_op." i i (i-1) + done; + for i = size+1 to size+3 do + pr " Instance w%i_op : ZnZ.Ops (word w%i %i%%nat) := mk_zn2z_ops_karatsuba w%i_op." i size (i-size) (i-1) done; pr ""; pr " Section Make_op."; - pr " Variable mk : forall w', znz_op w' -> znz_op (zn2z w')."; + pr " Variable mk : forall w', ZnZ.Ops w' -> ZnZ.Ops (zn2z w')."; pr ""; - pr " Fixpoint make_op_aux (n:nat) : znz_op (word w%i (S n)):=" size; - pr " match n return znz_op (word w%i (S n)) with" size; + pr " Fixpoint make_op_aux (n:nat) : ZnZ.Ops (word w%i (S n)):=" size; + pr " match n return ZnZ.Ops (word w%i (S n)) with" size; pr " | O => w%i_op" (size+1); pr " | S n1 =>"; - pr " match n1 return znz_op (word w%i (S (S n1))) with" size; + pr " match n1 return ZnZ.Ops (word w%i (S (S n1))) with" size; pr " | O => w%i_op" (size+2); pr " | S n2 =>"; - pr " match n2 return znz_op (word w%i (S (S (S n2)))) with" size; + pr " match n2 return ZnZ.Ops (word w%i (S (S (S n2)))) with" size; pr " | O => w%i_op" (size+3); pr " | S n3 => mk _ (mk _ (mk _ (make_op_aux n3)))"; pr " end"; @@ -110,12 +127,15 @@ let _ = pr ""; pr " End Make_op."; pr ""; - pr " Definition omake_op := make_op_aux mk_zn2z_op_karatsuba."; + pr " Definition omake_op := make_op_aux mk_zn2z_ops_karatsuba."; pr ""; pr ""; pr " Definition make_op_list := dmemo_list _ omake_op."; pr ""; - pr " Definition make_op n := dmemo_get _ omake_op n make_op_list."; + pr " Instance make_op n : ZnZ.Ops (word w6 (S n))"; + pr " := dmemo_get _ omake_op n make_op_list."; + pr ""; + pr ""; pr " Lemma make_op_omake: forall n, make_op n = omake_op n."; pr " intros n; unfold make_op, make_op_list."; @@ -123,6 +143,10 @@ let _ = pr " Qed."; pr ""; + + pr " (** * The main type [t], isomorphic with [exists n, word w0 n] *)"; + pr ""; + pr " Inductive %s_ :=" t; for i = 0 to size do pr " | %s%i : w%i -> %s_" c i i t @@ -131,49 +155,98 @@ let _ = pr ""; pr " Definition %s := %s_." t t; pr ""; - pr " Definition w_0 := w0_op.(znz_0)."; + + pr " Definition zero : t := %s0 ZnZ.zero." c; + pr " Definition one : t := %s0 ZnZ.one." c; + pr ""; + + pr " (** * A generic toolbox for building and deconstructing [t] *)"; + pr ""; + + let rec iter_str n s = if n = 0 then "" else (iter_str (n-1) s) ^ s + in + pr " Local Notation SizePlus n := %sn%s." + (iter_str size "(S ") (iter_str size ")"); pr ""; + pr " Definition dom_t n := match n with"; for i = 0 to size do - pr " Definition one%i := w%i_op.(znz_1)." i i + pr " | %i => w%i" i i; done; + pr " | SizePlus n => word w%i n" size; + pr " end."; pr ""; - - pr " Definition zero := %s0 w_0." c; - pr " Definition one := %s0 one0." c; + pr " Instance dom_op n : ZnZ.Ops (dom_t n) | 10."; + pa " Admitted."; + pp " Proof."; + pp " do %i (destruct n; [simpl;auto with *|])." (size+1); + pp " unfold dom_t. auto with *."; + pp " Defined."; pr ""; - pr " Definition to_Z x :="; + pr " Definition iter_t {A:Type}(f : forall n, dom_t n -> A)(x:t) : A :="; pr " match x with"; for i = 0 to size do - pr " | %s%i wx => w%i_op.(znz_to_Z) wx" c i i + pr " | %s%i wx => f %i wx" c i i; done; - pr " | %sn n wx => (make_op n).(znz_to_Z) wx" c; + pr " | %sn n wx => f (SizePlus (S n)) wx" c; pr " end."; pr ""; - pr " Open Scope Z_scope."; - pr " Notation \"[ x ]\" := (to_Z x)."; + pr " Definition mk_t (n:nat) : dom_t n -> t :="; + pr " match n as n' return dom_t n' -> t with"; + for i = 0 to size do + pr " | %i => %s%i" i c i; + done; + pr " | SizePlus (S n) => %sn n" c; + pr " end."; pr ""; - pr " Definition to_N x := Zabs_N (to_Z x)."; +pr " + Lemma dom_t_S : forall n, zn2z (dom_t n) = dom_t (S n). + Proof. + do %i (destruct n; try reflexivity). + Defined. +" (size+1); + +pr " + Definition cast w w' (H:w=w') (x:w) : w' := + match H in _=y return y with + | eq_refl => x + end. + + Definition mk_t_S n (x:zn2z (dom_t n)) : t := + Eval lazy beta delta [cast dom_t_S] in + mk_t (S n) (cast _ _ (dom_t_S n) x). +"; +pr " + + (** * Projection to ZArith *) + + Definition to_Z : t -> Z := + Eval lazy beta iota delta [iter_t dom_t dom_op] in + iter_t (fun _ x => ZnZ.to_Z x). +"; + + pr " Open Scope Z_scope."; + pr " Notation \"[ x ]\" := (to_Z x)."; pr ""; - pr " Definition eq x y := (to_Z x = to_Z y)."; + pr " Definition eq (x y : t) := (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 " znz_op (word ww n) :="; - pp " match n return znz_op (word ww n) with"; + pp " Fixpoint nmake_op (ww:Type) (ww_op: ZnZ.Ops ww) (n: nat) :"; + pp " ZnZ.Ops (word ww n) :="; + pp " match n return ZnZ.Ops (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_ops (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 " nmake_op _ w_op (S x) = mk_zn2z_op (nmake_op _ w_op x)."; + pp " Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x,"; + pp " nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x)."; pp " auto."; pp " Qed."; pp ""; @@ -182,27 +255,27 @@ let _ = pr " (* Eval and extend functions for each level *)"; 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; + pp " Let eval%in n := ZnZ.to_Z (Ops:=nmake_op%i n)." i i; if i == 0 then - pr " Let extend%i := DoubleBase.extend (WW w_0)." i + pr " Let extend%i := DoubleBase.extend (WW (ZnZ.zero:w0))." i else - pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i; + pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i; done; pr ""; - 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 " Theorem digits_doubled:forall n ww (w_op: ZnZ.Ops 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."; pp " intros n Hrec ww ww_op; simpl DoubleBase.double_digits."; pp " rewrite <- Hrec; auto."; pp " Qed."; pp ""; - 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 " Theorem nmake_double: forall n ww (w_op: ZnZ.Ops ww),"; + pp " ZnZ.to_Z (Ops:=nmake_op _ w_op n) ="; + pp " @DoubleBase.double_to_Z _ (ZnZ.digits w_op) (ZnZ.to_Z (Ops:=w_op)) n."; pp " Proof."; pp " intros n; elim n; auto; clear n."; pp " intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z."; @@ -212,9 +285,9 @@ let _ = pp ""; - 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 " Theorem digits_nmake:forall n ww (w_op: ZnZ.Ops ww),"; + pp " ZnZ.digits (nmake_op _ w_op (S n)) ="; + pp " xO (ZnZ.digits (nmake_op _ w_op n))."; pp " Proof."; pp " auto."; pp " Qed."; @@ -222,17 +295,17 @@ let _ = pp " Theorem znz_nmake_op: forall ww ww_op n xh xl,"; - pp " znz_to_Z (nmake_op ww ww_op (S n)) (WW xh xl) ="; - pp " znz_to_Z (nmake_op ww ww_op n) xh *"; - pp " base (znz_digits (nmake_op ww ww_op n)) +"; - pp " znz_to_Z (nmake_op ww ww_op n) xl."; + pp " ZnZ.to_Z (Ops:=nmake_op ww ww_op (S n)) (WW xh xl) ="; + pp " ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xh *"; + pp " base (ZnZ.digits (nmake_op ww ww_op n)) +"; + pp " ZnZ.to_Z (Ops:=nmake_op ww ww_op n) xl."; pp " Proof."; pp " auto."; pp " Qed."; pp ""; pp " Theorem make_op_S: forall n,"; - pp " make_op (S n) = mk_zn2z_op_karatsuba (make_op n)."; + pp " make_op (S n) = mk_zn2z_ops_karatsuba (make_op n)."; pp " intro n."; pp " do 2 rewrite make_op_omake."; pp " pattern n; apply lt_wf_ind; clear n."; @@ -244,71 +317,76 @@ let _ = pp " intros _; unfold omake_op, make_op_aux, w%i_op, w%i_op; apply refl_equal." (size + 3) (size + 2); pp " intros n Hrec."; pp " change (omake_op (S (S (S (S n))))) with"; - pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op (S n)))))."; + pp " (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (omake_op (S n)))))."; pp " change (omake_op (S (S (S n)))) with"; - pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op n))))."; + pp " (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (mk_zn2z_ops_karatsuba (omake_op n))))."; pp " rewrite Hrec; auto with arith."; pp " Qed."; pp ""; + pr " (** * The specification proofs for the word operators *)"; + pr ""; - 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 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 ""; - 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 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 ""; + pr " Typeclasses Opaque w1 w2 w3 w4 w5 w6."; + pr ""; - pp " Let w0_spec: znz_spec w0_op := W0.w_spec."; + pp " Instance w0_spec: ZnZ.Specs w0_op := W0.specs."; 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 " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs 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) + pp " Instance w%i_spec : ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1) done; pp ""; - pp " Let wn_spec: forall n, znz_spec (make_op n)."; + pp " Instance wn_spec (n:nat) : ZnZ.Specs (make_op n)."; + pp " Proof."; pp " intros n; elim n; clear n."; pp " exact w%i_spec." (size + 1); pp " intros n Hrec; rewrite make_op_S."; - pp " exact (mk_znz2_karatsuba_spec Hrec)."; + pp " exact (mk_zn2z_specs_karatsuba Hrec)."; pp " Qed."; pp ""; - for i = 0 to size do - pr " Definition w%i_eq0 := w%i_op.(znz_eq0)." i i; - pr " Let spec_w%i_eq0: forall x, if w%i_eq0 x then [%s%i x] = 0 else True." i i c i; - pa " Admitted."; +pr " + Instance spec_dom n : ZnZ.Specs (dom_op n) | 10. + Proof. + do %i (destruct n; auto with *). apply wn_spec. + Qed. +" (size+1); + + for i = 1 to size + 2 do + pp " Let to_Z_%i: forall x y," i; + pp " ZnZ.to_Z (Ops:=w%i_op) (WW x y) =" i; + pp " ZnZ.to_Z (Ops:=w%i_op) x * base (ZnZ.digits w%i_op) + ZnZ.to_Z (Ops:=w%i_op) y." (i-1) (i-1) (i-1); pp " Proof."; - pp " intros x; unfold w%i_eq0, to_Z; generalize (spec_eq0 w%i_spec x);" i i; - pp " case znz_eq0; auto."; + pp " auto."; pp " Qed."; - pr ""; + pp ""; done; - pr ""; + pp " Let to_Z_n: forall n x y,"; + pp " ZnZ.to_Z (Ops:=make_op (S n)) (WW x y) ="; + pp " ZnZ.to_Z (Ops:=make_op n) x * base (ZnZ.digits (make_op n)) + ZnZ.to_Z (Ops:=make_op n) y."; + pp " Proof."; + pp " intros n x y; rewrite make_op_S; auto."; + pp " Qed."; + pp ""; + + let rec iter_name i j base sep = + if i = j then base^(string_of_int i) + else (iter_name i (j-1) base sep)^sep^" "^base^(string_of_int j) + in 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 (Ops:=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."; @@ -317,20 +395,20 @@ 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 pp " auto." else begin - pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1); + pp " apply trans_equal with (xO (ZnZ.digits w%i_op))." (i + j -1); pp " auto."; pp " unfold nmake_op; auto."; end else begin - pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1); + pp " apply trans_equal with (xO (ZnZ.digits w%i_op))." (i + j -1); pp " auto."; pp " rewrite digits_nmake."; pp " rewrite digits_w%in%i." i (j - 1); @@ -346,7 +424,7 @@ let _ = begin pp " intros x; case x."; pp " auto."; - pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (i + j); + pp " intros xh xl; unfold to_Z; rewrite to_Z_%i." (i + j); pp " rewrite digits_w%in%i." i (j - 1); pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (j - 1); pp " unfold eval%in, nmake_op%i." i i; @@ -358,15 +436,15 @@ let _ = 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); - pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1); - pp " rewrite (spec_0 w%i_spec); auto." (i + j); + pp " intros x; change (extend%i 0 x) with (WW (ZnZ.zero (Ops:=w%i_op)) x)." i (i + j); + pp " unfold to_Z; rewrite to_Z_%i." (i + j + 1); + pp " rewrite ZnZ.spec_0; auto."; end else begin - 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); - pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1); - pp " rewrite (spec_0 w%i_spec)." (i + j); + pp " intros x; change (extend%i %i x) with (WW (ZnZ.zero (Ops:=w%i_op)) (extend%i %i x))." i j (i + j) i (j - 1); + pp " unfold to_Z; rewrite to_Z_%i." (i + j + 1); + pp " rewrite ZnZ.spec_0."; pp " generalize (spec_extend%in%i x); unfold to_Z." i (i + j); pp " intros HH; rewrite <- HH; auto."; end; @@ -375,9 +453,9 @@ let _ = end; done; - 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); + 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); pp " Proof."; - pp " apply trans_equal with (xO (znz_digits w%i_op))." size; + pp " apply trans_equal with (xO (ZnZ.digits w%i_op))." size; pp " auto."; pp " rewrite digits_nmake."; pp " rewrite digits_w%in%i." i (size - i); @@ -389,7 +467,7 @@ let _ = pp " Proof."; pp " intros x; case x."; pp " auto."; - pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 1); + pp " intros xh xl; unfold to_Z; rewrite to_Z_%i." (size + 1); pp " rewrite digits_w%in%i." i (size - i); pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (size - i); pp " unfold eval%in, nmake_op%i." i i; @@ -400,7 +478,7 @@ let _ = 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); + pp " intros xh xl; unfold to_Z; rewrite to_Z_%i." (size + 2); pp " rewrite digits_w%in%i." i (size + 1 - i); 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); pp " unfold eval%in, nmake_op%i." i i; @@ -410,12 +488,12 @@ let _ = done; pp " Let digits_w%in: forall n," size; - pp " znz_digits (make_op n) = znz_digits (nmake_op _ w%i_op (S n))." size; + pp " ZnZ.digits (make_op n) = ZnZ.digits (nmake_op _ w%i_op (S n))." size; pp " intros n; elim n; clear n."; - pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size; + pp " change (ZnZ.digits (make_op 0)) with (xO (ZnZ.digits w%i_op))." size; pp " rewrite nmake_op_S; apply sym_equal; auto."; pp " intros n Hrec."; - pp " replace (znz_digits (make_op (S n))) with (xO (znz_digits (make_op n)))."; + pp " replace (ZnZ.digits (make_op (S n))) with (xO (ZnZ.digits (make_op n)))."; pp " rewrite Hrec."; pp " rewrite nmake_op_S; apply sym_equal; auto."; pp " rewrite make_op_S; apply sym_equal; auto."; @@ -430,7 +508,7 @@ let _ = pp " rewrite make_op_S; rewrite nmake_op_S; auto."; pp " intros xh xl."; pp " unfold to_Z in Hrec |- *."; - pp " rewrite znz_to_Z_n."; + pp " rewrite to_Z_n."; pp " rewrite digits_w%in." size; pp " repeat rewrite Hrec."; pp " unfold eval%in, nmake_op%i." size size; @@ -440,29 +518,36 @@ let _ = 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 " intros x; change (extend%i 0 x) with (WW (ZnZ.zero (Ops:=w%i_op)) x)." size size; pp " unfold to_Z."; pp " change (make_op 0) with w%i_op." (size + 1); - pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto." (size + 1) size; + pp " rewrite to_Z_%i; rewrite ZnZ.spec_0; auto." (size + 1); pp " intros n Hrec x."; pp " change (extend%i (S n) x) with (WW W0 (extend%i n x))." size size; - pp " unfold to_Z in Hrec |- *; rewrite znz_to_Z_n; auto."; + pp " unfold to_Z in Hrec |- *; rewrite to_Z_n; auto."; pp " rewrite <- Hrec."; - pp " replace (znz_to_Z (make_op n) W0) with 0; auto."; + pp " replace (ZnZ.to_Z (Ops:=make_op n) W0) with 0; auto."; pp " case n; auto; intros; rewrite make_op_S; auto."; pp " Qed."; pp ""; - pr " Theorem spec_pos: forall x, 0 <= [x]."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; clear x."; - for i = 0 to size do - pp " intros x; case (spec_to_Z w%i_spec x); auto." i; - done; - pp " intros n x; case (spec_to_Z (wn_spec n) x); auto."; - pp " Qed."; - pr ""; +pr " + Lemma digits_dom_op : forall n, + Zpos (ZnZ.digits (dom_op n)) = Zpos (ZnZ.digits W0.ops) * 2 ^ Z_of_nat n. + Proof. + intros. rewrite Zmult_comm. + do 7 (destruct n; try reflexivity). + simpl. + rewrite <- shift_pos_correct. f_equal. + rewrite shift_pos_nat. + rewrite !nat_of_P_succ_morphism, nat_of_P_o_P_of_succ_nat_eq_succ. + unfold shift_nat. simpl. + generalize (digits_w%in n); simpl; intros ->. + rewrite digits_doubled. + rewrite digits_w%i, !digits_nmake. simpl. + induction n; simpl; congruence. + Qed. +" size size; pp " Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx]." c c; pp " intros n; elim n; auto."; @@ -474,8 +559,8 @@ let _ = pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c; pp " Proof."; pp " intros n x; unfold to_Z."; - pp " rewrite znz_to_Z_n."; - pp " rewrite <- (Zplus_0_l (znz_to_Z (make_op n) x))."; + pp " rewrite to_Z_n."; + pp " rewrite <- (Zplus_0_l (ZnZ.to_Z (Ops:=make_op n) x))."; pp " apply (f_equal2 Zplus); auto."; pp " case n; auto."; pp " intros n1; rewrite make_op_S; auto."; @@ -508,54 +593,29 @@ let _ = pp " Qed."; pp ""; - - pr " Section LevelAndIter."; + pr " Section SameLevel."; pr ""; pr " Variable res: Type."; - pr " Variable xxx: res."; - pr " Variable P: Z -> Z -> res -> Prop."; - pr " (* Abstraction function for each level *)"; + pr " Variable P : Z -> Z -> res -> Prop."; + pr " Variable f : forall n, dom_t n -> dom_t n -> res."; + pr " Variable Pf : forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)."; + pr ""; for i = 0 to size do - pr " Variable f%i: w%i -> w%i -> res." i i i; - pr " Variable f%in: forall n, w%i -> word w%i (S n) -> res." i i i; - pr " Variable fn%i: forall n, word w%i (S n) -> w%i -> res." i i i; - pp " Variable Pf%i: forall x y, P [%s%i x] [%s%i y] (f%i x y)." i c i c i i; - if i == size then - begin - 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; - 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; - end - else - begin - 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; - 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; - end; - pr ""; + pr " Let f%i : w%i -> w%i -> res := f %i." i i i i; done; - pr " Variable fnn: forall n, word w%i (S n) -> word w%i (S n) -> res." size size; - pp " Variable Pfnn: forall n x y, P [%sn n x] [%sn n y] (fnn n x y)." c c; - pr " Variable fnm: forall n m, word w%i (S n) -> word w%i (S m) -> res." size size; - pp " Variable Pfnm: forall n m x y, P [%sn n x] [%sn m y] (fnm n m x y)." c c; - pr ""; - pr " (* Special zero functions *)"; - pr " Variable f0t: t_ -> res."; - pp " Variable Pf0t: forall x, P 0 [x] (f0t x)."; - pr " Variable ft0: t_ -> res."; - pp " Variable Pft0: forall x, P [x] 0 (ft0 x)."; + pr " Let fn n := f (SizePlus (S n))."; pr ""; - - - pr " (* We level the two arguments before applying *)"; - pr " (* the functions at each leval *)"; - pr " Definition same_level (x y: t_): res :="; - pr0 " Eval lazy zeta beta iota delta ["; for i = 0 to size do - pr0 "extend%i " i; + pr " Let Pf%i : forall x y : w%i, P [%s%i x] [%s%i y] (f%i x y) := Pf %i." i i c i c i i i; done; + pr " Let Pfn n : forall x y, P [%sn n x] [%sn n y] (fn n x y) := Pf (SizePlus (S n))." c c; pr ""; - pr " DoubleBase.extend DoubleBase.extend_aux"; - pr " ] in"; - pr " match x, y with"; + pr " (* We level the two arguments before applying *)"; + pr " (* the functions at each level *)"; + pr ""; + pr " Definition same_level (x y: t_): res := Eval lazy zeta beta iota delta"; + pr " [ DoubleBase.extend DoubleBase.extend_aux %s ]" (iter_name 0 (size-1) "extend" ""); + pr " in match x, y with"; for i = 0 to size do for j = 0 to i - 1 do pr " | %s%i wx, %s%i wy => f%i wx (extend%i %i wy)" c i c j i j (i - j -1); @@ -565,20 +625,20 @@ 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 + pr " | %s%i wx, %sn m wy => fn 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); + pr " | %s%i wx, %sn m wy => fn 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 + pr " | %sn n wx, %s%i wy => fn 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); + pr " | %sn n wx, %s%i wy => fn 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; pr " let mn := Max.max n m in"; pr " let d := diff n m in"; - pr " fnn mn"; + pr " fn mn"; pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; pr " (castm (diff_l n m) (extend_tr wy (fst d)))"; pr " end."; @@ -597,126 +657,56 @@ let _ = pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j; done; if i == size then - pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size + pp " intros m y; rewrite (spec_extend%in m); apply (Pfn m)." size else - pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size; + pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply (Pfn m)." 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 + pp " intros y; rewrite (spec_extend%in n); apply (Pfn n)." size else - pp " intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size; + pp " intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply (Pfn n)." i size size; done; pp " intros m y; rewrite <- (spec_cast_l n m x);"; - pp " rewrite <- (spec_cast_r n m y); apply Pfnn."; + pp " rewrite <- (spec_cast_r n m y); apply (Pfn (Max.max n m))."; pp " Qed."; pp ""; - pr " (* We level the two arguments before applying *)"; - pr " (* the functions at each level (special zero case) *)"; - pr " Definition same_level0 (x y: t_): res :="; - pr0 " Eval lazy zeta beta iota delta ["; - for i = 0 to size do - pr0 "extend%i " i; - done; + pr " End SameLevel."; pr ""; - pr " DoubleBase.extend DoubleBase.extend_aux"; - pr " ] in"; - pr " match x with"; - for i = 0 to size do - pr " | %s%i wx =>" c i; - if i == 0 then - pr " if w0_eq0 wx then f0t y else"; - pr " match y with"; - for j = 0 to i - 1 do - pr " | %s%i wy =>" c j; - 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; - pr " | %s%i wy => f%i wx wy" c i i; - for j = i + 1 to size do - 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 (extend%i %i wx)) wy" c size i (size - i - 1); - pr" end"; - done; - pr " | %sn n wx =>" c; - pr " match y with"; - for i = 0 to size do - pr " | %s%i wy =>" c i; - 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 (extend%i %i wy))" size i (size - i - 1); - done; - pr " | %sn m wy =>" c; - pr " let mn := Max.max n m in"; - pr " let d := diff n m in"; - pr " fnn mn"; - pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; - pr " (castm (diff_l n m) (extend_tr wy (fst d)))"; - pr " end"; - pr " end."; + pr " Implicit Arguments same_level [res]."; pr ""; - - pp " Lemma spec_same_level0: forall x y, P [x] [y] (same_level0 x y)."; - pp " Proof."; - pp " intros x; case x; clear x; unfold same_level0."; + pr " Section Iter."; + pr ""; + pr " Variable res: Type."; + pr " Variable P: Z -> Z -> res -> Prop."; + pr " (* Abstraction function for each level *)"; for i = 0 to size do - pp " intros x."; - if i == 0 then - begin - pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H."; - pp " intros y; rewrite H; apply Pf0t."; - pp " clear H."; - end; - pp " intros y; case y; clear y."; - for j = 0 to i - 1 do - pp " intros y."; - if j == 0 then - begin - pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; - pp " rewrite H; apply Pft0."; - pp " clear H."; - end; - pp " rewrite spec_extend%in%i; apply Pf%i." j i i; - done; - pp " intros y; apply Pf%i." i; - for j = i + 1 to size do - pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j; - done; + pr " Variable f%i: w%i -> w%i -> res." i i i; + pr " Variable f%in: forall n, w%i -> word w%i (S n) -> res." i i i; + pr " Variable fn%i: forall n, word w%i (S n) -> w%i -> res." i i i; + pp " Variable Pf%i: forall x y, P [%s%i x] [%s%i y] (f%i x y)." i c i c i i; if i == size then - pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size + begin + 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; + 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; + end 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 - pp " intros y."; - if i = 0 then begin - pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; - pp " rewrite H; apply Pft0."; - pp " clear H."; + 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; + 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; end; - if i == size then - pp " rewrite (spec_extend%in n); apply Pfnn." size - else - pp " rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size; + pr ""; done; - 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 " Variable fnn: forall n, word w%i (S n) -> word w%i (S n) -> res." size size; + pp " Variable Pfnn: forall n x y, P [%sn n x] [%sn n y] (fnn n x y)." c c; + pr " Variable fnm: forall n m, word w%i (S n) -> word w%i (S m) -> res." size size; + pp " Variable Pfnm: forall n m x y, P [%sn n x] [%sn m y] (fnm n m x y)." c c; + pr ""; pr " (* We iter the smaller argument with the bigger *)"; + pr ""; pr " Definition iter (x y: t_): res :="; pr0 " Eval lazy zeta beta iota delta ["; for i = 0 to size do @@ -748,7 +738,11 @@ let _ = pr " | %sn n wx, %sn m wy => fnm n m wx wy" c c; pr " end."; pr ""; - + let break_eq0 v = + pp " generalize (ZnZ.spec_eq0 %s); case ZnZ.eq0; intros H." v; + pp " intros; simpl [N0 %s]; rewrite H; trivial." v; + pp " clear H." + in pp " Ltac zg_tac := try"; pp " (red; simpl Zcompare; auto;"; pp " let t := fresh \"H\" in (intros t; discriminate t))."; @@ -782,7 +776,14 @@ let _ = pp ""; - pr " (* We iter the smaller argument with the bigger (zero case) *)"; + pr " (* We iter the smaller argument with the bigger *)"; + pr " (* with special zero functions *)"; + pr ""; + pr " Variable f0t: t_ -> res."; + pp " Variable Pf0t: forall x, P 0 [x] (f0t x)."; + pr " Variable ft0: t_ -> res."; + pp " Variable Pft0: forall x, P [x] 0 (ft0 x)."; + pr ""; pr " Definition iter0 (x y: t_): res :="; pr0 " Eval lazy zeta beta iota delta ["; for i = 0 to size do @@ -795,12 +796,12 @@ let _ = for i = 0 to size do pr " | %s%i wx =>" c i; if i == 0 then - pr " if w0_eq0 wx then f0t y else"; + pr " if ZnZ.eq0 wx then f0t y else"; pr " match y with"; for j = 0 to i - 1 do pr " | %s%i wy =>" c j; if j == 0 then - pr " if w0_eq0 wy then ft0 x else"; + pr " if ZnZ.eq0 wy then ft0 x else"; pr " fn%i %i wx wy" j (i - j - 1); done; pr " | %s%i wy => f%i wx wy" c i i; @@ -818,7 +819,7 @@ let _ = for i = 0 to size do pr " | %s%i wy =>" c i; if i == 0 then - pr " if w0_eq0 wy then ft0 x else"; + pr " if ZnZ.eq0 wy then ft0 x else"; if i == size then pr " fn%i n wx wy" size else @@ -834,21 +835,11 @@ let _ = pp " intros x; case x; clear x; unfold iter0."; for i = 0 to size do pp " intros x."; - if i == 0 then - begin - pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H."; - pp " intros y; rewrite H; apply Pf0t."; - pp " clear H."; - end; + if i == 0 then break_eq0 "x"; pp " intros y; case y; clear y."; for j = 0 to i - 1 do pp " intros y."; - if j == 0 then - begin - pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; - pp " rewrite H; apply Pft0."; - pp " clear H."; - end; + if j == 0 then break_eq0 "y"; pp " rewrite spec_eval%in%i; apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1); done; pp " intros y; apply Pf%i." i; @@ -863,12 +854,7 @@ let _ = pp " intros n x y; case y; clear y."; for i = 0 to size do pp " intros y."; - if i = 0 then - begin - pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; - pp " rewrite H; apply Pft0."; - pp " clear H."; - end; + if i = 0 then break_eq0 "y"; if i == size then pp " rewrite spec_eval%in; apply Pfn%i." size size else @@ -879,7 +865,7 @@ let _ = pp ""; - pr " End LevelAndIter."; + pr " End Iter."; pr ""; @@ -890,19 +876,19 @@ let _ = pr " (***************************************************************)"; pr ""; - pr " Definition reduce_0 (x:w) := %s0 x." c; + pr " Definition reduce_0 (x:w0) := %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; + pr " reduce_n1 _ _ zero (ZnZ.eq0 (Ops:=w0_op)) %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 (ZnZ.eq0 (Ops:=w%i_op)) 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)." + pr " reduce_n1 _ _ zero (ZnZ.eq0 (Ops:=w%i_op)) reduce_%i (%sn 0)." size size c; pr " Definition reduce_n n :="; @@ -924,13 +910,13 @@ let _ = pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x]." i i c i; pp " Proof."; pp " intros x; case x; unfold reduce_%i." i; - pp " exact (spec_0 w0_spec)."; + pp " exact ZnZ.spec_0."; pp " intros x1 y1."; - pp " generalize (spec_w%i_eq0 x1);" (i - 1); - pp " case w%i_eq0; intros H1; auto." (i - 1); + pp " generalize (ZnZ.spec_eq0 x1);"; + pp " case ZnZ.eq0; intros H1; auto."; 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; rewrite to_Z_%i." i; pp " unfold to_Z in H1; rewrite H1; auto."; pp " Qed."; pp ""; @@ -942,471 +928,132 @@ let _ = pp " intros x; rewrite <- spec_reduce_%i; auto." (size + 1); pp " intros n1 Hrec x; case x."; pp " unfold to_Z; rewrite make_op_S; auto."; - pp " exact (spec_0 w0_spec)."; + pp " exact ZnZ.spec_0."; pp " intros x1 y1; case x1; auto."; pp " rewrite Hrec."; pp " rewrite spec_extendn0_0; auto."; pp " Qed."; pp ""; +pr " Definition reduce n : dom_t n -> t :="; +pr " match n with"; +for i = 0 to size do +pr " | %i => reduce_%i" i i; + done; +pr " | SizePlus (S n) => reduce_n n"; +pr " end%%nat."; +pr ""; + +pr " Lemma spec_reduce : forall n (x:dom_t n), [reduce n x] = ZnZ.to_Z x."; +pa " Admitted"; +pp " Proof."; +for i = 0 to size do +pp " destruct n. apply spec_reduce_%i." i; +done; +pp " apply spec_reduce_n."; +pp " Qed."; +pr ""; + pr " (***************************************************************)"; pr " (* *)"; - pr " (** * Successor *)"; + pr " (** * Comparison *)"; pr " (* *)"; pr " (***************************************************************)"; pr ""; for i = 0 to size do - pr " Definition w%i_succ_c := w%i_op.(znz_succ_c)." i i + pr " Definition compare_%i := ZnZ.compare (Ops:=w%i_op)." i i; + 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 " Definition comparenm n m wx wy :="; + pr " let mn := Max.max n m in"; + pr " let d := diff n m in"; + pr " let op := make_op mn in"; + pr " ZnZ.compare"; + pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; + pr " (castm (diff_l n m) (extend_tr wy (fst d)))."; + pr ""; + + pr " Local Notation compare_folded :="; + pr " (iter _"; for i = 0 to size do - pr " Definition w%i_succ := w%i_op.(znz_succ)." i i + pr " compare_%i" i; + pr " (fun n x y => CompOpp (comparen_%i (S n) y x))" i; + pr " (fun n => comparen_%i (S n))" i; done; + pr " comparenm)."; + pr " Definition compare : t -> t -> comparison :="; + pr " Eval lazy beta delta [iter] in compare_folded."; pr ""; - pr " Definition succ x :="; - pr " match x with"; - 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 " | C1 r => %s%i (WW one%i r)" c (i+1) i; - pr " end"; + for i = 0 to size do + pp " Let spec_compare_%i: forall x y," i; + pp " compare_%i x y = Zcompare [%s%i x] [%s%i y]." i c i c i; + pp " Proof."; + pp " unfold compare_%i, to_Z; exact ZnZ.spec_compare." 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 " comparen_%i n x y = Zcompare (eval%in n x) [%s%i y]." i i c i; + pp " Proof."; + pp " intros n x y."; + pp " unfold comparen_%i, to_Z; rewrite spec_double_eval%in." i i; + pp " apply spec_compare_mn_1."; + pp " exact ZnZ.spec_0."; + pp " intros x1; exact (ZnZ.spec_compare %s x1)." (pz i); + pp " exact ZnZ.spec_to_Z."; + pp " exact ZnZ.spec_compare."; + pp " exact ZnZ.spec_compare."; + pp " exact ZnZ.spec_to_Z."; + pp " Qed."; + pp ""; 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 " | 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 " | C1 r => %sn (S n) (WW op.(znz_1) r)" c; - pr " end"; - pr " end."; - pr ""; - pr " Theorem spec_succ: forall n, [succ n] = [n] + 1."; + pr " Theorem spec_compare : forall x y,"; + pr " compare x y = Zcompare [x] [y]."; pa " Admitted."; pp " Proof."; - pp " intros n; case n; unfold succ, to_Z."; - for i = 0 to size do - pp " intros n1; generalize (spec_succ_c w%i_spec n1);" i; - pp " unfold succ, to_Z, w%i_succ_c; case znz_succ_c; auto." i; - 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 " intros x y. change compare with compare_folded. apply spec_iter; clear x y."; + for i = 0 to size - 1 do + pp " exact spec_compare_%i." i; + pp " intros n x y H; rewrite spec_comparen_%i; apply Zcompare_antisym." i; + pp " intros n x y H; exact (spec_comparen_%i (S n) x y)." i; done; - pp " intros k n1; generalize (spec_succ_c (wn_spec k) n1)."; - pp " unfold succ, to_Z; case znz_succ_c; auto."; - 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 " exact spec_compare_%i." size; + pp " intros n x y; rewrite spec_comparen_%i; apply Zcompare_antisym." size; + pp " intros n; exact (spec_comparen_%i (S n))." size; + pp " intros n m x y; unfold comparenm."; + pp " rewrite <- (spec_cast_l n m x); rewrite <- (spec_cast_r n m y)."; + pp " unfold to_Z; apply ZnZ.spec_compare."; pp " Qed."; pr ""; - pr " (***************************************************************)"; pr " (* *)"; - pr " (** * Adddition *)"; + pr " (** * Multiplication *)"; 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 x y :=" i; - pr " match w%i_add_c x y with" i; - pr " | C0 r => %s%i r" c i; - if i == size then - pr " | C1 r => %sn 0 (WW one%i r)" c size - else - pr " | C1 r => %s%i (WW one%i r)" c (i + 1) i; - pr " end."; - pr ""; - done ; - pr " Definition addn n (x y : word w%i (S n)) :=" size; - pr " let op := make_op n in"; - pr " match op.(znz_add_c) x y with"; - pr " | C0 r => %sn n r" c; - pr " | C1 r => %sn (S n) (WW op.(znz_1) r) end." c; + pr " Definition w%i_mul_add :=" i; + pr " Eval lazy beta delta [w_mul_add] in"; + pr " @w_mul_add w%i %s ZnZ.succ ZnZ.add_c ZnZ.mul_c." i (pz i) + done; pr ""; - for i = 0 to size do - 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; - 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 " 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 ""; + pr " Definition w%i_0W := ZnZ.OW (ops:=w%i_op)." i i 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 " 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."; + pr ""; - pr " Definition add := Eval lazy beta delta [same_level] in"; - pr0 " (same_level t_ "; for i = 0 to size do - pr0 "w%i_add " i; - done; - pr "addn)."; - pr ""; - - pr " Theorem spec_add: forall x y, [add x y] = [x] + [y]."; - pa " Admitted."; - pp " Proof."; - pp " unfold add."; - pp " generalize (spec_same_level t_ (fun x y res => [res] = x + y))."; - pp " unfold same_level; intros HH; apply HH; clear HH."; - for i = 0 to size do - pp " exact spec_w%i_add." i; - done; - pp " exact spec_wn_add."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Predecessor *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_pred_c := w%i_op.(znz_pred_c)." i i - done; - pr ""; - - pr " Definition pred x :="; - pr " match x with"; - 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 " | 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 " | C1 r => zero"; - pr " end"; - pr " end."; - pr ""; - - 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 " 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."; - pp " case (spec_to_Z w%i_spec x1); intros HH1 HH2." i; - pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4 HH5." i; - 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 " 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."; - pp " case (spec_to_Z (wn_spec n) x1); intros HH1 HH2."; - pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4 HH5."; - 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 " 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 " 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 " 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 " (** * Subtraction *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_sub_c := w%i_op.(znz_sub_c)." i i - done; - pr ""; - - 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; - pr " | C1 r => zero"; - pr " end." - done; - pr ""; - - pr " Definition subn n (x y : word w%i (S n)) :=" size; - pr " let op := make_op n in"; - pr " match op.(znz_sub_c) x y with"; - pr " | C0 r => %sn n r" c; - pr " | C1 r => N0 w_0"; - pr " end."; - pr ""; - - for i = 0 to size do - 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 " intros x; auto." - else - pp " intros x; try rewrite spec_reduce_%i; auto." i; - pp " unfold interp_carry; unfold zero, w_0, to_Z."; - pp " rewrite (spec_0 w0_spec)."; - pp " case (spec_to_Z w%i_spec x); intros; auto with zarith." i; - 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 " intros x; auto."; - pp " unfold interp_carry, to_Z."; - pp " case (spec_to_Z (wn_spec k) x); intros; auto with zarith."; - pp " Qed."; - pp ""; - - pr " Definition sub := Eval lazy beta delta [same_level] in"; - pr0 " (same_level t_ "; - for i = 0 to size do - pr0 "w%i_sub " i; - done; - pr "subn)."; - pr ""; - - pr " Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y]."; - pa " Admitted."; - pp " Proof."; - pp " unfold sub."; - pp " generalize (spec_same_level t_ (fun x y res => y <= x -> [res] = x - y))."; - pp " unfold same_level; intros HH; apply HH; clear HH."; - for i = 0 to size do - pp " exact spec_w%i_sub." i; - done; - pp " exact spec_wn_sub."; - pp " Qed."; - pr ""; - - for i = 0 to size do - 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 " 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."; - pp " Qed."; - pp ""; - done; - - 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 " 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."; - pp " Qed."; - pp ""; - - pr " Theorem spec_sub0: forall x y, [x] < [y] -> [sub x y] = 0."; - pa " Admitted."; - pp " Proof."; - pp " unfold sub."; - pp " generalize (spec_same_level t_ (fun x y res => x < y -> [res] = 0))."; - pp " unfold same_level; intros HH; apply HH; clear HH."; - for i = 0 to size do - pp " exact spec_w%i_sub0." i; - done; - pp " exact spec_wn_sub0."; - pp " Qed."; - pr ""; - - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Comparison *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition compare_%i := w%i_op.(znz_compare)." i i; - 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 " Definition comparenm n m wx wy :="; - pr " let mn := Max.max n m in"; - pr " let d := diff n m in"; - pr " let op := make_op mn in"; - pr " op.(znz_compare)"; - pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; - pr " (castm (diff_l n m) (extend_tr wy (fst d)))."; - pr ""; - - 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; - pr " (fun n => comparen_%i (S n))" i; - done; - pr " comparenm)."; - 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 " 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; - pp " end."; - pp " Proof."; - 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; - pp " | Eq => eval%in n x = [%s%i y]" i c i; - pp " | Lt => eval%in n x < [%s%i y]" i c i; - pp " | Gt => eval%in n x > [%s%i y]" i c i; - pp " end."; - pp " intros n x y."; - pp " unfold comparen_%i, to_Z; rewrite spec_double_eval%in." i i; - pp " apply spec_compare_mn_1."; - pp " exact (spec_0 w%i_spec)." i; - pp " intros x1; exact (spec_compare w%i_spec %s x1)." i (pz i); - pp " exact (spec_to_Z w%i_spec)." i; - pp " exact (spec_compare w%i_spec)." i; - pp " exact (spec_compare w%i_spec)." i; - pp " exact (spec_to_Z w%i_spec)." i; - pp " Qed."; - pp ""; - done; - - pp " Let spec_opp_compare: forall c (u v: Z),"; - pp " match c with Eq => u = v | Lt => u < v | Gt => u > v end ->"; - pp " match opp_compare c with Eq => v = u | Lt => v < u | Gt => v > u end."; - pp " Proof."; - pp " intros c u v; case c; unfold opp_compare; auto with zarith."; - pp " Qed."; - pp ""; - - - 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 " Eq => x = y"; - pp " | Lt => x < y"; - pp " | Gt => x > y"; - pp " end)"; - for i = 0 to size do - pp " compare_%i" i; - pp " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; - 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; - 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; - pp " intros n m x y; unfold comparenm."; - pp " rewrite <- (spec_cast_l n m x); rewrite <- (spec_cast_r n m y)."; - pp " unfold to_Z; apply (spec_compare (wn_spec (Max.max n m)))."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Multiplication *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_mul_c := w%i_op.(znz_mul_c)." i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_mul_add :=" i; - pr " Eval lazy beta delta [w_mul_add] in"; - pr " @w_mul_add w%i %s w%i_succ w%i_add_c w%i_mul_c." i (pz i) i i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_0W := znz_0W w%i_op." i i - done; - pr ""; - - for i = 0 to size do - pr " Definition w%i_WW := znz_WW w%i_op." i i + pr " Definition w%i_WW := ZnZ.WW (ops:=w%i_op)." i i done; pr ""; @@ -1428,7 +1075,7 @@ let _ = else pr " | %i%s => fun x => %s%i x" j "%nat" c (i + j + 1) done; - pr " | _ => fun _ => N0 w_0"; + pr " | _ => fun _ => zero"; pr " end."; pr ""; done; @@ -1436,7 +1083,7 @@ let _ = for i = 0 to size - 1 do pp "Theorem to_Z%i_spec:" i; - 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; + pp " forall n x, Z_of_nat n <= %i -> [to_Z%i n x] = ZnZ.to_Z (Ops:=nmake_op _ w%i_op (S n)) x." (size + 1 - i) i i; for j = 1 to size + 2 - i do pp " intros n; case n; clear n."; pp " unfold to_Z%i." i; @@ -1454,12 +1101,12 @@ let _ = pr " let (w,r) := w%i_mul_add_n1 (S n) x y %s in" i (pz i); if i == size then begin - pr " if w%i_eq0 w then %sn n r" i c; + pr " if ZnZ.eq0 w then %sn n r" c; pr " else %sn (S n) (WW (extend%i n w) r)." c i; end else begin - pr " if w%i_eq0 w then to_Z%i n r" i i; + pr " if ZnZ.eq0 w then to_Z%i n r" i; pr " else to_Z%i (S n) (WW (extend%i n w) r)." i i; end; pr ""; @@ -1469,84 +1116,87 @@ let _ = pr " let mn := Max.max n m in"; pr " let d := diff n m in"; pr " let op := make_op mn in"; - pr " reduce_n (S mn) (op.(znz_mul_c)"; + pr " reduce_n (S mn) (ZnZ.mul_c"; pr " (castm (diff_r n m) (extend_tr x (snd d)))"; pr " (castm (diff_l n m) (extend_tr y (fst d))))."; pr ""; - pr " Definition mul := Eval lazy beta delta [iter0] in"; + pr " Local Notation mul_folded :="; 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 (ZnZ.mul_c x y))" (i + 1); pr " (fun n x y => w%i_mul n y x)" i; pr " w%i_mul" i; done; pr " mulnm"; - pr " (fun _ => N0 w_0)"; - pr " (fun _ => N0 w_0)"; + pr " (fun _ => zero)"; + pr " (fun _ => zero)"; pr " )."; + pr " Definition mul : t -> t -> t :="; + pr " Eval lazy beta delta [iter0] in mul_folded."; pr ""; for i = 0 to size do pp " Let spec_w%i_mul_add: forall x y z," i; pp " let (q,r) := w%i_mul_add x y z in" i; - pp " znz_to_Z w%i_op q * (base (znz_digits w%i_op)) + znz_to_Z w%i_op r =" i i i; - 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 ; - pp " (spec_mul_add w%i_spec)." i; + pp " ZnZ.to_Z (Ops:=w%i_op) q * (base (ZnZ.digits w%i_op)) + ZnZ.to_Z (Ops:=w%i_op) r =" i i i; + pp " ZnZ.to_Z (Ops:=w%i_op) x * ZnZ.to_Z (Ops:=w%i_op) y + ZnZ.to_Z (Ops:=w%i_op) z :=" i i i ; + pp " spec_mul_add."; pp ""; done; for i = 0 to size do pp " Theorem spec_w%i_mul_add_n1: forall n x y z," i; pp " let (q,r) := w%i_mul_add_n1 n x y z in" i; - pp " znz_to_Z w%i_op q * (base (znz_digits (nmake_op _ w%i_op n))) +" i i; - pp " znz_to_Z (nmake_op _ w%i_op n) r =" i; - pp " znz_to_Z (nmake_op _ w%i_op n) x * znz_to_Z w%i_op y +" i i; - pp " znz_to_Z w%i_op z." i; + pp " ZnZ.to_Z (Ops:=w%i_op) q * (base (ZnZ.digits (nmake_op _ w%i_op n))) +" i i; + pp " ZnZ.to_Z (Ops:=nmake_op _ w%i_op n) r =" i; + pp " ZnZ.to_Z (Ops:=nmake_op _ w%i_op n) x * ZnZ.to_Z (Ops:=w%i_op) y +" i i; + pp " ZnZ.to_Z (Ops:=w%i_op) z." i; pp " Proof."; pp " intros n x y z; unfold w%i_mul_add_n1." i; pp " rewrite nmake_double."; pp " rewrite digits_doubled."; - pp " change (base (DoubleBase.double_digits (znz_digits w%i_op) n)) with" i; - pp " (DoubleBase.double_wB (znz_digits w%i_op) n)." i; + pp " change (base (DoubleBase.double_digits (ZnZ.digits w%i_op) n)) with" i; + pp " (DoubleBase.double_wB (ZnZ.digits w%i_op) n)." i; pp " apply spec_double_mul_add_n1; auto."; - if i == 0 then pp " exact (spec_0 w%i_spec)." i; - pp " exact (spec_WW w%i_spec)." i; - pp " exact (spec_0W w%i_spec)." i; - pp " exact (spec_mul_add w%i_spec)." i; + if i == 0 then pp " exact ZnZ.spec_0."; + pp " exact ZnZ.spec_WW."; + pp " exact ZnZ.spec_OW."; + pp " exact spec_mul_add."; 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)) +"; - pp " znz_to_Z (nmake_op ww ww1 n) y."; + pp " ZnZ.to_Z (Ops:=nmake_op ww ww1 (S n)) (WW x y) ="; + pp " ZnZ.to_Z (Ops:=nmake_op ww ww1 n) x * base (ZnZ.digits (nmake_op ww ww1 n)) +"; + pp " ZnZ.to_Z (Ops:=nmake_op ww ww1 n) y."; + pp " Proof."; 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 w%i_op x1." i; + pp " ZnZ.to_Z (Ops:=nmake_op _ w%i_op (S n)) (extend%i n x1) =" i i; + pp " ZnZ.to_Z (Ops:=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 - pp " intros l; simpl; unfold w_0; rewrite (spec_0 w0_spec); ring."; + pp " intros l; simpl; unfold zero; rewrite ZnZ.spec_0; 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; + pp " [%sn (S n) (ZnZ.mul_c (Ops:=make_op n) x y)] = [%sn n x] * [%sn n y]." c c c; pp " Proof."; pp " intros n x y; unfold to_Z."; - pp " rewrite <- (spec_mul_c (wn_spec n))."; + pp " rewrite <- ZnZ.spec_mul_c."; pp " rewrite make_op_S."; - pp " case znz_mul_c; auto."; + pp " case ZnZ.mul_c; auto."; pp " Qed."; pr ""; @@ -1565,15 +1215,15 @@ let _ = pp " intros n x y H; unfold w%i_mul." i; pp " generalize (spec_w%i_mul_add_n1 (S n) x y %s)." i (pz i); pp " case w%i_mul_add_n1; intros x1 y1." i; - pp " change (znz_to_Z (nmake_op _ w%i_op (S n)) x) with (eval%in (S n) x)." i i; - pp " change (znz_to_Z w%i_op y) with ([%s%i y])." i c i; + pp " change (ZnZ.to_Z x) with (eval%in (S n) x)." i; + pp " change (ZnZ.to_Z y) with ([%s%i y])." c i; if i == 0 then - pp " unfold w_0; rewrite (spec_0 w0_spec); rewrite Zplus_0_r." + pp " rewrite ZnZ.spec_0; rewrite Zplus_0_r." else - pp " change (znz_to_Z w%i_op W0) with 0; rewrite Zplus_0_r." i; + pp " change (ZnZ.to_Z W0) with 0; rewrite Zplus_0_r."; pp " intros H1; rewrite <- H1; clear H1."; - pp " generalize (spec_w%i_eq0 x1); case w%i_eq0; intros HH." i i; - pp " unfold to_Z in HH; rewrite HH."; + pp " generalize (ZnZ.spec_eq0 x1); case ZnZ.eq0; intros HH."; + pp " unfold to_Z in HH; rewrite HH by trivial."; if i == size then begin pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i; auto." i i i; @@ -1586,20 +1236,11 @@ let _ = end; pp " rewrite nmake_op_WW; rewrite extend%in_spec; auto." i; 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 n x y => w%i_mul n y x)" i; - pp " w%i_mul _ _ _" i; - done; - pp " mulnm _"; - pp " (fun _ => N0 w_0) _"; - pp " (fun _ => N0 w_0) _"; - pp " )."; + pp " intros x y. change mul with mul_folded. apply spec_iter0; clear x y."; for i = 0 to size do pp " intros x y; rewrite spec_reduce_%i." (i + 1); - pp " unfold w%i_mul_c, to_Z." i; - pp " generalize (spec_mul_c w%i_spec x y)." i; + pp " unfold to_Z."; + pp " generalize (ZnZ.spec_mul_c x y)."; pp " intros HH; rewrite <- HH; clear HH; auto."; if i == size then begin @@ -1617,87 +1258,11 @@ let _ = pp " rewrite <- (spec_cast_l n m x)."; pp " rewrite <- (spec_cast_r n m y)."; pp " rewrite spec_muln; rewrite spec_cast_l; rewrite spec_cast_r; auto."; - pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring."; - pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring."; + pp " intros x; simpl; rewrite ZnZ.spec_0; ring."; + pp " intros x; simpl; rewrite ZnZ.spec_0; ring."; pp " Qed."; pr ""; - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Square *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_square_c := w%i_op.(znz_square_c)." i i - done; - pr ""; - - pr " Definition square x :="; - pr " match x with"; - pr " | %s0 wx => reduce_1 (w0_square_c wx)" c; - for i = 1 to size - 1 do - pr " | %s%i wx => %s%i (w%i_square_c wx)" c i c (i+1) i - done; - pr " | %s%i wx => %sn 0 (w%i_square_c wx)" c size c size; - pr " | %sn n wx =>" c; - pr " let op := make_op n in"; - pr " %sn (S n) (op.(znz_square_c) wx)" c; - pr " end."; - pr ""; - - pr " Theorem spec_square: forall x, [square x] = [x] * [x]."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold square; clear x."; - pp " intros x; rewrite spec_reduce_1; unfold to_Z."; - pp " exact (spec_square_c w%i_spec x)." 0; - for i = 1 to size do - pp " intros x; unfold to_Z."; - pp " exact (spec_square_c w%i_spec x)." i; - done; - pp " intros n x; unfold to_Z."; - pp " rewrite make_op_S."; - pp " exact (spec_square_c (wn_spec n) x)."; - pp "Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Square root *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - for i = 0 to size do - pr " Definition w%i_sqrt := w%i_op.(znz_sqrt)." i i - done; - pr ""; - - pr " Definition sqrt x :="; - pr " match x with"; - for i = 0 to size do - pr " | %s%i wx => reduce_%i (w%i_sqrt wx)" c i i i; - done; - pr " | %sn n wx =>" c; - pr " let op := make_op n in"; - pr " reduce_n n (op.(znz_sqrt) wx)"; - pr " end."; - pr ""; - - pr " Theorem spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2."; - pa " Admitted."; - pp " Proof."; - pp " intros x; unfold sqrt; case x; clear x."; - for i = 0 to size do - pp " intros x; rewrite spec_reduce_%i; exact (spec_sqrt w%i_spec x)." i i; - done; - pp " intros n x; rewrite spec_reduce_n; exact (spec_sqrt (wn_spec n) x)."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; pr " (* *)"; pr " (** * Division *)"; @@ -1705,37 +1270,32 @@ let _ = 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 " Let spec_divn1 ww (ww_op: ZnZ.Ops ww) (ww_spec: ZnZ.Specs 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_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 " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; + pp " (ZnZ.zdigits ww_op) ZnZ.zero"; + pp " ZnZ.WW ZnZ.head0"; + pp " ZnZ.add_mul_div ZnZ.div21"; + pp " ZnZ.compare ZnZ.sub ZnZ.to_Z"; + pp " ZnZ.spec_to_Z"; + pp " ZnZ.spec_zdigits"; + pp " ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0"; + pp " ZnZ.spec_add_mul_div ZnZ.spec_div21"; + pp " ZnZ.spec_compare ZnZ.spec_sub)."; pp ""; for i = 0 to size do pr " Definition w%i_divn1 n x y :=" i; pr " let (u, v) :="; - pr " double_divn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; - pr " (znz_WW w%i_op) w%i_op.(znz_head0)" i i; - pr " w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i; - pr " w%i_op.(znz_compare) w%i_op.(znz_sub) (S n) x y in" i i; + pr " double_divn1 (ZnZ.zdigits w%i_op) ZnZ.zero" i; + pr " ZnZ.WW ZnZ.head0"; + pr " ZnZ.add_mul_div ZnZ.div21"; + pr " ZnZ.compare ZnZ.sub (S n) x y in"; if i == size then pr " (%sn _ u, %s%i v)." c c i else pr " (to_Z%i _ u, %s%i v)." i c i; + pr ""; done; - pr ""; for i = 0 to size do pp " Lemma spec_get_end%i: forall n x y," i; @@ -1745,17 +1305,17 @@ let _ = pp " intros n x y H."; pp " rewrite spec_double_eval%in; unfold to_Z." i; pp " apply DoubleBase.spec_get_low."; - pp " exact (spec_0 w%i_spec)." i; - pp " exact (spec_to_Z w%i_spec)." i; + pp " exact ZnZ.spec_0."; + pp " exact ZnZ.spec_to_Z."; pp " apply Zle_lt_trans with [%s%i y]; auto." c i; pp " rewrite <- spec_double_eval%in; auto." i; - pp " unfold to_Z; case (spec_to_Z w%i_spec y); auto." i; + pp " unfold to_Z; case (ZnZ.spec_to_Z y); auto."; pp " Qed."; pp ""; done; for i = 0 to size do - 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; + pr " Let div_gt%i (x y:w%i) := let (u,v) := ZnZ.div_gt x y in (reduce_%i u, reduce_%i v)." i i i i; done; pr ""; @@ -1764,13 +1324,13 @@ let _ = pr " let mn := Max.max n m in"; pr " let d := diff n m in"; pr " let op := make_op mn in"; - pr " let (q, r):= op.(znz_div_gt)"; + pr " let (q, r):= ZnZ.div_gt"; pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; pr " (castm (diff_l n m) (extend_tr wy (fst d))) in"; pr " (reduce_n mn q, reduce_n mn r)."; pr ""; - pr " Definition div_gt := Eval lazy beta delta [iter] in"; + pr " Local Notation div_gt_folded :="; pr " (iter _"; for i = 0 to size do pr " div_gt%i" i; @@ -1778,6 +1338,7 @@ let _ = pr " w%i_divn1" i; done; pr " div_gtnm)."; + pr " Definition div_gt := Eval lazy beta delta [iter] in div_gt_folded."; pr ""; pr " Theorem spec_div_gt: forall x y,"; @@ -1790,44 +1351,29 @@ 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 " let (q,r) := res in"; - pp " x = [q] * y + [r] /\\ 0 <= [r] < y)"; + pp " intros x y. change div_gt with div_gt_folded. apply spec_iter; clear x y."; 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; - done; - pp " div_gtnm _)."; - for i = 0 to size do - pp " intros x y H1 H2; unfold div_gt%i, w%i_div_gt." i i; - pp " generalize (spec_div_gt w%i_spec x y H1 H2); case znz_div_gt." i; + pp " (* %i *)" i; + pp " intros x y H1 H2; unfold div_gt%i." i; + pp " generalize (ZnZ.spec_div_gt x y H1 H2); case ZnZ.div_gt."; pp " intros xx yy; repeat rewrite spec_reduce_%i; auto." i; if i == size then - pp " intros n x y H2 H3; unfold div_gt%i, w%i_div_gt." i i + pp " intros n x y H2 H3; unfold 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 " intros n x y H1 H2 H3; unfold div_gt%i." i; + pp " generalize (ZnZ.spec_div_gt x"; pp " (DoubleBase.get_low %s (S n) y))." (pz i); - pp0 ""; - for j = 0 to i do - pp0 "unfold w%i; " (i-j); - done; - pp "case znz_div_gt."; + pp " case ZnZ.div_gt."; pp " intros xx yy H4; repeat rewrite spec_reduce_%i." i; pp " generalize (spec_get_end%i (S n) y x); unfold to_Z; intros H5." i; pp " unfold to_Z in H2; rewrite H5 in H4; auto with zarith."; if i == size then - pp " intros n x y H2 H3." + pp " intros n x y H2 H3." else - pp " intros n x y H1 H2 H3."; + pp " intros n x y H1 H2 H3."; pp " generalize"; 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); - done; - pp "case double_divn1."; + pp " unfold w%i_divn1; case double_divn1." i; pp " intros xx yy H4."; if i == size then begin @@ -1840,13 +1386,13 @@ let _ = pp " repeat rewrite <- spec_double_eval%in in H4; auto." i; end; done; - pp " intros n m x y H1 H2; unfold div_gtnm."; - pp " generalize (spec_div_gt (wn_spec (Max.max n m))"; + pp " intros n m x y H1 H2; unfold div_gtnm."; + pp " generalize (ZnZ.spec_div_gt"; pp " (castm (diff_r n m)"; pp " (extend_tr x (snd (diff n m))))"; pp " (castm (diff_l n m)"; pp " (extend_tr y (fst (diff n m)))))."; - pp " case znz_div_gt."; + pp " case ZnZ.div_gt."; pp " intros xx yy HH."; pp " repeat rewrite spec_reduce_n."; pp " rewrite <- (spec_cast_l n m x)."; @@ -1871,16 +1417,11 @@ let _ = pr " (***************************************************************)"; pr ""; - for i = 0 to size do - pr " Definition w%i_mod_gt := w%i_op.(znz_mod_gt)." i i - done; - pr ""; - for i = 0 to size do pr " Definition w%i_modn1 :=" i; - pr " double_modn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; - pr " w%i_op.(znz_head0) w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i i; - pr " w%i_op.(znz_compare) w%i_op.(znz_sub)." i i; + pr " double_modn1 (ZnZ.zdigits w%i_op) (ZnZ.zero (Ops:=w%i_op))" i i; + pr " ZnZ.head0 ZnZ.add_mul_div ZnZ.div21"; + pr " ZnZ.compare ZnZ.sub."; done; pr ""; @@ -1888,56 +1429,49 @@ let _ = pr " let mn := Max.max n m in"; pr " let d := diff n m in"; pr " let op := make_op mn in"; - pr " reduce_n mn (op.(znz_mod_gt)"; + pr " reduce_n mn (ZnZ.modulo_gt"; pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; pr " (castm (diff_l n m) (extend_tr wy (fst d))))."; pr ""; - pr " Definition mod_gt := Eval lazy beta delta[iter] in"; + pr " Local Notation mod_gt_folded :="; 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); + pr " (fun x y => reduce_%i (ZnZ.modulo_gt x y))" i; + pr " (fun n x y => reduce_%i (ZnZ.modulo_gt x (DoubleBase.get_low %s (S n) y)))" i (pz i); pr " (fun n x y => reduce_%i (w%i_modn1 (S n) x y))" i i; done; 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 " 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_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 " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; + pr " Definition mod_gt := Eval lazy beta delta[iter] in mod_gt_folded."; + pr ""; + + pp " Let spec_modn1 ww (ww_op: ZnZ.Ops ww) (ww_spec: ZnZ.Specs ww_op) :="; + pp " spec_double_modn1"; + pp " (ZnZ.zdigits ww_op) ZnZ.zero"; + pp " ZnZ.WW ZnZ.head0"; + pp " ZnZ.add_mul_div ZnZ.div21"; + pp " ZnZ.compare ZnZ.sub ZnZ.to_Z"; + pp " ZnZ.spec_to_Z"; + pp " ZnZ.spec_zdigits"; + pp " ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0"; + pp " ZnZ.spec_add_mul_div ZnZ.spec_div21"; + pp " ZnZ.spec_compare ZnZ.spec_sub."; pp ""; pr " Theorem spec_mod_gt:"; pr " forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y]."; pa " Admitted."; pp " Proof."; - pp " refine (spec_iter _ (fun x y res => x > y -> 0 < y ->"; - pp " [res] = x mod y)"; - for i = 0 to size do - pp " (fun x y => reduce_%i (w%i_mod_gt x y))" i i; - pp " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i); - pp " (fun n x y => reduce_%i (w%i_modn1 (S n) x y)) _ _ _" i i; - done; - pp " mod_gtnm _)."; + pp " intros x y. change mod_gt with mod_gt_folded. apply spec_iter; clear x y."; for i = 0 to size do pp " intros x y H1 H2; rewrite spec_reduce_%i." i; - pp " exact (spec_mod_gt w%i_spec x y H1 H2)." i; + pp " exact (ZnZ.spec_modulo_gt x y H1 H2)."; if i == size then pp " intros n x y H2 H3; rewrite spec_reduce_%i." i else pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i; - pp " unfold w%i_mod_gt." i; pp " rewrite <- (spec_get_end%i (S n) y x); auto with zarith." i; - pp " unfold to_Z; apply (spec_mod_gt w%i_spec); auto." i; + pp " unfold to_Z; apply ZnZ.spec_modulo_gt; auto."; pp " rewrite <- (spec_get_end%i (S n) y x) in H2; auto with zarith." i; pp " rewrite <- (spec_get_end%i (S n) y x) in H3; auto with zarith." i; if i == size then @@ -1951,399 +1485,15 @@ let _ = pp " repeat rewrite spec_reduce_n."; pp " rewrite <- (spec_cast_l n m x)."; pp " rewrite <- (spec_cast_r n m y)."; - pp " unfold to_Z; apply (spec_mod_gt (wn_spec (Max.max n m)))."; + pp " unfold to_Z; apply ZnZ.spec_modulo_gt."; pp " rewrite <- (spec_cast_l n m x) in H1; auto."; pp " rewrite <- (spec_cast_r n m y) in H1; auto."; pp " rewrite <- (spec_cast_r n m y) in H2; auto."; pp " Qed."; pr ""; - pr " (** digits: a measure for gcd *)"; - pr ""; - - pr " Definition digits x :="; - pr " match x with"; - for i = 0 to size do - pr " | %s%i _ => w%i_op.(znz_digits)" c i i; - done; - pr " | %sn n _ => (make_op n).(znz_digits)" c; - pr " end."; - pr ""; - - pr " Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; clear x."; - for i = 0 to size do - pp " intros x; unfold to_Z, digits;"; - pp " generalize (spec_to_Z w%i_spec x); unfold base; intros H; exact H." i; - done; - pp " intros n x; unfold to_Z, digits;"; - pp " generalize (spec_to_Z (wn_spec n) x); unfold base; intros H; exact H."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Conversion *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - 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 " Zpos p < 2 ^ (Zpos (znz_digits w0_op) * 2 ^ (Z_of_nat (pheight p)))."; - pr " Proof."; - pr " intros p; unfold pheight."; - pr " assert (F1: forall x, Z_of_nat (Peano.pred (nat_of_P x)) = Zpos x - 1)."; - pr " intros x."; - pr " assert (Zsucc (Z_of_nat (Peano.pred (nat_of_P x))) = Zpos x); auto with zarith."; - pr " rewrite <- inj_S."; - pr " rewrite <- (fun x => S_pred x 0); auto with zarith."; - pr " rewrite Zpos_eq_Z_of_nat_o_nat_of_P; auto."; - pr " apply lt_le_trans with 1%snat; auto with zarith." "%"; - pr " exact (le_Pmult_nat x 1)."; - pr " rewrite F1; clear F1."; - pr " assert (F2:= (get_height_correct (znz_digits w0_op) (plength p)))."; - pr " apply Zlt_le_trans with (Zpos (Psucc p))."; - pr " rewrite Zpos_succ_morphism; auto with zarith."; - pr " apply Zle_trans with (1 := plength_pred_correct (Psucc p))."; - pr " rewrite Ppred_succ."; - pr " apply Zpower_le_monotone; auto with zarith."; - pr " Qed."; - pr ""; - - pr " Definition of_pos x :="; - pr " let h := pheight x in"; - pr " match h with"; - for i = 0 to size do - pr " | %i%snat => reduce_%i (snd (w%i_op.(znz_of_pos) x))" i "%" i i; - done; - pr " | _ =>"; - pr " let n := minus h %i in" (size + 1); - pr " reduce_n n (snd ((make_op n).(znz_of_pos) x))"; - pr " end."; - pr ""; - - pr " Theorem spec_of_pos: forall x,"; - pr " [of_pos x] = Zpos x."; - pa " Admitted."; - pp " Proof."; - pp " assert (F := spec_more_than_1_digit w0_spec)."; - pp " intros x; unfold of_pos; case_eq (pheight x)."; - for i = 0 to size do - if i <> 0 then - pp " intros n; case n; clear n."; - pp " intros H1; rewrite spec_reduce_%i; unfold to_Z." i; - pp " apply (znz_of_pos_correct w%i_spec)." i; - pp " apply Zlt_le_trans with (1 := pheight_correct x)."; - pp " rewrite H1; simpl Z_of_nat; change (2^%i) with (%s)." i (gen2 i); - pp " unfold base."; - pp " apply Zpower_le_monotone; split; auto with zarith."; - if i <> 0 then - begin - pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc."; - pp " repeat rewrite <- Zpos_xO."; - pp " refine (Zle_refl _)."; - end; - done; - pp " intros n."; - pp " intros H1; rewrite spec_reduce_n; unfold to_Z."; - pp " simpl minus; rewrite <- minus_n_O."; - pp " apply (znz_of_pos_correct (wn_spec n))."; - pp " apply Zlt_le_trans with (1 := pheight_correct x)."; - pp " unfold base."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " split; auto with zarith."; - pp " rewrite H1."; - pp " elim n; clear n H1."; - pp " simpl Z_of_nat; change (2^%i) with (%s)." (size + 1) (gen2 (size + 1)); - pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc."; - pp " repeat rewrite <- Zpos_xO."; - pp " refine (Zle_refl _)."; - pp " intros n Hrec."; - pp " rewrite make_op_S."; - pp " change (@znz_digits (word _ (S (S n))) (mk_zn2z_op_karatsuba (make_op n))) with"; - pp " (xO (znz_digits (make_op n)))."; - pp " rewrite (fun x y => (Zpos_xO (@znz_digits x y)))."; - pp " rewrite inj_S; unfold Zsucc."; - pp " rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith."; - pp " rewrite Zpower_1_r."; - pp " assert (tmp: forall x y z, x * (y * z) = y * (x * z));"; - pp " [intros; ring | rewrite tmp; clear tmp]."; - pp " apply Zmult_le_compat_l; auto with zarith."; - pp " Qed."; - pr ""; - - pr " (***************************************************************)"; - pr " (* *)"; - pr " (** * Shift *)"; - pr " (* *)"; - pr " (***************************************************************)"; - pr ""; - - (* Head0 *) - pr " Definition head0 w := match w with"; - for i = 0 to size do - pr " | %s%i w=> reduce_%i (w%i_op.(znz_head0) w)" c i i i; - done; - pr " | %sn n w=> reduce_n n ((make_op n).(znz_head0) w)" c; - pr " end."; - pr ""; - - pr " Theorem spec_head00: forall x, [x] = 0 ->[head0 x] = Zpos (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold head0; clear x."; - for i = 0 to size do - pp " intros x; rewrite spec_reduce_%i; exact (spec_head00 w%i_spec x)." i i; - done; - pp " intros n x; rewrite spec_reduce_n; exact (spec_head00 (wn_spec n) x)."; - pp " Qed."; - 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 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 " 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."; - done; - pp " intros n x Hx; rewrite spec_reduce_n."; - 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 " 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."; - pp " Qed."; - pr ""; - - - (* Tail0 *) - pr " Definition tail0 w := match w with"; - for i = 0 to size do - pr " | %s%i w=> reduce_%i (w%i_op.(znz_tail0) w)" c i i i; - done; - pr " | %sn n w=> reduce_n n ((make_op n).(znz_tail0) w)" c; - pr " end."; - pr ""; - - - pr " Theorem spec_tail00: forall x, [x] = 0 ->[tail0 x] = Zpos (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold tail0; clear x."; - for i = 0 to size do - pp " intros x; rewrite spec_reduce_%i; exact (spec_tail00 w%i_spec x)." i i; - done; - pp " intros n x; rewrite spec_reduce_n; exact (spec_tail00 (wn_spec n) x)."; - pp " Qed."; - pr ""; - - - pr " Theorem spec_tail0: forall x,"; - pr " 0 < [x] -> exists y, 0 <= y /\\ [x] = (2 * y + 1) * 2 ^ [tail0 x]."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; clear x; unfold tail0."; - for i = 0 to size do - pp " intros x Hx; rewrite spec_reduce_%i; exact (spec_tail0 w%i_spec x Hx)." i i; - done; - pp " intros n x Hx; rewrite spec_reduce_n; exact (spec_tail0 (wn_spec n) x Hx)."; - pp " Qed."; - pr ""; - - - (* Number of digits *) - pr " Definition %sdigits x :=" c; - pr " match x with"; - pr " | %s0 _ => %s0 w0_op.(znz_zdigits)" c c; - 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; - pr " end."; - pr ""; - - pr " Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; clear x; unfold Ndigits, digits."; - for i = 0 to size do - pp " intros _; try rewrite spec_reduce_%i; exact (spec_zdigits w%i_spec)." i i; - done; - pp " intros n _; try rewrite spec_reduce_n; exact (spec_zdigits (wn_spec n))."; - pp " Qed."; - pr ""; - - - (* Shiftr *) - for i = 0 to size do - 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 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 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 (unsafe_shiftr%i n x))" i i; - done; - pr " (fun n p x => reduce_n n (unsafe_shiftrn n p x))."; - pr ""; - - - 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)."; - pp " intros; ring."; - pp " assert (F2: forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z)."; - pp " intros x y z HH HH1 HH2."; - pp " split; auto with zarith."; - pp " apply Zle_lt_trans with (2 := HH2); auto with zarith."; - pp " apply Zdiv_le_upper_bound; auto with zarith."; - pp " pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith."; - pp " apply Zmult_le_compat_l; auto."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " rewrite Zpower_0_r; ring."; - pp " assert (F3: forall x y, 0 <= y -> y <= x -> 0 <= x - y < 2 ^ x)."; - pp " intros xx y HH HH1."; - 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 " (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) ->"; - pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->"; - pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->"; - pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->"; - pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->"; - pp " znz_to_Z ww_op"; - pp " (znz_add_mul_div ww_op (znz_sub ww_op (znz_zdigits ww_op) yy1)"; - pp " (znz_0 ww_op) xx1) = znz_to_Z ww1_op xx / 2 ^ znz_to_Z ww2_op yy)."; - pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy."; - pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2."; - pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4."; - pp " rewrite <- Hx."; - 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 " yy1)"; - pp " )."; - pp " rewrite (spec_0 Hw)."; - pp " rewrite Zmult_0_l; rewrite Zplus_0_l."; - pp " rewrite (CyclicAxioms.spec_sub Hw)."; - pp " rewrite Zmod_small; auto with zarith."; - pp " rewrite (spec_zdigits Hw)."; - pp " rewrite F0."; - pp " rewrite Zmod_small; auto with zarith."; - pp " unfold base; rewrite (spec_zdigits Hw) in Hl1 |- *;"; - pp " auto with zarith."; - pp " assert (F5: forall n m, (n <= m)%snat ->" "%"; - pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m)))."; - pp " intros n m HH; elim HH; clear m HH; auto with zarith."; - pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec)."; - pp " rewrite make_op_S."; - pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end."; - pp " rewrite Zpos_xO."; - pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith."; - pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size; - pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0)))."; - pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size; - 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 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 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; - pp " rewrite (spec_zdigits w%i_spec)." j; - pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)")); - pp " repeat rewrite (fun x => Zpos_xO (xO x))."; - pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; - 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 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 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 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 - begin - 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; - pp " rewrite <- (spec_extend%in m); rewrite <- spec_extend%in%i; auto." size i size; - end - done; - pp " intros n x y; case y; clear y;"; - 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; - pp " rewrite (spec_zdigits w%i_spec)." i; - pp " rewrite (spec_zdigits (wn_spec n))."; - pp " apply Zle_trans with (2 := F6 n)."; - pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)")); - pp " repeat rewrite (fun x => Zpos_xO (xO x))."; - pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; - pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i; - if i == size then - pp " change ([Nn n (extend%i n y)] = [N%i y])." size i - else - pp " change ([Nn n (extend%i n (extend%i %i y))] = [N%i y])." size i (size - i - 1) i; - pp " rewrite <- (spec_extend%in n); auto." size; - if i <> size then - pp " try (rewrite <- spec_extend%in%i; auto)." i size; - done; - pp " generalize y; clear y; intros m y."; - pp " rewrite spec_reduce_n; unfold to_Z; intros H1."; - pp " apply F4 with (3:=(wn_spec (Max.max n m)))(4:=wn_spec m)(5:=wn_spec n); auto with zarith."; - pp " rewrite (spec_zdigits (wn_spec m))."; - pp " rewrite (spec_zdigits (wn_spec (Max.max n m)))."; - pp " apply F5; auto with arith."; - pp " exact (spec_cast_r n m y)."; - pp " exact (spec_cast_l n m x)."; - pp " Qed."; - pr ""; +(* (* Unsafe_Shiftl *) for i = 0 to size do pr " Definition unsafe_shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i @@ -2380,35 +1530,35 @@ let _ = 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 " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)"; + pp " (ww_op: ZnZ.Ops ww) (ww1_op: ZnZ.Ops ww1) (ww2_op: ZnZ.Ops ww2)"; pp " xx yy xx1 yy1,"; - pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_head0 ww1_op xx) ->"; - pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->"; + pp " ZnZ.to_Z ww2_op yy <= ZnZ.to_Z ww1_op (znz_head0 ww1_op xx) ->"; + pp " ZnZ.to_Z ww1_op (ZnZ.zdigits ww1_op) <= ZnZ.to_Z ww_op (ZnZ.zdigits ww_op) ->"; pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->"; - pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->"; - pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->"; - pp " znz_to_Z ww_op"; + pp " ZnZ.to_Z ww_op xx1 = ZnZ.to_Z ww1_op xx ->"; + pp " ZnZ.to_Z ww_op yy1 = ZnZ.to_Z ww2_op yy ->"; + pp " ZnZ.to_Z ww_op"; pp " (znz_add_mul_div ww_op yy1"; - pp " xx1 (znz_0 ww_op)) = znz_to_Z ww1_op xx * 2 ^ znz_to_Z ww2_op yy)."; + pp " xx1 (znz_0 ww_op)) = ZnZ.to_Z ww1_op xx * 2 ^ ZnZ.to_Z ww2_op yy)."; pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy."; pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2."; pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4."; pp " rewrite <- Hx."; pp " rewrite <- Hy."; pp " generalize (spec_add_mul_div Hw xx1 (znz_0 ww_op) yy1)."; - pp " rewrite (spec_0 Hw)."; - pp " assert (F1: znz_to_Z ww1_op (znz_head0 ww1_op xx) <= Zpos (znz_digits ww1_op))."; + pp " rewrite ZnZ.spec_0."; + pp " assert (F1: ZnZ.to_Z ww1_op (znz_head0 ww1_op xx) <= Zpos (ZnZ.digits ww1_op))."; pp " case (Zle_lt_or_eq _ _ HH1); intros HH5."; pp " apply Zlt_le_weak."; pp " case (CyclicAxioms.spec_head0 Hw1 xx)."; pp " rewrite <- Hx; auto."; pp " intros _ Hu; unfold base in Hu."; - pp " case (Zle_or_lt (Zpos (znz_digits ww1_op))"; - pp " (znz_to_Z ww1_op (znz_head0 ww1_op xx))); auto; intros H1."; - pp " absurd (2 ^ (Zpos (znz_digits ww1_op)) <= 2 ^ (znz_to_Z ww1_op (znz_head0 ww1_op xx)))."; + pp " case (Zle_or_lt (Zpos (ZnZ.digits ww1_op))"; + pp " (ZnZ.to_Z ww1_op (znz_head0 ww1_op xx))); auto; intros H1."; + pp " absurd (2 ^ (Zpos (ZnZ.digits ww1_op)) <= 2 ^ (ZnZ.to_Z ww1_op (znz_head0 ww1_op xx)))."; pp " apply Zlt_not_le."; pp " case (spec_to_Z Hw1 xx); intros HHx3 HHx4."; - pp " rewrite <- (Zmult_1_r (2 ^ znz_to_Z ww1_op (znz_head0 ww1_op xx)))."; + pp " rewrite <- (Zmult_1_r (2 ^ ZnZ.to_Z ww1_op (znz_head0 ww1_op xx)))."; pp " apply Zle_lt_trans with (2 := Hu)."; pp " apply Zmult_le_compat_l; auto with zarith."; pp " apply Zpower_le_monotone; auto with zarith."; @@ -2423,7 +1573,7 @@ let _ = pp " apply Zle_trans with (2 := Hl1); auto."; pp " rewrite (spec_zdigits Hw1); auto with zarith."; pp " split; auto with zarith ."; - pp " apply Zlt_le_trans with (base (znz_digits ww1_op))."; + pp " apply Zlt_le_trans with (base (ZnZ.digits ww1_op))."; pp " rewrite Hx."; pp " case (CyclicAxioms.spec_head0 Hw1 xx); auto."; pp " rewrite <- Hx; auto."; @@ -2444,18 +1594,18 @@ let _ = pp " rewrite <- (spec_zdigits Hw); auto with zarith."; pp " rewrite <- (spec_zdigits Hw1); auto with zarith."; pp " assert (F5: forall n m, (n <= m)%snat ->" "%"; - pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m)))."; + pp " Zpos (ZnZ.digits (make_op n)) <= Zpos (ZnZ.digits (make_op m)))."; pp " intros n m HH; elim HH; clear m HH; auto with zarith."; pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec)."; pp " rewrite make_op_S."; pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end."; pp " rewrite Zpos_xO."; - pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith."; - pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size; - pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0)))."; - pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size; + pp " assert (0 <= Zpos (ZnZ.digits (make_op n))); auto with zarith."; + pp " assert (F6: forall n, Zpos (ZnZ.digits w%i_op) <= Zpos (ZnZ.digits (make_op n)))." size; + pp " intros n ; apply Zle_trans with (Zpos (ZnZ.digits (make_op 0)))."; + pp " change (ZnZ.digits (make_op 0)) with (xO (ZnZ.digits w%i_op))." size; pp " rewrite Zpos_xO."; - pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size; + 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 unsafe_shiftl, same_level."; for i = 0 to size do @@ -2466,10 +1616,10 @@ let _ = 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; pp " rewrite (spec_zdigits w%i_spec)." j; - pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)")); + pp " change (ZnZ.digits w%i_op) with %s." i (genxO (i - j) (" (ZnZ.digits w"^(string_of_int j)^"_op)")); pp " repeat rewrite (fun x => Zpos_xO (xO x))."; - pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; - pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j; + pp " repeat rewrite (fun x y => Zpos_xO (@ZnZ.digits x y))."; + 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 unsafe_shiftl%i, head0." i; @@ -2505,10 +1655,10 @@ let _ = pp " rewrite (spec_zdigits w%i_spec)." i; pp " rewrite (spec_zdigits (wn_spec n))."; pp " apply Zle_trans with (2 := F6 n)."; - pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)")); + pp " change (ZnZ.digits w%i_op) with %s." size (genxO (size - i) ("(ZnZ.digits w" ^ (string_of_int i) ^ "_op)")); pp " repeat rewrite (fun x => Zpos_xO (xO x))."; - pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; - pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i; + pp " repeat rewrite (fun x y => Zpos_xO (@ZnZ.digits x y))."; + pp " assert (H: 0 <= Zpos (ZnZ.digits w%i_op)); auto with zarith." i; if i == size then pp " change ([Nn n (extend%i n y)] = [N%i y])." size i else @@ -2527,147 +1677,7 @@ let _ = pp " exact (spec_cast_l n m x)."; pp " Qed."; pr ""; - - (* Double size *) - pr " Definition double_size w := match w with"; - for i = 0 to size-1 do - pr " | %s%i x => %s%i (WW (znz_0 w%i_op) x)" c i c (i + 1) i; - done; - pr " | %s%i x => %sn 0 (WW (znz_0 w%i_op) x)" c size c size; - pr " | %sn n x => %sn (S n) (WW (znz_0 (make_op n)) x)" c c; - pr " end."; - pr ""; - - pr " Theorem spec_double_size_digits:"; - pr " forall x, digits (double_size x) = xO (digits x)."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold double_size, digits; clear x; auto."; - pp " intros n x; rewrite make_op_S; auto."; - pp " Qed."; - pr ""; - - - pr " Theorem spec_double_size: forall x, [double_size x] = [x]."; - pa " Admitted."; - 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 " 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;"; - pp " generalize (znz_to_Z_n n); simpl word."; - pp " intros HH; rewrite HH; clear HH."; - pp " generalize (spec_0 (wn_spec n)); simpl word."; - pp " intros HH; rewrite HH; clear HH; auto with zarith."; - pp " Qed."; - pr ""; - - - pr " Theorem spec_double_size_head0:"; - pr " forall x, 2 * [head0 x] <= [head0 (double_size x)]."; - pa " Admitted."; - pp " Proof."; - pp " intros x."; - pp " assert (F1:= spec_pos (head0 x))."; - pp " assert (F2: 0 < Zpos (digits x))."; - pp " red; auto."; - pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH."; - pp " generalize HH; rewrite <- (spec_double_size x); intros HH1."; - pp " case (spec_head0 x HH); intros _ HH2."; - pp " case (spec_head0 _ HH1)."; - pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x)."; - pp " intros HH3 _."; - pp " case (Zle_or_lt ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4."; - pp " absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto."; - pp " apply Zle_not_lt."; - pp " apply Zmult_le_compat_r; auto with zarith."; - pp " apply Zpower_le_monotone; auto; auto with zarith."; - pp " generalize (spec_pos (head0 (double_size x))); auto with zarith."; - pp " assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1))."; - pp " case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5."; - pp " apply Zmult_le_reg_r with (2 ^ 1); auto with zarith."; - pp " rewrite <- (fun x y z => Zpower_exp x (y - z)); auto with zarith."; - pp " assert (tmp: forall x, x - 1 + 1 = x); [intros; ring | rewrite tmp; clear tmp]."; - pp " apply Zle_trans with (2 := Zlt_le_weak _ _ HH2)."; - 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 " 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."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " rewrite (Zmult_comm 2)."; - pp " rewrite Zpower_mult; auto with zarith."; - pp " rewrite Zpower_2."; - pp " apply Zlt_le_trans with (2 := HH3)."; - pp " rewrite <- Zmult_assoc."; - pp " replace (Zpos (xO (digits x)) - 1) with"; - pp " ((Zpos (digits x) - 1) + (Zpos (digits x)))."; - pp " rewrite Zpower_exp; auto with zarith."; - pp " apply Zmult_lt_compat2; auto with zarith."; - pp " split; auto with zarith."; - pp " apply Zmult_lt_0_compat; auto with zarith."; - pp " rewrite Zpos_xO; ring."; - pp " apply Zlt_le_weak; auto."; - pp " repeat rewrite spec_head00; auto."; - pp " rewrite spec_double_size_digits."; - pp " rewrite Zpos_xO; auto with zarith."; - pp " rewrite spec_double_size; auto."; - pp " Qed."; - pr ""; - - pr " Theorem spec_double_size_head0_pos:"; - pr " forall x, 0 < [head0 (double_size x)]."; - pa " Admitted."; - pp " Proof."; - pp " intros x."; - pp " assert (F: 0 < Zpos (digits x))."; - pp " red; auto."; - pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0."; - pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1."; - pp " apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith."; - pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3."; - pp " generalize F3; rewrite <- (spec_double_size x); intros F4."; - pp " absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x)))."; - pp " apply Zle_not_lt."; - pp " apply Zpower_le_monotone; auto with zarith."; - pp " split; auto with zarith."; - pp " rewrite Zpos_xO; auto with zarith."; - pp " case (spec_head0 x F3)."; - pp " rewrite <- F1; rewrite Zpower_0_r; rewrite Zmult_1_l; intros _ HH."; - pp " apply Zle_lt_trans with (2 := HH)."; - pp " case (spec_head0 _ F4)."; - pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x)."; - pp " rewrite <- F0; rewrite Zpower_0_r; rewrite Zmult_1_l; auto."; - pp " generalize F1; rewrite (spec_head00 _ (sym_equal F3)); auto with zarith."; - pp " Qed."; - pr ""; - - (* even *) - pr " Definition is_even x :="; - pr " match x with"; - for i = 0 to size do - pr " | %s%i wx => w%i_op.(znz_is_even) wx" c i i - done; - pr " | %sn n wx => (make_op n).(znz_is_even) wx" c; - pr " end."; - pr ""; - - - pr " Theorem spec_is_even: forall x,"; - pr " if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1."; - pa " Admitted."; - pp " Proof."; - pp " intros x; case x; unfold is_even, to_Z; clear x."; - for i = 0 to size do - pp " intros x; exact (spec_is_even w%i_spec x)." i; - done; - pp " intros n x; exact (spec_is_even (wn_spec n) x)."; - pp " Qed."; - pr ""; +*) pr "End Make."; pr ""; diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index d42db97d5..e6e4130b3 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -260,13 +260,6 @@ Section ReduceRec. End ReduceRec. -Definition opp_compare cmp := - match cmp with - | Lt => Gt - | Eq => Eq - | Gt => Lt - end. - Section CompareRec. Variable wm w : Type. @@ -294,11 +287,7 @@ Section CompareRec. Variable w_to_Z: w -> Z. Variable w_to_Z_0: w_to_Z w_0 = 0. Variable spec_compare0_m: forall x, - match compare0_m x with - Eq => w_to_Z w_0 = wm_to_Z x - | Lt => w_to_Z w_0 < wm_to_Z x - | Gt => w_to_Z w_0 > wm_to_Z x - end. + compare0_m x = (w_to_Z w_0 ?= wm_to_Z x). Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base. Let double_to_Z := double_to_Z wm_base wm_to_Z. @@ -315,29 +304,25 @@ Section CompareRec. Lemma spec_compare0_mn: forall n x, - match compare0_mn n x with - Eq => 0 = double_to_Z n x - | Lt => 0 < double_to_Z n x - | Gt => 0 > double_to_Z n x - end. - Proof. + compare0_mn n x = (0 ?= double_to_Z n x). + Proof. intros n; elim n; clear n; auto. - intros x; generalize (spec_compare0_m x); rewrite w_to_Z_0; auto. + intros x; rewrite spec_compare0_m; rewrite w_to_Z_0; auto. intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto. + fold word in *. intros xh xl. - generalize (Hrec xh); case compare0_mn; auto. - generalize (Hrec xl); case compare0_mn; auto. - simpl double_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto. - simpl double_to_Z; intros H1 H2; rewrite <- H2; auto. - case (double_to_Z_pos n xl); auto with zarith. - intros H1; simpl double_to_Z. - set (u := DoubleBase.double_wB wm_base n). - case (double_to_Z_pos n xl); intros H2 H3. - assert (0 < u); auto with zarith. - unfold u, DoubleBase.double_wB, base; auto with zarith. + rewrite 2 Hrec. + simpl double_to_Z. + set (wB := DoubleBase.double_wB wm_base n). + case Zcompare_spec; intros Cmp. + rewrite <- Cmp. reflexivity. + symmetry. apply Zgt_lt, Zlt_gt. (* ;-) *) + assert (0 < wB). + unfold wB, DoubleBase.double_wB, base; auto with zarith. change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. - case (double_to_Z_pos n xh); auto with zarith. + case (double_to_Z_pos n xl); auto with zarith. + case (double_to_Z_pos n xh); intros; exfalso; omega. Qed. Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison := @@ -355,17 +340,9 @@ Section CompareRec. end. Variable spec_compare: forall x y, - match compare x y with - Eq => w_to_Z x = w_to_Z y - | Lt => w_to_Z x < w_to_Z y - | Gt => w_to_Z x > w_to_Z y - end. + compare x y = Zcompare (w_to_Z x) (w_to_Z y). Variable spec_compare_m: forall x y, - match compare_m x y with - Eq => wm_to_Z x = w_to_Z y - | Lt => wm_to_Z x < w_to_Z y - | Gt => wm_to_Z x > w_to_Z y - end. + compare_m x y = Zcompare (wm_to_Z x) (w_to_Z y). Variable wm_base_lt: forall x, 0 <= w_to_Z x < base (wm_base). @@ -387,26 +364,23 @@ Section CompareRec. Lemma spec_compare_mn_1: forall n x y, - match compare_mn_1 n x y with - Eq => double_to_Z n x = w_to_Z y - | Lt => double_to_Z n x < w_to_Z y - | Gt => double_to_Z n x > w_to_Z y - end. + compare_mn_1 n x y = Zcompare (double_to_Z n x) (w_to_Z y). Proof. intros n; elim n; simpl; auto; clear n. intros n Hrec x; case x; clear x; auto. - intros y; generalize (spec_compare w_0 y); rewrite w_to_Z_0; case compare; auto. - intros xh xl y; simpl; generalize (spec_compare0_mn n xh); case compare0_mn; intros H1b. + intros y; rewrite spec_compare; rewrite w_to_Z_0. reflexivity. + intros xh xl y; simpl; + rewrite spec_compare0_mn, Hrec. case Zcompare_spec. + intros H1b. rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto. - apply Hrec. - apply Zlt_gt. + symmetry. apply Zlt_gt. case (double_wB_lt n y); intros _ H0. apply Zlt_le_trans with (1:= H0). fold double_wB. case (double_to_Z_pos n xl); intros H1 H2. apply Zle_trans with (double_to_Z n xh * double_wB n); auto with zarith. apply Zle_trans with (1 * double_wB n); auto with zarith. - case (double_to_Z_pos n xh); auto with zarith. + case (double_to_Z_pos n xh); intros; exfalso; omega. Qed. End CompareRec. @@ -440,22 +414,6 @@ Section AddS. End AddS. - - Lemma spec_opp: forall u x y, - match u with - | Eq => y = x - | Lt => y < x - | Gt => y > x - end -> - match opp_compare u with - | Eq => x = y - | Lt => x < y - | Gt => x > y - end. - Proof. - intros u x y; case u; simpl; auto with zarith. - Qed. - Fixpoint length_pos x := match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end. @@ -481,33 +439,37 @@ End AddS. Variable w: Type. - Theorem digits_zop: forall w (x: znz_op w), - znz_digits (mk_zn2z_op x) = xO (znz_digits x). + Theorem digits_zop: forall t (ops : ZnZ.Ops t), + @ZnZ.digits _ mk_zn2z_ops = xO ZnZ.digits. + Proof. intros ww x; auto. Qed. - Theorem digits_kzop: forall w (x: znz_op w), - znz_digits (mk_zn2z_op_karatsuba x) = xO (znz_digits x). + Theorem digits_kzop: forall t (ops : ZnZ.Ops t), + @ZnZ.digits _ mk_zn2z_ops_karatsuba = xO (@ZnZ.digits _ ops). + Proof. intros ww x; auto. Qed. - Theorem make_zop: forall w (x: znz_op w), - znz_to_Z (mk_zn2z_op x) = + Theorem make_zop: forall t (ops : ZnZ.Ops t), + @ZnZ.to_Z _ mk_zn2z_ops = fun z => match z with - W0 => 0 - | WW xh xl => znz_to_Z x xh * base (znz_digits x) - + znz_to_Z x xl + | W0 => 0 + | WW xh xl => ZnZ.to_Z xh * base ZnZ.digits + + ZnZ.to_Z xl end. + Proof. intros ww x; auto. Qed. - Theorem make_kzop: forall w (x: znz_op w), - znz_to_Z (mk_zn2z_op_karatsuba x) = + Theorem make_kzop: forall t (x: ZnZ.Ops t), + @ZnZ.to_Z _ mk_zn2z_ops_karatsuba = fun z => match z with - W0 => 0 - | WW xh xl => znz_to_Z x xh * base (znz_digits x) - + znz_to_Z x xl + | W0 => 0 + | WW xh xl => ZnZ.to_Z xh * base ZnZ.digits + + ZnZ.to_Z xl end. + Proof. intros ww x; auto. Qed. diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 85639aa6a..3f60cbf1a 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -51,6 +51,7 @@ Module Type NType. Parameter power_pos : t -> positive -> t. Parameter power : t -> N -> t. Parameter sqrt : t -> t. + Parameter log2 : t -> t. Parameter div_eucl : t -> t -> t * t. Parameter div : t -> t -> t. Parameter modulo : t -> t -> t. @@ -74,6 +75,8 @@ Module Type NType. Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. Parameter spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + Parameter spec_log2_0: forall x, [x] = 0 -> [log2 x] = 0. + Parameter spec_log2: forall x, [x]<>0 -> 2^[log2 x] <= [x] < 2^([log2 x]+1). Parameter spec_div_eucl: forall x y, let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. Parameter spec_div: forall x y, [div x y] = [x] / [y]. -- cgit v1.2.3