diff options
Diffstat (limited to 'flocq/Calc/Fcalc_digits.v')
-rw-r--r-- | flocq/Calc/Fcalc_digits.v | 319 |
1 files changed, 0 insertions, 319 deletions
diff --git a/flocq/Calc/Fcalc_digits.v b/flocq/Calc/Fcalc_digits.v index 4f76cc2d..45133e81 100644 --- a/flocq/Calc/Fcalc_digits.v +++ b/flocq/Calc/Fcalc_digits.v @@ -29,8 +29,6 @@ Section Fcalc_digits. Variable beta : radix. Notation bpow e := (bpow beta e). - - Theorem Zdigits_ln_beta : forall n, n <> Z0 -> @@ -62,321 +60,4 @@ apply sym_eq. now apply Zdigits_ln_beta. Qed. -Theorem Zdigits_mult_Zpower : - forall m e, - m <> Z0 -> (0 <= e)%Z -> - Zdigits beta (m * Zpower beta e) = (Zdigits beta m + e)%Z. -Proof. -intros m e Hm He. -rewrite <- ln_beta_F2R_Zdigits with (1 := Hm). -rewrite Zdigits_ln_beta. -rewrite Z2R_mult. -now rewrite Z2R_Zpower with (1 := He). -contradict Hm. -apply Zmult_integral_l with (2 := Hm). -apply neq_Z2R. -rewrite Z2R_Zpower with (1 := He). -apply Rgt_not_eq. -apply bpow_gt_0. -Qed. - -Theorem Zdigits_Zpower : - forall e, - (0 <= e)%Z -> - Zdigits beta (Zpower beta e) = (e + 1)%Z. -Proof. -intros e He. -rewrite <- (Zmult_1_l (Zpower beta e)). -rewrite Zdigits_mult_Zpower ; try easy. -apply Zplus_comm. -Qed. - -Theorem Zdigits_le : - forall x y, - (0 <= x)%Z -> (x <= y)%Z -> - (Zdigits beta x <= Zdigits beta y)%Z. -Proof. -intros x y Hx Hxy. -case (Z_lt_le_dec 0 x). -clear Hx. intros Hx. -rewrite 2!Zdigits_ln_beta. -apply ln_beta_le. -now apply (Z2R_lt 0). -now apply Z2R_le. -apply Zgt_not_eq. -now apply Zlt_le_trans with x. -now apply Zgt_not_eq. -intros Hx'. -rewrite (Zle_antisym _ _ Hx' Hx). -apply Zdigits_ge_0. -Qed. - -Theorem lt_Zdigits : - forall x y, - (0 <= y)%Z -> - (Zdigits beta x < Zdigits beta y)%Z -> - (x < y)%Z. -Proof. -intros x y Hy. -cut (y <= x -> Zdigits beta y <= Zdigits beta x)%Z. omega. -now apply Zdigits_le. -Qed. - -Theorem Zpower_le_Zdigits : - forall e x, - (e < Zdigits beta x)%Z -> - (Zpower beta e <= Zabs x)%Z. -Proof. -intros e x Hex. -destruct (Zdigits_correct beta x) as (H1,H2). -apply Zle_trans with (2 := H1). -apply Zpower_le. -clear -Hex ; omega. -Qed. - -Theorem Zdigits_le_Zpower : - forall e x, - (Zabs x < Zpower beta e)%Z -> - (Zdigits beta x <= e)%Z. -Proof. -intros e x. -generalize (Zpower_le_Zdigits e x). -omega. -Qed. - -Theorem Zpower_gt_Zdigits : - forall e x, - (Zdigits beta x <= e)%Z -> - (Zabs x < Zpower beta e)%Z. -Proof. -intros e x Hex. -destruct (Zdigits_correct beta x) as (H1,H2). -apply Zlt_le_trans with (1 := H2). -now apply Zpower_le. -Qed. - -Theorem Zdigits_gt_Zpower : - forall e x, - (Zpower beta e <= Zabs x)%Z -> - (e < Zdigits beta x)%Z. -Proof. -intros e x Hex. -generalize (Zpower_gt_Zdigits e x). -omega. -Qed. - -(** Characterizes the number digits of a product. - -This strong version is needed for proofs of division and square root -algorithms, since they involve operation remainders. -*) - -Theorem Zdigits_mult_strong : - forall x y, - (0 <= x)%Z -> (0 <= y)%Z -> - (Zdigits beta (x + y + x * y) <= Zdigits beta x + Zdigits beta y)%Z. -Proof. -intros x y Hx Hy. -case (Z_lt_le_dec 0 x). -clear Hx. intros Hx. -case (Z_lt_le_dec 0 y). -clear Hy. intros Hy. -(* . *) -assert (Hxy: (0 < Z2R (x + y + x * y))%R). -apply (Z2R_lt 0). -change Z0 with (0 + 0 + 0)%Z. -apply Zplus_lt_compat. -now apply Zplus_lt_compat. -now apply Zmult_lt_0_compat. -rewrite 3!Zdigits_ln_beta ; try now (apply sym_not_eq ; apply Zlt_not_eq). -apply ln_beta_le_bpow with (1 := Rgt_not_eq _ _ Hxy). -rewrite Rabs_pos_eq with (1 := Rlt_le _ _ Hxy). -destruct (ln_beta beta (Z2R x)) as (ex, Hex). simpl. -specialize (Hex (Rgt_not_eq _ _ (Z2R_lt _ _ Hx))). -destruct (ln_beta beta (Z2R y)) as (ey, Hey). simpl. -specialize (Hey (Rgt_not_eq _ _ (Z2R_lt _ _ Hy))). -apply Rlt_le_trans with (Z2R (x + 1) * Z2R (y + 1))%R. -rewrite <- Z2R_mult. -apply Z2R_lt. -apply Zplus_lt_reg_r with (- (x + y + x * y + 1))%Z. -now ring_simplify. -rewrite bpow_plus. -apply Rmult_le_compat ; try (apply (Z2R_le 0) ; omega). -rewrite <- (Rmult_1_r (Z2R (x + 1))). -change (F2R (Float beta (x + 1) 0) <= bpow ex)%R. -apply F2R_p1_le_bpow. -exact Hx. -unfold F2R. rewrite Rmult_1_r. -apply Rle_lt_trans with (Rabs (Z2R x)). -apply RRle_abs. -apply Hex. -rewrite <- (Rmult_1_r (Z2R (y + 1))). -change (F2R (Float beta (y + 1) 0) <= bpow ey)%R. -apply F2R_p1_le_bpow. -exact Hy. -unfold F2R. rewrite Rmult_1_r. -apply Rle_lt_trans with (Rabs (Z2R y)). -apply RRle_abs. -apply Hey. -apply neq_Z2R. -now apply Rgt_not_eq. -(* . *) -intros Hy'. -rewrite (Zle_antisym _ _ Hy' Hy). -rewrite Zmult_0_r, 3!Zplus_0_r. -apply Zle_refl. -intros Hx'. -rewrite (Zle_antisym _ _ Hx' Hx). -rewrite Zmult_0_l, Zplus_0_r, 2!Zplus_0_l. -apply Zle_refl. -Qed. - -Theorem Zdigits_mult : - forall x y, - (Zdigits beta (x * y) <= Zdigits beta x + Zdigits beta y)%Z. -Proof. -intros x y. -rewrite <- Zdigits_abs. -rewrite <- (Zdigits_abs _ x). -rewrite <- (Zdigits_abs _ y). -apply Zle_trans with (Zdigits beta (Zabs x + Zabs y + Zabs x * Zabs y)). -apply Zdigits_le. -apply Zabs_pos. -rewrite Zabs_Zmult. -generalize (Zabs_pos x) (Zabs_pos y). -omega. -apply Zdigits_mult_strong ; apply Zabs_pos. -Qed. - -Theorem Zdigits_mult_ge : - forall x y, - (x <> 0)%Z -> (y <> 0)%Z -> - (Zdigits beta x + Zdigits beta y - 1 <= Zdigits beta (x * y))%Z. -Proof. -intros x y Zx Zy. -cut ((Zdigits beta x - 1) + (Zdigits beta y - 1) < Zdigits beta (x * y))%Z. omega. -apply Zdigits_gt_Zpower. -rewrite Zabs_Zmult. -rewrite Zpower_exp. -apply Zmult_le_compat. -apply Zpower_le_Zdigits. -apply Zlt_pred. -apply Zpower_le_Zdigits. -apply Zlt_pred. -apply Zpower_ge_0. -apply Zpower_ge_0. -generalize (Zdigits_gt_0 beta x). omega. -generalize (Zdigits_gt_0 beta y). omega. -Qed. - -Theorem Zdigits_div_Zpower : - forall m e, - (0 <= m)%Z -> - (0 <= e <= Zdigits beta m)%Z -> - Zdigits beta (m / Zpower beta e) = (Zdigits beta m - e)%Z. -Proof. -intros m e Hm He. -destruct (Zle_lt_or_eq 0 m Hm) as [Hm'|Hm']. -(* *) -destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He']. -(* . *) -unfold Zminus. -rewrite <- ln_beta_F2R_Zdigits. -2: now apply Zgt_not_eq. -assert (Hp: (0 < Zpower beta e)%Z). -apply lt_Z2R. -rewrite Z2R_Zpower with (1 := proj1 He). -apply bpow_gt_0. -rewrite Zdigits_ln_beta. -rewrite <- Zfloor_div with (1 := Zgt_not_eq _ _ Hp). -rewrite Z2R_Zpower with (1 := proj1 He). -unfold Rdiv. -rewrite <- bpow_opp. -change (Z2R m * bpow (-e))%R with (F2R (Float beta m (-e))). -destruct (ln_beta beta (F2R (Float beta m (-e)))) as (e', E'). -simpl. -specialize (E' (Rgt_not_eq _ _ (F2R_gt_0_compat beta (Float beta m (-e)) Hm'))). -apply ln_beta_unique. -rewrite Rabs_pos_eq in E'. -2: now apply F2R_ge_0_compat. -rewrite Rabs_pos_eq. -split. -assert (H': (0 <= e' - 1)%Z). -(* .. *) -cut (1 <= e')%Z. omega. -apply bpow_lt_bpow with beta. -apply Rle_lt_trans with (2 := proj2 E'). -simpl. -rewrite <- (Rinv_r (bpow e)). -rewrite <- bpow_opp. -unfold F2R. simpl. -apply Rmult_le_compat_r. -apply bpow_ge_0. -rewrite <- Z2R_Zpower with (1 := proj1 He). -apply Z2R_le. -rewrite <- Zabs_eq with (1 := Hm). -now apply Zpower_le_Zdigits. -apply Rgt_not_eq. -apply bpow_gt_0. -(* .. *) -rewrite <- Z2R_Zpower with (1 := H'). -apply Z2R_le. -apply Zfloor_lub. -rewrite Z2R_Zpower with (1 := H'). -apply E'. -apply Rle_lt_trans with (2 := proj2 E'). -apply Zfloor_lb. -apply (Z2R_le 0). -apply Zfloor_lub. -now apply F2R_ge_0_compat. -apply Zgt_not_eq. -apply Zlt_le_trans with (beta^e / beta^e)%Z. -rewrite Z_div_same_full. -apply refl_equal. -now apply Zgt_not_eq. -apply Z_div_le. -now apply Zlt_gt. -rewrite <- Zabs_eq with (1 := Hm). -now apply Zpower_le_Zdigits. -(* . *) -unfold Zminus. -rewrite He', Zplus_opp_r. -rewrite Zdiv_small. -apply refl_equal. -apply conj with (1 := Hm). -pattern m at 1 ; rewrite <- Zabs_eq with (1 := Hm). -apply Zpower_gt_Zdigits. -apply Zle_refl. -(* *) -revert He. -rewrite <- Hm'. -intros (H1, H2). -simpl. -now rewrite (Zle_antisym _ _ H2 H1). -Qed. - End Fcalc_digits. - -Definition radix2 := Build_radix 2 (refl_equal _). - -Theorem Z_of_nat_S_digits2_Pnat : - forall m : positive, - Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m). -Proof. -intros m. -rewrite Zdigits_ln_beta. 2: easy. -apply sym_eq. -apply ln_beta_unique. -generalize (digits2_Pnat m) (digits2_Pnat_correct m). -intros d H. -simpl in H. -replace (Z_of_nat (S d) - 1)%Z with (Z_of_nat d). -rewrite <- Z2R_abs. -rewrite <- 2!Z2R_Zpower_nat. -split. -now apply Z2R_le. -now apply Z2R_lt. -rewrite inj_S. -apply Zpred_succ. -Qed. - |