diff options
| author |  thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-21 07:47:46 +0000 |
|---|---|---|
| committer | thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-21 07:47:46 +0000 |
| commit | 2c1c506d23118fb56fc07b4e334e0e1c7995e36b (patch) | |
| tree | 40fe1b8d8b6225ef09443f3073840e0b65f73536 | |
| parent | 79d1421ce90b7f3c0c6a719a93a87d36b3abdfcd (diff) | |
add_mul_pos uses int31 only
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9845 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Ints/BigN.v | 17 | ||||
| -rw-r--r-- | theories/Ints/Int31.v | 7 | ||||
| -rw-r--r-- | theories/Ints/Z/ZDivModAux.v | 2 | ||||
| -rw-r--r-- | theories/Ints/Z/ZPowerAux.v | 20 | ||||
| -rw-r--r-- | theories/Ints/num/GenBase.v | 4 | ||||
| -rw-r--r-- | theories/Ints/num/GenDiv.v | 527 | ||||
| -rw-r--r-- | theories/Ints/num/GenDivn1.v | 282 | ||||
| -rw-r--r-- | theories/Ints/num/GenLift.v | 270 | ||||
| -rw-r--r-- | theories/Ints/num/GenSqrt.v | 342 | ||||
| -rw-r--r-- | theories/Ints/num/NMake.v | 130 | ||||
| -rw-r--r-- | theories/Ints/num/Zn2Z.v | 230 | ||||
| -rw-r--r-- | theories/Ints/num/ZnZ.v | 19 |
12 files changed, 1160 insertions, 690 deletions
diff --git a/theories/Ints/BigN.v b/theories/Ints/BigN.v index 2ad6ef030..98e24c63f 100644 --- a/theories/Ints/BigN.v +++ b/theories/Ints/BigN.v @@ -9,9 +9,10 @@ Definition int31_op : znz_op int31. (* Conversion functions with Z *) exact (31%positive). (* number of digits *) + exact (31). (* number of digits *) exact (phi). (* conversion to Z *) exact (positive_to_int31). (* positive -> N*int31 : p => N,i where p = N*2^31+phi i *) - exact (head031). (* number of head 0 *) + exact head031. (* number of head 0 *) (* Basic constructors *) exact 0. (* 0 *) @@ -65,19 +66,13 @@ Definition int31_op : znz_op int31. exact gcd31. (*gcd*) (* shift operations *) - exact (fun p => let (_,i) := positive_to_int31 p in addmuldiv31 i). (*add_mul_div with positive ? *) + exact addmuldiv31. (*add_mul_div with positive ? *) (*modulo 2^p (p positive) *) exact (fun p i => - let (n,j) := positive_to_int31 p in - match n with - | N0 => - match compare31 j 32 with - | Lt => addmuldiv31 j 0 (addmuldiv31 (31-j) i 0) + match compare31 p 32 with + | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0) | _ => i - end - | _ => i - end). - + end). (* is i even ? *) exact (fun i => let (_,r) := i/2 in diff --git a/theories/Ints/Int31.v b/theories/Ints/Int31.v index 5d185a66a..8a19e878d 100644 --- a/theories/Ints/Int31.v +++ b/theories/Ints/Int31.v @@ -38,6 +38,7 @@ Definition On := I31 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 Definition In := I31 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D1. Definition Tn := I31 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1 D1. Definition Twon := I31 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D1 D0. +Definition T31 := I31 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D0 D1 D1 D1 D1 D1. Definition sneakr b i := match i with @@ -388,9 +389,9 @@ Definition positive_to_int31 (p:positive) := . Definition head031 (i:int31) := - recl _ (fun _ => sizeN) (fun b si rec n => match b with - | D0 => rec (n+1)%N + recl _ (fun _ => T31) (fun b si rec n => match b with + | D0 => rec (add31 n In) | D1 => n end) - i 0%N + i On .
\ No newline at end of file diff --git a/theories/Ints/Z/ZDivModAux.v b/theories/Ints/Z/ZDivModAux.v index d07b92d80..be7955aad 100644 --- a/theories/Ints/Z/ZDivModAux.v +++ b/theories/Ints/Z/ZDivModAux.v @@ -386,7 +386,7 @@ Hint Resolve Zlt_gt Zle_ge: zarith. Lemma shift_unshift_mod : forall n p a, 0 <= a < 2^n -> - 0 < p < n -> + 0 <= p <= n -> a * 2^p = a / 2^(n - p) * 2^n + (a*2^p) mod 2^n. Proof. intros n p a H1 H2. diff --git a/theories/Ints/Z/ZPowerAux.v b/theories/Ints/Z/ZPowerAux.v index b56b52d49..151b9a73a 100644 --- a/theories/Ints/Z/ZPowerAux.v +++ b/theories/Ints/Z/ZPowerAux.v @@ -181,3 +181,23 @@ replace (a^c) with 0. auto with zarith. destruct c;trivial;unfold Zgt in z0;discriminate z0. destruct b;trivial;unfold Zgt in z;discriminate z. Qed. + +Theorem Zpower2_lt_lin: forall n, + 0 <= n -> n < 2 ^ n. +intros n; apply (natlike_ind (fun n => n < 2 ^n)); clear n. + simpl; auto with zarith. +intros n H1 H2; unfold Zsucc. +case (Zle_lt_or_eq _ _ H1); clear H1; intros H1. + apply Zle_lt_trans with (n + n); auto with zarith. + rewrite Zpower_exp; auto with zarith. + rewrite Zpower_exp_1. + assert (tmp: forall p, p * 2 = p + p); intros; try ring; + rewrite tmp; auto with zarith. +subst n; simpl; unfold Zpower_pos; simpl; auto with zarith. +Qed. + +Theorem Zpower2_le_lin: forall n, + 0 <= n -> n <= 2 ^ n. +intros; apply Zlt_le_weak. +apply Zpower2_lt_lin; auto. +Qed. diff --git a/theories/Ints/num/GenBase.v b/theories/Ints/num/GenBase.v index b953566ed..04749f79c 100644 --- a/theories/Ints/num/GenBase.v +++ b/theories/Ints/num/GenBase.v @@ -25,11 +25,15 @@ Section GenBase. Variable w_WW : w -> w -> zn2z w. Variable w_0W : w -> zn2z w. Variable w_digits : positive. + Variable w_zdigits: w. + Variable w_add: w -> w -> zn2z w. Variable w_to_Z : w -> Z. Variable w_compare : w -> w -> comparison. Definition ww_digits := xO w_digits. + Definition ww_zdigits := w_add w_zdigits w_zdigits. + Definition ww_to_Z := zn2z_to_Z (base w_digits) w_to_Z. Definition ww_1 := WW w_0 w_1. diff --git a/theories/Ints/num/GenDiv.v b/theories/Ints/num/GenDiv.v index 4bcea709d..4a30fa2c3 100644 --- a/theories/Ints/num/GenDiv.v +++ b/theories/Ints/num/GenDiv.v @@ -12,6 +12,7 @@ Require Import ZArith. Require Import ZAux. Require Import ZDivModAux. Require Import ZPowerAux. +Require Import Zmod. Require Import Basic_type. Require Import GenBase. Require Import GenDivn1. @@ -28,19 +29,32 @@ Section POS_MOD. Variable w:Set. Variable w_0 : w. Variable w_digits : positive. + Variable w_zdigits : w. Variable w_WW : w -> w -> zn2z w. - Variable w_pos_mod : positive -> w -> w. + Variable w_pos_mod : w -> w -> w. + Variable w_compare : w -> w -> comparison. + Variable ww_compare : zn2z w -> zn2z w -> comparison. + Variable w_0W : w -> zn2z w. + Variable low: zn2z w -> w. + Variable ww_sub: zn2z w -> zn2z w -> zn2z w. + Variable ww_zdigits : zn2z w. + Definition ww_pos_mod p x := + let zdigits := w_0W w_zdigits in match x with | W0 => W0 | WW xh xl => - match Pcompare p w_digits Eq with + match ww_compare p zdigits with | Eq => w_WW w_0 xl - | Lt => w_WW w_0 (w_pos_mod p xl) + | Lt => w_WW w_0 (w_pos_mod (low p) xl) | Gt => - let n := Pminus p w_digits in - w_WW (w_pos_mod n xh) xl + match ww_compare p ww_zdigits with + | Lt => + let n := low (ww_sub p zdigits) in + w_WW (w_pos_mod n xh) xl + | _ => x + end end end. @@ -58,79 +72,129 @@ Section POS_MOD. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. + Variable spec_to_w_Z : forall x, 0 <= [[x]] < wwB. + Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. Variable spec_pos_mod : forall w p, - [|w_pos_mod p w|] = [|w|] mod (2 ^ Zpos p). + [|w_pos_mod p w|] = [|w|] mod (2 ^ [|p|]). + + Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. + Variable spec_ww_compare : forall x y, + match ww_compare x y with + | Eq => [[x]] = [[y]] + | Lt => [[x]] < [[y]] + | Gt => [[x]] > [[y]] + end. + Variable spec_ww_sub: forall x y, + [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB. + + Variable spec_zdigits : [| w_zdigits |] = Zpos w_digits. + Variable spec_low: forall x, [| low x|] = [[x]] mod wB. + Variable spec_ww_zdigits : [[ww_zdigits]] = 2 * [|w_zdigits|]. + Variable spec_ww_digits : ww_digits w_digits = xO w_digits. + Hint Rewrite spec_w_0 spec_w_WW : w_rewrite. Lemma spec_ww_pos_mod : forall w p, - [[ww_pos_mod p w]] = [[w]] mod (2 ^ Zpos p). + [[ww_pos_mod p w]] = [[w]] mod (2 ^ [[p]]). assert (HHHHH:= lt_0_wB w_digits). assert (F0: forall x y, x - y + y = x); auto with zarith. - intros w1 p; unfold ww_pos_mod; case w1. - autorewrite with w_rewrite; rewrite Zmod_def_small; auto with zarith. - match goal with |- context [(?X ?= ?Y)%positive Eq] => - case_eq (Pcompare X Y Eq) end; intros H1. - assert (E1: Zpos p = Zpos w_digits); auto. - rewrite Pcompare_Eq_eq with (1:= H1); auto with zarith. - rewrite E1. - intros xh xl; simpl ww_to_Z;autorewrite with w_rewrite rm10. - match goal with |- context id [2 ^Zpos w_digits] => - let v := context id [wB] in change v - end. - rewrite Zmod_plus; auto with zarith. - rewrite Zmod_mult_0; auto with zarith. - autorewrite with rm10. - rewrite Zmod_mod; auto with zarith. - rewrite Zmod_def_small; auto with zarith. - assert (Eq1: Zpos p < Zpos w_digits); auto. - intros xh xl; autorewrite with w_rewrite rm10. - rewrite spec_pos_mod; auto with zarith. - assert (Eq2: Zpos p+(Zpos w_digits -Zpos p) = Zpos w_digits);auto with zarith. - simpl ww_to_Z;unfold base; rewrite <- Eq2. - rewrite Zpower_exp; auto with zarith. - rewrite (fun x => (Zmult_comm (2 ^ x))); rewrite Zmult_assoc. - rewrite Zmod_plus; auto with zarith. - rewrite Zmod_mult_0; auto with zarith. - autorewrite with rm10. - rewrite Zmod_mod; auto with zarith. - assert (Eq1: Zpos p > Zpos w_digits); auto. - intros xh xl; autorewrite with w_rewrite rm10. - rewrite spec_pos_mod; auto with zarith. - simpl ww_to_Z. - pattern [|xh|] at 2; rewrite Z_div_mod_eq with (b := 2 ^ Zpos (p - w_digits)); - auto with zarith. - rewrite (fun x => (Zmult_comm (2 ^ x))); rewrite Zmult_plus_distr_l. - unfold base; rewrite <- Zmult_assoc; rewrite <- Zpower_exp; + intros w1 p; case (spec_to_w_Z p); intros HH1 HH2. + unfold ww_pos_mod; case w1. + simpl; rewrite Zmod_def_small; split; auto with zarith. + intros xh xl; generalize (spec_ww_compare p (w_0W w_zdigits)); + case ww_compare; + rewrite spec_w_0W; rewrite spec_zdigits; fold wB; + intros H1. + rewrite H1; simpl ww_to_Z. + autorewrite with w_rewrite rm10. + rewrite Zmod_plus; auto with zarith. + rewrite Zmod_mult_0; auto with zarith. + autorewrite with rm10. + rewrite Zmod_mod; auto with zarith. + rewrite Zmod_def_small; auto with zarith. + autorewrite with w_rewrite rm10. + simpl ww_to_Z. + rewrite spec_pos_mod. + assert (HH0: [|low p|] = [[p]]). + rewrite spec_low. + apply Zmod_def_small; auto with zarith. + case (spec_to_w_Z p); intros HHH1 HHH2; split; auto with zarith. + apply Zlt_le_trans with (1 := H1). + unfold base. + apply Zpower2_le_lin; auto with zarith. + rewrite HH0. + rewrite Zmod_plus; auto with zarith. + unfold base. + rewrite <- (F0 (Zpos w_digits) [[p]]). + rewrite Zpower_exp; auto with zarith. + rewrite Zmult_assoc. + rewrite Zmod_mult_0; auto with zarith. + autorewrite with w_rewrite rm10. + rewrite Zmod_mod; auto with zarith. +generalize (spec_ww_compare p ww_zdigits); + case ww_compare; rewrite spec_ww_zdigits; + rewrite spec_zdigits; intros H2. + replace (2^[[p]]) with wwB. + rewrite Zmod_def_small; auto with zarith. + unfold base; rewrite H2. + rewrite spec_ww_digits; auto. + assert (HH0: [|low (ww_sub p (w_0W w_zdigits))|] = + [[p]] - Zpos w_digits). + rewrite spec_low. + rewrite spec_ww_sub. + rewrite spec_w_0W; rewrite spec_zdigits. + rewrite <- Zmod_div_mod; auto with zarith. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + apply Zlt_le_trans with (Zpos w_digits); auto with zarith. + unfold base; apply Zpower2_le_lin; auto with zarith. + exists wB; unfold base; rewrite <- Zpower_exp; auto with zarith. + rewrite spec_ww_digits; + apply f_equal with (f := Zpower 2); rewrite Zpos_xO; auto with zarith. + simpl ww_to_Z; autorewrite with w_rewrite. + rewrite spec_pos_mod; rewrite HH0. + pattern [|xh|] at 2; + rewrite Z_div_mod_eq with (b := 2 ^ ([[p]] - Zpos w_digits)); + auto with zarith. + rewrite (fun x => (Zmult_comm (2 ^ x))); rewrite Zmult_plus_distr_l. + unfold base; rewrite <- Zmult_assoc; rewrite <- Zpower_exp; auto with zarith. - rewrite Zpos_minus; auto with zarith. - rewrite F0; auto with zarith. - rewrite <- Zplus_assoc; rewrite Zmod_plus; auto with zarith. - rewrite Zmod_mult_0; auto with zarith. - autorewrite with rm10. - rewrite Zmod_mod; auto with zarith. - apply sym_equal; apply Zmod_def_small; auto with zarith. - case (spec_to_Z xh); intros U1 U2. - case (spec_to_Z xl); intros U3 U4. - split; auto with zarith. - apply Zplus_le_0_compat; auto with zarith. - apply Zmult_le_0_compat; auto with zarith. - match goal with |- 0 <= ?X mod ?Y => - case (Z_mod_lt X Y); auto with zarith - end. - match goal with |- ?X mod ?Y * ?U + ?Z < ?T => - apply Zle_lt_trans with ((Y - 1) * U + Z ); - [case (Z_mod_lt X Y); auto with zarith | idtac] - end. - match goal with |- ?X * ?U + ?Y < ?Z => - apply Zle_lt_trans with (X * U + (U - 1)) - end. - apply Zplus_le_compat_l; auto with zarith. - case (spec_to_Z xl); unfold base; auto with zarith. - rewrite Zmult_minus_distr_r; rewrite <- Zpower_exp; auto with zarith. - rewrite F0; auto with zarith. + rewrite F0; auto with zarith. + rewrite <- Zplus_assoc; rewrite Zmod_plus; auto with zarith. + rewrite Zmod_mult_0; auto with zarith. + autorewrite with rm10. + rewrite Zmod_mod; auto with zarith. + apply sym_equal; apply Zmod_def_small; auto with zarith. + case (spec_to_Z xh); intros U1 U2. + case (spec_to_Z xl); intros U3 U4. + split; auto with zarith. + apply Zplus_le_0_compat; auto with zarith. + apply Zmult_le_0_compat; auto with zarith. + match goal with |- 0 <= ?X mod ?Y => + case (Z_mod_lt X Y); auto with zarith + end. + match goal with |- ?X mod ?Y * ?U + ?Z < ?T => + apply Zle_lt_trans with ((Y - 1) * U + Z ); + [case (Z_mod_lt X Y); auto with zarith | idtac] + end. + match goal with |- ?X * ?U + ?Y < ?Z => + apply Zle_lt_trans with (X * U + (U - 1)) + end. + apply Zplus_le_compat_l; auto with zarith. + case (spec_to_Z xl); unfold base; auto with zarith. + rewrite Zmult_minus_distr_r; rewrite <- Zpower_exp; auto with zarith. + rewrite F0; auto with zarith. + rewrite Zmod_def_small; auto with zarith. + case (spec_to_w_Z (WW xh xl)); intros U1 U2. + split; auto with zarith. + apply Zlt_le_trans with (1:= U2). + unfold base; rewrite spec_ww_digits. + apply Zpower_le_monotone; auto with zarith. + split; auto with zarith. + rewrite Zpos_xO; auto with zarith. Qed. End POS_MOD. @@ -587,30 +651,34 @@ Section GenDivGt. Variable w_div_gt : w -> w -> w*w. Variable w_mod_gt : w -> w -> w. Variable w_gcd_gt : w -> w -> w. - Variable w_add_mul_div : positive -> w -> w -> w. - Variable w_head0 : w -> N. + Variable w_add_mul_div : w -> w -> w -> w. + Variable w_head0 : w -> w. Variable w_div21 : w -> w -> w -> w * w. Variable w_div32 : w -> w -> w -> w -> w -> w * zn2z w. - Variable _ww_digits : positive. + Variable _ww_zdigits : zn2z w. Variable ww_1 : zn2z w. - Variable ww_add_mul_div : positive -> zn2z w -> zn2z w -> zn2z w. + Variable ww_add_mul_div : zn2z w -> zn2z w -> zn2z w -> zn2z w. + + Variable w_zdigits : w. Definition ww_div_gt_aux ah al bh bl := Eval lazy beta iota delta [ww_sub ww_opp] in - let nb0 := w_head0 bh in - match nb0 with - | N0 => (ww_1, ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c - w_opp w_sub w_sub_carry (WW ah al) (WW bh bl)) - | Npos p => + let p := w_head0 bh in + match w_compare p w_0 with + | Gt => let b1 := w_add_mul_div p bh bl in let b2 := w_add_mul_div p bl w_0 in let a1 := w_add_mul_div p w_0 ah in let a2 := w_add_mul_div p ah al in let a3 := w_add_mul_div p al w_0 in let (q,r) := w_div32 a1 a2 a3 b1 b2 in - (WW w_0 q, ww_add_mul_div (Pminus _ww_digits p) W0 r) + (WW w_0 q, ww_add_mul_div + (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c + w_opp w_sub w_sub_carry _ww_zdigits (w_0W p)) W0 r) + | _ => (ww_1, ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c + w_opp w_sub w_sub_carry (WW ah al) (WW bh bl)) end. Definition ww_div_gt a b := @@ -628,7 +696,8 @@ Section GenDivGt. match w_compare w_0 bh with | Eq => let(q,r):= - gen_divn1 w_digits w_0 w_WW w_head0 w_add_mul_div w_div21 1 a bl in + gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 a bl in (q, w_0W r) | Lt => ww_div_gt_aux ah al bh bl | Gt => (W0,W0) (* cas absurde *) @@ -637,19 +706,20 @@ Section GenDivGt. Definition ww_mod_gt_aux ah al bh bl := Eval lazy beta iota delta [ww_sub ww_opp] in - let nb0 := w_head0 bh in - match nb0 with - | N0 => - ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c - w_opp w_sub w_sub_carry (WW ah al) (WW bh bl) - | Npos p => + let p := w_head0 bh in + match w_compare p w_0 with + | Gt => let b1 := w_add_mul_div p bh bl in let b2 := w_add_mul_div p bl w_0 in let a1 := w_add_mul_div p w_0 ah in let a2 := w_add_mul_div p ah al in let a3 := w_add_mul_div p al w_0 in let (q,r) := w_div32 a1 a2 a3 b1 b2 in - ww_add_mul_div (Pminus _ww_digits p) W0 r + ww_add_mul_div (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c + w_opp w_sub w_sub_carry _ww_zdigits (w_0W p)) W0 r + | _ => + ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c + w_opp w_sub w_sub_carry (WW ah al) (WW bh bl) end. Definition ww_mod_gt a b := @@ -664,7 +734,8 @@ Section GenDivGt. else match w_compare w_0 bh with | Eq => - w_0W (gen_modn1 w_digits w_0 w_head0 w_add_mul_div w_div21 1 a bl) + w_0W (gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 a bl) | Lt => ww_mod_gt_aux ah al bh bl | Gt => W0 (* cas absurde *) end @@ -679,8 +750,8 @@ Section GenDivGt. match w_compare w_0 bl with | Eq => WW ah al (* normalement n'arrive pas si forme normale *) | Lt => - let m := gen_modn1 w_digits w_0 w_head0 w_add_mul_div w_div21 1 - (WW ah al) bl in + let m := gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 (WW ah al) bl in WW w_0 (w_gcd_gt bl m) | Gt => W0 (* absurde *) end @@ -694,8 +765,8 @@ Section GenDivGt. match w_compare w_0 ml with | Eq => WW bh bl | _ => - let r := gen_modn1 w_digits w_0 w_head0 w_add_mul_div w_div21 1 - (WW bh bl) ml in + let r := gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 (WW bh bl) ml in WW w_0 (w_gcd_gt ml r) end | Lt => @@ -734,6 +805,7 @@ Section GenDivGt. Variable spec_w_0 : [|w_0|] = 0. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. + Variable spec_to_w_Z : forall x, 0 <= [[x]] < wwB. Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. @@ -765,12 +837,12 @@ Section GenDivGt. Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|]. Variable spec_add_mul_div : forall x y p, - Zpos p < Zpos w_digits -> + [|p|] <= Zpos w_digits -> [| w_add_mul_div p x y |] = - ([|x|] * (Zpower 2 (Zpos p)) + - [|y|] / (Zpower 2 ((Zpos w_digits) - (Zpos p)))) mod wB. + ([|x|] * (2 ^ ([|p|])) + + [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB. Variable spec_head0 : forall x, 0 < [|x|] -> - wB/ 2 <= 2 ^ (Z_of_N (w_head0 x)) * [|x|] < wB. + wB/ 2 <= 2 ^ [|w_head0 x|] * [|x|] < wB. Variable spec_div21 : forall a1 a2 b, wB/2 <= [|b|] -> @@ -787,13 +859,15 @@ Section GenDivGt. [|q|] * ([|b1|] * wB + [|b2|]) + [[r]] /\ 0 <= [[r]] < [|b1|] * wB + [|b2|]. - Variable spec_ww_digits_ : _ww_digits = xO w_digits. + Variable spec_w_zdigits: [|w_zdigits|] = Zpos w_digits. + + Variable spec_ww_digits_ : [[_ww_zdigits]] = Zpos (xO w_digits). Variable spec_ww_1 : [[ww_1]] = 1. Variable spec_ww_add_mul_div : forall x y p, - Zpos p < Zpos (xO w_digits) -> + [[p]] <= Zpos (xO w_digits) -> [[ ww_add_mul_div p x y ]] = - ([[x]] * (2^Zpos p) + - [[y]] / (2^(Zpos (xO w_digits) - Zpos p))) mod wwB. + ([[x]] * (2^[[p]]) + + [[y]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB. Ltac Spec_w_to_Z x := let H:= fresh "HH" in @@ -804,14 +878,14 @@ Section GenDivGt. assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x). Lemma to_Z_div_minus_p : forall x p, - 0 < Zpos p < Zpos w_digits -> - 0 <= [|x|] / 2 ^ (Zpos w_digits - Zpos p) < 2 ^ Zpos p. + 0 < [|p|] < Zpos w_digits -> + 0 <= [|x|] / 2 ^ (Zpos w_digits - [|p|]) < 2 ^ [|p|]. Proof. intros x p H;Spec_w_to_Z x. split. apply Zdiv_le_lower_bound;zarith. apply Zdiv_lt_upper_bound;zarith. rewrite <- Zpower_exp;zarith. - ring_simplify (Zpos p + (Zpos w_digits - Zpos p)); unfold base in HH;zarith. + ring_simplify ([|p|] + (Zpos w_digits - [|p|])); unfold base in HH;zarith. Qed. Hint Resolve to_Z_div_minus_p : zarith. @@ -824,20 +898,27 @@ Section GenDivGt. Proof. intros ah al bh bl Hgt Hpos;unfold ww_div_gt_aux. change - (let (q, r) := match w_head0 bh with - | N0 => (ww_1, ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c - w_opp w_sub w_sub_carry (WW ah al) (WW bh bl)) - | Npos p => + (let (q, r) := let p := w_head0 bh in + match w_compare p w_0 with + | Gt => let b1 := w_add_mul_div p bh bl in let b2 := w_add_mul_div p bl w_0 in let a1 := w_add_mul_div p w_0 ah in let a2 := w_add_mul_div p ah al in let a3 := w_add_mul_div p al w_0 in let (q,r) := w_div32 a1 a2 a3 b1 b2 in - (WW w_0 q, ww_add_mul_div (Pminus _ww_digits p) W0 r) + (WW w_0 q, ww_add_mul_div + (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c + w_opp w_sub w_sub_carry _ww_zdigits (w_0W p)) W0 r) + | _ => (ww_1, ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c + w_opp w_sub w_sub_carry (WW ah al) (WW bh bl)) end in [[WW ah al]]=[[q]]*[[WW bh bl]]+[[r]] /\ 0 <=[[r]]< [[WW bh bl]]). - assert (Hh := spec_head0 Hpos);destruct (w_head0 bh). - simpl Zpower in Hh;rewrite Zmult_1_l in Hh;destruct Hh. + assert (Hh := spec_head0 Hpos). + lazy zeta. + generalize (spec_compare (w_head0 bh) w_0); case w_compare; + rewrite spec_w_0; intros HH. + generalize Hh; rewrite HH; simpl Zpower; + rewrite Zmult_1_l; intros (HH1, HH2); clear HH. assert (wwB <= 2*[[WW bh bl]]). apply Zle_trans with (2*[|bh|]*wB). rewrite wwB_wBwB; rewrite Zpower_2; apply Zmult_le_compat_r; zarith. @@ -847,22 +928,22 @@ Section GenDivGt. Spec_ww_to_Z (WW ah al). rewrite spec_ww_sub;eauto. simpl;rewrite spec_ww_1;rewrite Zmult_1_l;simpl. - simpl ww_to_Z in Hgt, H1, HH;rewrite Zmod_def_small;split;zarith. - unfold Z_of_N in Hh. - assert (Zpos p < Zpos w_digits). - destruct (Z_lt_ge_dec (Zpos p) (Zpos w_digits));trivial. + simpl ww_to_Z in Hgt, H, HH;rewrite Zmod_def_small;split;zarith. + case (spec_to_Z (w_head0 bh)); auto with zarith. + assert ([|w_head0 bh|] < Zpos w_digits). + destruct (Z_lt_ge_dec [|w_head0 bh|] (Zpos w_digits));trivial. elimtype False. - assert (2 ^ Zpos p * [|bh|] >= wB);auto with zarith. + assert (2 ^ [|w_head0 bh|] * [|bh|] >= wB);auto with zarith. apply Zle_ge; replace wB with (wB * 1);try ring. Spec_w_to_Z bh;apply Zmult_le_compat;zarith. unfold base;apply Zpower_le_monotone;zarith. - assert (HHHH : 0 < Zpos p < Zpos w_digits). - split;trivial. unfold Zlt;reflexivity. - generalize (spec_add_mul_div w_0 ah H) - (spec_add_mul_div ah al H) - (spec_add_mul_div al w_0 H) - (spec_add_mul_div bh bl H) - (spec_add_mul_div bl w_0 H); + assert (HHHH : 0 < [|w_head0 bh|] < Zpos w_digits); auto with zarith. + assert (Hb:= Zlt_le_weak _ _ H). + generalize (spec_add_mul_div w_0 ah Hb) + (spec_add_mul_div ah al Hb) + (spec_add_mul_div al w_0 Hb) + (spec_add_mul_div bh bl Hb) + (spec_add_mul_div bl w_0 Hb); rewrite spec_w_0; repeat rewrite Zmult_0_l;repeat rewrite Zplus_0_l; rewrite Zdiv_0;repeat rewrite Zplus_0_r. Spec_w_to_Z ah;Spec_w_to_Z bh. 2:apply Zpower_lt_0;zarith. @@ -870,35 +951,35 @@ Section GenDivGt. assert (H3:=to_Z_div_minus_p ah HHHH);assert(H4:=to_Z_div_minus_p al HHHH); assert (H5:=to_Z_div_minus_p bl HHHH). rewrite Zmult_comm in Hh. - assert (2^Zpos p < wB). unfold base;apply Zpower_lt_monotone;zarith. + assert (2^[|w_head0 bh|] < wB). unfold base;apply Zpower_lt_monotone;zarith. unfold base in H0;rewrite Zmod_def_small;zarith. - fold wB; rewrite (Zmod_def_small ([|bh|] * 2 ^ Zpos p));zarith. + fold wB; rewrite (Zmod_def_small ([|bh|] * 2 ^ [|w_head0 bh|]));zarith. intros U1 U2 U3 V1 V2. - generalize (@spec_w_div32 (w_add_mul_div p w_0 ah) - (w_add_mul_div p ah al) - (w_add_mul_div p al w_0) - (w_add_mul_div p bh bl) - (w_add_mul_div p bl w_0)). - destruct (w_div32 (w_add_mul_div p w_0 ah) - (w_add_mul_div p ah al) - (w_add_mul_div p al w_0) - (w_add_mul_div p bh bl) - (w_add_mul_div p bl w_0)) as (q,r). + generalize (@spec_w_div32 (w_add_mul_div (w_head0 bh) w_0 ah) + (w_add_mul_div (w_head0 bh) ah al) + (w_add_mul_div (w_head0 bh) al w_0) + (w_add_mul_div (w_head0 bh) bh bl) + (w_add_mul_div (w_head0 bh) bl w_0)). + destruct (w_div32 (w_add_mul_div (w_head0 bh) w_0 ah) + (w_add_mul_div (w_head0 bh) ah al) + (w_add_mul_div (w_head0 bh) al w_0) + (w_add_mul_div (w_head0 bh) bh bl) + (w_add_mul_div (w_head0 bh) bl w_0)) as (q,r). rewrite V1;rewrite V2. rewrite Zmult_plus_distr_l. - rewrite <- (Zplus_assoc ([|bh|] * 2 ^ Zpos p * wB)). + rewrite <- (Zplus_assoc ([|bh|] * 2 ^ [|w_head0 bh|] * wB)). unfold base;rewrite <- shift_unshift_mod;zarith. fold wB. - replace ([|bh|] * 2 ^ Zpos p * wB + [|bl|] * 2 ^ Zpos p) with - ([[WW bh bl]] * 2^Zpos p). 2:simpl;ring. + replace ([|bh|] * 2 ^ [|w_head0 bh|] * wB + [|bl|] * 2 ^ [|w_head0 bh|]) with + ([[WW bh bl]] * 2^[|w_head0 bh|]). 2:simpl;ring. fold wwB. rewrite wwB_wBwB. rewrite Zpower_2. rewrite U1;rewrite U2;rewrite U3. rewrite Zmult_assoc. rewrite Zmult_plus_distr_l. - rewrite (Zplus_assoc ([|ah|] / 2^(Zpos(w_digits) - Zpos p)*wB * wB)). + rewrite (Zplus_assoc ([|ah|] / 2^(Zpos(w_digits) - [|w_head0 bh|])*wB * wB)). rewrite <- Zmult_plus_distr_l. rewrite <- Zplus_assoc. unfold base;repeat rewrite <- shift_unshift_mod;zarith. fold wB. - replace ([|ah|] * 2 ^ Zpos p * wB + [|al|] * 2 ^ Zpos p) with - ([[WW ah al]] * 2^Zpos p). 2:simpl;ring. + replace ([|ah|] * 2 ^ [|w_head0 bh|] * wB + [|al|] * 2 ^ [|w_head0 bh|]) with + ([[WW ah al]] * 2^[|w_head0 bh|]). 2:simpl;ring. intros Hd;destruct Hd;zarith. simpl. apply beta_lex_inv;zarith. rewrite U1;rewrite V1. - assert ([|ah|] / 2 ^ (Zpos (w_digits) - Zpos p) < wB/2);zarith. + assert ([|ah|] / 2 ^ (Zpos (w_digits) - [|w_head0 bh|]) < wB/2);zarith. apply Zdiv_lt_upper_bound;zarith. unfold base. replace (2^Zpos (w_digits)) with (2^(Zpos (w_digits) - 1)*2). @@ -908,24 +989,39 @@ Section GenDivGt. pattern 2 at 2;replace 2 with (2^1);trivial. rewrite <- Zpower_exp;zarith. ring_simplify (Zpos (w_digits) - 1 + 1);trivial. change [[WW w_0 q]] with ([|w_0|]*wB+[|q|]);rewrite spec_w_0;rewrite - Zmult_0_l;rewrite Zplus_0_l;rewrite spec_ww_digits_. - replace [[ww_add_mul_div (xO (w_digits) - p) W0 r]] with ([[r]]/2^Zpos p). - assert (0 < 2^Zpos p). apply Zpower_lt_0;zarith. + Zmult_0_l;rewrite Zplus_0_l. + replace [[ww_add_mul_div (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry + _ww_zdigits (w_0W (w_head0 bh))) W0 r]] with ([[r]]/2^[|w_head0 bh|]). + assert (0 < 2^[|w_head0 bh|]). apply Zpower_lt_0;zarith. split. - rewrite <- (Z_div_mult [[WW ah al]] (2^Zpos p));zarith. + rewrite <- (Z_div_mult [[WW ah al]] (2^[|w_head0 bh|]));zarith. rewrite H1;rewrite Zmult_assoc;apply Z_div_plus_l;trivial. split;[apply Zdiv_le_lower_bound| apply Zdiv_lt_upper_bound];zarith. - rewrite spec_ww_add_mul_div;rewrite Zpos_minus. + rewrite spec_ww_add_mul_div. + rewrite spec_ww_sub; auto with zarith. + rewrite spec_ww_digits_. change (Zpos (xO (w_digits))) with (2*Zpos (w_digits));zarith. simpl ww_to_Z;rewrite Zmult_0_l;rewrite Zplus_0_l. - ring_simplify (2*Zpos (w_digits)-(2*Zpos (w_digits) - Zpos p));trivial. + rewrite spec_w_0W. + rewrite (fun x y => Zmod_def_small (x-y)); auto with zarith. + ring_simplify (2 * Zpos w_digits - (2 * Zpos w_digits - [|w_head0 bh|])). rewrite Zmod_def_small;zarith. split;[apply Zdiv_le_lower_bound| apply Zdiv_lt_upper_bound];zarith. Spec_ww_to_Z r. apply Zlt_le_trans with wwB;zarith. rewrite <- (Zmult_1_r wwB);apply Zmult_le_compat;zarith. - rewrite Zpos_xO;zarith. rewrite Zpos_xO;zarith. rewrite Zpos_xO;zarith. - Qed. + split; auto with zarith. + apply Zle_lt_trans with (2 * Zpos w_digits); auto with zarith. + unfold base, ww_digits; rewrite (Zpos_xO w_digits). + apply Zpower2_lt_lin; auto with zarith. + rewrite spec_ww_sub; auto with zarith. + rewrite spec_ww_digits_; rewrite spec_w_0W. + rewrite Zmod_def_small;zarith. + rewrite Zpos_xO; split; auto with zarith. + apply Zle_lt_trans with (2 * Zpos w_digits); auto with zarith. + unfold base, ww_digits; rewrite (Zpos_xO w_digits). + apply Zpower2_lt_lin; auto with zarith. + Qed. Lemma spec_ww_div_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] -> let (q,r) := ww_div_gt a b in @@ -933,21 +1029,24 @@ Section GenDivGt. 0 <= [[r]] < [[b]]. Proof. intros a b Hgt Hpos;unfold ww_div_gt. - change (let (q,r) := match a, b with - | W0, _ => (W0,W0) - | _, W0 => (W0,W0) - | WW ah al, WW bh bl => - if w_eq0 ah then let (q,r) := w_div_gt al bl in (WW w_0 q, w_0W r) - else - match w_compare w_0 bh with - | Eq => - let(q,r):= - gen_divn1 w_digits w_0 w_WW w_head0 w_add_mul_div w_div21 1 a bl in - (q, w_0W r) - | Lt => ww_div_gt_aux ah al bh bl - | Gt => (W0,W0) (* cas absurde *) - end - end in [[a]] = [[q]] * [[b]] + [[r]] /\ 0 <= [[r]] < [[b]]). + change (let (q,r) := match a, b with + | W0, _ => (W0,W0) + | _, W0 => (W0,W0) + | WW ah al, WW bh bl => + if w_eq0 ah then + let (q,r) := w_div_gt al bl in + (WW w_0 q, w_0W r) + else + match w_compare w_0 bh with + | Eq => + let(q,r):= + gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 a bl in + (q, w_0W r) + | Lt => ww_div_gt_aux ah al bh bl + | Gt => (W0,W0) (* cas absurde *) + end + end in [[a]] = [[q]] * [[b]] + [[r]] /\ 0 <= [[r]] < [[b]]). destruct a as [ |ah al]. simpl in Hgt;omega. destruct b as [ |bh bl]. simpl in Hpos;omega. Spec_w_to_Z ah; Spec_w_to_Z al; Spec_w_to_Z bh; Spec_w_to_Z bl. @@ -964,11 +1063,12 @@ Section GenDivGt. rewrite spec_w_0 in Hcmp. change [[WW bh bl]] with ([|bh|]*wB+[|bl|]). rewrite <- Hcmp;rewrite Zmult_0_l;rewrite Zplus_0_l. simpl in Hpos;rewrite <- Hcmp in Hpos;simpl in Hpos. - assert (H2:= @spec_gen_divn1 w w_digits w_0 w_WW w_head0 w_add_mul_div - w_div21 w_to_Z spec_to_Z spec_w_0 spec_w_WW spec_head0 - spec_add_mul_div spec_div21 1 (WW ah al) bl Hpos). + assert (H2:= @spec_gen_divn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div + w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 + spec_add_mul_div spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hpos). unfold gen_to_Z,gen_wB,gen_digits in H2. - destruct (gen_divn1 w_digits w_0 w_WW w_head0 w_add_mul_div w_div21 1 + destruct (gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 (WW ah al) bl). rewrite spec_w_0W;unfold ww_to_Z;trivial. apply spec_ww_div_gt_aux;trivial. rewrite spec_w_0 in Hcmp;trivial. @@ -979,10 +1079,8 @@ Section GenDivGt. ww_mod_gt_aux ah al bh bl = snd (ww_div_gt_aux ah al bh bl). Proof. intros ah al bh bl. unfold ww_mod_gt_aux, ww_div_gt_aux. - destruct (w_head0 bh). trivial. - destruct (w_div32 (w_add_mul_div p w_0 ah) (w_add_mul_div p ah al) - (w_add_mul_div p al w_0) (w_add_mul_div p bh bl) - (w_add_mul_div p bl w_0));trivial. + case w_compare; auto. + case w_div32; auto. Qed. Lemma spec_ww_mod_gt_aux : forall ah al bh bl, @@ -1014,34 +1112,37 @@ Section GenDivGt. intros a b Hgt Hpos. change (ww_mod_gt a b) with (match a, b with - | W0, _ => W0 - | _, W0 => W0 - | WW ah al, WW bh bl => - if w_eq0 ah then w_0W (w_mod_gt al bl) - else - match w_compare w_0 bh with - | Eq => - w_0W (gen_modn1 w_digits w_0 w_head0 w_add_mul_div w_div21 1 a bl) - | Lt => ww_mod_gt_aux ah al bh bl - | Gt => W0 (* cas absurde *) - end - end). + | W0, _ => W0 + | _, W0 => W0 + | WW ah al, WW bh bl => + if w_eq0 ah then w_0W (w_mod_gt al bl) + else + match w_compare w_0 bh with + | Eq => + w_0W (gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 a bl) + | Lt => ww_mod_gt_aux ah al bh bl + | Gt => W0 (* cas absurde *) + end end). change (ww_div_gt a b) with (match a, b with - | W0, _ => (W0,W0) - | _, W0 => (W0,W0) - | WW ah al, WW bh bl => - if w_eq0 ah then let (q,r) := w_div_gt al bl in (WW w_0 q, w_0W r) - else - match w_compare w_0 bh with - | Eq => - let(q,r):= - gen_divn1 w_digits w_0 w_WW w_head0 w_add_mul_div w_div21 1 a bl in - (q, w_0W r) - | Lt => ww_div_gt_aux ah al bh bl - | Gt => (W0,W0) (* cas absurde *) - end - end). + | W0, _ => (W0,W0) + | _, W0 => (W0,W0) + | WW ah al, WW bh bl => + if w_eq0 ah then + let (q,r) := w_div_gt al bl in + (WW w_0 q, w_0W r) + else + match w_compare w_0 bh with + | Eq => + let(q,r):= + gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 a bl in + (q, w_0W r) + | Lt => ww_div_gt_aux ah al bh bl + | Gt => (W0,W0) (* cas absurde *) + end + end). destruct a as [ |ah al];trivial. destruct b as [ |bh bl];trivial. Spec_w_to_Z ah; Spec_w_to_Z al; Spec_w_to_Z bh; Spec_w_to_Z bl. @@ -1055,9 +1156,9 @@ Section GenDivGt. destruct (w_div_gt al bl);simpl;rewrite spec_w_0W;trivial. clear H. assert (H2 := spec_compare w_0 bh);destruct (w_compare w_0 bh). - rewrite (@spec_gen_modn1_aux w w_digits w_0 w_WW w_head0 w_add_mul_div - w_div21 1 (WW ah al) bl). - destruct (gen_divn1 w_digits w_0 w_WW w_head0 w_add_mul_div w_div21 1 + rewrite (@spec_gen_modn1_aux w w_zdigits w_0 w_WW w_head0 w_add_mul_div + w_div21 w_compare w_sub w_to_Z spec_w_0 spec_compare 1 (WW ah al) bl). + destruct (gen_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW ah al) bl);simpl;trivial. rewrite spec_ww_mod_gt_aux_eq;trivial;symmetry;trivial. trivial. @@ -1097,8 +1198,8 @@ Section GenDivGt. match w_compare w_0 bl with | Eq => WW ah al (* normalement n'arrive pas si forme normale *) | Lt => - let m := gen_modn1 w_digits w_0 w_head0 w_add_mul_div w_div21 1 - (WW ah al) bl in + let m := gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 (WW ah al) bl in WW w_0 (w_gcd_gt bl m) | Gt => W0 (* absurde *) end @@ -1112,8 +1213,8 @@ Section GenDivGt. match w_compare w_0 ml with | Eq => WW bh bl | _ => - let r := gen_modn1 w_digits w_0 w_head0 w_add_mul_div w_div21 1 - (WW bh bl) ml in + let r := gen_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 + w_compare w_sub 1 (WW bh bl) ml in WW w_0 (w_gcd_gt ml r) end | Lt => @@ -1136,10 +1237,11 @@ Section GenDivGt. rewrite spec_w_0 in Hbl. apply Zis_gcd_mod;zarith. change ([|ah|] * wB + [|al|]) with (gen_to_Z w_digits w_to_Z 1 (WW ah al)). - rewrite <- (@spec_gen_modn1 w w_digits w_0 w_WW w_head0 w_add_mul_div - w_div21 w_to_Z spec_to_Z spec_w_0 spec_w_WW spec_head0 spec_add_mul_div - spec_div21 1 (WW ah al) bl Hbl). - apply spec_gcd_gt. rewrite spec_gen_modn1 with (w_WW := w_WW);trivial. + rewrite <- (@spec_gen_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div + w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 spec_add_mul_div + spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hbl). + apply spec_gcd_gt. + rewrite (@spec_gen_modn1 w w_digits w_zdigits w_0 w_WW); trivial. apply Zlt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. rewrite spec_w_0 in Hbl;Spec_w_to_Z bl;elimtype False;omega. @@ -1157,10 +1259,11 @@ Section GenDivGt. simpl;rewrite spec_w_0;simpl. rewrite spec_w_0 in Hml. apply Zis_gcd_mod;zarith. change ([|bh|] * wB + [|bl|]) with (gen_to_Z w_digits w_to_Z 1 (WW bh bl)). - rewrite <- (@spec_gen_modn1 w w_digits w_0 w_WW w_head0 w_add_mul_div - w_div21 w_to_Z spec_to_Z spec_w_0 spec_w_WW spec_head0 spec_add_mul_div - spec_div21 1 (WW bh bl) ml Hml). - apply spec_gcd_gt. rewrite spec_gen_modn1 with (w_WW := w_WW);trivial. + rewrite <- (@spec_gen_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div + w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 spec_add_mul_div + spec_div21 spec_compare spec_sub 1 (WW bh bl) ml Hml). + apply spec_gcd_gt. + rewrite (@spec_gen_modn1 w w_digits w_zdigits w_0 w_WW); trivial. apply Zlt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. rewrite spec_w_0 in Hml;Spec_w_to_Z ml;elimtype False;omega. diff --git a/theories/Ints/num/GenDivn1.v b/theories/Ints/num/GenDivn1.v index 4b54d825d..34b3b35e0 100644 --- a/theories/Ints/num/GenDivn1.v +++ b/theories/Ints/num/GenDivn1.v @@ -20,11 +20,16 @@ Section GENDIVN1. Variable w : Set. Variable w_digits : positive. + Variable w_zdigits : w. Variable w_0 : w. Variable w_WW : w -> w -> zn2z w. - Variable w_head0 : w -> N. - Variable w_add_mul_div : positive -> w -> w -> w. + Variable w_head0 : w -> w. + Variable w_add_mul_div : w -> w -> w -> w. Variable w_div21 : w -> w -> w -> w * w. + Variable w_compare : w -> w -> comparison. + Variable w_sub : w -> w -> w. + + (* ** For proofs ** *) Variable w_to_Z : w -> Z. @@ -37,22 +42,34 @@ Section GENDIVN1. Notation "[[ x ]]" := (zn2z_to_Z wB w_to_Z x) (at level 0, x at level 99). Variable spec_to_Z : forall x, 0 <= [| x |] < wB. + Variable spec_w_zdigits: [|w_zdigits|] = Zpos w_digits. Variable spec_0 : [|w_0|] = 0. Variable spec_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. Variable spec_head0 : forall x, 0 < [|x|] -> - wB/ 2 <= 2 ^ (Z_of_N (w_head0 x)) * [|x|] < wB. + wB/ 2 <= 2 ^ [|w_head0 x|] * [|x|] < wB. Variable spec_add_mul_div : forall x y p, - Zpos p < Zpos w_digits -> + [|p|] <= Zpos w_digits -> [| w_add_mul_div p x y |] = - ([|x|] * (Zpower 2 (Zpos p)) + - [|y|] / (Zpower 2 ((Zpos w_digits) - (Zpos p)))) mod wB. + ([|x|] * (2 ^ [|p|]) + + [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB. Variable spec_div21 : forall a1 a2 b, wB/2 <= [|b|] -> [|a1|] < [|b|] -> let (q,r) := w_div21 a1 a2 b in [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. + Variable spec_compare : + forall x y, + match w_compare x y with + | Eq => [|x|] = [|y|] + | Lt => [|x|] < [|y|] + | Gt => [|x|] > [|y|] + end. + Variable spec_sub: forall x y, + [|w_sub x y|] = ([|x|] - [|y|]) mod wB. + + Section DIVAUX. Variable b2p : w. Variable b2p_le : wB/2 <= [|b2p|]. @@ -117,13 +134,13 @@ Section GENDIVN1. rewrite IHn. destruct (gen_divn1_0 n rh hl);trivial. Qed. - Variable p : positive. - Variable p_bounded : Zpos p < Zpos w_digits. + Variable p : w. + Variable p_bounded : [|p|] <= Zpos w_digits. Lemma spec_add_mul_divp : forall x y, [| w_add_mul_div p x y |] = - ([|x|] * (Zpower 2 (Zpos p)) + - [|y|] / (Zpower 2 ((Zpos w_digits) - (Zpos p)))) mod wB. + ([|x|] * (2 ^ [|p|]) + + [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB. Proof. intros;apply spec_add_mul_div;auto. Qed. @@ -142,22 +159,26 @@ Section GENDIVN1. | S n => gen_divn1_p_aux n (gen_divn1_p n) end. - Lemma p_lt_gen_digits : forall n, Zpos p < Zpos (gen_digits w_digits n). + Lemma p_lt_gen_digits : forall n, [|p|] <= Zpos (gen_digits w_digits n). Proof. +(* induction n;simpl. destruct p_bounded;trivial. - assert (0 < Zpos p). unfold Zlt;reflexivity. - rewrite Zpos_xO;auto with zarith. + case (spec_to_Z p); rewrite Zpos_xO;auto with zarith. +*) + induction n;simpl. trivial. + case (spec_to_Z p); rewrite Zpos_xO;auto with zarith. Qed. Lemma spec_gen_divn1_p : forall n r h l, [|r|] < [|b2p|] -> let (q,r') := gen_divn1_p n r h l in [|r|] * gen_wB w_digits n + - ([!n|h!]*2^(Zpos p) + - [!n|l!] / (2^(Zpos(gen_digits w_digits n) - Zpos p))) + ([!n|h!]*2^[|p|] + + [!n|l!] / (2^(Zpos(gen_digits w_digits n) - [|p|]))) mod gen_wB w_digits n = [!n|q!] * [|b2p|] + [|r'|] /\ 0 <= [|r'|] < [|b2p|]. Proof. + case (spec_to_Z p); intros HH0 HH1. induction n;intros. unfold gen_divn1_p, gen_divn1_p_aux, gen_to_Z, gen_wB, gen_digits. rewrite <- spec_add_mul_divp. @@ -168,26 +189,26 @@ Section GENDIVN1. assert (H2 := spec_split n l);destruct (gen_split w_0 n l) as (lh,ll). rewrite H2. replace ([|r|] * (gen_wB w_digits n * gen_wB w_digits n) + - (([!n|hh!] * gen_wB w_digits n + [!n|hl!]) * 2 ^ Zpos p + + (([!n|hh!] * gen_wB w_digits n + [!n|hl!]) * 2 ^ [|p|] + ([!n|lh!] * gen_wB w_digits n + [!n|ll!]) / - 2^(Zpos (gen_digits w_digits (S n)) - Zpos p)) mod + 2^(Zpos (gen_digits w_digits (S n)) - [|p|])) mod (gen_wB w_digits n * gen_wB w_digits n)) with - (([|r|] * gen_wB w_digits n + ([!n|hh!] * 2^Zpos p + - [!n|hl!] / 2^(Zpos (gen_digits w_digits n) - Zpos p)) mod + (([|r|] * gen_wB w_digits n + ([!n|hh!] * 2^[|p|] + + [!n|hl!] / 2^(Zpos (gen_digits w_digits n) - [|p|])) mod gen_wB w_digits n) * gen_wB w_digits n + - ([!n|hl!] * 2^Zpos p + - [!n|lh!] / 2^(Zpos (gen_digits w_digits n) - Zpos p)) mod + ([!n|hl!] * 2^[|p|] + + [!n|lh!] / 2^(Zpos (gen_digits w_digits n) - [|p|])) mod gen_wB w_digits n). generalize (IHn r hh hl H);destruct (gen_divn1_p n r hh hl) as (qh,rh); intros (H3,H4);rewrite H3. assert ([|rh|] < [|b2p|]). omega. replace (([!n|qh!] * [|b2p|] + [|rh|]) * gen_wB w_digits n + - ([!n|hl!] * 2 ^ Zpos p + - [!n|lh!] / 2 ^ (Zpos (gen_digits w_digits n) - Zpos p)) mod + ([!n|hl!] * 2 ^ [|p|] + + [!n|lh!] / 2 ^ (Zpos (gen_digits w_digits n) - [|p|])) mod gen_wB w_digits n) with ([!n|qh!] * [|b2p|] *gen_wB w_digits n + ([|rh|]*gen_wB w_digits n + - ([!n|hl!] * 2 ^ Zpos p + - [!n|lh!] / 2 ^ (Zpos (gen_digits w_digits n) - Zpos p)) mod + ([!n|hl!] * 2 ^ [|p|] + + [!n|lh!] / 2 ^ (Zpos (gen_digits w_digits n) - [|p|])) mod gen_wB w_digits n)). 2:ring. generalize (IHn rh hl lh H0);destruct (gen_divn1_p n rh hl lh) as (ql,rl); intros (H5,H6);rewrite H5. @@ -205,32 +226,32 @@ Section GENDIVN1. rewrite Zdiv_shift_r;auto with zarith. 2:change (Zpos (gen_digits w_digits (S n))) with (2*Zpos (gen_digits w_digits n));auto with zarith. - replace (2 ^ (Zpos (gen_digits w_digits (S n)) - Zpos p)) with - (2^(Zpos (gen_digits w_digits n) - Zpos p)*2^Zpos (gen_digits w_digits n)). + replace (2 ^ (Zpos (gen_digits w_digits (S n)) - [|p|])) with + (2^(Zpos (gen_digits w_digits n) - [|p|])*2^Zpos (gen_digits w_digits n)). rewrite Zdiv_Zmult_compat_r;auto with zarith. - rewrite Zmult_plus_distr_l with (p:= 2^Zpos p). - pattern ([!n|hl!] * 2^Zpos p) at 2; - rewrite (shift_unshift_mod (Zpos(gen_digits w_digits n))(Zpos p)([!n|hl!])); + rewrite Zmult_plus_distr_l with (p:= 2^[|p|]). + pattern ([!n|hl!] * 2^[|p|]) at 2; + rewrite (shift_unshift_mod (Zpos(gen_digits w_digits n))([|p|])([!n|hl!])); auto with zarith. rewrite Zplus_assoc. replace - ([!n|hh!] * 2^Zpos (gen_digits w_digits n)* 2^Zpos p + - ([!n|hl!] / 2^(Zpos (gen_digits w_digits n)-Zpos p)* + ([!n|hh!] * 2^Zpos (gen_digits w_digits n)* 2^[|p|] + + ([!n|hl!] / 2^(Zpos (gen_digits w_digits n)-[|p|])* 2^Zpos(gen_digits w_digits n))) with - (([!n|hh!] *2^Zpos p + gen_to_Z w_digits w_to_Z n hl / - 2^(Zpos (gen_digits w_digits n)-Zpos p)) + (([!n|hh!] *2^[|p|] + gen_to_Z w_digits w_to_Z n hl / + 2^(Zpos (gen_digits w_digits n)-[|p|])) * 2^Zpos(gen_digits w_digits n));try (ring;fail). rewrite <- Zplus_assoc. - rewrite <- (Zmod_shift_r (Zpos p));auto with zarith. + rewrite <- (Zmod_shift_r ([|p|]));auto with zarith. replace (2 ^ Zpos (gen_digits w_digits n) * 2 ^ Zpos (gen_digits w_digits n)) with (2 ^ (Zpos (gen_digits w_digits n) + Zpos (gen_digits w_digits n))). rewrite (Zmod_shift_r (Zpos (gen_digits w_digits n)));auto with zarith. replace (2 ^ (Zpos (gen_digits w_digits n) + Zpos (gen_digits w_digits n))) with (2^Zpos(gen_digits w_digits n) *2^Zpos(gen_digits w_digits n)). - rewrite (Zmult_comm (([!n|hh!] * 2 ^ Zpos p + - [!n|hl!] / 2 ^ (Zpos (gen_digits w_digits n) - Zpos p)))). + rewrite (Zmult_comm (([!n|hh!] * 2 ^ [|p|] + + [!n|hl!] / 2 ^ (Zpos (gen_digits w_digits n) - [|p|])))). rewrite Zmod_Zmult_compat_l;auto with zarith. ring. rewrite Zpower_exp;auto with zarith. @@ -241,12 +262,11 @@ Section GENDIVN1. split;auto with zarith. apply Zdiv_lt_upper_bound;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos p + (Zpos (gen_digits w_digits n) - Zpos p)) with + replace ([|p|] + (Zpos (gen_digits w_digits n) - [|p|])) with (Zpos(gen_digits w_digits n));auto with zarith. - assert (0 < Zpos p). unfold Zlt;reflexivity. auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (gen_digits w_digits (S n)) - Zpos p) with - (Zpos (gen_digits w_digits n) - Zpos p + + replace (Zpos (gen_digits w_digits (S n)) - [|p|]) with + (Zpos (gen_digits w_digits n) - [|p|] + Zpos (gen_digits w_digits n));trivial. change (Zpos (gen_digits w_digits (S n))) with (2*Zpos (gen_digits w_digits n)). ring. @@ -275,14 +295,14 @@ Section GENDIVN1. End DIVAUX. - Fixpoint hight (n:nat) : word w n -> w := + Fixpoint high (n:nat) : word w n -> w := match n return word w n -> w with | O => fun a => a | S n => fun (a:zn2z (word w n)) => match a with | W0 => w_0 - | WW h l => hight n h + | WW h l => high n h end end. @@ -295,16 +315,16 @@ Section GENDIVN1. exact (refl_equal Lt). Qed. - Lemma spec_hight : forall n (x:word w n), - [|hight n x|] = [!n|x!] / 2^(Zpos (gen_digits w_digits n) - Zpos w_digits). + Lemma spec_high : forall n (x:word w n), + [|high n x|] = [!n|x!] / 2^(Zpos (gen_digits w_digits n) - Zpos w_digits). Proof. induction n;intros. - unfold hight,gen_digits,gen_to_Z. + unfold high,gen_digits,gen_to_Z. replace (Zpos w_digits - Zpos w_digits) with 0;try ring. simpl. rewrite <- (Zdiv_unique [|x|] 1 [|x|] 0);auto with zarith. assert (U2 := spec_gen_digits n). assert (U3 : 0 < Zpos w_digits). exact (refl_equal Lt). - destruct x;unfold hight;fold hight. + destruct x;unfold high;fold high. unfold gen_to_Z,zn2z_to_Z;rewrite spec_0. rewrite Zdiv_0;trivial. apply Zpower_lt_0;auto with zarith. @@ -330,16 +350,17 @@ Section GENDIVN1. Qed. Definition gen_divn1 (n:nat) (a:word w n) (b:w) := - match w_head0 b with - | N0 => gen_divn1_0 b n w_0 a - | Npos p => + let p := w_head0 b in + match w_compare p w_0 with + | Gt => let b2p := w_add_mul_div p b w_0 in - let ha := hight n a in - let k := Pminus w_digits p in + let ha := high n a in + let k := w_sub w_zdigits p in let lsr_n := w_add_mul_div k w_0 in let r0 := w_add_mul_div p w_0 ha in let (q,r) := gen_divn1_p b2p p n r0 a (gen_0 w_0 n) in (q, lsr_n r) + | _ => gen_divn1_0 b n w_0 a end. Lemma spec_gen_divn1 : forall n a b, @@ -349,131 +370,150 @@ Section GENDIVN1. 0 <= [|r|] < [|b|]. Proof. intros n a b H. unfold gen_divn1. - assert (H0 := spec_head0 H). - destruct (w_head0 b). - unfold Z_of_N, Zpower in H0. - rewrite Zmult_1_l in H0;destruct H0. - rewrite <- spec_0 in H. - assert (H2 := spec_gen_divn1_0 H0 n a H). - rewrite spec_0 in H2;rewrite Zmult_0_l in H2;rewrite Zplus_0_l in H2. - exact H2. - unfold Z_of_N in H0. - assert (HHHH : 0 < Zpos p). unfold Zlt;reflexivity. - assert (Zpos p < Zpos w_digits). - destruct (Z_lt_le_dec (Zpos p) (Zpos w_digits));trivial. - assert (2 ^ Zpos p < wB). - apply Zle_lt_trans with (2 ^ Zpos p * [|b|]);auto with zarith. - replace (2 ^ Zpos p) with (2^Zpos p * 1);try (ring;fail). + case (spec_head0 H); intros H0 H1. + case (spec_to_Z (w_head0 b)); intros HH1 HH2. + generalize (spec_compare (w_head0 b) w_0); case w_compare; + rewrite spec_0; intros H2; auto with zarith. + assert (Hv1: wB/2 <= [|b|]). + generalize H0; rewrite H2; rewrite Zpower_exp_0; + rewrite Zmult_1_l; auto. + assert (Hv2: [|w_0|] < [|b|]). + rewrite spec_0; auto. + generalize (spec_gen_divn1_0 Hv1 n a Hv2). + rewrite spec_0;rewrite Zmult_0_l; rewrite Zplus_0_l; auto. + contradict H2; auto with zarith. + assert (HHHH : 0 < [|w_head0 b|]); auto with zarith. + assert ([|w_head0 b|] < Zpos w_digits). + case (Zle_or_lt (Zpos w_digits) [|w_head0 b|]); auto; intros HH. + assert (2 ^ [|w_head0 b|] < wB). + apply Zle_lt_trans with (2 ^ [|w_head0 b|] * [|b|]);auto with zarith. + replace (2 ^ [|w_head0 b|]) with (2^[|w_head0 b|] * 1);try (ring;fail). apply Zmult_le_compat;auto with zarith. - assert (wB <= 2^Zpos p). + assert (wB <= 2^[|w_head0 b|]). unfold base;apply Zpower_le_monotone;auto with zarith. omega. - assert ([|w_add_mul_div p b w_0|] = 2 ^ Zpos p * [|b|]). - assert (H2 := spec_add_mul_div b w_0 H1). - rewrite spec_0 in H2;rewrite Zdiv_0 in H2; - rewrite Zplus_0_r in H2;rewrite Zmult_comm in H2. - rewrite Zmod_def_small in H2;auto with zarith. - apply Zpower_lt_0;auto with zarith. - destruct H0. - assert (H4 := spec_to_Z (hight n a)). + assert ([|w_add_mul_div (w_head0 b) b w_0|] = + 2 ^ [|w_head0 b|] * [|b|]). + rewrite (spec_add_mul_div b w_0); auto with zarith. + rewrite spec_0;rewrite Zdiv_0; try omega. + rewrite Zplus_0_r; rewrite Zmult_comm. + rewrite Zmod_def_small; auto with zarith. + apply Zpower_lt_0; try omega. + assert (H5 := spec_to_Z (high n a)). assert - ([|w_add_mul_div p w_0 (hight n a)|]<[|w_add_mul_div p b w_0|]). - rewrite H2. + ([|w_add_mul_div (w_head0 b) w_0 (high n a)|] + <[|w_add_mul_div (w_head0 b) b w_0|]). + rewrite H4. rewrite spec_add_mul_div;auto with zarith. rewrite spec_0;rewrite Zmult_0_l;rewrite Zplus_0_l. - assert (([|hight n a|]/2^(Zpos w_digits - Zpos p)) < wB). + assert (([|high n a|]/2^(Zpos w_digits - [|w_head0 b|])) < wB). apply Zdiv_lt_upper_bound;auto with zarith. apply Zlt_le_trans with wB;auto with zarith. pattern wB at 1;replace wB with (wB*1);try ring. apply Zmult_le_compat;auto with zarith. - assert (H5 := Zpower_lt_0 2 (Zpos w_digits - Zpos p)); + assert (H6 := Zpower_lt_0 2 (Zpos w_digits - [|w_head0 b|])); auto with zarith. rewrite Zmod_def_small;auto with zarith. apply Zdiv_lt_upper_bound;auto with zarith. apply Zlt_le_trans with wB;auto with zarith. - apply Zle_trans with (2 ^ Zpos p * [|b|] * 2). - rewrite <- wB_div_2;auto with zarith. + apply Zle_trans with (2 ^ [|w_head0 b|] * [|b|] * 2). + rewrite <- wB_div_2; try omega. apply Zmult_le_compat;auto with zarith. pattern 2 at 1;rewrite <- Zpower_exp_1. apply Zpower_le_monotone;split;auto with zarith. - rewrite <- H2 in H0. - assert (H6:= spec_gen_divn1_p H0 H1 n a (gen_0 w_0 n) H5). - destruct (gen_divn1_p (w_add_mul_div p b w_0) p n - (w_add_mul_div p w_0 (hight n a)) a + rewrite <- H4 in H0. + assert (Hb3: [|w_head0 b|] <= Zpos w_digits); auto with zarith. + assert (H7:= spec_gen_divn1_p H0 Hb3 n a (gen_0 w_0 n) H6). + destruct (gen_divn1_p (w_add_mul_div (w_head0 b) b w_0) (w_head0 b) n + (w_add_mul_div (w_head0 b) w_0 (high n a)) a (gen_0 w_0 n)) as (q,r). assert (U:= spec_gen_digits n). - rewrite spec_gen_0 in H6;trivial;rewrite Zdiv_0 in H6. - rewrite Zplus_0_r in H6. - rewrite spec_add_mul_div in H6;auto with zarith. - rewrite spec_0 in H6;rewrite Zmult_0_l in H6;rewrite Zplus_0_l in H6. - assert (([|hight n a|] / 2 ^ (Zpos w_digits - Zpos p)) mod wB - = [!n|a!] / 2^(Zpos (gen_digits w_digits n) - Zpos p)). + rewrite spec_gen_0 in H7;trivial;rewrite Zdiv_0 in H7. + rewrite Zplus_0_r in H7. + rewrite spec_add_mul_div in H7;auto with zarith. + rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7. + assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB + = [!n|a!] / 2^(Zpos (gen_digits w_digits n) - [|w_head0 b|])). rewrite Zmod_def_small;auto with zarith. - rewrite spec_hight. rewrite Zdiv_Zdiv;auto with zarith. + rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith. rewrite <- Zpower_exp;auto with zarith. replace (Zpos (gen_digits w_digits n) - Zpos w_digits + - (Zpos w_digits - Zpos p)) - with (Zpos (gen_digits w_digits n) - Zpos p);trivial;ring. - assert (H7 := Zpower_lt_0 2 (Zpos w_digits - Zpos p));auto with zarith. + (Zpos w_digits - [|w_head0 b|])) + with (Zpos (gen_digits w_digits n) - [|w_head0 b|]);trivial;ring. + assert (H8 := Zpower_lt_0 2 (Zpos w_digits - [|w_head0 b|]));auto with zarith. split;auto with zarith. - apply Zle_lt_trans with ([|hight n a|]);auto with zarith. + apply Zle_lt_trans with ([|high n a|]);auto with zarith. apply Zdiv_le_upper_bound;auto with zarith. - pattern ([|hight n a|]) at 1;rewrite <- Zmult_1_r. + pattern ([|high n a|]) at 1;rewrite <- Zmult_1_r. apply Zmult_le_compat;auto with zarith. - rewrite H7 in H6;unfold gen_wB,base in H6. - rewrite <- shift_unshift_mod in H6;auto with zarith. - rewrite H2 in H6. - assert ([|w_add_mul_div (w_digits - p) w_0 r|] = [|r|]/2^Zpos p). + rewrite H8 in H7;unfold gen_wB,base in H7. + rewrite <- shift_unshift_mod in H7;auto with zarith. + rewrite H4 in H7. + assert ([|w_add_mul_div (w_sub w_zdigits (w_head0 b)) w_0 r|] + = [|r|]/2^[|w_head0 b|]). rewrite spec_add_mul_div. rewrite spec_0;rewrite Zmult_0_l;rewrite Zplus_0_l. - replace (Zpos w_digits - Zpos (w_digits - p)) with (Zpos p). + replace (Zpos w_digits - [|w_sub w_zdigits (w_head0 b)|]) + with ([|w_head0 b|]). rewrite Zmod_def_small;auto with zarith. - assert (H8 := spec_to_Z r). + assert (H9 := spec_to_Z r). split;auto with zarith. apply Zle_lt_trans with ([|r|]);auto with zarith. apply Zdiv_le_upper_bound;auto with zarith. pattern ([|r|]) at 1;rewrite <- Zmult_1_r. apply Zmult_le_compat;auto with zarith. - assert (H9 := Zpower_lt_0 2 (Zpos p));auto with zarith. - rewrite Zpos_minus;auto with zarith. - rewrite Zpos_minus;auto with zarith. - destruct H6. + assert (H10 := Zpower_lt_0 2 ([|w_head0 b|]));auto with zarith. + rewrite spec_sub. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + case (spec_to_Z w_zdigits); auto with zarith. + rewrite spec_sub. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + case (spec_to_Z w_zdigits); auto with zarith. + case H7; intros H71 H72. split. - rewrite <- (Z_div_mult [!n|a!] (2^Zpos p));auto with zarith. - rewrite H8;rewrite H6. - replace ([!n|q!] * (2 ^ Zpos p * [|b|])) with ([!n|q!] *[|b|] * 2^Zpos p); + rewrite <- (Z_div_mult [!n|a!] (2^[|w_head0 b|]));auto with zarith. + rewrite H71;rewrite H9. + replace ([!n|q!] * (2 ^ [|w_head0 b|] * [|b|])) + with ([!n|q!] *[|b|] * 2^[|w_head0 b|]); try (ring;fail). rewrite Z_div_plus_l;auto with zarith. - assert (H10 := spec_to_Z (w_add_mul_div (w_digits - p) w_0 r));split; + assert (H10 := spec_to_Z + (w_add_mul_div (w_sub w_zdigits (w_head0 b)) w_0 r));split; auto with zarith. - rewrite H8. + rewrite H9. apply Zdiv_lt_upper_bound;auto with zarith. rewrite Zmult_comm;auto with zarith. exact (spec_gen_to_Z w_digits w_to_Z spec_to_Z n a). apply Zpower_lt_0;auto with zarith. Qed. + Definition gen_modn1 (n:nat) (a:word w n) (b:w) := - match w_head0 b with - | N0 => gen_modn1_0 b n w_0 a - | Npos p => + let p := w_head0 b in + match w_compare p w_0 with + | Gt => let b2p := w_add_mul_div p b w_0 in - let ha := hight n a in - let k := Pminus w_digits p in + let ha := high n a in + let k := w_sub w_zdigits p in let lsr_n := w_add_mul_div k w_0 in let r0 := w_add_mul_div p w_0 ha in let r := gen_modn1_p b2p p n r0 a (gen_0 w_0 n) in lsr_n r + | _ => gen_modn1_0 b n w_0 a end. Lemma spec_gen_modn1_aux : forall n a b, gen_modn1 n a b = snd (gen_divn1 n a b). Proof. intros n a b;unfold gen_divn1,gen_modn1. - destruct (w_head0 b). + generalize (spec_compare (w_head0 b) w_0); case w_compare; + rewrite spec_0; intros H2; auto with zarith. + apply spec_gen_modn1_0. apply spec_gen_modn1_0. rewrite spec_gen_modn1_p. - destruct (gen_divn1_p (w_add_mul_div p b w_0) p n - (w_add_mul_div p w_0 (hight n a)) a (gen_0 w_0 n));simpl;trivial. + destruct (gen_divn1_p (w_add_mul_div (w_head0 b) b w_0) (w_head0 b) n + (w_add_mul_div (w_head0 b) w_0 (high n a)) a (gen_0 w_0 n));simpl;trivial. Qed. Lemma spec_gen_modn1 : forall n a b, 0 < [|b|] -> diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v index 14aa86979..8b9271e32 100644 --- a/theories/Ints/num/GenLift.v +++ b/theories/Ints/num/GenLift.v @@ -12,6 +12,7 @@ Require Import ZArith. Require Import ZAux. Require Import ZPowerAux. Require Import ZDivModAux. +Require Import Zmod. Require Import Basic_type. Require Import GenBase. @@ -24,47 +25,54 @@ Section GenLift. Variable w_W0 : w -> zn2z w. Variable w_0W : w -> zn2z w. Variable w_compare : w -> w -> comparison. - Variable w_head0 : w -> N. - Variable w_add_mul_div : positive -> w -> w -> w. + Variable ww_compare : zn2z w -> zn2z w -> comparison. + Variable w_head0 : w -> w. + Variable w_add: w -> w -> zn2z w. + Variable w_add_mul_div : w -> w -> w -> w. + Variable ww_sub: zn2z w -> zn2z w -> zn2z w. Variable w_digits : positive. Variable ww_Digits : positive. + Variable w_zdigits : w. + Variable ww_zdigits : zn2z w. + Variable low: zn2z w -> w. Definition ww_head0 x := match x with - | W0 => Npos ww_Digits + | W0 => ww_zdigits | WW xh xl => match w_compare w_0 xh with - | Eq => Nplus (Npos w_digits) (w_head0 xl) - | _ => w_head0 xh + | Eq => w_add w_zdigits (w_head0 xl) + | _ => w_0W (w_head0 xh) end end. (* 0 < p < ww_digits *) Definition ww_add_mul_div p x y := + let zdigits := w_0W w_zdigits in match x, y with | W0, W0 => W0 | W0, WW yh yl => - match Pcompare p w_digits Eq with + match ww_compare p zdigits with | Eq => w_0W yh - | Lt => w_0W (w_add_mul_div p w_0 yh) + | Lt => w_0W (w_add_mul_div (low p) w_0 yh) | Gt => - let n := Pminus p w_digits in + let n := low (ww_sub p zdigits) in w_WW (w_add_mul_div n w_0 yh) (w_add_mul_div n yh yl) end | WW xh xl, W0 => - match Pcompare p w_digits Eq with + match ww_compare p zdigits with | Eq => w_W0 xl - | Lt => w_WW (w_add_mul_div p xh xl) (w_add_mul_div p xl w_0) + | Lt => w_WW (w_add_mul_div (low p) xh xl) (w_add_mul_div (low p) xl w_0) | Gt => - let n := Pminus p w_digits in + let n := low (ww_sub p zdigits) in w_W0 (w_add_mul_div n xl w_0) end | WW xh xl, WW yh yl => - match Pcompare p w_digits Eq with + match ww_compare p zdigits with | Eq => w_WW xl yh - | Lt => w_WW (w_add_mul_div p xh xl) (w_add_mul_div p xl yh) + | Lt => w_WW (w_add_mul_div (low p) xh xl) (w_add_mul_div (low p) xl yh) | Gt => - let n := Pminus p w_digits in + let n := low (ww_sub p zdigits) in w_WW (w_add_mul_div n xl yh) (w_add_mul_div n yh yl) end end. @@ -79,6 +87,7 @@ Section GenLift. Variable spec_w_0 : [|w_0|] = 0. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. + Variable spec_to_w_Z : forall x, 0 <= [[x]] < wwB. Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. @@ -88,47 +97,60 @@ Section GenLift. | Lt => [|x|] < [|y|] | Gt => [|x|] > [|y|] end. + Variable spec_ww_compare : forall x y, + match ww_compare x y with + | Eq => [[x]] = [[y]] + | Lt => [[x]] < [[y]] + | Gt => [[x]] > [[y]] + end. Variable spec_ww_digits : ww_Digits = xO w_digits. Variable spec_w_head0 : forall x, 0 < [|x|] -> - wB/ 2 <= 2 ^ (Z_of_N (w_head0 x)) * [|x|] < wB. + wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB. Variable spec_w_add_mul_div : forall x y p, - Zpos p < Zpos w_digits -> + [|p|] <= Zpos w_digits -> [| w_add_mul_div p x y |] = - ([|x|] * (Zpower 2 (Zpos p)) + - [|y|] / (Zpower 2 ((Zpos w_digits) - (Zpos p)))) mod wB. + ([|x|] * (2 ^ [|p|]) + + [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB. + Variable spec_w_add: forall x y, + [[w_add x y]] = [|x|] + [|y|]. + Variable spec_ww_sub: forall x y, + [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB. + + Variable spec_zdigits : [| w_zdigits |] = Zpos w_digits. + Variable spec_low: forall x, [| low x|] = [[x]] mod wB. Hint Resolve div_le_0 div_lt w_to_Z_wwB: lift. Ltac zarith := auto with zarith lift. Lemma spec_ww_head0 : forall x, 0 < [[x]] -> - wwB/ 2 <= 2 ^ (Z_of_N (ww_head0 x)) * [[x]] < wwB. + wwB/ 2 <= 2 ^ [[ww_head0 x]] * [[x]] < wwB. Proof. rewrite wwB_div_2;rewrite Zmult_comm;rewrite wwB_wBwB. assert (U:= lt_0_wB w_digits); destruct x as [ |xh xl];simpl ww_to_Z;intros H. unfold Zlt in H;discriminate H. assert (H0 := spec_compare w_0 xh);rewrite spec_w_0 in H0. - simpl Z_of_N; destruct (w_compare w_0 xh). + destruct (w_compare w_0 xh). rewrite <- H0. simpl Zplus. rewrite <- H0 in H;simpl in H. - generalize (spec_w_head0 H);destruct (w_head0 xl) as [ |q]. - intros H1;simpl Zpower in H1;rewrite Zmult_1_l in H1. - change (2 ^ Z_of_N (Npos w_digits)) with wB;split;zarith. - rewrite Zpower_2; apply Zmult_lt_compat_l;zarith. - unfold Z_of_N;intros. - change (Zpos(w_digits + q))with (Zpos w_digits + Zpos q);rewrite Zpower_exp. - fold wB;rewrite <- Zmult_assoc;split;zarith. - rewrite Zpower_2; apply Zmult_lt_compat_l;zarith. - intro H2;discriminate H2. intro H2;discriminate H2. + case (spec_to_Z w_zdigits); + case (spec_to_Z (w_head0 xl)); intros HH1 HH2 HH3 HH4. + rewrite spec_w_add. + rewrite spec_zdigits; rewrite Zpower_exp; auto with zarith. + case (spec_w_head0 H); intros H1 H2. + rewrite Zpower_2; fold wB; rewrite <- Zmult_assoc; split. + apply Zmult_le_compat_l; auto with zarith. + apply Zmult_lt_compat_l; auto with zarith. assert (H1 := spec_w_head0 H0). + rewrite spec_w_0W. split. rewrite Zmult_plus_distr_r;rewrite Zmult_assoc. - apply Zle_trans with (2 ^ Z_of_N (w_head0 xh) * [|xh|] * wB). - rewrite Zmult_comm;zarith. - assert (0 <= 2 ^ Z_of_N (w_head0 xh) * [|xl|]);zarith. + apply Zle_trans with (2 ^ [|w_head0 xh|] * [|xh|] * wB). + rewrite Zmult_comm; zarith. + assert (0 <= 2 ^ [|w_head0 xh|] * [|xl|]);zarith. assert (H2:=spec_to_Z xl);apply Zmult_le_0_compat;zarith. - assert (0<= Z_of_N (w_head0 xh)). - case (w_head0 xh);intros;simpl;intro H2;discriminate H2. - generalize (Z_of_N (w_head0 xh)) H1 H2;clear H1 H2;intros p H1 H2. + case (spec_to_Z (w_head0 xh)); intros H2 _. + generalize ([|w_head0 xh|]) H1 H2;clear H1 H2; + intros p H1 H2. assert (Eq1 : 2^p < wB). rewrite <- (Zmult_1_r (2^p));apply Zle_lt_trans with (2^p*[|xh|]);zarith. assert (Eq2: p < Zpos w_digits). @@ -150,59 +172,62 @@ Section GenLift. (wB_div w_digits w_to_Z spec_to_Z) (wB_div_plus w_digits w_to_Z spec_to_Z) : w_rewrite. Ltac w_rewrite := autorewrite with w_rewrite;trivial. - + Lemma spec_ww_add_mul_div_aux : forall xh xl yh yl p, - Zpos p < Zpos (xO w_digits) -> - [[match (p ?= w_digits)%positive Eq with + let zdigits := w_0W w_zdigits in + [[p]] <= Zpos (xO w_digits) -> + [[match ww_compare p zdigits with | Eq => w_WW xl yh - | Lt => w_WW (w_add_mul_div p xh xl) (w_add_mul_div p xl yh) + | Lt => w_WW (w_add_mul_div (low p) xh xl) + (w_add_mul_div (low p) xl yh) | Gt => - let n := (p - w_digits)%positive in + let n := low (ww_sub p zdigits) in w_WW (w_add_mul_div n xl yh) (w_add_mul_div n yh yl) end]] = - ([[WW xh xl]] * (2^Zpos p) + - [[WW yh yl]] / (2^(Zpos (xO w_digits) - Zpos p))) mod wwB. + ([[WW xh xl]] * (2^[[p]]) + + [[WW yh yl]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB. Proof. - intros xh xl yh yl p;assert (HwwB := wwB_pos w_digits). - assert (0 < Zpos p). unfold Zlt;reflexivity. + intros xh xl yh yl p zdigits;assert (HwwB := wwB_pos w_digits). + case (spec_to_w_Z p); intros Hv1 Hv2. replace (Zpos (xO w_digits)) with (Zpos w_digits + Zpos w_digits). 2 : rewrite Zpos_xO;ring. - replace (Zpos w_digits + Zpos w_digits - Zpos p) with - (Zpos w_digits + (Zpos w_digits - Zpos p)). 2:ring. + replace (Zpos w_digits + Zpos w_digits - [[p]]) with + (Zpos w_digits + (Zpos w_digits - [[p]])). 2:ring. intros Hp; assert (Hxh := spec_to_Z xh);assert (Hxl:=spec_to_Z xl); assert (Hx := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh xl)); simpl in Hx;assert (Hyh := spec_to_Z yh);assert (Hyl:=spec_to_Z yl); assert (Hy:=spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW yh yl));simpl in Hy. - case_eq ((p ?= w_digits)%positive Eq);intros;w_rewrite; - match goal with - | [H: (p ?= w_digits)%positive Eq = Eq |- _] => - let H1:= fresh "H" in - (assert (H1 : Zpos p = Zpos w_digits); - [ rewrite Pcompare_Eq_eq with (1:= H);trivial - | rewrite H1;try rewrite Zminus_diag;try rewrite Zplus_0_r]); - fold wB - | [H: (p ?= w_digits)%positive Eq = Lt |- _] => - change ((p ?= w_digits)%positive Eq = Lt) with - (Zpos p < Zpos w_digits) in H; - repeat rewrite spec_w_add_mul_div;zarith - | [H: (p ?= w_digits)%positive Eq = Gt |- _] => - change ((p ?= w_digits)%positive Eq=Gt)with(Zpos p > Zpos w_digits) in H; - let H1 := fresh "H" in - assert (H1 := Zpos_minus _ _ (Zgt_lt _ _ H)); - replace (Zpos w_digits + (Zpos w_digits - Zpos p)) with - (Zpos w_digits - Zpos (p - w_digits)); - [ repeat rewrite spec_w_add_mul_div;zarith - | zarith ] - | _ => idtac - end;simpl ww_to_Z;w_rewrite;zarith. + generalize (spec_ww_compare p zdigits); case ww_compare; intros H1. + rewrite H1; unfold zdigits; rewrite spec_w_0W. + rewrite spec_zdigits; rewrite Zminus_diag; rewrite Zplus_0_r. + simpl ww_to_Z; w_rewrite;zarith. + fold wB. rewrite Zmult_plus_distr_l;rewrite <- Zmult_assoc;rewrite <- Zplus_assoc. rewrite <- Zpower_2. rewrite <- wwB_wBwB;apply Zmod_unique with [|xh|]. apply lt_0_wwB. exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xl yh)). ring. + simpl ww_to_Z; w_rewrite;zarith. + assert (HH0: [|low p|] = [[p]]). + rewrite spec_low. + apply Zmod_def_small. + case (spec_to_w_Z p); intros HH1 HH2; split; auto. + generalize H1; unfold zdigits; rewrite spec_w_0W; + rewrite spec_zdigits; intros tmp. + apply Zlt_le_trans with (1 := tmp). + unfold base. + apply Zpower2_le_lin; auto with zarith. + 2: generalize H1; unfold zdigits; rewrite spec_w_0W; + rewrite spec_zdigits; auto with zarith. + generalize H1; unfold zdigits; rewrite spec_w_0W; + rewrite spec_zdigits; auto; clear H1; intros H1. + assert (HH: [|low p|] <= Zpos w_digits). + rewrite HH0; auto with zarith. + repeat rewrite spec_w_add_mul_div with (1 := HH). + rewrite HH0. rewrite Zmult_plus_distr_l. - pattern ([|xl|] * 2 ^ Zpos p) at 2; + pattern ([|xl|] * 2 ^ [[p]]) at 2; rewrite shift_unshift_mod with (n:= Zpos w_digits);fold wB;zarith. - replace ([|xh|] * wB * 2^Zpos p) with ([|xh|] * 2^Zpos p * wB). 2:ring. + replace ([|xh|] * wB * 2^[[p]]) with ([|xh|] * 2^[[p]] * wB). 2:ring. rewrite Zplus_assoc;rewrite <- Zmult_plus_distr_l. rewrite <- Zplus_assoc. unfold base at 5;rewrite <- Zmod_shift_r;zarith. unfold base;rewrite Zmod_shift_r with (b:= Zpos (ww_digits w_digits)); @@ -211,14 +236,40 @@ Section GenLift. unfold ww_digits;rewrite Zpos_xO;zarith. apply Z_mod_lt;zarith. split;zarith. apply Zdiv_lt_upper_bound;zarith. rewrite <- Zpower_exp;zarith. - ring_simplify (Zpos p + (Zpos w_digits - Zpos p));fold wB;zarith. + ring_simplify ([[p]] + (Zpos w_digits - [[p]]));fold wB;zarith. + assert (Hv: [[p]] > Zpos w_digits). + generalize H1; clear H1. + unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits; auto. + clear H1. + assert (HH0: [|low (ww_sub p zdigits)|] = [[p]] - Zpos w_digits). + rewrite spec_low. + rewrite spec_ww_sub. + unfold zdigits; rewrite spec_w_0W; rewrite spec_zdigits. + rewrite <- Zmod_div_mod; auto with zarith. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + apply Zle_lt_trans with (Zpos w_digits); auto with zarith. + unfold base; apply Zpower2_lt_lin; auto with zarith. + exists wB; unfold base. + unfold ww_digits; rewrite (Zpos_xO w_digits). + rewrite <- Zpower_exp; auto with zarith. + apply f_equal with (f := fun x => 2 ^ x); auto with zarith. + assert (HH: [|low (ww_sub p zdigits)|] <= Zpos w_digits). + rewrite HH0; auto with zarith. + replace (Zpos w_digits + (Zpos w_digits - [[p]])) with + (Zpos w_digits - ([[p]] - Zpos w_digits)); zarith. + lazy zeta; simpl ww_to_Z; w_rewrite;zarith. + repeat rewrite spec_w_add_mul_div;zarith. + rewrite HH0. pattern wB at 5;replace wB with - (2^(Zpos (p - w_digits) + (Zpos w_digits - Zpos (p - w_digits)))). + (2^(([[p]] - Zpos w_digits) + + (Zpos w_digits - ([[p]] - Zpos w_digits)))). rewrite Zpower_exp;zarith. rewrite Zmult_assoc. rewrite Z_div_plus_l;zarith. - rewrite shift_unshift_mod with (a:= [|yh|]) (p:= Zpos (p - w_digits)) + rewrite shift_unshift_mod with (a:= [|yh|]) (p:= [[p]] - Zpos w_digits) (n := Zpos w_digits);zarith. fold wB. - replace (Zpos p) with (Zpos (p - w_digits) + Zpos w_digits);zarith. + set (u := [[p]] - Zpos w_digits). + replace [[p]] with (u + Zpos w_digits);zarith. rewrite Zpower_exp;zarith. rewrite Zmult_assoc. fold wB. repeat rewrite Zplus_assoc. rewrite <- Zmult_plus_distr_l. repeat rewrite <- Zplus_assoc. @@ -228,30 +279,36 @@ Section GenLift. (b:= Zpos w_digits);fold wB;fold wwB;zarith. rewrite wwB_wBwB; rewrite Zpower_2; rewrite Zmult_mod_distr_r;zarith. rewrite Zmult_plus_distr_l. - replace ([|xh|] * wB * 2 ^ Zpos (p - w_digits)) with - ([|xh|]*2^Zpos(p - w_digits)*wB). 2:ring. + replace ([|xh|] * wB * 2 ^ u) with + ([|xh|]*2^u*wB). 2:ring. repeat rewrite <- Zplus_assoc. - rewrite (Zplus_comm ([|xh|] * 2 ^ Zpos (p - w_digits) * wB)). + rewrite (Zplus_comm ([|xh|] * 2 ^ u * wB)). rewrite Z_mod_plus;zarith. rewrite Zmod_mult_0;zarith. unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith. - split;zarith. apply Zdiv_lt_upper_bound;zarith. - rewrite <- Zpower_exp;zarith. - ring_simplify (Zpos (p - w_digits) + (Zpos w_digits - Zpos (p - w_digits))); fold + unfold u; split;zarith. + split;zarith. unfold u; apply Zdiv_lt_upper_bound;zarith. + rewrite <- Zpower_exp;zarith. + fold u. + ring_simplify (u + (Zpos w_digits - u)); fold wB;zarith. unfold ww_digits;rewrite Zpos_xO;zarith. unfold base;rewrite <- Zmod_shift_r;zarith. fold base;apply Z_mod_lt;zarith. - split;zarith. apply Zdiv_lt_upper_bound;zarith. - rewrite <- Zpower_exp;zarith. - ring_simplify (Zpos (p - w_digits) + (Zpos w_digits - Zpos (p - w_digits))); fold - wB;zarith. - ring_simplify (Zpos (p - w_digits) + (Zpos w_digits - Zpos (p - w_digits))); fold - wB;trivial. + unfold u; split;zarith. + unfold u; split;zarith. + apply Zdiv_lt_upper_bound;zarith. + rewrite <- Zpower_exp;zarith. + fold u. + ring_simplify (u + (Zpos w_digits - u)); fold wB; auto with zarith. + unfold u;zarith. + unfold u;zarith. + set (u := [[p]] - Zpos w_digits). + ring_simplify (u + (Zpos w_digits - u)); fold wB; auto with zarith. Qed. Lemma spec_ww_add_mul_div : forall x y p, - Zpos p < Zpos (xO w_digits) -> + [[p]] <= Zpos (xO w_digits) -> [[ ww_add_mul_div p x y ]] = - ([[x]] * (2^Zpos p) + - [[y]] / (2^(Zpos (xO w_digits) - Zpos p))) mod wwB. + ([[x]] * (2^[[p]]) + + [[y]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB. Proof. intros x y p H. destruct x as [ |xh xl]; @@ -261,15 +318,40 @@ Section GenLift. [generalize (H1 w_0 w_0 p H) | generalize (H1 yh yl p H)]; clear H1;w_rewrite);simpl ww_add_mul_div. replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial]. - intros Heq;rewrite <- Heq;clear Heq. - case_eq ((p ?= w_digits)%positive Eq);w_rewrite;intros;trivial. + intros Heq;rewrite <- Heq;clear Heq; auto. + generalize (spec_ww_compare p (w_0W w_zdigits)); + case ww_compare; intros H1; w_rewrite. rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith. + generalize H1; w_rewrite; rewrite spec_zdigits; clear H1; intros H1. + assert (HH0: [|low p|] = [[p]]). + rewrite spec_low. + apply Zmod_def_small. + case (spec_to_w_Z p); intros HH1 HH2; split; auto. + apply Zlt_le_trans with (1 := H1). + unfold base; apply Zpower2_le_lin; auto with zarith. + rewrite HH0; auto with zarith. replace [[WW w_0 w_0]] with 0;[w_rewrite|simpl;w_rewrite;trivial]. intros Heq;rewrite <- Heq;clear Heq. - case_eq ((p ?= w_digits)%positive Eq);w_rewrite;intros;trivial. + generalize (spec_ww_compare p (w_0W w_zdigits)); + case ww_compare; intros H1; w_rewrite. rewrite (spec_w_add_mul_div w_0 w_0);w_rewrite;zarith. - change ((p ?= w_digits)%positive Eq = Gt)with(Zpos p > Zpos w_digits) in H0. - rewrite Zpos_minus;zarith. rewrite Zpos_xO in H;zarith. + rewrite Zpos_xO in H;zarith. + assert (HH: [|low (ww_sub p (w_0W w_zdigits)) |] = [[p]] - Zpos w_digits). + generalize H1; clear H1. + rewrite spec_low. + rewrite spec_ww_sub; w_rewrite; intros H1. + rewrite <- Zmod_div_mod; auto with zarith. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + apply Zle_lt_trans with (Zpos w_digits); auto with zarith. + unfold base; apply Zpower2_lt_lin; auto with zarith. + unfold base; auto with zarith. + unfold base; auto with zarith. + exists wB; unfold base. + unfold ww_digits; rewrite (Zpos_xO w_digits). + rewrite <- Zpower_exp; auto with zarith. + apply f_equal with (f := fun x => 2 ^ x); auto with zarith. + case (spec_to_Z xh); auto with zarith. Qed. End GenProof. diff --git a/theories/Ints/num/GenSqrt.v b/theories/Ints/num/GenSqrt.v index 074f7eb53..3d1bb6a24 100644 --- a/theories/Ints/num/GenSqrt.v +++ b/theories/Ints/num/GenSqrt.v @@ -11,6 +11,7 @@ Set Implicit Arguments. Require Import ZArith. Require Import ZAux. Require Import ZDivModAux. +Require Import ZPowerAux. Require Import Basic_type. Require Import GenBase. @@ -30,18 +31,22 @@ Section GenSqrt. Variable w_sub_c : w -> w -> carry w. Variable w_square_c : w -> zn2z w. Variable w_div21 : w -> w -> w -> w * w. - Variable w_add_mul_div : positive -> w -> w -> w. + Variable w_add_mul_div : w -> w -> w -> w. Variable w_digits : positive. + Variable w_zdigits : w. + Variable ww_zdigits : zn2z w. Variable w_add_c : w -> w -> carry w. Variable w_sqrt2 : w -> w -> w * carry w. + Variable w_pred : w -> w. Variable ww_pred_c : zn2z w -> carry (zn2z w). Variable ww_pred : zn2z w -> zn2z w. Variable ww_add_c : zn2z w -> zn2z w -> carry (zn2z w). Variable ww_add : zn2z w -> zn2z w -> zn2z w. Variable ww_sub_c : zn2z w -> zn2z w -> carry (zn2z w). - Variable ww_add_mul_div : positive -> zn2z w -> zn2z w -> zn2z w. - Variable ww_head0 : zn2z w -> N. + Variable ww_add_mul_div : zn2z w -> zn2z w -> zn2z w -> zn2z w. + Variable ww_head0 : zn2z w -> zn2z w. Variable ww_compare : zn2z w -> zn2z w -> comparison. + Variable low : zn2z w -> w. Let wwBm1 := ww_Bm1 w_Bm1. @@ -76,28 +81,28 @@ Section GenSqrt. match q with C0 q1 => if w_is_even q1 then - (C0 (w_add_mul_div (w_digits - 1) w_1 q1), C0 r) + (C0 (w_add_mul_div (w_pred w_zdigits) w_1 q1), C0 r) else - (C0 (w_add_mul_div (w_digits - 1) w_1 q1), w_add_c r s) + (C0 (w_add_mul_div (w_pred w_zdigits) w_1 q1), w_add_c r s) | C1 q1 => if w_is_even q1 then - (C1 (w_add_mul_div (w_digits - 1) w_0 q1), C0 r) + (C1 (w_add_mul_div (w_pred w_zdigits) w_0 q1), C0 r) else - (C1 (w_add_mul_div (w_digits - 1) w_0 q1), w_add_c r s) + (C1 (w_add_mul_div (w_pred w_zdigits) w_0 q1), w_add_c r s) end | C0 x1 => let (q, r) := w_div21c x1 y s in match q with C0 q1 => if w_is_even q1 then - (C0 (w_add_mul_div (w_digits - 1) w_0 q1), C0 r) + (C0 (w_add_mul_div (w_pred w_zdigits) w_0 q1), C0 r) else - (C0 (w_add_mul_div (w_digits - 1) w_0 q1), w_add_c r s) + (C0 (w_add_mul_div (w_pred w_zdigits) w_0 q1), w_add_c r s) | C1 q1 => if w_is_even q1 then - (C0 (w_add_mul_div (w_digits - 1) w_1 q1), C0 r) + (C0 (w_add_mul_div (w_pred w_zdigits) w_1 q1), C0 r) else - (C0 (w_add_mul_div (w_digits - 1) w_1 q1), w_add_c r s) + (C0 (w_add_mul_div (w_pred w_zdigits) w_1 q1), w_add_c r s) end end. @@ -126,7 +131,7 @@ Section GenSqrt. match ww_sub_c (WW r2 y2) q2 with C0 r3 => (a, C0 r3) | C1 r3 => - let a2 := ww_add_mul_div 1 a W0 in + let a2 := ww_add_mul_div (w_0W w_1) a W0 in match ww_pred_c a2 with C0 a3 => (ww_pred a, ww_add_c a3 r3) @@ -137,7 +142,7 @@ Section GenSqrt. end | C1 q1 => let a1 := WW q w_Bm1 in - let a2 := ww_add_mul_div 1 a1 wwBm1 in + let a2 := ww_add_mul_div (w_0W w_1) a1 wwBm1 in (a1, ww_add_c a2 y) end. @@ -148,28 +153,28 @@ Section GenSqrt. end. Definition ww_head1 x := - match ww_head0 x with - N0 => N0 - | Npos xH => N0 - | Npos (xO _) as U => U - | Npos (xI V) => Npos (xO V) - end. + let p := ww_head0 x in + if (ww_is_even p) then p else ww_pred p. Definition ww_sqrt x := if (ww_is_zero x) then W0 else - match (ww_head1 x) with - N0 => - match x with - W0 => W0 - | WW x1 x2 => WW w_0 (fst (w_sqrt2 x1 x2)) - end - | Npos p => + let p := ww_head1 x in + match ww_compare p W0 with + | Gt => match ww_add_mul_div p x W0 with W0 => W0 | WW x1 x2 => let (r, _) := w_sqrt2 x1 x2 in - WW w_0 (w_add_mul_div (w_digits - (Pdiv2 p)) w_0 r) + WW w_0 (w_add_mul_div + (w_sub w_zdigits + (low (ww_add_mul_div (ww_pred ww_zdigits) + W0 p))) w_0 r) + end + | _ => + match x with + W0 => W0 + | WW x1 x2 => WW w_0 (fst (w_sqrt2 x1 x2)) end end. @@ -201,8 +206,10 @@ Section GenSqrt. Variable spec_w_0 : [|w_0|] = 0. Variable spec_w_1 : [|w_1|] = 1. Variable spec_w_Bm1 : [|w_Bm1|] = wB - 1. - + Variable spec_w_zdigits : [|w_zdigits|] = Zpos w_digits. + Variable spec_ww_zdigits : [[ww_zdigits]] = Zpos (xO w_digits). Variable spec_to_Z : forall x, 0 <= [|x|] < wB. + Variable spec_to_w_Z : forall x, 0 <= [[x]] < wwB. Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. Variable spec_w_W0 : forall h, [[w_W0 h]] = [|h|] * wB. @@ -224,15 +231,15 @@ Section GenSqrt. [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Variable spec_w_add_mul_div : forall x y p, - Zpos p < Zpos w_digits -> + [|p|] <= Zpos w_digits -> [| w_add_mul_div p x y |] = - ([|x|] * (Zpower 2 (Zpos p)) + - [|y|] / (Zpower 2 ((Zpos w_digits) - (Zpos p)))) mod wB. + ([|x|] * (2 ^ [|p|]) + + [|y|] / (Zpower 2 ((Zpos w_digits) - [|p|]))) mod wB. Variable spec_ww_add_mul_div : forall x y p, - Zpos p < Zpos (xO w_digits) -> + [[p]] <= Zpos (xO w_digits) -> [[ ww_add_mul_div p x y ]] = - ([[x]] * (2^ Zpos p) + - [[y]] / (2^ (Zpos (xO w_digits) - Zpos p))) mod wwB. + ([[x]] * (2^ [[p]]) + + [[y]] / (2^ (Zpos (xO w_digits) - [[p]]))) mod wwB. Variable spec_w_add_c : forall x y, [+|w_add_c x y|] = [|x|] + [|y|]. Variable spec_ww_add : forall x y, [[ww_add x y]] = ([[x]] + [[y]]) mod wwB. Variable spec_w_sqrt2 : forall x y, @@ -242,6 +249,7 @@ Section GenSqrt. [+|r|] <= 2 * [|s|]. Variable spec_ww_sub_c : forall x y, [-[ww_sub_c x y]] = [[x]] - [[y]]. Variable spec_ww_pred_c : forall x, [-[ww_pred_c x]] = [[x]] - 1. + Variable spec_pred : forall x, [|w_pred x|] = ([|x|] - 1) mod wB. Variable spec_ww_pred : forall x, [[ww_pred x]] = ([[x]] - 1) mod wwB. Variable spec_ww_add_c : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]]. Variable spec_ww_compare : forall x y, @@ -251,7 +259,8 @@ Section GenSqrt. | Gt => [[x]] > [[y]] end. Variable spec_ww_head0 : forall x, 0 < [[x]] -> - wwB/ 2 <= 2 ^ (Z_of_N (ww_head0 x)) * [[x]] < wwB. + wwB/ 2 <= 2 ^ [[ww_head0 x]] * [[x]] < wwB. + Variable spec_low: forall x, [|low x|] = [[x]] mod wB. Let spec_ww_Bm1 : [[wwBm1]] = wwB - 1. Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed. @@ -351,8 +360,14 @@ Section GenSqrt. Hypothesis more_than_one_bit: 1 < Zpos w_digits. Theorem add_mult_div_2: forall w, - [|w_add_mul_div (w_digits - 1) w_0 w|] = [|w|] / 2. + [|w_add_mul_div (w_pred w_zdigits) w_0 w|] = [|w|] / 2. intros w1. + assert (Hp: [|w_pred w_zdigits|] = Zpos w_digits - 1). + rewrite spec_pred; rewrite spec_w_zdigits. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + apply Zlt_le_trans with (Zpos w_digits); auto with zarith. + unfold base; apply Zpower2_le_lin; auto with zarith. rewrite spec_w_add_mul_div; auto with zarith. autorewrite with w_rewrite rm10. match goal with |- context[?X - ?Y] => @@ -361,19 +376,25 @@ Section GenSqrt. rewrite Zpower_exp_1; rewrite Zmod_def_small; auto with zarith. destruct (spec_to_Z w1) as [H1 H2];auto with zarith. split; auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. - rewrite Zpos_minus; auto with zarith. - rewrite Zpos_minus; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + rewrite Hp; ring. Qed. Theorem add_mult_div_2_plus_1: forall w, - [|w_add_mul_div (w_digits - 1) w_1 w|] = + [|w_add_mul_div (w_pred w_zdigits) w_1 w|] = [|w|] / 2 + 2 ^ Zpos (w_digits - 1). intros w1. + assert (Hp: [|w_pred w_zdigits|] = Zpos w_digits - 1). + rewrite spec_pred; rewrite spec_w_zdigits. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + apply Zlt_le_trans with (Zpos w_digits); auto with zarith. + unfold base; apply Zpower2_le_lin; auto with zarith. autorewrite with w_rewrite rm10; auto with zarith. match goal with |- context[?X - ?Y] => replace (X - Y) with 1 - end. + end; rewrite Hp; try ring. + rewrite Zpos_minus; auto with zarith. rewrite Zpower_exp_1; rewrite Zmod_def_small; auto with zarith. destruct (spec_to_Z w1) as [H1 H2];auto with zarith. split; auto with zarith. @@ -383,7 +404,8 @@ Section GenSqrt. rewrite <- (tmp X); clear tmp end. rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith. - rewrite Zpos_minus; auto with zarith. + assert (tmp: forall p, 1 + (p -1) - 1 = p - 1); auto with zarith; + rewrite tmp; clear tmp; auto with zarith. match goal with |- ?X + ?Y < _ => assert (Y < X); auto with zarith end. @@ -392,12 +414,10 @@ Section GenSqrt. auto with zarith. assert (tmp: forall p, (p - 1) + 1 = p); auto with zarith; rewrite tmp; clear tmp; auto with zarith. - rewrite Zpos_minus; auto with zarith. - rewrite Zpos_minus; auto with zarith. Qed. Theorem add_mult_mult_2: forall w, - [|w_add_mul_div 1 w w_0|] = 2 * [|w|] mod wB. + [|w_add_mul_div w_1 w w_0|] = 2 * [|w|] mod wB. intros w1. autorewrite with w_rewrite rm10; auto with zarith. rewrite Zpower_exp_1; auto with zarith. @@ -405,19 +425,23 @@ Section GenSqrt. Qed. Theorem ww_add_mult_mult_2: forall w, - [[ww_add_mul_div 1 w W0]] = 2 * [[w]] mod wwB. + [[ww_add_mul_div (w_0W w_1) w W0]] = 2 * [[w]] mod wwB. intros w1. rewrite spec_ww_add_mul_div; auto with zarith. autorewrite with w_rewrite rm10. + rewrite spec_w_0W; rewrite spec_w_1. rewrite Zpower_exp_1; auto with zarith. rewrite Zmult_comm; auto. + rewrite spec_w_0W; rewrite spec_w_1; auto with zarith. + red; simpl; intros; discriminate. Qed. Theorem ww_add_mult_mult_2_plus_1: forall w, - [[ww_add_mul_div 1 w wwBm1]] = + [[ww_add_mul_div (w_0W w_1) w wwBm1]] = (2 * [[w]] + 1) mod wwB. intros w1. rewrite spec_ww_add_mul_div; auto with zarith. + rewrite spec_w_0W; rewrite spec_w_1; auto with zarith. rewrite Zpower_exp_1; auto with zarith. eq_tac; auto. rewrite Zmult_comm; eq_tac; auto. @@ -450,6 +474,8 @@ Section GenSqrt. match goal with |- ?X - 1 >= 0 => assert (0 < X); auto with zarith; red; reflexivity end. + rewrite spec_w_0W; rewrite spec_w_1; auto with zarith. + red; simpl; intros; discriminate. Qed. Theorem Zmod_plus_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1. @@ -1114,50 +1140,54 @@ Section GenSqrt. Lemma spec_ww_head1 : forall x : zn2z w, - (forall p, ww_head1 x = Npos p -> (2 * Zpos (Pdiv2 p) = Zpos p)) /\ - (0 < [[x]] -> wwB / 4 <= 2 ^ Z_of_N (ww_head1 x) * [[x]] < wwB). + (ww_is_even (ww_head1 x) = true) /\ + (0 < [[x]] -> wwB / 4 <= 2 ^ [[ww_head1 x]] * [[x]] < wwB). assert (U := wB_pos w_digits). intros x; unfold ww_head1. - generalize (spec_ww_head0 x); case (ww_head0 x); simpl Z_of_N; - autorewrite with rm10. - intros H1; split. - intros; discriminate. - intros H2; assert (H3:= H1 H2). - split; auto with zarith. - apply Zle_trans with (wwB/2); auto with zarith. + generalize (spec_ww_is_even (ww_head0 x)); case_eq (ww_is_even (ww_head0 x)). + intros HH H1; rewrite HH; split; auto. + intros H2. + generalize (spec_ww_head0 x H2); case (ww_head0 x); autorewrite with rm10. + intros (H3, H4); split; auto with zarith. + apply Zle_trans with (2 := H3). apply Zdiv_le_monotone; auto with zarith. - intros p; case p; clear p; simpl Z_of_N. - intros p H1; split. - intros p1 H2; injection H2; intros; subst; clear H2; auto. - intros H2; assert (H3:= H1 H2). - split; auto with zarith. - apply Zmult_le_reg_r with 2; auto with zarith. - repeat rewrite (fun x => Zmult_comm x 2). - rewrite wwB_4_2. - pattern 2 at 2; rewrite <- Zpower_exp_1; rewrite Zmult_assoc; - rewrite <- Zpower_exp; auto with zarith. - replace (1 + Zpos (xO p)) with (Zpos (xI p)); auto with zarith. - case H3; intros _ tmp; apply Zlt_trans with (2 := tmp). - apply Zmult_lt_compat_r; auto with zarith. - apply Zpower_lt_monotone; auto with zarith. - split; try (red; intros; discriminate). - replace (Zpos (xI p)) with (1 + Zpos (xO p)); auto with zarith. - intros p H1; split. - intros p1 H2; injection H2; intros; subst; clear H2; auto. - intros H2; assert (H3:= H1 H2). - split; auto with zarith. - apply Zle_trans with (wwB/2); auto with zarith. + intros xh xl (H3, H4); split; auto with zarith. + apply Zle_trans with (2 := H3). apply Zdiv_le_monotone; auto with zarith. - generalize (wwB_pos w_digits); auto with zarith. - rewrite Zpower_exp_1; try rewrite Zpower_exp_0. - intros H1; split. - intros; discriminate. - intros H2; assert (H3 := H1 H2). - autorewrite with rm10. + intros H1. + case (spec_to_w_Z (ww_head0 x)); intros Hv1 Hv2. + assert (Hp0: 0 < [[ww_head0 x]]). + generalize (spec_ww_is_even (ww_head0 x)); rewrite H1. + generalize Hv1; case [[ww_head0 x]]. + rewrite Zmod_def_small; auto with zarith. + intros; assert (0 < Zpos p); auto with zarith. + red; simpl; auto. + intros p H2; case H2; auto. + assert (Hp: [[ww_pred (ww_head0 x)]] = [[ww_head0 x]] - 1). + rewrite spec_ww_pred. + rewrite Zmod_def_small; auto with zarith. + intros H2; split. + generalize (spec_ww_is_even (ww_pred (ww_head0 x))); + case ww_is_even; auto. + rewrite Hp. + rewrite Zmod_minus; auto with zarith. + rewrite H2; repeat rewrite Zmod_def_small; auto with zarith. + intros H3; rewrite Hp. + case (spec_ww_head0 x); auto; intros Hv3 Hv4. + assert (Hu: forall u, 0 < u -> 2 * 2 ^ (u - 1) = 2 ^u). + intros u Hu. + pattern 2 at 1; rewrite <- Zpower_exp_1. + rewrite <- Zpower_exp; auto with zarith. + ring_simplify (1 + (u - 1)); auto with zarith. split; auto with zarith. apply Zmult_le_reg_r with 2; auto with zarith. repeat rewrite (fun x => Zmult_comm x 2). - rewrite wwB_4_2; auto with zarith. + rewrite wwB_4_2. + rewrite Zmult_assoc; rewrite Hu; auto with zarith. + apply Zle_lt_trans with (2 * 2 ^ ([[ww_head0 x]] - 1) * [[x]]); auto with zarith; + rewrite Hu; auto with zarith. + apply Zmult_le_compat_r; auto with zarith. + apply Zpower_le_monotone; auto with zarith. Qed. Theorem wwB_4_wB_4: wwB / 4 = wB / 4 * wB. @@ -1173,14 +1203,16 @@ Section GenSqrt. intro x; unfold ww_sqrt. generalize (spec_ww_is_zero x); case (ww_is_zero x). simpl ww_to_Z; simpl Zpower; unfold Zpower_pos; simpl; - auto with zarith. - intros H1; generalize (spec_ww_head1 x); case (ww_head1 x); simpl Z_of_N; - autorewrite with rm10. + auto with zarith. + intros H1. + generalize (spec_ww_compare (ww_head1 x) W0); case ww_compare; + simpl ww_to_Z; autorewrite with rm10. generalize H1; case x. intros HH; contradict HH; simpl ww_to_Z; auto with zarith. intros w0 w1; simpl ww_to_Z; autorewrite with w_rewrite rm10. - intros H2 (H3, H4). - generalize (H4 H2); clear H4; intros (H4, H5). + intros H2; case (spec_ww_head1 (WW w0 w1)); intros H3 H4 H5. + generalize (H4 H2); clear H4; rewrite H5; clear H5; autorewrite with rm10. + intros (H4, H5). assert (V: wB/4 <= [|w0|]). apply beta_lex with 0 [|w1|] wB; auto with zarith; autorewrite with rm10. rewrite <- wwB_4_wB_4; auto. @@ -1204,21 +1236,21 @@ Section GenSqrt. replace Z with (X + 1); auto with zarith end. repeat rewrite Zsquare_mult; ring. - intros p (Hp1, Hp2). - assert (F0: 0 < Zpos (Pdiv2 p)); try (red; reflexivity). - assert (Hp3 := Hp1 p (refl_equal _)). - assert (U0: Zpos p < Zpos (ww_digits w_digits)). - case (Zle_or_lt (Zpos (ww_digits w_digits)) (Zpos p)); auto; intros H2; - case (Hp2 H1); intros _ tmp; contradict tmp; apply Zle_not_lt; - unfold base. - apply Zle_trans with (2 ^ Zpos p * 1); auto with zarith. - autorewrite with rm10; apply Zpower_le_monotone; auto with zarith. - assert (U1: Zpos (Pdiv2 p) < Zpos (ww_digits w_digits)); auto with zarith. - match goal with |- context[ww_add_mul_div ?y ?z ?t] => - assert (UU:= spec_ww_add_mul_div z t ); - generalize (UU p U0); - case (ww_add_mul_div y z t) - end. + intros HH; case (spec_to_w_Z (ww_head1 x)); auto with zarith. + intros Hv1. + case (spec_ww_head1 x); intros Hp1 Hp2. + generalize (Hp2 H1); clear Hp2; intros Hp2. + assert (Hv2: [[ww_head1 x]] <= Zpos (xO w_digits)). + case (Zle_or_lt (Zpos (xO w_digits)) [[ww_head1 x]]); auto with zarith; intros HH1. + case Hp2; intros _ HH2; contradict HH2. + apply Zle_not_lt; unfold base. + apply Zle_trans with (2 ^ [[ww_head1 x]]). + apply Zpower_le_monotone; auto with zarith. + pattern (2 ^ [[ww_head1 x]]) at 1; + rewrite <- (Zmult_1_r (2 ^ [[ww_head1 x]])). + apply Zmult_le_compat_l; auto with zarith. + generalize (spec_ww_add_mul_div x W0 (ww_head1 x) Hv2); + case ww_add_mul_div. simpl ww_to_Z; autorewrite with w_rewrite rm10. rewrite Zmod_def_small; auto with zarith. intros H2; case (Zmult_integral _ _ (sym_equal H2)); clear H2; intros H2. @@ -1228,9 +1260,14 @@ Section GenSqrt. end. apply Zpower_lt_0; auto with zarith. split; auto with zarith. - case (Hp2 H1); intros _ tmp; apply Zle_lt_trans with (2 := tmp); + case Hp2; intros _ tmp; apply Zle_lt_trans with (2 := tmp); clear tmp. rewrite Zmult_comm; apply Zmult_le_compat_r; auto with zarith. + assert (Hv0: [[ww_head1 x]] = 2 * ([[ww_head1 x]]/2)). + pattern [[ww_head1 x]] at 1; rewrite (Z_div_mod_eq [[ww_head1 x]] 2); + auto with zarith. + generalize (spec_ww_is_even (ww_head1 x)); rewrite Hp1; + intros tmp; rewrite tmp; rewrite Zplus_0_r; auto. intros w0 w1; autorewrite with w_rewrite rm10. rewrite Zmod_def_small; auto with zarith. 2: rewrite Zmult_comm; auto with zarith. @@ -1243,42 +1280,71 @@ Section GenSqrt. assert (V1 := spec_to_Z w1);auto with zarith. generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith. case (w_sqrt2 w0 w1); intros w2 c. + case (spec_to_Z w2); intros HH1 HH2. simpl ww_to_Z; simpl fst. - assert (U2: Zpos (Pdiv2 p) < Zpos w_digits). - apply Zmult_lt_reg_r with 2; auto with zarith. - repeat rewrite (fun x => Zmult_comm x 2). - rewrite Hp3. - rewrite <- Zpos_xO; auto. - autorewrite with w_rewrite rm10. - 2: rewrite Zpos_minus; auto with zarith; auto. - rewrite Zpos_minus; auto with zarith. - match goal with |- context[?X - (?X -?Y)] => - replace (X - (X - Y)) with Y; try ring - end. - assert (V2 := spec_to_Z w2);auto with zarith. - rewrite Zmod_def_small; auto with zarith. + assert (Hv3: [[ww_pred ww_zdigits]] + = Zpos (xO w_digits) - 1). + rewrite spec_ww_pred; rewrite spec_ww_zdigits. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + apply Zlt_le_trans with (Zpos (xO w_digits)); auto with zarith. + unfold base; apply Zpower2_le_lin; auto with zarith. + assert (Hv4: [[ww_head1 x]]/2 < wB). + apply Zle_lt_trans with (Zpos w_digits). + apply Zmult_le_reg_r with 2; auto with zarith. + repeat rewrite (fun x => Zmult_comm x 2). + rewrite <- Hv0; rewrite <- Zpos_xO; auto. + unfold base; apply Zpower2_lt_lin; auto with zarith. + assert (Hv5: [[(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))]] + = [[ww_head1 x]]/2). + rewrite spec_ww_add_mul_div. + simpl ww_to_Z; autorewrite with rm10. + rewrite Hv3. + ring_simplify (Zpos (xO w_digits) - (Zpos (xO w_digits) - 1)). + rewrite Zpower_exp_1. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + apply Zlt_le_trans with (1 := Hv4); auto with zarith. + unfold base; apply Zpower_le_monotone; auto with zarith. + split; unfold ww_digits; try rewrite Zpos_xO; auto with zarith. + rewrite Hv3; auto with zarith. + assert (Hv6: [|low(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))|] + = [[ww_head1 x]]/2). + rewrite spec_low. + rewrite Hv5; rewrite Zmod_def_small; auto with zarith. + rewrite spec_w_add_mul_div; auto with zarith. + rewrite spec_w_sub; auto with zarith. + rewrite spec_w_0. + simpl ww_to_Z; autorewrite with rm10. + rewrite Hv6; rewrite spec_w_zdigits. + rewrite (fun x y => Zmod_def_small (x - y)). + ring_simplify (Zpos w_digits - (Zpos w_digits - [[ww_head1 x]] / 2)). + rewrite Zmod_def_small. simpl ww_to_Z in H2; rewrite H2; auto with zarith. intros (H4, H5); split. - apply Zmult_le_reg_r with (2 ^ Zpos p); auto with zarith. + apply Zmult_le_reg_r with (2 ^ [[ww_head1 x]]); auto with zarith. rewrite H4. apply Zle_trans with ([|w2|] ^ 2); auto with zarith. - repeat rewrite (fun x => Zmult_comm x (2 ^ Zpos p)). - rewrite <- Hp3; rewrite (Zmult_comm 2); rewrite Zpower_mult; - auto with zarith. + rewrite Zmult_comm. + pattern [[ww_head1 x]] at 1; + rewrite Hv0; auto with zarith. + rewrite (Zmult_comm 2); rewrite Zpower_mult; + auto with zarith. assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2); try (intros; repeat rewrite Zsquare_mult; ring); rewrite tmp; clear tmp. apply ZPowerAux.Zpower_le_monotone_exp; auto with zarith. split; auto with zarith. - pattern [|w2|] at 2; rewrite (Z_div_mod_eq [|w2|] (2 ^ Zpos (Pdiv2 p))); - auto with zarith. + pattern [|w2|] at 2; + rewrite (Z_div_mod_eq [|w2|] (2 ^ ([[ww_head1 x]] / 2))); + auto with zarith. match goal with |- ?X <= ?X + ?Y => assert (0 <= Y); auto with zarith end. - case (Z_mod_lt [|w2|] (2 ^ Zpos (Pdiv2 p))); auto with zarith. + case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]] / 2))); auto with zarith. case c; unfold interp_carry; autorewrite with rm10; intros w3; assert (V3 := spec_to_Z w3);auto with zarith. - apply Zmult_lt_reg_r with (2 ^ Zpos p); auto with zarith. + apply Zmult_lt_reg_r with (2 ^ [[ww_head1 x]]); auto with zarith. rewrite H4. apply Zle_lt_trans with ([|w2|] ^ 2 + 2 * [|w2|]); auto with zarith. apply Zlt_le_trans with (([|w2|] + 1) ^ 2); auto with zarith. @@ -1286,19 +1352,20 @@ Section GenSqrt. replace Y with (X + 1); auto with zarith end. repeat rewrite (Zsquare_mult); ring. - repeat rewrite (fun x => Zmult_comm x (2 ^ Zpos p)). - rewrite <- Hp3; rewrite (Zmult_comm 2); rewrite Zpower_mult; + rewrite Zmult_comm. + pattern [[ww_head1 x]] at 1; rewrite Hv0. + rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith. assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2); try (intros; repeat rewrite Zsquare_mult; ring); rewrite tmp; clear tmp. apply ZPowerAux.Zpower_le_monotone_exp; auto with zarith. split; auto with zarith. - pattern [|w2|] at 1; rewrite (Z_div_mod_eq [|w2|] (2 ^ Zpos (Pdiv2 p))); + pattern [|w2|] at 1; rewrite (Z_div_mod_eq [|w2|] (2 ^ ([[ww_head1 x]]/2))); auto with zarith. rewrite <- Zplus_assoc; rewrite Zmult_plus_distr_r. autorewrite with rm10; apply Zplus_le_compat_l; auto with zarith. - case (Z_mod_lt [|w2|] (2 ^ Zpos (Pdiv2 p))); auto with zarith. + case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]]/2))); auto with zarith. split; auto with zarith. apply Zle_lt_trans with ([|w2|]); auto with zarith. apply Zdiv_le_upper_bound; auto with zarith. @@ -1307,6 +1374,21 @@ Section GenSqrt. apply Zmult_le_compat_l; auto with zarith. apply Zpower_le_monotone; auto with zarith. rewrite Zpower_exp_0; autorewrite with rm10; auto. + split; auto with zarith. + rewrite Hv0 in Hv2; rewrite (Zpos_xO w_digits) in Hv2; auto with zarith. + apply Zle_lt_trans with (Zpos w_digits); auto with zarith. + unfold base; apply Zpower2_lt_lin; auto with zarith. + rewrite spec_w_sub; auto with zarith. + rewrite Hv6; rewrite spec_w_zdigits; auto with zarith. + assert (Hv7: 0 < [[ww_head1 x]]/2); auto with zarith. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + assert ([[ww_head1 x]]/2 <= Zpos w_digits); auto with zarith. + apply Zmult_le_reg_r with 2; auto with zarith. + repeat rewrite (fun x => Zmult_comm x 2). + rewrite <- Hv0; rewrite <- Zpos_xO; auto with zarith. + apply Zle_lt_trans with (Zpos w_digits); auto with zarith. + unfold base; apply Zpower2_lt_lin; auto with zarith. Qed. End GenSqrt. diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v index c7cd3360f..dbc893c84 100644 --- a/theories/Ints/num/NMake.v +++ b/theories/Ints/num/NMake.v @@ -2317,57 +2317,70 @@ Module Make (W0:W0Type). Definition w12_div_gt := w12_op.(znz_div_gt). Definition w0_divn1 := - gen_divn1 w0_op.(znz_digits) w0_op.(znz_0) + gen_divn1 w0_op.(znz_zdigits) w0_op.(znz_0) w0_op.(znz_WW) w0_op.(znz_head0) - w0_op.(znz_add_mul_div) w0_op.(znz_div21). + w0_op.(znz_add_mul_div) w0_op.(znz_div21) + w0_op.(znz_compare) w0_op.(znz_sub). Definition w1_divn1 := - gen_divn1 w1_op.(znz_digits) w1_op.(znz_0) + gen_divn1 w1_op.(znz_zdigits) w1_op.(znz_0) w1_op.(znz_WW) w1_op.(znz_head0) - w1_op.(znz_add_mul_div) w1_op.(znz_div21). + w1_op.(znz_add_mul_div) w1_op.(znz_div21) + w1_op.(znz_compare) w1_op.(znz_sub). Definition w2_divn1 := - gen_divn1 w2_op.(znz_digits) w2_op.(znz_0) + gen_divn1 w2_op.(znz_zdigits) w2_op.(znz_0) w2_op.(znz_WW) w2_op.(znz_head0) - w2_op.(znz_add_mul_div) w2_op.(znz_div21). + w2_op.(znz_add_mul_div) w2_op.(znz_div21) + w2_op.(znz_compare) w2_op.(znz_sub). Definition w3_divn1 := - gen_divn1 w3_op.(znz_digits) w3_op.(znz_0) + gen_divn1 w3_op.(znz_zdigits) w3_op.(znz_0) w3_op.(znz_WW) w3_op.(znz_head0) - w3_op.(znz_add_mul_div) w3_op.(znz_div21). + w3_op.(znz_add_mul_div) w3_op.(znz_div21) + w3_op.(znz_compare) w3_op.(znz_sub). Definition w4_divn1 := - gen_divn1 w4_op.(znz_digits) w4_op.(znz_0) + gen_divn1 w4_op.(znz_zdigits) w4_op.(znz_0) w4_op.(znz_WW) w4_op.(znz_head0) - w4_op.(znz_add_mul_div) w4_op.(znz_div21). + w4_op.(znz_add_mul_div) w4_op.(znz_div21) + w4_op.(znz_compare) w4_op.(znz_sub). Definition w5_divn1 := - gen_divn1 w5_op.(znz_digits) w5_op.(znz_0) + gen_divn1 w5_op.(znz_zdigits) w5_op.(znz_0) w5_op.(znz_WW) w5_op.(znz_head0) - w5_op.(znz_add_mul_div) w5_op.(znz_div21). + w5_op.(znz_add_mul_div) w5_op.(znz_div21) + w5_op.(znz_compare) w5_op.(znz_sub). Definition w6_divn1 := - gen_divn1 w6_op.(znz_digits) w6_op.(znz_0) + gen_divn1 w6_op.(znz_zdigits) w6_op.(znz_0) w6_op.(znz_WW) w6_op.(znz_head0) - w6_op.(znz_add_mul_div) w6_op.(znz_div21). + w6_op.(znz_add_mul_div) w6_op.(znz_div21) + w6_op.(znz_compare) w6_op.(znz_sub). Definition w7_divn1 := - gen_divn1 w7_op.(znz_digits) w7_op.(znz_0) + gen_divn1 w7_op.(znz_zdigits) w7_op.(znz_0) w7_op.(znz_WW) w7_op.(znz_head0) - w7_op.(znz_add_mul_div) w7_op.(znz_div21). + w7_op.(znz_add_mul_div) w7_op.(znz_div21) + w7_op.(znz_compare) w7_op.(znz_sub). Definition w8_divn1 := - gen_divn1 w8_op.(znz_digits) w8_op.(znz_0) + gen_divn1 w8_op.(znz_zdigits) w8_op.(znz_0) w8_op.(znz_WW) w8_op.(znz_head0) - w8_op.(znz_add_mul_div) w8_op.(znz_div21). + w8_op.(znz_add_mul_div) w8_op.(znz_div21) + w8_op.(znz_compare) w8_op.(znz_sub). Definition w9_divn1 := - gen_divn1 w9_op.(znz_digits) w9_op.(znz_0) + gen_divn1 w9_op.(znz_zdigits) w9_op.(znz_0) w9_op.(znz_WW) w9_op.(znz_head0) - w9_op.(znz_add_mul_div) w9_op.(znz_div21). + w9_op.(znz_add_mul_div) w9_op.(znz_div21) + w9_op.(znz_compare) w9_op.(znz_sub). Definition w10_divn1 := - gen_divn1 w10_op.(znz_digits) w10_op.(znz_0) + gen_divn1 w10_op.(znz_zdigits) w10_op.(znz_0) w10_op.(znz_WW) w10_op.(znz_head0) - w10_op.(znz_add_mul_div) w10_op.(znz_div21). + w10_op.(znz_add_mul_div) w10_op.(znz_div21) + w10_op.(znz_compare) w10_op.(znz_sub). Definition w11_divn1 := - gen_divn1 w11_op.(znz_digits) w11_op.(znz_0) + gen_divn1 w11_op.(znz_zdigits) w11_op.(znz_0) w11_op.(znz_WW) w11_op.(znz_head0) - w11_op.(znz_add_mul_div) w11_op.(znz_div21). + w11_op.(znz_add_mul_div) w11_op.(znz_div21) + w11_op.(znz_compare) w11_op.(znz_sub). Definition w12_divn1 := - gen_divn1 w12_op.(znz_digits) w12_op.(znz_0) + gen_divn1 w12_op.(znz_zdigits) w12_op.(znz_0) w12_op.(znz_WW) w12_op.(znz_head0) - w12_op.(znz_add_mul_div) w12_op.(znz_div21). + w12_op.(znz_add_mul_div) w12_op.(znz_div21) + w12_op.(znz_compare) w12_op.(znz_sub). Definition div_gt x y := match x, y with @@ -2913,44 +2926,57 @@ Module Make (W0:W0Type). Definition w12_mod_gt := w12_op.(znz_mod_gt). Definition w0_modn1 := - gen_modn1 w0_op.(znz_digits) w0_op.(znz_0) - w0_op.(znz_head0) w0_op.(znz_add_mul_div) w0_op.(znz_div21). + gen_modn1 w0_op.(znz_zdigits) w0_op.(znz_0) + w0_op.(znz_head0) w0_op.(znz_add_mul_div) w0_op.(znz_div21) + w0_op.(znz_compare) w0_op.(znz_sub). Definition w1_modn1 := - gen_modn1 w1_op.(znz_digits) w1_op.(znz_0) - w1_op.(znz_head0) w1_op.(znz_add_mul_div) w1_op.(znz_div21). + gen_modn1 w1_op.(znz_zdigits) w1_op.(znz_0) + w1_op.(znz_head0) w1_op.(znz_add_mul_div) w1_op.(znz_div21) + w1_op.(znz_compare) w1_op.(znz_sub). Definition w2_modn1 := - gen_modn1 w2_op.(znz_digits) w2_op.(znz_0) - w2_op.(znz_head0) w2_op.(znz_add_mul_div) w2_op.(znz_div21). + gen_modn1 w2_op.(znz_zdigits) w2_op.(znz_0) + w2_op.(znz_head0) w2_op.(znz_add_mul_div) w2_op.(znz_div21) + w2_op.(znz_compare) w2_op.(znz_sub). Definition w3_modn1 := - gen_modn1 w3_op.(znz_digits) w3_op.(znz_0) - w3_op.(znz_head0) w3_op.(znz_add_mul_div) w3_op.(znz_div21). + gen_modn1 w3_op.(znz_zdigits) w3_op.(znz_0) + w3_op.(znz_head0) w3_op.(znz_add_mul_div) w3_op.(znz_div21) + w3_op.(znz_compare) w3_op.(znz_sub). Definition w4_modn1 := - gen_modn1 w4_op.(znz_digits) w4_op.(znz_0) - w4_op.(znz_head0) w4_op.(znz_add_mul_div) w4_op.(znz_div21). + gen_modn1 w4_op.(znz_zdigits) w4_op.(znz_0) + w4_op.(znz_head0) w4_op.(znz_add_mul_div) w4_op.(znz_div21) + w4_op.(znz_compare) w4_op.(znz_sub). Definition w5_modn1 := - gen_modn1 w5_op.(znz_digits) w5_op.(znz_0) - w5_op.(znz_head0) w5_op.(znz_add_mul_div) w5_op.(znz_div21). + gen_modn1 w5_op.(znz_zdigits) w5_op.(znz_0) + w5_op.(znz_head0) w5_op.(znz_add_mul_div) w5_op.(znz_div21) + w5_op.(znz_compare) w5_op.(znz_sub). Definition w6_modn1 := - gen_modn1 w6_op.(znz_digits) w6_op.(znz_0) - w6_op.(znz_head0) w6_op.(znz_add_mul_div) w6_op.(znz_div21). + gen_modn1 w6_op.(znz_zdigits) w6_op.(znz_0) + w6_op.(znz_head0) w6_op.(znz_add_mul_div) w6_op.(znz_div21) + w6_op.(znz_compare) w6_op.(znz_sub). Definition w7_modn1 := - gen_modn1 w7_op.(znz_digits) w7_op.(znz_0) - w7_op.(znz_head0) w7_op.(znz_add_mul_div) w7_op.(znz_div21). + gen_modn1 w7_op.(znz_zdigits) w7_op.(znz_0) + w7_op.(znz_head0) w7_op.(znz_add_mul_div) w7_op.(znz_div21) + w7_op.(znz_compare) w7_op.(znz_sub). Definition w8_modn1 := - gen_modn1 w8_op.(znz_digits) w8_op.(znz_0) - w8_op.(znz_head0) w8_op.(znz_add_mul_div) w8_op.(znz_div21). + gen_modn1 w8_op.(znz_zdigits) w8_op.(znz_0) + w8_op.(znz_head0) w8_op.(znz_add_mul_div) w8_op.(znz_div21) + w8_op.(znz_compare) w8_op.(znz_sub). Definition w9_modn1 := - gen_modn1 w9_op.(znz_digits) w9_op.(znz_0) - w9_op.(znz_head0) w9_op.(znz_add_mul_div) w9_op.(znz_div21). + gen_modn1 w9_op.(znz_zdigits) w9_op.(znz_0) + w9_op.(znz_head0) w9_op.(znz_add_mul_div) w9_op.(znz_div21) + w9_op.(znz_compare) w9_op.(znz_sub). Definition w10_modn1 := - gen_modn1 w10_op.(znz_digits) w10_op.(znz_0) - w10_op.(znz_head0) w10_op.(znz_add_mul_div) w10_op.(znz_div21). + gen_modn1 w10_op.(znz_zdigits) w10_op.(znz_0) + w10_op.(znz_head0) w10_op.(znz_add_mul_div) w10_op.(znz_div21) + w10_op.(znz_compare) w10_op.(znz_sub). Definition w11_modn1 := - gen_modn1 w11_op.(znz_digits) w11_op.(znz_0) - w11_op.(znz_head0) w11_op.(znz_add_mul_div) w11_op.(znz_div21). + gen_modn1 w11_op.(znz_zdigits) w11_op.(znz_0) + w11_op.(znz_head0) w11_op.(znz_add_mul_div) w11_op.(znz_div21) + w11_op.(znz_compare) w11_op.(znz_sub). Definition w12_modn1 := - gen_modn1 w12_op.(znz_digits) w12_op.(znz_0) - w12_op.(znz_head0) w12_op.(znz_add_mul_div) w12_op.(znz_div21). + gen_modn1 w12_op.(znz_zdigits) w12_op.(znz_0) + w12_op.(znz_head0) w12_op.(znz_add_mul_div) w12_op.(znz_div21) + w12_op.(znz_compare) w12_op.(znz_sub). Definition mod_gt x y := match x, y with diff --git a/theories/Ints/num/Zn2Z.v b/theories/Ints/num/Zn2Z.v index b5c646658..ac13d6922 100644 --- a/theories/Ints/num/Zn2Z.v +++ b/theories/Ints/num/Zn2Z.v @@ -30,6 +30,7 @@ Section Zn2Z. Variable w : Set. Variable w_op : znz_op w. Let w_digits := w_op.(znz_digits). + Let w_zdigits := w_op.(znz_zdigits). Variable more_than_one_digit: 1 < Zpos w_digits. @@ -98,8 +99,12 @@ Section Zn2Z. Let ww_1 := ww_1 w_0 w_1. Let ww_Bm1 := ww_Bm1 w_Bm1. + Let w_add2 a b := match w_add_c a b with C0 p => WW w_0 p | C1 p => WW w_1 p end. + Let _ww_digits := xO w_digits. + Let _ww_zdigits := w_add2 w_zdigits w_zdigits. + Let to_Z := zn2z_to_Z wB w_to_Z. Let ww_of_pos p := @@ -109,9 +114,10 @@ Section Zn2Z. let (n,h) := w_of_pos ph in (n, w_WW h l) end. + Let head0 := Eval lazy beta delta [ww_head0] in - ww_head0 w_0 w_compare w_head0 w_digits _ww_digits. + ww_head0 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits. Let ww_WW := Eval lazy beta delta [ww_WW] in (@ww_WW w). Let ww_0W := Eval lazy beta delta [ww_0W] in (@ww_0W w). @@ -215,47 +221,53 @@ Section Zn2Z. Eval lazy beta iota delta [ww_div21] in ww_div21 w_0 w_0W div32 ww_1 compare sub. + Let low (p: zn2z w) := match p with WW _ p1 => p1 | _ => w_0 end. + Let add_mul_div := Eval lazy beta delta [ww_add_mul_div] in - ww_add_mul_div w_0 w_WW w_W0 w_0W w_add_mul_div w_digits. + ww_add_mul_div w_0 w_WW w_W0 w_0W compare w_add_mul_div sub w_zdigits low. Let div_gt := Eval lazy beta delta [ww_div_gt] in - ww_div_gt w_digits w_0 w_WW w_0W w_compare w_eq0 w_sub_c w_sub w_sub_carry - w_div_gt w_add_mul_div w_head0 w_div21 div32 _ww_digits ww_1 add_mul_div. + ww_div_gt w_0 w_WW w_0W w_compare w_eq0 w_opp_c w_opp + w_opp_carry w_sub_c w_sub w_sub_carry + w_div_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits. Let div := Eval lazy beta delta [ww_div] in ww_div ww_1 compare div_gt. Let mod_gt := Eval lazy beta delta [ww_mod_gt] in - ww_mod_gt w_digits w_0 w_WW w_0W w_compare w_eq0 w_sub_c w_sub w_sub_carry - w_mod_gt w_add_mul_div w_head0 w_div21 div32 _ww_digits add_mul_div. + ww_mod_gt w_0 w_WW w_0W w_compare w_eq0 w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry + w_mod_gt w_add_mul_div w_head0 w_div21 div32 _ww_zdigits add_mul_div w_zdigits. Let mod_ := Eval lazy beta delta [ww_mod] in ww_mod compare mod_gt. Let pos_mod := - Eval lazy beta delta [ww_pos_mod] in ww_pos_mod w_0 w_digits w_WW w_pos_mod. + Eval lazy beta delta [ww_pos_mod] in + ww_pos_mod w_0 w_zdigits w_WW w_pos_mod compare w_0W low sub _ww_zdigits. Let is_even := Eval lazy beta delta [ww_is_even] in ww_is_even w_is_even. Let sqrt2 := Eval lazy beta delta [ww_sqrt2] in - ww_sqrt2 w_is_even w_compare w_0 w_1 w_Bm1 w_sub w_square_c - w_div21 w_add_mul_div w_digits w_add_c w_sqrt2 pred_c + ww_sqrt2 w_is_even w_compare w_0 w_1 w_Bm1 w_0W w_sub w_square_c + w_div21 w_add_mul_div w_zdigits w_add_c w_sqrt2 w_pred pred_c pred add_c add sub_c add_mul_div. Let sqrt := Eval lazy beta delta [ww_sqrt] in - ww_sqrt w_0 w_add_mul_div w_digits w_sqrt2 - add_mul_div head0 compare. + ww_sqrt w_is_even w_0 w_sub w_add_mul_div w_zdigits + _ww_zdigits w_sqrt2 pred add_mul_div head0 compare low. Let gcd_gt_fix := Eval cbv beta delta [ww_gcd_gt_aux ww_gcd_gt_body] in - ww_gcd_gt_aux w_digits w_0 w_WW w_compare w_sub_c w_sub w_sub_carry w_gcd_gt - w_add_mul_div w_head0 w_div21 div32 _ww_digits add_mul_div. + ww_gcd_gt_aux w_0 w_WW w_0W w_compare w_opp_c w_opp w_opp_carry + w_sub_c w_sub w_sub_carry w_gcd_gt + w_add_mul_div w_head0 w_div21 div32 _ww_zdigits add_mul_div + w_zdigits. Let gcd_cont := Eval lazy beta delta [gcd_cont] in gcd_cont ww_1 w_1 w_compare. @@ -271,7 +283,7 @@ Section Zn2Z. (* ** Record of operators on 2 words *) Definition mk_zn2z_op := - mk_znz_op _ww_digits + mk_znz_op _ww_digits _ww_zdigits to_Z ww_of_pos head0 W0 ww_1 ww_Bm1 ww_WW ww_W0 ww_0W @@ -292,7 +304,7 @@ Section Zn2Z. sqrt. Definition mk_zn2z_op_karatsuba := - mk_znz_op _ww_digits + mk_znz_op _ww_digits _ww_zdigits to_Z ww_of_pos head0 W0 ww_1 ww_Bm1 ww_WW ww_W0 ww_0W @@ -588,22 +600,65 @@ Section Zn2Z. _ _ _ _ _ _ _);auto. exact (spec_0W op_spec). Qed. + Let spec_add2: forall x y, + [|w_add2 x y|] = w_to_Z x + w_to_Z y. + unfold w_add2. + intros xh xl; generalize (spec_add_c op_spec xh xl). + unfold w_add_c; case znz_add_c; unfold interp_carry; simpl ww_to_Z. + intros w0 Hw0; simpl; unfold w_to_Z; rewrite Hw0. + unfold w_0; rewrite spec_0; simpl; auto with zarith. + intros w0; rewrite Zmult_1_l; simpl. + unfold w_to_Z, w_1; rewrite spec_1; auto with zarith. + rewrite Zmult_1_l; auto. + Qed. + + Let spec_low: forall x, + w_to_Z (low x) = [|x|] mod wB. + intros x; case x; simpl low. + unfold ww_to_Z, w_to_Z, w_0; rewrite (spec_0 op_spec); simpl. + rewrite Zmod_def_small; auto with zarith. + split; auto with zarith. + unfold wB, base; auto with zarith. + intros xh xl; simpl. + rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith. + rewrite Zmod_def_small; auto with zarith. + unfold wB, base; auto with zarith. + Qed. + + Let spec_ww_digits: + [|_ww_zdigits|] = Zpos (xO w_digits). + Proof. + unfold w_to_Z, _ww_zdigits. + rewrite spec_add2. + unfold w_to_Z, w_zdigits, w_digits. + rewrite spec_zdigits; auto. + rewrite Zpos_xO; auto with zarith. + Qed. + Let spec_ww_head0 : forall x, 0 < [|x|] -> - wwB/ 2 <= 2 ^ (Z_of_N (head0 x)) * [|x|] < wwB. + wwB/ 2 <= 2 ^ [|head0 x|] * [|x|] < wwB. Proof. - refine (spec_ww_head0 w_0 w_compare w_head0 w_digits _ww_digits - w_to_Z _ _ _ _);auto. exact (spec_compare op_spec). + refine (spec_ww_head0 w_0 w_0W w_compare w_head0 + w_add2 w_zdigits _ww_zdigits + w_to_Z _ _ _ _ _ _ _);auto. + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_zdigits op_spec). Qed. Lemma spec_ww_add_mul_div : forall x y p, - Zpos p < Zpos _ww_digits -> + [|p|] <= Zpos _ww_digits -> [| add_mul_div p x y |] = - ([|x|] * (Zpower 2 (Zpos p)) + - [|y|] / (Zpower 2 ((Zpos _ww_digits) - (Zpos p)))) mod wwB. + ([|x|] * (2 ^ [|p|]) + + [|y|] / (2 ^ ((Zpos _ww_digits) - [|p|]))) mod wwB. Proof. - refine (@spec_ww_add_mul_div w w_0 w_WW w_W0 w_0W w_add_mul_div w_digits - w_to_Z _ _ _ _ _ _);auto. exact (spec_WW op_spec). - exact (spec_W0 op_spec). exact (spec_0W op_spec). + refine (@spec_ww_add_mul_div w w_0 w_WW w_W0 w_0W compare w_add_mul_div + sub w_digits w_zdigits low w_to_Z + _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_W0 op_spec). + exact (spec_0W op_spec). + exact (spec_zdigits op_spec). Qed. Let spec_ww_div_gt : forall a b, @@ -611,13 +666,33 @@ Section Zn2Z. let (q,r) := div_gt a b in [|a|] = [|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|]. Proof. - refine (@spec_ww_div_gt w w_digits w_0 w_WW w_0W w_compare w_eq0 +refine +(@spec_ww_div_gt w w_digits w_0 w_WW w_0W w_compare w_eq0 w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt - w_add_mul_div w_head0 w_div21 div32 _ww_digits ww_1 add_mul_div w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). exact (spec_0W op_spec). - exact (spec_compare op_spec). exact (spec_div_gt op_spec). - exact (spec_div21 op_spec). exact spec_ww_add_mul_div. + w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ +). + exact (spec_0 op_spec). + exact (spec_to_Z op_spec). + exact (spec_WW op_spec). + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_eq0 op_spec). + exact (spec_opp_c op_spec). + exact (spec_opp op_spec). + exact (spec_opp_carry op_spec). + exact (spec_sub_c op_spec). + exact (spec_sub op_spec). + exact (spec_sub_carry op_spec). + exact (spec_div_gt op_spec). + exact (spec_add_mul_div op_spec). + exact (spec_head0 op_spec). + exact (spec_div21 op_spec). + exact spec_w_div32. + exact (spec_zdigits op_spec). + exact spec_ww_digits. + exact spec_ww_1. + exact spec_ww_add_mul_div. Qed. Let spec_ww_div : forall a b, 0 < [|b|] -> @@ -634,11 +709,16 @@ Section Zn2Z. Proof. refine (@spec_ww_mod_gt w w_digits w_0 w_WW w_0W w_compare w_eq0 w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_div_gt w_mod_gt - w_add_mul_div w_head0 w_div21 div32 _ww_digits ww_1 add_mul_div w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). exact (spec_0W op_spec). - exact (spec_compare op_spec). exact (spec_div_gt op_spec). - exact (spec_div21 op_spec). exact spec_ww_add_mul_div. + w_add_mul_div w_head0 w_div21 div32 _ww_zdigits ww_1 add_mul_div + w_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_div_gt op_spec). + exact (spec_div21 op_spec). + exact (spec_zdigits op_spec). + exact spec_ww_add_mul_div. Qed. Let spec_ww_mod : forall a b, 0 < [|b|] -> [|mod_ a b|] = [|a|] mod [|b|]. @@ -652,28 +732,38 @@ Section Zn2Z. refine (@spec_ww_gcd_gt w w_digits W0 w_to_Z _ w_0 w_0 w_eq0 w_gcd_gt _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto. - refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_compare w_opp_c w_opp + refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 - w_div21 div32 _ww_digits ww_1 add_mul_div w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). exact (spec_compare op_spec). - exact (spec_div21 op_spec). exact spec_ww_add_mul_div. + w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_div21 op_spec). + exact (spec_zdigits op_spec). + exact spec_ww_add_mul_div. refine (@spec_gcd_cont w w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare - _ _);auto. exact (spec_compare op_spec). + _ _);auto. + exact (spec_compare op_spec). Qed. Let spec_ww_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]. Proof. refine (@spec_ww_gcd w w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto. - refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_compare w_opp_c w_opp + refine (@spec_ww_gcd_gt_aux w w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0 - w_div21 div32 _ww_digits ww_1 add_mul_div w_to_Z - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. - exact (spec_WW op_spec). exact (spec_compare op_spec). - exact (spec_div21 op_spec). exact spec_ww_add_mul_div. + w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_0W op_spec). + exact (spec_compare op_spec). + exact (spec_div21 op_spec). + exact (spec_zdigits op_spec). + exact spec_ww_add_mul_div. refine (@spec_gcd_cont w w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare - _ _);auto. exact (spec_compare op_spec). + _ _);auto. + exact (spec_compare op_spec). Qed. Let spec_ww_is_even : forall x, @@ -682,7 +772,7 @@ Section Zn2Z. | false => [|x|] mod 2 = 1 end. Proof. - refine (@spec_ww_is_even w w_is_even w_0 w_1 w_Bm1 w_digits _ _ _); auto. + refine (@spec_ww_is_even w w_is_even w_0 w_1 w_Bm1 w_digits _ _ _ _ _); auto. exact (spec_is_even op_spec). Qed. @@ -694,9 +784,12 @@ Section Zn2Z. Proof. intros x y H. refine (@spec_ww_sqrt2 w w_is_even w_compare w_0 w_1 w_Bm1 - w_sub w_square_c w_div21 w_add_mul_div w_digits - w_add_c w_sqrt2 pred_c pred add_c add sub_c add_mul_div - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. + w_0W w_sub w_square_c w_div21 w_add_mul_div w_digits w_zdigits + _ww_zdigits + w_add_c w_sqrt2 w_pred pred_c pred add_c add sub_c add_mul_div + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. + exact (spec_zdigits op_spec). + exact (spec_0W op_spec). exact (spec_is_even op_spec). exact (spec_compare op_spec). exact (spec_square_c op_spec). @@ -708,9 +801,12 @@ Section Zn2Z. Let spec_ww_sqrt : forall x, [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. Proof. - refine (@spec_ww_sqrt w w_0 w_1 w_Bm1 w_add_mul_div w_digits - w_sqrt2 add_mul_div head0 compare - _ _ _ _ _ _ _ _ _ _); auto. + refine (@spec_ww_sqrt w w_is_even w_0 w_1 w_Bm1 + w_sub w_add_mul_div w_digits w_zdigits _ww_zdigits + w_sqrt2 pred add_mul_div head0 compare + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. + exact (spec_zdigits op_spec). + exact (spec_is_even op_spec). exact (spec_ww_add_mul_div). exact (spec_sqrt2 op_spec). Qed. @@ -719,17 +815,35 @@ Section Zn2Z. Proof. apply mk_znz_spec;auto. exact spec_ww_add_mul_div. - refine (@spec_ww_pos_mod w w_0 w_digits w_WW w_pos_mod w_to_Z - _ _ _ _);auto. exact (spec_WW op_spec). exact (spec_pos_mod op_spec). + + refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW + w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_pos_mod op_spec). + exact (spec_0W op_spec). + exact (spec_zdigits op_spec). + unfold w_to_Z, w_zdigits. + rewrite (spec_zdigits op_spec). + rewrite <- Zpos_xO; exact spec_ww_digits. Qed. Lemma mk_znz2_karatsuba_spec : znz_spec mk_zn2z_op_karatsuba. Proof. apply mk_znz_spec;auto. exact spec_ww_add_mul_div. - refine (@spec_ww_pos_mod w w_0 w_digits w_WW w_pos_mod w_to_Z - _ _ _ _);auto. exact (spec_WW op_spec). exact (spec_pos_mod op_spec). + refine (@spec_ww_pos_mod w w_0 w_digits w_zdigits w_WW + w_pos_mod compare w_0W low sub _ww_zdigits w_to_Z + _ _ _ _ _ _ _ _ _ _ _ _);auto. + exact (spec_WW op_spec). + exact (spec_pos_mod op_spec). + exact (spec_0W op_spec). + exact (spec_zdigits op_spec). + unfold w_to_Z, w_zdigits. + rewrite (spec_zdigits op_spec). + rewrite <- Zpos_xO; exact spec_ww_digits. Qed. + End Zn2Z. diff --git a/theories/Ints/num/ZnZ.v b/theories/Ints/num/ZnZ.v index 5efcad2d0..5096c81cf 100644 --- a/theories/Ints/num/ZnZ.v +++ b/theories/Ints/num/ZnZ.v @@ -23,9 +23,10 @@ Section ZnZ_Op. Record znz_op : Set := mk_znz_op { (* Conversion functions with Z *) znz_digits : positive; + znz_zdigits: znz; znz_to_Z : znz -> Z; znz_of_pos : positive -> N * znz; - znz_head0 : znz -> N; + znz_head0 : znz -> znz; (* Basic constructors *) znz_0 : znz; znz_1 : znz; @@ -71,8 +72,8 @@ Section ZnZ_Op. znz_gcd_gt : znz -> znz -> znz; znz_gcd : znz -> znz -> znz; - znz_add_mul_div : positive -> znz -> znz -> znz; - znz_pos_mod : positive -> znz -> znz; + znz_add_mul_div : znz -> znz -> znz -> znz; + znz_pos_mod : znz -> znz -> znz; (* square root *) znz_is_even : znz -> bool; @@ -86,6 +87,7 @@ Section Spec. Variable w_op : znz_op w. Let w_digits := w_op.(znz_digits). + Let w_zdigits := w_op.(znz_zdigits). Let w_to_Z := w_op.(znz_to_Z). Let w_of_pos := w_op.(znz_of_pos). Let w_head0 := w_op.(znz_head0). @@ -163,6 +165,7 @@ Section Spec. spec_to_Z : forall x, 0 <= [| x |] < wB; spec_of_pos : forall p, Zpos p = (Z_of_N (fst (w_of_pos p)))*wB + [|(snd (w_of_pos p))|]; + spec_zdigits : [| w_zdigits |] = Zpos w_digits; (* Basic constructors *) spec_0 : [|w0|] = 0; @@ -234,14 +237,14 @@ Section Spec. (* shift operations *) spec_head0 : forall x, 0 < [|x|] -> - wB/ 2 <= 2 ^ (Z_of_N (w_head0 x)) * [|x|] < wB; + wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB; spec_add_mul_div : forall x y p, - Zpos p < Zpos w_digits -> + [|p|] <= Zpos w_digits -> [| w_add_mul_div p x y |] = - ([|x|] * (Zpower 2 (Zpos p)) + - [|y|] / (Zpower 2 ((Zpos w_digits) - (Zpos p)))) mod wB; + ([|x|] * (2 ^ [|p|]) + + [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB; spec_pos_mod : forall w p, - [|w_pos_mod p w|] = [|w|] mod (2 ^ Zpos p); + [|w_pos_mod p w|] = [|w|] mod (2 ^ [|p|]); (* sqrt *) spec_is_even : forall x, if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1; |