diff options
| author | thery | 2007-05-21 07:47:46 +0000 |
|---|---|---|
| committer | thery | 2007-05-21 07:47:46 +0000 |
| commit | 2c1c506d23118fb56fc07b4e334e0e1c7995e36b (patch) | |
| tree | 40fe1b8d8b6225ef09443f3073840e0b65f73536 /theories/Ints/num | |
| 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
Diffstat (limited to 'theories/Ints/num')
| -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 |
8 files changed, 1129 insertions, 675 deletions
diff --git a/theories/Ints/num/GenBase.v b/theories/Ints/num/GenBase.v index b953566ede..04749f79c6 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 4bcea709d0..4a30fa2c32 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 4b54d825d1..34b3b35e06 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 14aa869796..8b9271e32a 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 074f7eb537..3d1bb6a24c 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 c7cd3360fc..dbc893c84b 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 b5c6466584..ac13d6922e 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 5efcad2d0f..5096c81cf8 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; |