diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Ints/BigN.v | 1 | ||||
| -rw-r--r-- | theories/Ints/Int31.v | 8 | ||||
| -rw-r--r-- | theories/Ints/num/GenLift.v | 64 | ||||
| -rw-r--r-- | theories/Ints/num/Zn2Z.v | 20 | ||||
| -rw-r--r-- | theories/Ints/num/ZnZ.v | 4 |
5 files changed, 95 insertions, 2 deletions
diff --git a/theories/Ints/BigN.v b/theories/Ints/BigN.v index 1d2b177df..d7b406d3d 100644 --- a/theories/Ints/BigN.v +++ b/theories/Ints/BigN.v @@ -13,6 +13,7 @@ Definition int31_op : znz_op int31. exact (phi). (* conversion to Z *) exact (positive_to_int31). (* positive -> N*int31 : p => N,i where p = N*2^31+phi i *) exact head031. (* number of head 0 *) + exact tail031. (* number of tail 0 *) (* Basic constructors *) exact 0. (* 0 *) diff --git a/theories/Ints/Int31.v b/theories/Ints/Int31.v index 8a19e878d..59e45c320 100644 --- a/theories/Ints/Int31.v +++ b/theories/Ints/Int31.v @@ -394,4 +394,12 @@ Definition head031 (i:int31) := | D1 => n end) i On +. + +Definition tail031 (i:int31) := + recr _ (fun _ => T31) (fun b si rec n => match b with + | D0 => rec (add31 n In) + | D1 => n + end) + i On .
\ No newline at end of file diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v index 8b9271e32..c1283aefb 100644 --- a/theories/Ints/num/GenLift.v +++ b/theories/Ints/num/GenLift.v @@ -27,6 +27,7 @@ Section GenLift. Variable w_compare : w -> w -> comparison. Variable ww_compare : zn2z w -> zn2z w -> comparison. Variable w_head0 : w -> w. + Variable w_tail0 : 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. @@ -46,6 +47,18 @@ Section GenLift. end end. + + Definition ww_tail0 x := + match x with + | W0 => ww_zdigits + | WW xh xl => + match w_compare w_0 xl with + | Eq => w_add w_zdigits (w_tail0 xh) + | _ => w_0W (w_tail0 xl) + end + end. + + (* 0 < p < ww_digits *) Definition ww_add_mul_div p x y := let zdigits := w_0W w_zdigits in @@ -106,6 +119,8 @@ Section GenLift. Variable spec_ww_digits : ww_Digits = xO w_digits. Variable spec_w_head0 : forall x, 0 < [|x|] -> wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB. + Variable spec_w_tail0 : forall x, 0 < [|x|] -> + exists y, 0 <= y /\ [|x|] = (2* y + 1) * (2 ^ [|w_tail0 x|]). Variable spec_w_add_mul_div : forall x y p, [|p|] <= Zpos w_digits -> [| w_add_mul_div p x y |] = @@ -167,6 +182,55 @@ Section GenLift. assert (H1 := spec_to_Z xh);zarith. Qed. + Lemma spec_ww_tail0 : forall x, 0 < [[x]] -> + exists y, 0 <= y /\ [[x]] = (2 * y + 1) * 2 ^ [[ww_tail0 x]]. + Proof. + destruct x as [ |xh xl];simpl ww_to_Z;intros H. + unfold Zlt in H;discriminate H. + assert (H0 := spec_compare w_0 xl);rewrite spec_w_0 in H0. + destruct (w_compare w_0 xl). + rewrite <- H0; rewrite Zplus_0_r. + case (spec_to_Z (w_tail0 xh)); intros HH1 HH2. + generalize H; rewrite <- H0; rewrite Zplus_0_r; clear H; intros H. + case (@spec_w_tail0 xh). + apply Zmult_lt_reg_r with wB; auto with zarith. + unfold base; auto with zarith. + intros z (Hz1, Hz2); exists z; split; auto. + rewrite spec_w_add; rewrite (fun x => Zplus_comm [|x|]). + rewrite spec_zdigits; rewrite Zpower_exp; auto with zarith. + rewrite Zmult_assoc; rewrite <- Hz2; auto. + + case (spec_to_Z (w_tail0 xh)); intros HH1 HH2. + case (spec_w_tail0 H0); intros z (Hz1, Hz2). + assert (Hp: [|w_tail0 xl|] < Zpos w_digits). + case (Zle_or_lt (Zpos w_digits) [|w_tail0 xl|]); auto; intros H1. + absurd (2 ^ (Zpos w_digits) <= 2 ^ [|w_tail0 xl|]). + apply Zlt_not_le. + case (spec_to_Z xl); intros HH3 HH4. + apply Zle_lt_trans with (2 := HH4). + apply Zle_trans with (1 * 2 ^ [|w_tail0 xl|]); auto with zarith. + rewrite Hz2. + apply Zmult_le_compat_r; auto with zarith. + apply Zpower_le_monotone; auto with zarith. + exists ([|xh|] * (2 ^ ((Zpos w_digits - [|w_tail0 xl|]) - 1)) + z); split. + apply Zplus_le_0_compat; auto. + apply Zmult_le_0_compat; auto with zarith. + case (spec_to_Z xh); auto. + rewrite spec_w_0W. + rewrite (Zmult_plus_distr_r 2); rewrite <- Zplus_assoc. + rewrite Zmult_plus_distr_l; rewrite <- Hz2. + apply f_equal2 with (f := Zplus); auto. + rewrite (Zmult_comm 2). + repeat rewrite <- Zmult_assoc. + apply f_equal2 with (f := Zmult); auto. + case (spec_to_Z (w_tail0 xl)); intros HH3 HH4. + pattern 2 at 2; rewrite <- Zpower_exp_1. + lazy beta; repeat rewrite <- Zpower_exp; auto with zarith. + unfold base; apply f_equal with (f := Zpower 2); auto with zarith. + + contradict H0; case (spec_to_Z xl); auto with zarith. + Qed. + Hint Rewrite Zdiv_0 Zmult_0_l Zplus_0_l Zmult_0_r Zplus_0_r spec_w_W0 spec_w_0W spec_w_WW spec_w_0 (wB_div w_digits w_to_Z spec_to_Z) diff --git a/theories/Ints/num/Zn2Z.v b/theories/Ints/num/Zn2Z.v index ac13d6922..78447c75d 100644 --- a/theories/Ints/num/Zn2Z.v +++ b/theories/Ints/num/Zn2Z.v @@ -37,6 +37,7 @@ Section Zn2Z. 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). + Let w_tail0 := w_op.(znz_tail0). Let w_0 := w_op.(znz_0). Let w_1 := w_op.(znz_1). @@ -119,6 +120,10 @@ Section Zn2Z. Eval lazy beta delta [ww_head0] in ww_head0 w_0 w_0W w_compare w_head0 w_add2 w_zdigits _ww_zdigits. + Let tail0 := + Eval lazy beta delta [ww_tail0] in + ww_tail0 w_0 w_0W w_compare w_tail0 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). Let ww_W0 := Eval lazy beta delta [ww_W0] in (@ww_W0 w). @@ -284,7 +289,7 @@ Section Zn2Z. Definition mk_zn2z_op := mk_znz_op _ww_digits _ww_zdigits - to_Z ww_of_pos head0 + to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 ww_WW ww_W0 ww_0W compare eq0 @@ -305,7 +310,7 @@ Section Zn2Z. Definition mk_zn2z_op_karatsuba := mk_znz_op _ww_digits _ww_zdigits - to_Z ww_of_pos head0 + to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 ww_WW ww_W0 ww_0W compare eq0 @@ -364,6 +369,7 @@ Section Zn2Z. (spec_gcd_gt op_spec) (spec_gcd op_spec) (spec_head0 op_spec) + (spec_tail0 op_spec) (spec_add_mul_div op_spec) (spec_pos_mod) (spec_is_even) @@ -646,6 +652,16 @@ Section Zn2Z. exact (spec_zdigits op_spec). Qed. + Let spec_ww_tail0 : forall x, 0 < [|x|] -> + exists y, 0 <= y /\ [|x|] = (2 * y + 1) * 2 ^ [|tail0 x|]. + Proof. + refine (spec_ww_tail0 (w_digits := w_digits) w_0 w_0W w_compare w_tail0 + 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, [|p|] <= Zpos _ww_digits -> [| add_mul_div p x y |] = diff --git a/theories/Ints/num/ZnZ.v b/theories/Ints/num/ZnZ.v index 5096c81cf..ee4098989 100644 --- a/theories/Ints/num/ZnZ.v +++ b/theories/Ints/num/ZnZ.v @@ -27,6 +27,7 @@ Section ZnZ_Op. znz_to_Z : znz -> Z; znz_of_pos : positive -> N * znz; znz_head0 : znz -> znz; + znz_tail0 : znz -> znz; (* Basic constructors *) znz_0 : znz; znz_1 : znz; @@ -91,6 +92,7 @@ Section Spec. 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). + Let w_tail0 := w_op.(znz_tail0). Let w0 := w_op.(znz_0). Let w1 := w_op.(znz_1). @@ -238,6 +240,8 @@ Section Spec. (* shift operations *) spec_head0 : forall x, 0 < [|x|] -> wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB; + spec_tail0 : forall x, 0 < [|x|] -> + exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|w_tail0 x|]) ; spec_add_mul_div : forall x y p, [|p|] <= Zpos w_digits -> [| w_add_mul_div p x y |] = |