diff options
Diffstat (limited to 'flocq/Appli/Fappli_rnd_odd.v')
| -rw-r--r-- | flocq/Appli/Fappli_rnd_odd.v | 67 |
1 files changed, 25 insertions, 42 deletions
diff --git a/flocq/Appli/Fappli_rnd_odd.v b/flocq/Appli/Fappli_rnd_odd.v index 4741047f..b6d985ac 100644 --- a/flocq/Appli/Fappli_rnd_odd.v +++ b/flocq/Appli/Fappli_rnd_odd.v @@ -20,7 +20,7 @@ COPYING file for more details. (** * Rounding to odd and its properties, including the equivalence between rnd_NE and double rounding with rnd_odd and then rnd_NE *) - +Require Import Reals Psatz. Require Import Fcore. Require Import Fcalc_ops. @@ -577,29 +577,23 @@ Qed. Lemma d_le_m: (F2R d <= m)%R. -apply Rmult_le_reg_l with 2%R. -auto with real. -apply Rplus_le_reg_l with (-F2R d)%R. -apply Rle_trans with (F2R d). -right; ring. -apply Rle_trans with (F2R u). -apply Rle_trans with x. -apply Hd. -apply Hu. -right; unfold m; field. +Proof. +assert (F2R d <= F2R u)%R. + apply Rle_trans with x. + apply Hd. + apply Hu. +unfold m. +lra. Qed. Lemma m_le_u: (m <= F2R u)%R. -apply Rmult_le_reg_l with 2%R. -auto with real. -apply Rplus_le_reg_l with (-F2R u)%R. -apply Rle_trans with (F2R d). -right; unfold m; field. -apply Rle_trans with (F2R u). -apply Rle_trans with x. -apply Hd. -apply Hu. -right; ring. +Proof. +assert (F2R d <= F2R u)%R. + apply Rle_trans with x. + apply Hd. + apply Hu. +unfold m. +lra. Qed. Lemma ln_beta_m: (0 < F2R d)%R -> (ln_beta beta m =ln_beta beta (F2R d) :>Z). @@ -641,20 +635,13 @@ now apply Rgt_not_eq. now apply generic_format_canonic. now left. replace m with (F2R d). -destruct (ln_beta beta (F2R d)) as (e,He). +destruct (ln_beta beta (F2R d)) as (e,He). simpl in *; rewrite Rabs_right in He. apply He. now apply Rgt_not_eq. apply Rle_ge; now left. -assert (F2R d = F2R u). -apply Rmult_eq_reg_l with (/2)%R. -apply Rplus_eq_reg_l with (/2*F2R u)%R. -apply trans_eq with m. -unfold m, Rdiv; ring. -rewrite H; field. -auto with real. -apply Rgt_not_eq, Rlt_gt; auto with real. -unfold m; rewrite <- H0; field. +unfold m in H |- *. +lra. Qed. @@ -666,7 +653,7 @@ apply ln_beta_unique_pos. unfold m; rewrite <- Y, Rplus_0_l. rewrite u_eq. destruct (ln_beta beta x) as (e,He). -rewrite Rabs_right in He. +rewrite Rabs_pos_eq in He by now apply Rlt_le. rewrite round_UP_small_pos with (ex:=e). rewrite ln_beta_bpow. ring_simplify (fexp e + 1 - 1)%Z. @@ -676,7 +663,7 @@ unfold Rdiv; apply Rmult_le_compat_l. apply bpow_ge_0. simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le. -auto with real. +exact Rlt_0_2. apply (Z2R_le 2). specialize (radix_gt_1 beta). omega. @@ -684,13 +671,11 @@ apply Rlt_le_trans with (bpow (fexp e)*1)%R. 2: right; ring. unfold Rdiv; apply Rmult_lt_compat_l. apply bpow_gt_0. -rewrite <- Rinv_1 at 3. -apply Rinv_lt; auto with real. +lra. now apply He, Rgt_not_eq. apply exp_small_round_0_pos with beta (Zfloor) x... now apply He, Rgt_not_eq. now rewrite <- d_eq, Y. -now left. Qed. @@ -723,9 +708,8 @@ unfold Rdiv; apply f_equal. unfold F2R; simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r, Hb, Z2R_mult. simpl; field. -apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2). -simpl; auto with real. -rewrite Rmult_0_r, <-Z2R_mult, <-Hb. +apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2). +rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb. apply radix_pos. apply trans_eq with (-1+Fexp (Fplus beta d u'))%Z. unfold Fmult. @@ -752,9 +736,8 @@ unfold Rdiv; apply f_equal. unfold F2R; simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r, Hb, Z2R_mult. simpl; field. -apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2). -simpl; auto with real. -rewrite Rmult_0_r, <-Z2R_mult, <-Hb. +apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2). +rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb. apply radix_pos. apply trans_eq with (-1+Fexp u)%Z. unfold Fmult. |