diff options
Diffstat (limited to 'flocq/Appli/Fappli_double_round.v')
| -rw-r--r-- | flocq/Appli/Fappli_double_round.v | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/flocq/Appli/Fappli_double_round.v b/flocq/Appli/Fappli_double_round.v index 3ff6c31a..2c4937ab 100644 --- a/flocq/Appli/Fappli_double_round.v +++ b/flocq/Appli/Fappli_double_round.v @@ -183,8 +183,8 @@ destruct (Req_dec x' 0) as [Zx'|Nzx']. apply Rplus_le_compat_r. apply (Rmult_le_reg_r (bpow (- ln_beta x))); [now apply bpow_gt_0|]. unfold ulp, canonic_exp; bpow_simplify. - rewrite <- (Rinv_r 2) at 3; [|lra]. - rewrite Rmult_comm; apply Rmult_le_compat_r; [lra|]. + apply Rmult_le_reg_l with (1 := Rlt_0_2). + replace (2 * (/ 2 * _)) with (bpow (fexp1 (ln_beta x) - ln_beta x)) by field. apply Rle_trans with 1; [|lra]. change 1 with (bpow 0); apply bpow_le. omega. @@ -1037,10 +1037,11 @@ destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z); [now apply Hexp4; omega|]. assert (Bpow2 : bpow (- 2) <= / 2 * / 2). -{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite <- Rinv_mult_distr; [|lra|lra]. +{ replace (/2 * /2) with (/4) by field. + rewrite (bpow_opp _ 2). apply Rinv_le; [lra|]. - change 4 with (Z2R (2 * 2)); apply Z2R_le; rewrite Zmult_1_r. + apply (Z2R_le (2 * 2) (beta * (beta * 1))). + rewrite Zmult_1_r. now apply Zmult_le_compat; omega. } assert (P2 : (0 < 2)%Z) by omega. unfold double_round_eq. @@ -1384,10 +1385,11 @@ assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z); assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. assert (Bpow2 : bpow (- 2) <= / 2 * / 2). -{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl. - rewrite <- Rinv_mult_distr; [|lra|lra]. +{ replace (/2 * /2) with (/4) by field. + rewrite (bpow_opp _ 2). apply Rinv_le; [lra|]. - change 4 with (Z2R (2 * 2)); apply Z2R_le; rewrite Zmult_1_r. + apply (Z2R_le (2 * 2) (beta * (beta * 1))). + rewrite Zmult_1_r. now apply Zmult_le_compat; omega. } assert (Ly : y < bpow (ln_beta y)). { apply Rabs_lt_inv. @@ -1449,7 +1451,7 @@ apply double_round_gt_mid. unfold canonic_exp. apply (Rplus_le_reg_r (bpow (fexp2 (ln_beta (x - y))))); ring_simplify. apply Rle_trans with (2 * bpow (fexp1 (ln_beta (x - y)) - 1)). - * rewrite Rmult_plus_distr_r; rewrite Rmult_1_l. + * replace (2 * bpow (fexp1 (ln_beta (x - y)) - 1)) with (bpow (fexp1 (ln_beta (x - y)) - 1) + bpow (fexp1 (ln_beta (x - y)) - 1)) by ring. apply Rplus_le_compat_l. now apply bpow_le. * unfold Zminus; rewrite bpow_plus. @@ -1458,10 +1460,10 @@ apply double_round_gt_mid. apply Rmult_le_compat_l; [now apply bpow_ge_0|]. unfold Fcore_Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r. - rewrite <- (Rinv_r 2) at 3; [|lra]. - rewrite Rmult_comm; apply Rmult_le_compat_l; [lra|]. - apply Rinv_le; [lra|]. - now change 2 with (Z2R 2); apply Z2R_le. + apply Z2R_le, Rinv_le in Hbeta. + simpl in Hbeta. + lra. + apply Rlt_0_2. Qed. (* double_round_minus_aux{0,1,2} together *) @@ -4220,7 +4222,7 @@ destruct (Zle_or_lt Z0 (fexp1 (ln_beta x) - fexp1 (ln_beta (x / y)) bpow_simplify. rewrite (Rmult_comm _ y). do 2 rewrite Rmult_assoc. - change (Z2R _ * _) with x'. + change (Z2R (Zfloor _) * _) with x'. change (bpow _) with u1. apply (Rmult_lt_reg_l (/ 2)); [lra|]. rewrite Rmult_plus_distr_l. |