From 0af966a42eb60e9af43f9a450d924758a83946c6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Sep 2015 15:41:50 +0200 Subject: Upgrade to Flocq 2.5.0. Note: this version of Flocq is compatible with both Coq 8.4 and 8.5. --- flocq/Appli/Fappli_IEEE.v | 38 +- flocq/Appli/Fappli_IEEE_bits.v | 4 +- flocq/Appli/Fappli_double_round.v | 179 ++- flocq/Appli/Fappli_rnd_odd.v | 98 +- flocq/Core/Fcore_FIX.v | 13 + flocq/Core/Fcore_FLT.v | 71 +- flocq/Core/Fcore_FLX.v | 38 + flocq/Core/Fcore_FTZ.v | 17 +- flocq/Core/Fcore_Raux.v | 185 +++ flocq/Core/Fcore_Zaux.v | 62 + flocq/Core/Fcore_digits.v | 11 +- flocq/Core/Fcore_float_prop.v | 31 + flocq/Core/Fcore_generic_fmt.v | 25 +- flocq/Core/Fcore_rnd.v | 4 +- flocq/Core/Fcore_rnd_ne.v | 8 +- flocq/Core/Fcore_ulp.v | 2906 ++++++++++++++++++++++++------------- flocq/Flocq_version.v | 5 +- flocq/Prop/Fprop_div_sqrt_error.v | 16 +- flocq/Prop/Fprop_mult_error.v | 5 +- flocq/Prop/Fprop_relative.v | 168 +-- 20 files changed, 2625 insertions(+), 1259 deletions(-) (limited to 'flocq') diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v index 9b5826c1..23999a50 100644 --- a/flocq/Appli/Fappli_IEEE.v +++ b/flocq/Appli/Fappli_IEEE.v @@ -48,9 +48,9 @@ Section Binary. Implicit Arguments exist [[A] [P]]. -(** prec is the number of bits of the mantissa including the implicit one - emax is the exponent of the infinities - Typically p=24 and emax = 128 in single precision *) +(** [prec] is the number of bits of the mantissa including the implicit one; + [emax] is the exponent of the infinities. + For instance, binary32 is defined by [prec = 24] and [emax = 128]. *) Variable prec emax : Z. Context (prec_gt_0_ : Prec_gt_0 prec). Hypothesis Hmax : (prec < emax)%Z. @@ -74,8 +74,7 @@ Definition valid_binary x := end. (** Basic type used for representing binary FP numbers. - Note that there is exactly one such object per FP datum. - NaNs do not have any payload. They cannot be distinguished. *) + Note that there is exactly one such object per FP datum. *) Definition nan_pl := {pl | (Zpos (digits2_pos pl) @@ -647,7 +648,8 @@ generalize (prec_gt_0 prec). clear -Hmax ; omega. Qed. -(** mantissa, round and sticky bits *) +(** Truncation *) + Record shr_record := { shr_m : Z ; shr_r : bool ; shr_s : bool }. Definition shr_1 mrs := @@ -695,7 +697,7 @@ Qed. Definition shr mrs e n := match n with - | Zpos p => (iter_pos p _ shr_1 mrs, (e + n)%Z) + | Zpos p => (iter_pos shr_1 p mrs, (e + n)%Z) | _ => (mrs, e) end. @@ -746,24 +748,24 @@ destruct n as [|n|n]. now destruct l as [|[| |]]. 2: now destruct l as [|[| |]]. unfold shr. -rewrite iter_nat_of_P. +rewrite iter_pos_nat. rewrite Zpos_eq_Z_of_nat_o_nat_of_P. induction (nat_of_P n). simpl. rewrite Zplus_0_r. now destruct l as [|[| |]]. -simpl nat_rect. +rewrite iter_nat_S. rewrite inj_S. unfold Zsucc. -rewrite Zplus_assoc. +rewrite Zplus_assoc. revert IHn0. apply inbetween_shr_1. clear -Hm. induction n0. now destruct l as [|[| |]]. -simpl. +rewrite iter_nat_S. revert IHn0. -generalize (iter_nat n0 shr_record shr_1 (shr_record_of_loc m l)). +generalize (iter_nat shr_1 n0 (shr_record_of_loc m l)). clear. intros (m, r, s) Hm. now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|]. @@ -827,6 +829,8 @@ intros H. now inversion H. Qed. +(** Rounding modes *) + Inductive mode := mode_NE | mode_ZR | mode_DN | mode_UP | mode_NA. Definition round_mode m := @@ -927,7 +931,6 @@ destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2). rewrite shr_m_shr_record_of_loc. intros Hm2. rewrite Hm2. -intros z. repeat split. rewrite Rlt_bool_true. repeat split. @@ -1178,6 +1181,8 @@ destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Hx], y as [sy|sy|sy [ply Hply]|sy my apply B2FF_FF2B. Qed. +(** Normalization and rounding *) + Definition shl_align mx ex ex' := match (ex' - ex)%Z with | Zneg d => (shift_pos d mx, ex') @@ -1361,6 +1366,7 @@ now apply F2R_lt_0_compat. Qed. (** Addition *) + Definition Bplus plus_nan m x y := let f pl := B754_nan (fst pl) (snd pl) in match x, y with @@ -1475,7 +1481,7 @@ elim Rle_not_lt with (1 := Bz). generalize (bounded_lt_emax _ _ Hx) (bounded_lt_emax _ _ Hy) (andb_prop _ _ Hx) (andb_prop _ _ Hy). intros Bx By (Hx',_) (Hy',_). generalize (canonic_canonic_mantissa sx _ _ Hx') (canonic_canonic_mantissa sy _ _ Hy'). -clear -Bx By Hs. +clear -Bx By Hs prec_gt_0_. intros Cx Cy. destruct sx. (* ... *) @@ -1542,6 +1548,8 @@ now apply f_equal. apply Sz. Qed. +(** Subtraction *) + Definition Bminus minus_nan m x y := Bplus minus_nan m x (Bopp pair y). Theorem Bminus_correct : @@ -1571,6 +1579,7 @@ rewrite is_finite_Bopp. auto. now destruct y as [ | | | ]. Qed. (** Division *) + Definition Fdiv_core_binary m1 e1 m2 e2 := let d1 := Zdigits2 m1 in let d2 := Zdigits2 m2 in @@ -1737,6 +1746,7 @@ now rewrite B2FF_FF2B. Qed. (** Square root *) + Definition Fsqrt_core_binary m e := let d := Zdigits2 m in let s := Zmax (2 * prec - d) 0 in diff --git a/flocq/Appli/Fappli_IEEE_bits.v b/flocq/Appli/Fappli_IEEE_bits.v index 5a77bf57..87aa1046 100644 --- a/flocq/Appli/Fappli_IEEE_bits.v +++ b/flocq/Appli/Fappli_IEEE_bits.v @@ -617,7 +617,7 @@ apply refl_equal. Qed. Definition default_nan_pl32 : bool * nan_pl 24 := - (false, exist _ (iter_nat 22 _ xO xH) (refl_equal true)). + (false, exist _ (iter_nat xO 22 xH) (refl_equal true)). Definition unop_nan_pl32 (f : binary32) : bool * nan_pl 24 := match f with @@ -660,7 +660,7 @@ apply refl_equal. Qed. Definition default_nan_pl64 : bool * nan_pl 53 := - (false, exist _ (iter_nat 51 _ xO xH) (refl_equal true)). + (false, exist _ (iter_nat xO 51 xH) (refl_equal true)). Definition unop_nan_pl64 (f : binary64) : bool * nan_pl 53 := match f with diff --git a/flocq/Appli/Fappli_double_round.v b/flocq/Appli/Fappli_double_round.v index f83abc47..3ff6c31a 100644 --- a/flocq/Appli/Fappli_double_round.v +++ b/flocq/Appli/Fappli_double_round.v @@ -72,12 +72,15 @@ assert (Hx2 : x - round beta fexp1 Zfloor x < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)). { now apply (Rplus_lt_reg_r (round beta fexp1 Zfloor x)); ring_simplify. } set (x'' := round beta fexp2 (Znearest choice2) x). -assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x))); - [now unfold x''; apply ulp_half_error|]. +assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x))). +apply Rle_trans with (/ 2 * ulp beta fexp2 x). +now unfold x''; apply error_le_half_ulp... +rewrite ulp_neq_0;[now right|now apply Rgt_not_eq]. assert (Pxx' : 0 <= x - x'). { apply Rle_0_minus. apply round_DN_pt. exact Vfexp1. } +rewrite 2!ulp_neq_0 in Hx2; try (apply Rgt_not_eq; assumption). assert (Hr2 : Rabs (x'' - x') < / 2 * bpow (fexp1 (ln_beta x))). { replace (x'' - x') with (x'' - x + (x - x')) by ring. apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)). @@ -114,6 +117,7 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx'']. + (bpow (ln_beta x) - / 2 * bpow (fexp2 (ln_beta x)))) by ring. apply Rplus_le_lt_compat; [exact Hr1|]. + rewrite ulp_neq_0 in Hx1;[idtac| now apply Rgt_not_eq]. now rewrite Rabs_right; [|apply Rle_ge; apply Rlt_le]. - unfold x'' in Nzx'' |- *. now apply ln_beta_round_ge; [|apply valid_rnd_N|]. } @@ -168,12 +172,14 @@ assert (Pxx' : 0 <= x - x'). apply round_DN_pt. exact Vfexp1. } assert (x < bpow (ln_beta x) - / 2 * bpow (fexp2 (ln_beta x))); - [|now apply double_round_lt_mid_further_place']. + [|apply double_round_lt_mid_further_place'; try assumption]... +2: rewrite ulp_neq_0;[assumption|now apply Rgt_not_eq]. destruct (Req_dec x' 0) as [Zx'|Nzx']. - (* x' = 0 *) rewrite Zx' in Hx2; rewrite Rminus_0_r in Hx2. apply (Rlt_le_trans _ _ _ Hx2). rewrite Rmult_minus_distr_l. + rewrite 2!ulp_neq_0;[idtac|now apply Rgt_not_eq|now apply Rgt_not_eq]. 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. @@ -199,7 +205,7 @@ destruct (Req_dec x' 0) as [Zx'|Nzx']. { apply (Rplus_le_reg_r (ulp beta fexp1 x)); ring_simplify. rewrite <- ulp_DN. - change (round _ _ _ _) with x'. - apply succ_le_bpow. + apply id_p_ulp_le_bpow. + exact Px'. + change x' with (round beta fexp1 Zfloor x). now apply generic_format_round; [|apply valid_rnd_DN]. @@ -210,10 +216,14 @@ destruct (Req_dec x' 0) as [Zx'|Nzx']. - exact Vfexp1. - exact Px'. } fold (canonic_exp beta fexp2 x); fold (ulp beta fexp2 x). - assert (/ 2 * ulp beta fexp1 x <= ulp beta fexp1 x); [|lra]. + assert (/ 2 * ulp beta fexp1 x <= ulp beta fexp1 x). rewrite <- (Rmult_1_l (ulp _ _ _)) at 2. apply Rmult_le_compat_r; [|lra]. - apply bpow_ge_0. + apply ulp_ge_0. + rewrite 2!ulp_neq_0 in Hx2;[|now apply Rgt_not_eq|now apply Rgt_not_eq]. + rewrite ulp_neq_0 in Hx';[|now apply Rgt_not_eq]. + rewrite ulp_neq_0 in H;[|now apply Rgt_not_eq]. + lra. Qed. Lemma double_round_lt_mid_same_place : @@ -256,7 +266,7 @@ assert (H : Rabs (x * bpow (- fexp1 (ln_beta x)) - rewrite <- (Rmult_0_r (/ 2)). apply Rmult_lt_compat_l; [lra|]. apply bpow_gt_0. - - exact Hx. } + - rewrite ulp_neq_0 in Hx;try apply Rgt_not_eq; assumption. } unfold round at 2. unfold F2R, scaled_mantissa, canonic_exp; simpl. rewrite Hf2f1. @@ -320,8 +330,10 @@ unfold double_round_eq. set (x' := round beta fexp1 Zceil x). set (x'' := round beta fexp2 (Znearest choice2) x). intros Hx1 Hx2. -assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x))); - [now unfold x''; apply ulp_half_error|]. +assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x))). + apply Rle_trans with (/2* ulp beta fexp2 x). + now unfold x''; apply error_le_half_ulp... + rewrite ulp_neq_0;[now right|now apply Rgt_not_eq]. assert (Px'x : 0 <= x' - x). { apply Rle_0_minus. apply round_UP_pt. @@ -335,6 +347,7 @@ assert (Hr2 : Rabs (x'' - x') < / 2 * bpow (fexp1 (ln_beta x))). apply Rplus_le_lt_compat. - exact Hr1. - rewrite Rabs_minus_sym. + rewrite 2!ulp_neq_0 in Hx2; try (apply Rgt_not_eq; assumption). now rewrite Rabs_right; [|now apply Rle_ge]; apply Hx2. } destruct (Req_dec x'' 0) as [Zx''|Nzx'']. - (* x'' = 0 *) @@ -382,7 +395,8 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx'']. apply (Rlt_le_trans _ _ _ Hx2). apply Rmult_le_compat_l; [lra|]. generalize (bpow_ge_0 beta (fexp2 (ln_beta x))). - unfold ulp, canonic_exp; lra. + rewrite 2!ulp_neq_0; try (apply Rgt_not_eq; assumption). + unfold canonic_exp; lra. + apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; [|now apply Rle_ge; apply bpow_ge_0]. @@ -422,7 +436,7 @@ assert (Hx''pow : x'' = bpow (ln_beta x)). { apply Rle_lt_trans with (x + / 2 * ulp beta fexp2 x). - apply (Rplus_le_reg_r (- x)); ring_simplify. apply Rabs_le_inv. - apply ulp_half_error. + apply error_le_half_ulp. exact Vfexp2. - apply Rplus_lt_compat_r. rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. @@ -442,15 +456,17 @@ assert (Hx''pow : x'' = bpow (ln_beta x)). apply (Rlt_le_trans _ _ _ H'x''). apply Rplus_le_compat_l. rewrite <- (Rmult_1_l (Fcore_Raux.bpow _ _)). + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. lra. } assert (Hr : Rabs (x - x'') < / 2 * ulp beta fexp1 x). { apply Rle_lt_trans with (/ 2 * ulp beta fexp2 x). - rewrite Rabs_minus_sym. - apply ulp_half_error. + apply error_le_half_ulp. exact Vfexp2. - apply Rmult_lt_compat_l; [lra|]. - unfold ulp, canonic_exp; apply bpow_lt. + rewrite 2!ulp_neq_0; try now apply Rgt_not_eq. + unfold canonic_exp; apply bpow_lt. omega. } unfold round, F2R, scaled_mantissa, canonic_exp; simpl. assert (Hf : (0 <= ln_beta x - fexp1 (ln_beta x''))%Z). @@ -475,6 +491,7 @@ rewrite (Znearest_imp _ _ (beta ^ (ln_beta x - fexp1 (ln_beta x'')))%Z). rewrite <- Rabs_mult. rewrite Rmult_minus_distr_r. bpow_simplify. + rewrite ulp_neq_0 in Hr;[idtac|now apply Rgt_not_eq]. rewrite <- Hx''pow; exact Hr. - rewrite Z2R_Zpower; [|exact Hf]. apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x'')))); [now apply bpow_gt_0|]. @@ -522,7 +539,7 @@ assert (H : Rabs (Z2R (Zceil (x * bpow (- fexp1 (ln_beta x)))) + apply Rle_0_minus. apply round_UP_pt. exact Vfexp1. - - exact Hx. } + - rewrite ulp_neq_0 in Hx;[exact Hx|now apply Rgt_not_eq]. } unfold double_round_eq, round at 2. unfold F2R, scaled_mantissa, canonic_exp; simpl. rewrite Hf2f1. @@ -761,9 +778,10 @@ destruct (Req_dec y 0) as [Zy|Nzy]. - (* y = 0 *) now rewrite Zy; rewrite Rplus_0_r. - (* y <> 0 *) - apply (ln_beta_succ beta fexp); [assumption|assumption|]. + apply (ln_beta_plus_eps beta fexp); [assumption|assumption|]. split; [assumption|]. - unfold ulp, canonic_exp. + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. + unfold canonic_exp. destruct (ln_beta y) as (ey, Hey); simpl in *. apply Rlt_le_trans with (bpow ey). + now rewrite <- (Rabs_right y); [apply Hey|apply Rle_ge]. @@ -797,8 +815,7 @@ apply ln_beta_unique. split. - apply Rabs_ge; right. assert (Hy : y < ulp beta fexp (bpow (ln_beta x - 1))). - { unfold ulp, canonic_exp. - rewrite ln_beta_bpow. + { rewrite ulp_bpow. replace (_ + _)%Z with (ln_beta x : Z) by ring. rewrite <- (Rabs_right y); [|now apply Rle_ge; apply Rlt_le]. apply Rlt_le_trans with (bpow (ln_beta y)). @@ -808,7 +825,8 @@ split. apply Rle_trans with (bpow (ln_beta x - 1) + ulp beta fexp (bpow (ln_beta x - 1))). + now apply Rplus_le_compat_l; apply Rlt_le. - + apply succ_le_lt; [|exact Fx|now split; [apply bpow_gt_0|]]. + + rewrite <- succ_eq_pos;[idtac|apply bpow_ge_0]. + apply succ_le_lt; [apply Vfexp|idtac|exact Fx|assumption]. apply (generic_format_bpow beta fexp (ln_beta x - 1)). replace (_ + _)%Z with (ln_beta x : Z) by ring. assert (fexp (ln_beta x) < ln_beta x)%Z; [|omega]. @@ -1039,13 +1057,15 @@ apply double_round_lt_mid. apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 2 P2 fexp1 x y Px Py Hly Lxy Fx))). ring_simplify. - unfold ulp, canonic_exp; rewrite Lxy. + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. + unfold canonic_exp; rewrite Lxy. apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. bpow_simplify. apply (Rle_trans _ _ _ Bpow2). rewrite <- (Rmult_1_r (/ 2)) at 3. apply Rmult_le_compat_l; lra. -- unfold ulp, round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy. +- rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. + unfold round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy. intro Hf2'. apply (Rmult_lt_reg_r (bpow (- fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. @@ -1056,7 +1076,8 @@ apply double_round_lt_mid. apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 2 P2 fexp1 x y Px Py Hly Lxy Fx))). apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. - unfold ulp, canonic_exp; rewrite Lxy, Rmult_minus_distr_r; bpow_simplify. + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. + unfold canonic_exp; rewrite Lxy, Rmult_minus_distr_r; bpow_simplify. apply (Rle_trans _ _ _ Bpow2). rewrite <- (Rmult_1_r (/ 2)) at 3; rewrite <- Rmult_minus_distr_l. apply Rmult_le_compat_l; [lra|]. @@ -1391,7 +1412,8 @@ apply double_round_gt_mid. [now apply double_round_minus_aux2_aux; try assumption; omega|]. apply (Rlt_le_trans _ _ _ Ly). now apply bpow_le. - + unfold ulp, canonic_exp. + + rewrite ulp_neq_0;[idtac|now apply sym_not_eq, Rlt_not_eq, Rgt_minus]. + unfold canonic_exp. replace (_ - 2)%Z with (fexp1 (ln_beta (x - y)) - 1 - 1)%Z by ring. unfold Zminus at 1; rewrite bpow_plus. rewrite Rmult_comm. @@ -1423,7 +1445,8 @@ apply double_round_gt_mid. + unfold Fcore_Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le; [lra|]. now change 2 with (Z2R 2); apply Z2R_le. - + unfold ulp, canonic_exp. + + rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, Rgt_minus. + 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. @@ -1868,19 +1891,22 @@ apply double_round_lt_mid. apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 1 P1 fexp1 x y Px Py Hly Lxy Fx))). ring_simplify. - unfold ulp, canonic_exp; rewrite Lxy. + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. + unfold canonic_exp; rewrite Lxy. apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. bpow_simplify. apply (Rle_trans _ _ _ Bpow3); lra. -- unfold ulp, round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy. +- rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. + unfold round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy. intro Hf2'. unfold midp. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))); ring_simplify. rewrite <- Rmult_minus_distr_l. apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 1 P1 fexp1 x y Px Py Hly Lxy Fx))). - unfold ulp, canonic_exp; rewrite Lxy. + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. + unfold canonic_exp; rewrite Lxy. apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); [now apply bpow_gt_0|]. rewrite (Rmult_assoc (/ 2)). @@ -2106,7 +2132,8 @@ apply double_round_gt_mid. [now apply double_round_minus_aux2_aux|]. apply (Rlt_le_trans _ _ _ Ly). now apply bpow_le. - + unfold ulp, canonic_exp. + + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rgt_minus]. + unfold canonic_exp. unfold Zminus at 1; rewrite bpow_plus. rewrite Rmult_comm. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. @@ -2124,7 +2151,8 @@ apply double_round_gt_mid. apply (Rlt_le_trans _ _ _ Ly). apply Rle_trans with (bpow (fexp1 (ln_beta (x - y)) - 1)); [now apply bpow_le|]. - unfold ulp, canonic_exp. + rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, Rgt_minus. + unfold canonic_exp. apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta (x - y))))); [now apply bpow_gt_0|]. rewrite Rmult_assoc. @@ -2533,7 +2561,7 @@ destruct (generic_format_EM beta fexp1 x) as [Fx|Nfx]. now apply (generic_inclusion_ln_beta beta fexp1); [omega|]. - (* ~ generic_format beta fexp1 x *) assert (Hceil : round beta fexp1 Zceil x = rd + u1); - [now apply ulp_DN_UP|]. + [now apply round_UP_DN_ulp|]. assert (Hf2' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z); [omega|]. destruct (Rlt_or_le (x - rd) (/ 2 * (u1 - u2))). + (* x - rd < / 2 * (u1 - u2) *) @@ -2589,10 +2617,11 @@ assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop). now apply Zle_bool_imp_le. } set (a := round beta fexp1 Zfloor (sqrt x)). -set (u1 := ulp beta fexp1 (sqrt x)). -set (u2 := ulp beta fexp2 (sqrt x)). +set (u1 := bpow (fexp1 (ln_beta (sqrt x)))). +set (u2 := bpow (fexp2 (ln_beta (sqrt x)))). set (b := / 2 * (u1 - u2)). set (b' := / 2 * (u1 + u2)). +unfold midp; rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, sqrt_lt_R0. apply Rnot_ge_lt; intro H; apply Rge_le in H. assert (Fa : generic_format beta fexp1 a). { unfold a. @@ -2619,7 +2648,7 @@ assert (Pb : 0 < b). rewrite <- (Rmult_0_r (/ 2)). apply Rmult_lt_compat_l; [lra|]. apply Rlt_Rminus. - unfold u2, u1, ulp, canonic_exp. + unfold u2, u1. apply bpow_lt. omega. } assert (Pb' : 0 < b'). @@ -2686,7 +2715,7 @@ destruct (Req_dec a 0) as [Za|Nza]. - (* a <> 0 *) assert (Pa : 0 < a); [lra|]. assert (Hla : (ln_beta a = ln_beta (sqrt x) :> Z)). - { unfold a; apply ln_beta_round_DN. + { unfold a; apply ln_beta_DN. - exact Vfexp1. - now fold a. } assert (Hl' : 0 < - (u2 * a) + b * b). @@ -2697,12 +2726,14 @@ destruct (Req_dec a 0) as [Za|Nza]. replace (_ / 8) with (/ 4 * (u2 ^ 2 + u1 ^ 2)) by field. apply Rlt_le_trans with (u2 * bpow (ln_beta (sqrt x))). - apply Rmult_lt_compat_l; [now unfold u2, ulp; apply bpow_gt_0|]. - unfold u1, ulp, canonic_exp; rewrite <- Hla. - apply Rlt_le_trans with (a + ulp beta fexp1 a). + unfold u1; rewrite <- Hla. + apply Rlt_le_trans with (a + bpow (fexp1 (ln_beta a))). + apply Rplus_lt_compat_l. - rewrite <- (Rmult_1_l (ulp _ _ _)). + rewrite <- (Rmult_1_l (bpow _)) at 2. apply Rmult_lt_compat_r; [apply bpow_gt_0|lra]. - + apply (succ_le_bpow _ _ _ _ Pa Fa). + + apply Rle_trans with (a+ ulp beta fexp1 a). + right; now rewrite ulp_neq_0. + apply (id_p_ulp_le_bpow _ _ _ _ Pa Fa). apply Rabs_lt_inv, bpow_ln_beta_gt. - apply Rle_trans with (bpow (- 2) * u1 ^ 2). + unfold pow; rewrite Rmult_1_r. @@ -2745,9 +2776,10 @@ destruct (Req_dec a 0) as [Za|Nza]. apply Rlt_le_trans with (bpow (ln_beta (sqrt x)) * u2). - apply Rmult_lt_compat_r; [now unfold u2, ulp; apply bpow_gt_0|]. apply Rlt_le_trans with (a + u1); [lra|]. - unfold u1. - rewrite <- ulp_DN; [|exact Vfexp1|exact Pa]; fold a. - apply succ_le_bpow. + unfold u1; fold (canonic_exp beta fexp1 (sqrt x)). + rewrite <- canonic_exp_DN; [|exact Vfexp1|exact Pa]; fold a. + rewrite <- ulp_neq_0; trivial. + apply id_p_ulp_le_bpow. + exact Pa. + now apply round_DN_pt. + apply Rle_lt_trans with (sqrt x). @@ -2782,21 +2814,6 @@ destruct (Req_dec a 0) as [Za|Nza]. + now apply Rle_trans with x. Qed. -(* --> Fcore_Raux *) -Lemma sqrt_neg : forall x, x <= 0 -> sqrt x = 0. -Proof. -intros x Npx. -destruct (Req_dec x 0) as [Zx|Nzx]. -- (* x = 0 *) - rewrite Zx. - exact sqrt_0. -- (* x < 0 *) - unfold sqrt. - destruct Rcase_abs. - + reflexivity. - + casetype False. - now apply Nzx, Rle_antisym; [|apply Rge_le]. -Qed. Lemma double_round_sqrt : forall fexp1 fexp2 : Z -> Z, @@ -3028,10 +3045,11 @@ Lemma double_round_sqrt_beta_ge_4_aux : Proof. intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx. set (a := round beta fexp1 Zfloor (sqrt x)). -set (u1 := ulp beta fexp1 (sqrt x)). -set (u2 := ulp beta fexp2 (sqrt x)). +set (u1 := bpow (fexp1 (ln_beta (sqrt x)))). +set (u2 := bpow (fexp2 (ln_beta (sqrt x)))). set (b := / 2 * (u1 - u2)). set (b' := / 2 * (u1 + u2)). +unfold midp; rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, sqrt_lt_R0. apply Rnot_ge_lt; intro H; apply Rge_le in H. assert (Fa : generic_format beta fexp1 a). { unfold a. @@ -3125,7 +3143,7 @@ destruct (Req_dec a 0) as [Za|Nza]. - (* a <> 0 *) assert (Pa : 0 < a); [lra|]. assert (Hla : (ln_beta a = ln_beta (sqrt x) :> Z)). - { unfold a; apply ln_beta_round_DN. + { unfold a; apply ln_beta_DN. - exact Vfexp1. - now fold a. } assert (Hl' : 0 < - (u2 * a) + b * b). @@ -3136,12 +3154,13 @@ destruct (Req_dec a 0) as [Za|Nza]. replace (_ / 8) with (/ 4 * (u2 ^ 2 + u1 ^ 2)) by field. apply Rlt_le_trans with (u2 * bpow (ln_beta (sqrt x))). - apply Rmult_lt_compat_l; [now unfold u2, ulp; apply bpow_gt_0|]. - unfold u1, ulp, canonic_exp; rewrite <- Hla. + unfold u1; rewrite <- Hla. apply Rlt_le_trans with (a + ulp beta fexp1 a). + apply Rplus_lt_compat_l. rewrite <- (Rmult_1_l (ulp _ _ _)). + rewrite ulp_neq_0; trivial. apply Rmult_lt_compat_r; [apply bpow_gt_0|lra]. - + apply (succ_le_bpow _ _ _ _ Pa Fa). + + apply (id_p_ulp_le_bpow _ _ _ _ Pa Fa). apply Rabs_lt_inv, bpow_ln_beta_gt. - apply Rle_trans with (bpow (- 1) * u1 ^ 2). + unfold pow; rewrite Rmult_1_r. @@ -3184,9 +3203,10 @@ destruct (Req_dec a 0) as [Za|Nza]. apply Rlt_le_trans with (bpow (ln_beta (sqrt x)) * u2). - apply Rmult_lt_compat_r; [now unfold u2, ulp; apply bpow_gt_0|]. apply Rlt_le_trans with (a + u1); [lra|]. - unfold u1. - rewrite <- ulp_DN; [|exact Vfexp1|exact Pa]; fold a. - apply succ_le_bpow. + unfold u1; fold (canonic_exp beta fexp1 (sqrt x)). + rewrite <- canonic_exp_DN; [|exact Vfexp1|exact Pa]; fold a. + rewrite <- ulp_neq_0; trivial. + apply id_p_ulp_le_bpow. + exact Pa. + now apply round_DN_pt. + apply Rle_lt_trans with (sqrt x). @@ -3504,9 +3524,11 @@ assert (Hf : F2R f = x). rewrite (Rmult_assoc _ (Z2R n)). rewrite Rinv_r; [rewrite Rmult_1_r|change 0 with (Z2R 0); apply Z2R_neq; omega]. - simpl; fold (canonic_exp beta fexp1 x); fold (ulp beta fexp1 x); fold u. - rewrite Xmid at 2. + simpl; fold (canonic_exp beta fexp1 x). + rewrite <- 2!ulp_neq_0; try now apply Rgt_not_eq. + fold u; rewrite Xmid at 2. apply f_equal2; [|reflexivity]. + rewrite ulp_neq_0; try now apply Rgt_not_eq. destruct (Req_dec rd 0) as [Zrd|Nzrd]. - (* rd = 0 *) rewrite Zrd. @@ -3657,7 +3679,7 @@ split. replace (bpow _) with (bpow (ln_beta x) - / 2 * u2 + / 2 * u2) by ring. apply Rplus_lt_le_compat; [exact Hx|]. apply Rabs_le_inv. - now apply ulp_half_error. + now apply error_le_half_ulp. Qed. Lemma double_round_all_mid_cases : @@ -3714,7 +3736,7 @@ destruct (Ztrichotomy (ln_beta x) (fexp1 (ln_beta x) - 1)) as [Hlt|[Heq|Hgt]]. now apply (generic_inclusion_ln_beta beta fexp1); [omega|]. - (* ~ generic_format beta fexp1 x *) assert (Hceil : round beta fexp1 Zceil x = x' + u1); - [now apply ulp_DN_UP|]. + [now apply round_UP_DN_ulp|]. assert (Hf2' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z); [omega|]. assert (midp' fexp1 x + / 2 * ulp beta fexp2 x < x); @@ -3769,12 +3791,15 @@ assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); assert (Hfy : (fexp1 (ln_beta y) < ln_beta y)%Z); [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. set (p := bpow (ln_beta (x / y))). -set (u2 := ulp beta fexp2 (x / y)). +set (u2 := bpow (fexp2 (ln_beta (x / y)))). revert Fx Fy. unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl. set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))). set (my := Ztrunc (y * bpow (- fexp1 (ln_beta y)))). intros Fx Fy. +rewrite ulp_neq_0. +2: apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac]. +2: now apply Rinv_neq_0_compat, Rgt_not_eq. intro Hl. assert (Hr : x / y < p); [now apply Rabs_lt_inv; apply bpow_ln_beta_gt|]. @@ -3903,6 +3928,9 @@ assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z); [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. assert (Hfy : (fexp1 (ln_beta y) < ln_beta y)%Z); [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|]. +assert (S : (x / y <> 0)%R). +apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac]. +now apply Rinv_neq_0_compat, Rgt_not_eq. cut (~ (/ 2 * (ulp beta fexp1 (x / y) - ulp beta fexp2 (x / y)) <= x / y - round beta fexp1 Zfloor (x / y) < / 2 * ulp beta fexp1 (x / y))). @@ -3913,9 +3941,10 @@ cut (~ (/ 2 * (ulp beta fexp1 (x / y) - ulp beta fexp2 (x / y)) - apply (Rplus_lt_reg_l (round beta fexp1 Zfloor (x / y))). ring_simplify. apply H'. } -set (u1 := ulp beta fexp1 (x / y)). -set (u2 := ulp beta fexp2 (x / y)). +set (u1 := bpow (fexp1 (ln_beta (x / y)))). +set (u2 := bpow (fexp2 (ln_beta (x / y)))). set (x' := round beta fexp1 Zfloor (x / y)). +rewrite 2!ulp_neq_0; trivial. revert Fx Fy. unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl. set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))). @@ -4098,9 +4127,13 @@ cut (~ (/ 2 * ulp beta fexp1 (x / y) - apply (Rplus_le_reg_l (round beta fexp1 Zfloor (x / y))). ring_simplify. apply H'. } -set (u1 := ulp beta fexp1 (x / y)). -set (u2 := ulp beta fexp2 (x / y)). +set (u1 := bpow (fexp1 (ln_beta (x / y)))). +set (u2 := bpow (fexp2 (ln_beta (x / y)))). set (x' := round beta fexp1 Zfloor (x / y)). +assert (S : (x / y <> 0)%R). +apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac]. +now apply Rinv_neq_0_compat, Rgt_not_eq. +rewrite 2!ulp_neq_0; trivial. revert Fx Fy. unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl. set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))). diff --git a/flocq/Appli/Fappli_rnd_odd.v b/flocq/Appli/Fappli_rnd_odd.v index b3244589..4741047f 100644 --- a/flocq/Appli/Fappli_rnd_odd.v +++ b/flocq/Appli/Fappli_rnd_odd.v @@ -356,6 +356,80 @@ simpl; ring. apply Rgt_not_eq, bpow_gt_0. Qed. + + +Theorem Rnd_odd_pt_unicity : + forall x f1 f2 : R, + Rnd_odd_pt x f1 -> Rnd_odd_pt x f2 -> + f1 = f2. +Proof. +intros x f1 f2 (Ff1,H1) (Ff2,H2). +(* *) +case (generic_format_EM beta fexp x); intros L. +apply trans_eq with x. +case H1; try easy. +intros (J,_); case J; intros J'. +apply Rnd_DN_pt_idempotent with format; assumption. +apply Rnd_UP_pt_idempotent with format; assumption. +case H2; try easy. +intros (J,_); case J; intros J'; apply sym_eq. +apply Rnd_DN_pt_idempotent with format; assumption. +apply Rnd_UP_pt_idempotent with format; assumption. +(* *) +destruct H1 as [H1|(H1,H1')]. +contradict L; now rewrite <- H1. +destruct H2 as [H2|(H2,H2')]. +contradict L; now rewrite <- H2. +destruct H1 as [H1|H1]; destruct H2 as [H2|H2]. +apply Rnd_DN_pt_unicity with format x; assumption. +destruct H1' as (ff,(K1,(K2,K3))). +destruct H2' as (gg,(L1,(L2,L3))). +absurd (true = false); try discriminate. +rewrite <- L3. +apply trans_eq with (negb (Zeven (Fnum ff))). +rewrite K3; easy. +apply sym_eq. +generalize (DN_UP_parity_generic beta fexp). +unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption... +rewrite <- K1; apply Rnd_DN_pt_unicity with (generic_format beta fexp) x; try easy... +now apply round_DN_pt... +rewrite <- L1; apply Rnd_UP_pt_unicity with (generic_format beta fexp) x; try easy... +now apply round_UP_pt... +(* *) +destruct H1' as (ff,(K1,(K2,K3))). +destruct H2' as (gg,(L1,(L2,L3))). +absurd (true = false); try discriminate. +rewrite <- K3. +apply trans_eq with (negb (Zeven (Fnum gg))). +rewrite L3; easy. +apply sym_eq. +generalize (DN_UP_parity_generic beta fexp). +unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption... +rewrite <- L1; apply Rnd_DN_pt_unicity with (generic_format beta fexp) x; try easy... +now apply round_DN_pt... +rewrite <- K1; apply Rnd_UP_pt_unicity with (generic_format beta fexp) x; try easy... +now apply round_UP_pt... +apply Rnd_UP_pt_unicity with format x; assumption. +Qed. + + + +Theorem Rnd_odd_pt_monotone : + round_pred_monotone (Rnd_odd_pt). +Proof with auto with typeclass_instances. +intros x y f g H1 H2 Hxy. +apply Rle_trans with (round beta fexp Zrnd_odd x). +right; apply Rnd_odd_pt_unicity with x; try assumption. +apply round_odd_pt. +apply Rle_trans with (round beta fexp Zrnd_odd y). +apply round_le... +right; apply Rnd_odd_pt_unicity with y; try assumption. +apply round_odd_pt. +Qed. + + + + End Fcore_rnd_odd. Section Odd_prop_aux. @@ -462,7 +536,7 @@ Lemma ln_beta_d: (0< F2R d)%R -> (ln_beta beta (F2R d) = ln_beta beta x :>Z). Proof with auto with typeclass_instances. intros Y. -rewrite d_eq; apply ln_beta_round_DN... +rewrite d_eq; apply ln_beta_DN... now rewrite <- d_eq. Qed. @@ -861,13 +935,9 @@ case K2; clear K2; intros K2. case (Rle_or_lt x m); intros Y;[destruct Y|idtac]. (* . *) apply trans_eq with (F2R d). -apply round_N_DN_betw with (F2R u)... +apply round_N_eq_DN_pt with (F2R u)... apply DN_odd_d_aux; split; try left; assumption. apply UP_odd_d_aux; split; try left; assumption. -split. -apply round_ge_generic... -apply generic_format_fexpe_fexp, Hd. -apply Hd. assert (o <= (F2R d + F2R u) / 2)%R. apply round_le_generic... apply Fm. @@ -876,10 +946,7 @@ destruct H1; trivial. apply P. now apply Rlt_not_eq. trivial. -apply sym_eq, round_N_DN_betw with (F2R u)... -split. -apply Hd. -exact H0. +apply sym_eq, round_N_eq_DN_pt with (F2R u)... (* . *) replace o with x. reflexivity. @@ -887,10 +954,9 @@ apply sym_eq, round_generic... rewrite H0; apply Fm. (* . *) apply trans_eq with (F2R u). -apply round_N_UP_betw with (F2R d)... +apply round_N_eq_UP_pt with (F2R d)... apply DN_odd_d_aux; split; try left; assumption. apply UP_odd_d_aux; split; try left; assumption. -split. assert ((F2R d + F2R u) / 2 <= o)%R. apply round_ge_generic... apply Fm. @@ -899,13 +965,7 @@ destruct H0; trivial. apply P. now apply Rgt_not_eq. rewrite <- H0; trivial. -apply round_le_generic... -apply generic_format_fexpe_fexp, Hu. -apply Hu. -apply sym_eq, round_N_UP_betw with (F2R d)... -split. -exact Y. -apply Hu. +apply sym_eq, round_N_eq_UP_pt with (F2R d)... Qed. diff --git a/flocq/Core/Fcore_FIX.v b/flocq/Core/Fcore_FIX.v index a3b8d4d0..e224a64a 100644 --- a/flocq/Core/Fcore_FIX.v +++ b/flocq/Core/Fcore_FIX.v @@ -22,6 +22,7 @@ Require Import Fcore_Raux. Require Import Fcore_defs. Require Import Fcore_rnd. Require Import Fcore_generic_fmt. +Require Import Fcore_ulp. Require Import Fcore_rnd_ne. Section RND_FIX. @@ -84,4 +85,16 @@ intros ex ey H. apply Zle_refl. Qed. +Theorem ulp_FIX: forall x, ulp beta FIX_exp x = bpow emin. +Proof. +intros x; unfold ulp. +case Req_bool_spec; intros Zx. +case (negligible_exp_spec FIX_exp). +intros T; specialize (T (emin-1)%Z); contradict T. +unfold FIX_exp; omega. +intros n _; reflexivity. +reflexivity. +Qed. + + End RND_FIX. diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v index 273ff69f..372af6ad 100644 --- a/flocq/Core/Fcore_FLT.v +++ b/flocq/Core/Fcore_FLT.v @@ -25,6 +25,7 @@ Require Import Fcore_generic_fmt. Require Import Fcore_float_prop. Require Import Fcore_FLX. Require Import Fcore_FIX. +Require Import Fcore_ulp. Require Import Fcore_rnd_ne. Section RND_FLT. @@ -222,7 +223,6 @@ Theorem generic_format_FLT_FIX : generic_format beta (FIX_exp emin) x -> generic_format beta FLT_exp x. Proof with auto with typeclass_instances. -clear prec_gt_0_. apply generic_inclusion_le... intros e He. unfold FIX_exp. @@ -231,6 +231,75 @@ omega. apply Zle_refl. Qed. +Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R -> + ulp beta FLT_exp x = bpow emin. +Proof with auto with typeclass_instances. +intros x Hx. +unfold ulp; case Req_bool_spec; intros Hx2. +(* x = 0 *) +case (negligible_exp_spec FLT_exp). +intros T; specialize (T (emin-1)%Z); contradict T. +apply Zle_not_lt; unfold FLT_exp. +apply Zle_trans with (2:=Z.le_max_r _ _); omega. +assert (V:FLT_exp emin = emin). +unfold FLT_exp; apply Z.max_r. +unfold Prec_gt_0 in prec_gt_0_; omega. +intros n H2; rewrite <-V. +apply f_equal, fexp_negligible_exp_eq... +omega. +(* x <> 0 *) +apply f_equal; unfold canonic_exp, FLT_exp. +apply Z.max_r. +assert (ln_beta beta x-1 < emin+prec)%Z;[idtac|omega]. +destruct (ln_beta beta x) as (e,He); simpl. +apply lt_bpow with beta. +apply Rle_lt_trans with (2:=Hx). +now apply He. +Qed. + +Theorem ulp_FLT_le: forall x, (bpow (emin+prec) <= Rabs x)%R -> + (ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R. +Proof. +intros x Hx. +assert (x <> 0)%R. +intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt. +rewrite Z, Rabs_R0; apply bpow_gt_0. +rewrite ulp_neq_0; try assumption. +unfold canonic_exp, FLT_exp. +destruct (ln_beta beta x) as (e,He). +apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R. +rewrite <- bpow_plus. +right; apply f_equal. +apply trans_eq with (e-prec)%Z;[idtac|ring]. +simpl; apply Z.max_l. +assert (emin+prec <= e)%Z; try omega. +apply le_bpow with beta. +apply Rle_trans with (1:=Hx). +left; now apply He. +apply Rmult_le_compat_r. +apply bpow_ge_0. +now apply He. +Qed. + + +Theorem ulp_FLT_ge: forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R. +Proof. +intros x; case (Req_dec x 0); intros Hx. +rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0. +rewrite Rabs_R0; apply bpow_gt_0. +rewrite ulp_neq_0; try exact Hx. +unfold canonic_exp, FLT_exp. +apply Rlt_le_trans with (bpow (ln_beta beta x)*bpow (-prec))%R. +apply Rmult_lt_compat_r. +apply bpow_gt_0. +now apply bpow_ln_beta_gt. +rewrite <- bpow_plus. +apply bpow_le. +apply Z.le_max_l. +Qed. + + + (** FLT is a nice format: it has a monotone exponent... *) Global Instance FLT_exp_monotone : Monotone_exp FLT_exp. Proof. diff --git a/flocq/Core/Fcore_FLX.v b/flocq/Core/Fcore_FLX.v index 800540f2..55f6db61 100644 --- a/flocq/Core/Fcore_FLX.v +++ b/flocq/Core/Fcore_FLX.v @@ -24,6 +24,7 @@ Require Import Fcore_rnd. Require Import Fcore_generic_fmt. Require Import Fcore_float_prop. Require Import Fcore_FIX. +Require Import Fcore_ulp. Require Import Fcore_rnd_ne. Section RND_FLX. @@ -211,6 +212,43 @@ now apply FLXN_format_generic. now apply generic_format_FLXN. Qed. +Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R. +Proof. +unfold ulp; rewrite Req_bool_true; trivial. +case (negligible_exp_spec FLX_exp). +intros _; reflexivity. +intros n H2; contradict H2. +unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega. +Qed. + +Theorem ulp_FLX_le: forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R. +Proof. +intros x; case (Req_dec x 0); intros Hx. +rewrite Hx, ulp_FLX_0, Rabs_R0. +right; ring. +rewrite ulp_neq_0; try exact Hx. +unfold canonic_exp, FLX_exp. +replace (ln_beta beta x - prec)%Z with ((ln_beta beta x - 1) + (1-prec))%Z by ring. +rewrite bpow_plus. +apply Rmult_le_compat_r. +apply bpow_ge_0. +now apply bpow_ln_beta_le. +Qed. + + +Theorem ulp_FLX_ge: forall x, (Rabs x * bpow (-prec) <= ulp beta FLX_exp x)%R. +Proof. +intros x; case (Req_dec x 0); intros Hx. +rewrite Hx, ulp_FLX_0, Rabs_R0. +right; ring. +rewrite ulp_neq_0; try exact Hx. +unfold canonic_exp, FLX_exp. +unfold Zminus; rewrite bpow_plus. +apply Rmult_le_compat_r. +apply bpow_ge_0. +left; now apply bpow_ln_beta_gt. +Qed. + (** FLX is a nice format: it has a monotone exponent... *) Global Instance FLX_exp_monotone : Monotone_exp FLX_exp. Proof. diff --git a/flocq/Core/Fcore_FTZ.v b/flocq/Core/Fcore_FTZ.v index 5f3e5337..2ebc7851 100644 --- a/flocq/Core/Fcore_FTZ.v +++ b/flocq/Core/Fcore_FTZ.v @@ -23,6 +23,7 @@ Require Import Fcore_defs. Require Import Fcore_rnd. Require Import Fcore_generic_fmt. Require Import Fcore_float_prop. +Require Import Fcore_ulp. Require Import Fcore_FLX. Section RND_FTZ. @@ -182,7 +183,6 @@ Theorem FTZ_format_FLXN : (bpow (emin + prec - 1) <= Rabs x)%R -> FLXN_format beta prec x -> FTZ_format x. Proof. -clear prec_gt_0_. intros x Hx Fx. apply FTZ_format_generic. apply generic_format_FLXN in Fx. @@ -195,6 +195,21 @@ apply Zle_refl. omega. Qed. +Theorem ulp_FTZ_0: ulp beta FTZ_exp 0 = bpow (emin+prec-1). +Proof with auto with typeclass_instances. +unfold ulp; rewrite Req_bool_true; trivial. +case (negligible_exp_spec FTZ_exp). +intros T; specialize (T (emin-1)%Z); contradict T. +apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_. +rewrite Zlt_bool_true; omega. +assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z). +unfold FTZ_exp; rewrite Zlt_bool_true; omega. +intros n H2; rewrite <-V. +apply f_equal, fexp_negligible_exp_eq... +omega. +Qed. + + Section FTZ_round. (** Rounding with FTZ *) diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v index 3758324f..d728e0ba 100644 --- a/flocq/Core/Fcore_Raux.v +++ b/flocq/Core/Fcore_Raux.v @@ -207,6 +207,27 @@ rewrite 3!(Rmult_comm r). now apply Rmult_min_distr_r. Qed. +Lemma Rmin_opp: forall x y, (Rmin (-x) (-y) = - Rmax x y)%R. +Proof. +intros x y. +apply Rmax_case_strong; intros H. +rewrite Rmin_left; trivial. +now apply Ropp_le_contravar. +rewrite Rmin_right; trivial. +now apply Ropp_le_contravar. +Qed. + +Lemma Rmax_opp: forall x y, (Rmax (-x) (-y) = - Rmin x y)%R. +Proof. +intros x y. +apply Rmin_case_strong; intros H. +rewrite Rmax_left; trivial. +now apply Ropp_le_contravar. +rewrite Rmax_right; trivial. +now apply Ropp_le_contravar. +Qed. + + Theorem exp_le : forall x y : R, (x <= y)%R -> (exp x <= exp y)%R. @@ -1930,6 +1951,16 @@ destruct (ln_beta x) as (ex, Ex) ; simpl. now apply Ex. Qed. +Theorem bpow_ln_beta_le : + forall x, (x <> 0)%R -> + (bpow (ln_beta x-1) <= Rabs x)%R. +Proof. +intros x Hx. +destruct (ln_beta x) as (ex, Ex) ; simpl. +now apply Ex. +Qed. + + Theorem ln_beta_le_Zpower : forall m e, m <> Z0 -> @@ -2306,6 +2337,160 @@ Qed. End cond_Ropp. + +(** LPO taken from Coquelicot *) + +Theorem LPO_min : + forall P : nat -> Prop, (forall n, P n \/ ~ P n) -> + {n : nat | P n /\ forall i, (i < n)%nat -> ~ P i} + {forall n, ~ P n}. +Proof. +assert (Hi: forall n, (0 < INR n + 1)%R). + intros N. + rewrite <- S_INR. + apply lt_0_INR. + apply lt_0_Sn. +intros P HP. +set (E y := exists n, (P n /\ y = / (INR n + 1))%R \/ (~ P n /\ y = 0)%R). +assert (HE: forall n, P n -> E (/ (INR n + 1))%R). + intros n Pn. + exists n. + left. + now split. +assert (BE: is_upper_bound E 1). + intros x [y [[_ ->]|[_ ->]]]. + rewrite <- Rinv_1 at 2. + apply Rinv_le. + exact Rlt_0_1. + rewrite <- S_INR. + apply (le_INR 1), le_n_S, le_0_n. + exact Rle_0_1. +destruct (completeness E) as [l [ub lub]]. + now exists 1%R. + destruct (HP O) as [H0|H0]. + exists 1%R. + exists O. + left. + apply (conj H0). + rewrite Rplus_0_l. + apply sym_eq, Rinv_1. + exists 0%R. + exists O. + right. + now split. +destruct (Rle_lt_dec l 0) as [Hl|Hl]. + right. + intros n Pn. + apply Rle_not_lt with (1 := Hl). + apply Rlt_le_trans with (/ (INR n + 1))%R. + now apply Rinv_0_lt_compat. + apply ub. + now apply HE. +left. +set (N := Zabs_nat (up (/l) - 2)). +exists N. +assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R). + unfold N. + rewrite INR_IZR_INZ. + rewrite inj_Zabs_nat. + replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R. + apply (f_equal (fun v => IZR v + 1)%R). + apply Zabs_eq. + apply Zle_minus_le_0. + apply (Zlt_le_succ 1). + apply lt_IZR. + apply Rle_lt_trans with (/l)%R. + apply Rmult_le_reg_r with (1 := Hl). + rewrite Rmult_1_l, Rinv_l by now apply Rgt_not_eq. + apply lub. + exact BE. + apply archimed. + rewrite minus_IZR. + simpl. + ring. +assert (H: forall i, (i < N)%nat -> ~ P i). + intros i HiN Pi. + unfold is_upper_bound in ub. + refine (Rle_not_lt _ _ (ub (/ (INR i + 1))%R _) _). + now apply HE. + rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq. + apply Rinv_1_lt_contravar. + rewrite <- S_INR. + apply (le_INR 1). + apply le_n_S. + apply le_0_n. + apply Rlt_le_trans with (INR N + 1)%R. + apply Rplus_lt_compat_r. + now apply lt_INR. + rewrite HN. + apply Rplus_le_reg_r with (-/l + 1)%R. + ring_simplify. + apply archimed. +destruct (HP N) as [PN|PN]. + now split. +elimtype False. +refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _). + intros x [y [[Py ->]|[_ ->]]]. + destruct (eq_nat_dec y N) as [HyN|HyN]. + elim PN. + now rewrite <- HyN. + apply Rinv_le. + apply Hi. + apply Rplus_le_compat_r. + apply Rnot_lt_le. + intros Hy. + refine (H _ _ Py). + apply INR_lt in Hy. + clear -Hy HyN. + omega. + now apply Rlt_le, Rinv_0_lt_compat. +rewrite S_INR, HN. +ring_simplify (IZR (up (/ l)) - 1 + 1)%R. +rewrite <- (Rinv_involutive l) at 2 by now apply Rgt_not_eq. +apply Rinv_1_lt_contravar. +rewrite <- Rinv_1. +apply Rinv_le. +exact Hl. +now apply lub. +apply archimed. +Qed. + +Theorem LPO : + forall P : nat -> Prop, (forall n, P n \/ ~ P n) -> + {n : nat | P n} + {forall n, ~ P n}. +Proof. +intros P HP. +destruct (LPO_min P HP) as [[n [Pn _]]|Pn]. +left. +now exists n. +now right. +Qed. + + +Lemma LPO_Z : forall P : Z -> Prop, (forall n, P n \/ ~P n) -> + {n : Z| P n} + {forall n, ~ P n}. +Proof. +intros P H. +destruct (LPO (fun n => P (Z.of_nat n))) as [J|J]. +intros n; apply H. +destruct J as (n, Hn). +left; now exists (Z.of_nat n). +destruct (LPO (fun n => P (-Z.of_nat n)%Z)) as [K|K]. +intros n; apply H. +destruct K as (n, Hn). +left; now exists (-Z.of_nat n)%Z. +right; intros n; case (Zle_or_lt 0 n); intros M. +rewrite <- (Zabs_eq n); trivial. +rewrite <- Zabs2Nat.id_abs. +apply J. +rewrite <- (Zopp_involutive n). +rewrite <- (Z.abs_neq n). +rewrite <- Zabs2Nat.id_abs. +apply K. +omega. +Qed. + + + (** A little tactic to simplify terms of the form [bpow a * bpow b]. *) Ltac bpow_simplify := (* bpow ex * bpow ey ~~> bpow (ex + ey) *) diff --git a/flocq/Core/Fcore_Zaux.v b/flocq/Core/Fcore_Zaux.v index 4702d62e..f6731b4c 100644 --- a/flocq/Core/Fcore_Zaux.v +++ b/flocq/Core/Fcore_Zaux.v @@ -927,3 +927,65 @@ intros [|a|a] [|b|b] ; try rewrite Zpos_div_eucl_aux_correct ; easy. Qed. End faster_div. + +Section Iter. + +Context {A : Type}. +Variable (f : A -> A). + +Fixpoint iter_nat (n : nat) (x : A) {struct n} : A := + match n with + | S n' => iter_nat n' (f x) + | O => x + end. + +Lemma iter_nat_plus : + forall (p q : nat) (x : A), + iter_nat (p + q) x = iter_nat p (iter_nat q x). +Proof. +induction q. +now rewrite plus_0_r. +intros x. +rewrite <- plus_n_Sm. +apply IHq. +Qed. + +Lemma iter_nat_S : + forall (p : nat) (x : A), + iter_nat (S p) x = f (iter_nat p x). +Proof. +induction p. +easy. +simpl. +intros x. +apply IHp. +Qed. + +Fixpoint iter_pos (n : positive) (x : A) {struct n} : A := + match n with + | xI n' => iter_pos n' (iter_pos n' (f x)) + | xO n' => iter_pos n' (iter_pos n' x) + | xH => f x + end. + +Lemma iter_pos_nat : + forall (p : positive) (x : A), + iter_pos p x = iter_nat (Pos.to_nat p) x. +Proof. +induction p ; intros x. +rewrite Pos2Nat.inj_xI. +simpl. +rewrite plus_0_r. +rewrite iter_nat_plus. +rewrite (IHp (f x)). +apply IHp. +rewrite Pos2Nat.inj_xO. +simpl. +rewrite plus_0_r. +rewrite iter_nat_plus. +rewrite (IHp x). +apply IHp. +easy. +Qed. + +End Iter. diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v index 13174d29..d40c1a09 100644 --- a/flocq/Core/Fcore_digits.v +++ b/flocq/Core/Fcore_digits.v @@ -21,7 +21,7 @@ Require Import ZArith. Require Import Zquot. Require Import Fcore_Zaux. -(** Computes the number of bits (radix 2) of a positive integer. +(** Number of bits (radix 2) of a positive integer. It serves as an upper bound on the number of digits to ensure termination. *) @@ -466,6 +466,8 @@ now apply Hd. now rewrite 3!Zdigit_lt. Qed. +(** Left and right shifts *) + Definition Zscale n k := if Zle_bool 0 k then (n * Zpower beta k)%Z else Z.quot n (Zpower beta (-k)). @@ -545,6 +547,8 @@ rewrite Zle_bool_true with (1 := Hk). now apply Zscale_mul_pow. Qed. +(** Slice of an integer *) + Definition Zslice n k1 k2 := if Zle_bool 0 k2 then Z.rem (Zscale n (-k1)) (Zpower beta k2) else Z0. @@ -756,6 +760,7 @@ Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z := End digits_aux. (** Number of digits of an integer *) + Definition Zdigits n := match n with | Z0 => Z0 @@ -1011,7 +1016,7 @@ generalize (Zpower_gt_Zdigits e x). omega. Qed. -(** Characterizes the number digits of a product. +(** Number of digits of a product. This strong version is needed for proofs of division and square root algorithms, since they involve operation remainders. @@ -1126,6 +1131,8 @@ Qed. End Fcore_digits. +(** Specialized version for computing the number of bits of an integer *) + Section Zdigits2. Theorem Z_of_nat_S_digits2_Pnat : diff --git a/flocq/Core/Fcore_float_prop.v b/flocq/Core/Fcore_float_prop.v index e1535bc9..8199ede6 100644 --- a/flocq/Core/Fcore_float_prop.v +++ b/flocq/Core/Fcore_float_prop.v @@ -233,6 +233,37 @@ rewrite <- F2R_0 with (Fexp f). now apply F2R_lt_compat. Qed. +Theorem F2R_neq_0_compat : + forall f : float beta, + (Fnum f <> 0)%Z -> + (F2R f <> 0)%R. +Proof. +intros f H H1. +apply H. +now apply F2R_eq_0_reg with (Fexp f). +Qed. + + +Lemma Fnum_ge_0_compat: forall (f : float beta), + (0 <= F2R f)%R -> (0 <= Fnum f)%Z. +Proof. +intros f H. +case (Zle_or_lt 0 (Fnum f)); trivial. +intros H1; contradict H. +apply Rlt_not_le. +now apply F2R_lt_0_compat. +Qed. + +Lemma Fnum_le_0_compat: forall (f : float beta), + (F2R f <= 0)%R -> (Fnum f <= 0)%Z. +Proof. +intros f H. +case (Zle_or_lt (Fnum f) 0); trivial. +intros H1; contradict H. +apply Rlt_not_le. +now apply F2R_gt_0_compat. +Qed. + (** Floats and bpow *) Theorem F2R_bpow : forall e : Z, diff --git a/flocq/Core/Fcore_generic_fmt.v b/flocq/Core/Fcore_generic_fmt.v index 45729f2a..bac65b9d 100644 --- a/flocq/Core/Fcore_generic_fmt.v +++ b/flocq/Core/Fcore_generic_fmt.v @@ -1015,7 +1015,7 @@ Qed. End monotone. -Theorem round_abs_abs' : +Theorem round_abs_abs : forall P : R -> R -> Prop, ( forall rnd (Hr : Valid_rnd rnd) x, (0 <= x)%R -> P x (round rnd x) ) -> forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)). @@ -1043,18 +1043,6 @@ apply round_le... now apply Rlt_le. Qed. -(* TODO: remove *) -Theorem round_abs_abs : - forall P : R -> R -> Prop, - ( forall rnd (Hr : Valid_rnd rnd) x, P x (round rnd x) ) -> - forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)). -Proof. -intros P HP. -apply round_abs_abs'. -intros. -now apply HP. -Qed. - Theorem round_bounded_large : forall rnd {Hr : Valid_rnd rnd} x ex, (fexp ex < ex)%Z -> @@ -1064,7 +1052,7 @@ Proof with auto with typeclass_instances. intros rnd Hr x ex He. apply round_abs_abs... clear rnd Hr x. -intros rnd' Hr x. +intros rnd' Hr x _. apply round_bounded_large_pos... Qed. @@ -1076,7 +1064,7 @@ Proof. intros rnd Hr x ex H1 H2. generalize Rabs_R0. rewrite <- H2 at 1. -apply (round_abs_abs' (fun t rt => forall (ex : Z), +apply (round_abs_abs (fun t rt => forall (ex : Z), (bpow (ex - 1) <= t < bpow ex)%R -> rt = 0%R -> (ex <= fexp ex)%Z)); trivial. clear; intros rnd Hr x Hx. @@ -1496,7 +1484,7 @@ right. now rewrite Zmax_l with (1 := Zlt_le_weak _ _ He). Qed. -Theorem ln_beta_round_DN : +Theorem ln_beta_DN : forall x, (0 < round Zfloor x)%R -> (ln_beta beta (round Zfloor x) = ln_beta beta x :> Z). @@ -1513,7 +1501,6 @@ now apply Rgt_not_eq. now apply Rlt_le. Qed. -(* TODO: remove *) Theorem canonic_exp_DN : forall x, (0 < round Zfloor x)%R -> @@ -1521,7 +1508,7 @@ Theorem canonic_exp_DN : Proof. intros x Hd. apply (f_equal fexp). -now apply ln_beta_round_DN. +now apply ln_beta_DN. Qed. Theorem scaled_mantissa_DN : @@ -2312,7 +2299,7 @@ intros x Gx. apply generic_format_abs_inv. apply generic_format_abs in Gx. revert rnd valid_rnd x Gx. -refine (round_abs_abs' _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _). +refine (round_abs_abs _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _). intros rnd valid_rnd x [Hx|Hx] Gx. (* x > 0 *) generalize (ln_beta_generic_gt _ x (Rgt_not_eq _ _ Hx) Gx). diff --git a/flocq/Core/Fcore_rnd.v b/flocq/Core/Fcore_rnd.v index 94c94203..171c27fc 100644 --- a/flocq/Core/Fcore_rnd.v +++ b/flocq/Core/Fcore_rnd.v @@ -39,7 +39,7 @@ exists f. intros g Hg. now apply H2 with (3 := Rle_refl x). (* . *) -exists (projT1 (completeness _ H3 H1)). +exists (proj1_sig (completeness _ H3 H1)). destruct completeness as (f1, (H4, H5)). simpl. destruct H1 as (f2, H1). @@ -58,7 +58,7 @@ Theorem round_fun_of_pred : { f : R -> R | forall x, rnd x (f x) }. Proof. intros rnd H. -exists (fun x => projT1 (round_val_of_pred rnd H x)). +exists (fun x => proj1_sig (round_val_of_pred rnd H x)). intros x. now destruct round_val_of_pred as (f, H1). Qed. diff --git a/flocq/Core/Fcore_rnd_ne.v b/flocq/Core/Fcore_rnd_ne.v index 6829c0c8..1f265406 100644 --- a/flocq/Core/Fcore_rnd_ne.v +++ b/flocq/Core/Fcore_rnd_ne.v @@ -164,7 +164,7 @@ now apply Rlt_le. assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now apply valid_exp. assert (Hud: (F2R xu = F2R xd + ulp beta fexp x)%R). rewrite Hxu, Hxd. -now apply ulp_DN_UP. +now apply round_UP_DN_ulp. destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2]. (* - xu > bpow ex *) elim (Rlt_not_le _ _ Hu2). @@ -191,7 +191,8 @@ rewrite Rmult_plus_distr_r. rewrite Z2R_Zpower, <- bpow_plus. ring_simplify (ex - fexp ex + fexp ex)%Z. rewrite Hu2, Hud. -unfold ulp, canonic_exp. +rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. +unfold canonic_exp. rewrite ln_beta_unique with beta x ex. unfold F2R. simpl. ring. @@ -223,7 +224,8 @@ specialize (H ex). omega. (* - xu < bpow ex *) revert Hud. -unfold ulp, F2R. +rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. +unfold F2R. rewrite Hd, Hu. unfold canonic_exp. rewrite ln_beta_unique with beta (F2R xu) ex. diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v index 04bed01c..1c27de31 100644 --- a/flocq/Core/Fcore_ulp.v +++ b/flocq/Core/Fcore_ulp.v @@ -32,9 +32,79 @@ Notation bpow e := (bpow beta e). Variable fexp : Z -> Z. +(** Definition and basic properties about the minimal exponent, when it exists *) + +Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z. +intros. +destruct (Z_le_dec x y). +now left. +now right. +Qed. + + +(** [negligible_exp] is either none (as in FLX) or Some n such that n <= fexp n. *) +Definition negligible_exp: option Z := + match (LPO_Z _ (fun z => Z_le_dec_aux z (fexp z))) with + | inleft N => Some (proj1_sig N) + | inright _ => None + end. + + +Inductive negligible_exp_prop: option Z -> Prop := + | negligible_None: (forall n, (fexp n < n)%Z) -> negligible_exp_prop None + | negligible_Some: forall n, (n <= fexp n)%Z -> negligible_exp_prop (Some n). + + +Lemma negligible_exp_spec: negligible_exp_prop negligible_exp. +Proof. +unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. +now apply negligible_Some. +apply negligible_None. +intros n; specialize (Hn n); omega. +Qed. + +Lemma negligible_exp_spec': (negligible_exp = None /\ forall n, (fexp n < n)%Z) + \/ exists n, (negligible_exp = Some n /\ (n <= fexp n)%Z). +Proof. +unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. +right; simpl; exists n; now split. +left; split; trivial. +intros n; specialize (Hn n); omega. +Qed. + Context { valid_exp : Valid_exp fexp }. -Definition ulp x := bpow (canonic_exp beta fexp x). +Lemma fexp_negligible_exp_eq: forall n m, (n <= fexp n)%Z -> (m <= fexp m)%Z -> fexp n = fexp m. +Proof. +intros n m Hn Hm. +case (Zle_or_lt n m); intros H. +apply valid_exp; omega. +apply sym_eq, valid_exp; omega. +Qed. + + +(** Definition and basic properties about the ulp *) +(** Now includes a nice ulp(0): ulp(0) is now 0 when there is no minimal + exponent, such as in FLX, and beta^(fexp n) when there is a n such + that n <= fexp n. For instance, the value of ulp(O) is then + beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that + is equivalent to the previous "unfold ulp" provided the value is + not zero. *) + +Definition ulp x := match Req_bool x 0 with + | true => match negligible_exp with + | Some n => bpow (fexp n) + | None => 0%R + end + | false => bpow (canonic_exp beta fexp x) + end. + +Lemma ulp_neq_0 : forall x:R, (x <> 0)%R -> ulp x = bpow (canonic_exp beta fexp x). +Proof. +intros x Hx. +unfold ulp; case (Req_bool_spec x); trivial. +intros H; now contradict H. +Qed. Notation F := (generic_format beta fexp). @@ -43,17 +113,37 @@ Theorem ulp_opp : Proof. intros x. unfold ulp. +case Req_bool_spec; intros H1. +rewrite Req_bool_true; trivial. +rewrite <- (Ropp_involutive x), H1; ring. +rewrite Req_bool_false. now rewrite canonic_exp_opp. +intros H2; apply H1; rewrite H2; ring. Qed. Theorem ulp_abs : forall x, ulp (Rabs x) = ulp x. Proof. intros x. -unfold ulp. +unfold ulp; case (Req_bool_spec x 0); intros H1. +rewrite Req_bool_true; trivial. +now rewrite H1, Rabs_R0. +rewrite Req_bool_false. now rewrite canonic_exp_abs. +now apply Rabs_no_R0. +Qed. + +Theorem ulp_ge_0: + forall x, (0 <= ulp x)%R. +Proof. +intros x; unfold ulp; case Req_bool_spec; intros. +case negligible_exp; intros. +apply bpow_ge_0. +apply Rle_refl. +apply bpow_ge_0. Qed. + Theorem ulp_le_id: forall x, (0 < x)%R -> @@ -63,7 +153,9 @@ Proof. intros x Zx Fx. rewrite <- (Rmult_1_l (ulp x)). pattern x at 2; rewrite Fx. -unfold F2R, ulp; simpl. +rewrite ulp_neq_0. +2: now apply Rgt_not_eq. +unfold F2R; simpl. apply Rmult_le_compat_r. apply bpow_ge_0. replace 1%R with (Z2R (Zsucc 0)) by reflexivity. @@ -86,12 +178,15 @@ now apply Rabs_pos_lt. now apply generic_format_abs. Qed. -Theorem ulp_DN_UP : + +(* was ulp_DN_UP *) +Theorem round_UP_DN_ulp : forall x, ~ F x -> round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R. Proof. intros x Fx. -unfold round, ulp. simpl. +rewrite ulp_neq_0. +unfold round. simpl. unfold F2R. simpl. rewrite Zceil_floor_neq. rewrite Z2R_plus. simpl. @@ -103,17 +198,282 @@ rewrite <- H. rewrite Ztrunc_Z2R. rewrite H. now rewrite scaled_mantissa_mult_bpow. +intros V; apply Fx. +rewrite V. +apply generic_format_0. +Qed. + + +Theorem ulp_bpow : + forall e, ulp (bpow e) = bpow (fexp (e + 1)). +intros e. +rewrite ulp_neq_0. +apply f_equal. +apply canonic_exp_fexp. +rewrite Rabs_pos_eq. +split. +ring_simplify (e + 1 - 1)%Z. +apply Rle_refl. +apply bpow_lt. +apply Zlt_succ. +apply bpow_ge_0. +apply Rgt_not_eq, Rlt_gt, bpow_gt_0. +Qed. + + +Lemma generic_format_ulp_0: + F (ulp 0). +Proof. +unfold ulp. +rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros _; apply generic_format_0. +intros n H1. +apply generic_format_bpow. +now apply valid_exp. +Qed. + +Lemma generic_format_bpow_ge_ulp_0: forall e, + (ulp 0 <= bpow e)%R -> F (bpow e). +Proof. +intros e; unfold ulp. +rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros H1 _. +apply generic_format_bpow. +specialize (H1 (e+1)%Z); omega. +intros n H1 H2. +apply generic_format_bpow. +case (Zle_or_lt (e+1) (fexp (e+1))); intros H4. +absurd (e+1 <= e)%Z. +omega. +apply Zle_trans with (1:=H4). +replace (fexp (e+1)) with (fexp n). +now apply le_bpow with beta. +now apply fexp_negligible_exp_eq. +omega. +Qed. + +(** The three following properties are equivalent: + [Exp_not_FTZ] ; forall x, F (ulp x) ; forall x, ulp 0 <= ulp x *) + +Lemma generic_format_ulp: Exp_not_FTZ fexp -> + forall x, F (ulp x). +Proof. +unfold Exp_not_FTZ; intros H x. +case (Req_dec x 0); intros Hx. +rewrite Hx; apply generic_format_ulp_0. +rewrite (ulp_neq_0 _ Hx). +apply generic_format_bpow; unfold canonic_exp. +apply H. +Qed. + +Lemma not_FTZ_generic_format_ulp: + (forall x, F (ulp x)) -> Exp_not_FTZ fexp. +intros H e. +specialize (H (bpow (e-1))). +rewrite ulp_neq_0 in H. +2: apply Rgt_not_eq, bpow_gt_0. +unfold canonic_exp in H. +rewrite ln_beta_bpow in H. +apply generic_format_bpow_inv' in H... +now replace (e-1+1)%Z with e in H by ring. +Qed. + + +Lemma ulp_ge_ulp_0: Exp_not_FTZ fexp -> + forall x, (ulp 0 <= ulp x)%R. +Proof. +unfold Exp_not_FTZ; intros H x. +case (Req_dec x 0); intros Hx. +rewrite Hx; now right. +unfold ulp at 1. +rewrite Req_bool_true; trivial. +case negligible_exp_spec'. +intros (H1,H2); rewrite H1; apply ulp_ge_0. +intros (n,(H1,H2)); rewrite H1. +rewrite ulp_neq_0; trivial. +apply bpow_le; unfold canonic_exp. +generalize (ln_beta beta x); intros l. +case (Zle_or_lt l (fexp l)); intros Hl. +rewrite (fexp_negligible_exp_eq n l); trivial; apply Zle_refl. +case (Zle_or_lt (fexp n) (fexp l)); trivial; intros K. +absurd (fexp n <= fexp l)%Z. +omega. +apply Zle_trans with (2:= H _). +apply Zeq_le, sym_eq, valid_exp; trivial. +omega. +Qed. + +Lemma not_FTZ_ulp_ge_ulp_0: + (forall x, (ulp 0 <= ulp x)%R) -> Exp_not_FTZ fexp. +Proof. +intros H e. +apply generic_format_bpow_inv' with beta. +apply generic_format_bpow_ge_ulp_0. +replace e with ((e-1)+1)%Z by ring. +rewrite <- ulp_bpow. +apply H. +Qed. + + + +Theorem ulp_le_pos : + forall { Hm : Monotone_exp fexp }, + forall x y: R, + (0 <= x)%R -> (x <= y)%R -> + (ulp x <= ulp y)%R. +Proof with auto with typeclass_instances. +intros Hm x y Hx Hxy. +destruct Hx as [Hx|Hx]. +rewrite ulp_neq_0. +rewrite ulp_neq_0. +apply bpow_le. +apply Hm. +now apply ln_beta_le. +apply Rgt_not_eq, Rlt_gt. +now apply Rlt_le_trans with (1:=Hx). +now apply Rgt_not_eq. +rewrite <- Hx. +apply ulp_ge_ulp_0. +apply monotone_exp_not_FTZ... +Qed. + + +Theorem ulp_le : + forall { Hm : Monotone_exp fexp }, + forall x y: R, + (Rabs x <= Rabs y)%R -> + (ulp x <= ulp y)%R. +Proof. +intros Hm x y Hxy. +rewrite <- ulp_abs. +rewrite <- (ulp_abs y). +apply ulp_le_pos; trivial. +apply Rabs_pos. +Qed. + + + +(** Definition and properties of pred and succ *) + +Definition pred_pos x := + if Req_bool x (bpow (ln_beta beta x - 1)) then + (x - bpow (fexp (ln_beta beta x - 1)))%R + else + (x - ulp x)%R. + +Definition succ x := + if (Rle_bool 0 x) then + (x+ulp x)%R + else + (- pred_pos (-x))%R. + +Definition pred x := (- succ (-x))%R. + +Theorem pred_eq_pos: + forall x, (0 <= x)%R -> (pred x = pred_pos x)%R. +Proof. +intros x Hx; unfold pred, succ. +case Rle_bool_spec; intros Hx'. +assert (K:(x = 0)%R). +apply Rle_antisym; try assumption. +apply Ropp_le_cancel. +now rewrite Ropp_0. +rewrite K; unfold pred_pos. +rewrite Req_bool_false. +2: apply Rlt_not_eq, bpow_gt_0. +rewrite Ropp_0; ring. +now rewrite 2!Ropp_involutive. +Qed. + +Theorem succ_eq_pos: + forall x, (0 <= x)%R -> (succ x = x + ulp x)%R. +Proof. +intros x Hx; unfold succ. +now rewrite Rle_bool_true. +Qed. + +Lemma pred_eq_opp_succ_opp: forall x, pred x = (- succ (-x))%R. +Proof. +reflexivity. +Qed. + +Lemma succ_eq_opp_pred_opp: forall x, succ x = (- pred (-x))%R. +Proof. +intros x; unfold pred. +now rewrite 2!Ropp_involutive. +Qed. + +Lemma succ_opp: forall x, (succ (-x) = - pred x)%R. +Proof. +intros x; rewrite succ_eq_opp_pred_opp. +now rewrite Ropp_involutive. +Qed. + +Lemma pred_opp: forall x, (pred (-x) = - succ x)%R. +Proof. +intros x; rewrite pred_eq_opp_succ_opp. +now rewrite Ropp_involutive. +Qed. + + + + +(** pred and succ are in the format *) + +(* cannont be x <> ulp 0, due to the counter-example 1-bit FP format fexp: e -> e-1 *) +(* was pred_ge_bpow *) +Theorem id_m_ulp_ge_bpow : + forall x e, F x -> + x <> ulp x -> + (bpow e < x)%R -> + (bpow e <= x - ulp x)%R. +Proof. +intros x e Fx Hx' Hx. +(* *) +assert (1 <= Ztrunc (scaled_mantissa beta fexp x))%Z. +assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. +apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). +rewrite <- Fx. +apply Rle_lt_trans with (2:=Hx). +apply bpow_ge_0. +omega. +case (Zle_lt_or_eq _ _ H); intros Hm. +(* *) +pattern x at 1 ; rewrite Fx. +rewrite ulp_neq_0. +unfold F2R. simpl. +pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. +rewrite <- Rmult_minus_distr_r. +change 1%R with (Z2R 1). +rewrite <- Z2R_minus. +change (bpow e <= F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) - 1) (canonic_exp beta fexp x)))%R. +apply bpow_le_F2R_m1; trivial. +now rewrite <- Fx. +apply Rgt_not_eq, Rlt_gt. +apply Rlt_trans with (2:=Hx), bpow_gt_0. +(* *) +contradict Hx'. +pattern x at 1; rewrite Fx. +rewrite <- Hm. +rewrite ulp_neq_0. +unfold F2R; simpl. +now rewrite Rmult_1_l. +apply Rgt_not_eq, Rlt_gt. +apply Rlt_trans with (2:=Hx), bpow_gt_0. Qed. -(** The successor of x is x + ulp x *) -Theorem succ_le_bpow : +(* was succ_le_bpow *) +Theorem id_p_ulp_le_bpow : forall x e, (0 < x)%R -> F x -> (x < bpow e)%R -> (x + ulp x <= bpow e)%R. Proof. intros x e Zx Fx Hx. pattern x at 1 ; rewrite Fx. -unfold ulp, F2R. simpl. +rewrite ulp_neq_0. +unfold F2R. simpl. pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. rewrite <- Rmult_plus_distr_r. change 1%R with (Z2R 1). @@ -123,88 +483,142 @@ apply F2R_p1_le_bpow. apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). now rewrite <- Fx. now rewrite <- Fx. +now apply Rgt_not_eq. Qed. -Theorem ln_beta_succ : + + +Lemma generic_format_pred_aux1: forall x, (0 < x)%R -> F x -> - forall eps, (0 <= eps < ulp x)%R -> - ln_beta beta (x + eps) = ln_beta beta x :> Z. + x <> bpow (ln_beta beta x - 1) -> + F (x - ulp x). Proof. -intros x Zx Fx eps Heps. -destruct (ln_beta beta x) as (ex, He). -simpl. -specialize (He (Rgt_not_eq _ _ Zx)). -apply ln_beta_unique. +intros x Zx Fx Hx. +destruct (ln_beta beta x) as (ex, Ex). +simpl in Hx. +specialize (Ex (Rgt_not_eq _ _ Zx)). +assert (Ex' : (bpow (ex - 1) < x < bpow ex)%R). +rewrite Rabs_pos_eq in Ex. +destruct Ex as (H,H'); destruct H; split; trivial. +contradict Hx; easy. +now apply Rlt_le. +unfold generic_format, scaled_mantissa, canonic_exp. +rewrite ln_beta_unique with beta (x - ulp x)%R ex. +pattern x at 1 3 ; rewrite Fx. +rewrite ulp_neq_0. +unfold scaled_mantissa. +rewrite canonic_exp_fexp with (1 := Ex). +unfold F2R. simpl. +rewrite Rmult_minus_distr_r. +rewrite Rmult_assoc. +rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r. +change (bpow 0) with (Z2R 1). +rewrite <- Z2R_minus. +rewrite Ztrunc_Z2R. +rewrite Z2R_minus. +rewrite Rmult_minus_distr_r. +now rewrite Rmult_1_l. +now apply Rgt_not_eq. rewrite Rabs_pos_eq. -rewrite Rabs_pos_eq in He. split. -apply Rle_trans with (1 := proj1 He). -pattern x at 1 ; rewrite <- Rplus_0_r. -now apply Rplus_le_compat_l. -apply Rlt_le_trans with (x + ulp x)%R. -now apply Rplus_lt_compat_l. -pattern x at 1 ; rewrite Fx. -unfold ulp, F2R. simpl. -pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. -rewrite <- Rmult_plus_distr_r. -change 1%R with (Z2R 1). -rewrite <- Z2R_plus. -change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R. -apply F2R_p1_le_bpow. +apply id_m_ulp_ge_bpow; trivial. +rewrite ulp_neq_0. +intro H. +assert (ex-1 < canonic_exp beta fexp x < ex)%Z. +split ; apply (lt_bpow beta) ; rewrite <- H ; easy. +clear -H0. omega. +now apply Rgt_not_eq. +apply Ex'. +apply Rle_lt_trans with (2 := proj2 Ex'). +pattern x at 3 ; rewrite <- Rplus_0_r. +apply Rplus_le_compat_l. +rewrite <-Ropp_0. +apply Ropp_le_contravar. +apply ulp_ge_0. +apply Rle_0_minus. +pattern x at 2; rewrite Fx. +rewrite ulp_neq_0. +unfold F2R; simpl. +pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l. +apply Rmult_le_compat_r. +apply bpow_ge_0. +replace 1%R with (Z2R 1) by reflexivity. +apply Z2R_le. +assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). -now rewrite <- Fx. -now rewrite <- Fx. -now apply Rlt_le. -apply Rplus_le_le_0_compat. -now apply Rlt_le. -apply Heps. +rewrite <- Fx. +apply Rle_lt_trans with (2:=proj1 Ex'). +apply bpow_ge_0. +omega. +now apply Rgt_not_eq. Qed. -Theorem round_DN_succ : +Lemma generic_format_pred_aux2 : forall x, (0 < x)%R -> F x -> - forall eps, (0 <= eps < ulp x)%R -> - round beta fexp Zfloor (x + eps) = x. + let e := ln_beta_val beta x (ln_beta beta x) in + x = bpow (e - 1) -> + F (x - bpow (fexp (e - 1))). Proof. -intros x Zx Fx eps Heps. -pattern x at 2 ; rewrite Fx. -unfold round. -unfold scaled_mantissa. simpl. -unfold canonic_exp at 1 2. -rewrite ln_beta_succ ; trivial. -apply (f_equal (fun m => F2R (Float beta m _))). -rewrite Ztrunc_floor. -apply Zfloor_imp. +intros x Zx Fx e Hx. +pose (f:=(x - bpow (fexp (e - 1)))%R). +fold f. +assert (He:(fexp (e-1) <= e-1)%Z). +apply generic_format_bpow_inv with beta; trivial. +rewrite <- Hx; assumption. +case (Zle_lt_or_eq _ _ He); clear He; intros He. +assert (f = F2R (Float beta (Zpower beta (e-1-(fexp (e-1))) -1) (fexp (e-1))))%R. +unfold f; rewrite Hx. +unfold F2R; simpl. +rewrite Z2R_minus, Z2R_Zpower. +rewrite Rmult_minus_distr_r, Rmult_1_l. +rewrite <- bpow_plus. +now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring. +omega. +rewrite H. +apply generic_format_F2R. +intros _. +apply Zeq_le. +apply canonic_exp_fexp. +rewrite <- H. +unfold f; rewrite Hx. +rewrite Rabs_right. split. -apply (Rle_trans _ _ _ (Zfloor_lb _)). +apply Rplus_le_reg_l with (bpow (fexp (e-1))). +ring_simplify. +apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. +apply Rplus_le_compat ; apply bpow_le ; omega. +apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. +apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. apply bpow_ge_0. -pattern x at 1 ; rewrite <- Rplus_0_r. -now apply Rplus_le_compat_l. -apply Rlt_le_trans with ((x + ulp x) * bpow (- canonic_exp beta fexp x))%R. -apply Rmult_lt_compat_r. -apply bpow_gt_0. -now apply Rplus_lt_compat_l. -rewrite Rmult_plus_distr_r. -rewrite Z2R_plus. -apply Rplus_le_compat. -pattern x at 1 3 ; rewrite Fx. -unfold F2R. simpl. -rewrite Rmult_assoc. -rewrite <- bpow_plus. -rewrite Zplus_opp_r. -rewrite Rmult_1_r. -rewrite Zfloor_Z2R. -apply Rle_refl. -unfold ulp. +replace 2%R with (Z2R 2) by reflexivity. +replace (bpow 1) with (Z2R beta). +apply Z2R_le. +apply <- Zle_is_le_bool. +now destruct beta. +simpl. +unfold Zpower_pos; simpl. +now rewrite Zmult_1_r. rewrite <- bpow_plus. -rewrite Zplus_opp_r. -apply Rle_refl. -apply Rmult_le_pos. -now apply Rlt_le. -apply bpow_ge_0. +replace (1+(e-2))%Z with (e-1)%Z by ring. +now right. +rewrite <- Rplus_0_r. +apply Rplus_lt_compat_l. +rewrite <- Ropp_0. +apply Ropp_lt_contravar. +apply bpow_gt_0. +apply Rle_ge; apply Rle_0_minus. +apply bpow_le. +omega. +replace f with 0%R. +apply generic_format_0. +unfold f. +rewrite Hx, He. +ring. Qed. -Theorem generic_format_succ : + +Theorem generic_format_succ_aux1 : forall x, (0 < x)%R -> F x -> F (x + ulp x). Proof. @@ -213,11 +627,12 @@ destruct (ln_beta beta x) as (ex, Ex). specialize (Ex (Rgt_not_eq _ _ Zx)). assert (Ex' := Ex). rewrite Rabs_pos_eq in Ex'. -destruct (succ_le_bpow x ex) ; try easy. +destruct (id_p_ulp_le_bpow x ex) ; try easy. unfold generic_format, scaled_mantissa, canonic_exp. rewrite ln_beta_unique with beta (x + ulp x)%R ex. pattern x at 1 3 ; rewrite Fx. -unfold ulp, scaled_mantissa. +rewrite ulp_neq_0. +unfold scaled_mantissa. rewrite canonic_exp_fexp with (1 := Ex). unfold F2R. simpl. rewrite Rmult_plus_distr_r. @@ -229,16 +644,17 @@ rewrite Ztrunc_Z2R. rewrite Z2R_plus. rewrite Rmult_plus_distr_r. now rewrite Rmult_1_l. +now apply Rgt_not_eq. rewrite Rabs_pos_eq. split. apply Rle_trans with (1 := proj1 Ex'). pattern x at 1 ; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. -apply bpow_ge_0. +apply ulp_ge_0. exact H. apply Rplus_le_le_0_compat. now apply Rlt_le. -apply bpow_ge_0. +apply ulp_ge_0. rewrite H. apply generic_format_bpow. apply valid_exp. @@ -261,427 +677,240 @@ now apply Rlt_le. now apply Rlt_le. Qed. -Theorem round_UP_succ : - forall x, (0 < x)%R -> F x -> - forall eps, (0 < eps <= ulp x)%R -> - round beta fexp Zceil (x + eps) = (x + ulp x)%R. -Proof with auto with typeclass_instances. -intros x Zx Fx eps (Heps1,[Heps2|Heps2]). -assert (Heps: (0 <= eps < ulp x)%R). -split. -now apply Rlt_le. -exact Heps2. -assert (Hd := round_DN_succ x Zx Fx eps Heps). -rewrite ulp_DN_UP. -rewrite Hd. -unfold ulp, canonic_exp. -now rewrite ln_beta_succ. -intros Fs. -rewrite round_generic in Hd... -apply Rgt_not_eq with (2 := Hd). -pattern x at 2 ; rewrite <- Rplus_0_r. -now apply Rplus_lt_compat_l. -rewrite Heps2. -apply round_generic... -now apply generic_format_succ. +Theorem generic_format_pred_pos : + forall x, F x -> (0 < x)%R -> + F (pred_pos x). +Proof. +intros x Fx Zx. +unfold pred_pos; case Req_bool_spec; intros H. +now apply generic_format_pred_aux2. +now apply generic_format_pred_aux1. Qed. -Theorem succ_le_lt: - forall x y, - F x -> F y -> - (0 < x < y)%R -> - (x + ulp x <= y)%R. -Proof with auto with typeclass_instances. -intros x y Hx Hy H. -case (Rle_or_lt (ulp x) (y-x)); intros H1. -apply Rplus_le_reg_r with (-x)%R. -now ring_simplify (x+ulp x + -x)%R. -replace y with (x+(y-x))%R by ring. -absurd (x < y)%R. -2: apply H. -apply Rle_not_lt; apply Req_le. -rewrite <- round_DN_succ with (eps:=(y-x)%R); try easy. -ring_simplify (x+(y-x))%R. -apply sym_eq. -apply round_generic... -split; trivial. -apply Rlt_le; now apply Rlt_Rminus. + +Theorem generic_format_succ : + forall x, F x -> + F (succ x). +Proof. +intros x Fx. +unfold succ; case Rle_bool_spec; intros Zx. +destruct Zx as [Zx|Zx]. +now apply generic_format_succ_aux1. +rewrite <- Zx, Rplus_0_l. +apply generic_format_ulp_0. +apply generic_format_opp. +apply generic_format_pred_pos. +now apply generic_format_opp. +now apply Ropp_0_gt_lt_contravar. Qed. -(** Error of a rounding, expressed in number of ulps *) -Theorem ulp_error : - forall rnd { Zrnd : Valid_rnd rnd } x, - (Rabs (round beta fexp rnd x - x) < ulp x)%R. -Proof with auto with typeclass_instances. -intros rnd Zrnd x. -destruct (generic_format_EM beta fexp x) as [Hx|Hx]. -(* x = rnd x *) -rewrite round_generic... -unfold Rminus. -rewrite Rplus_opp_r, Rabs_R0. -apply bpow_gt_0. -(* x <> rnd x *) -destruct (round_DN_or_UP beta fexp rnd x) as [H|H] ; rewrite H ; clear H. -(* . *) -rewrite Rabs_left1. -rewrite Ropp_minus_distr. -apply Rplus_lt_reg_l with (round beta fexp Zfloor x). -rewrite <- ulp_DN_UP with (1 := Hx). -ring_simplify. -assert (Hu: (x <= round beta fexp Zceil x)%R). -apply round_UP_pt... -destruct Hu as [Hu|Hu]. -exact Hu. -elim Hx. -rewrite Hu. -apply generic_format_round... -apply Rle_minus. -apply round_DN_pt... -(* . *) -rewrite Rabs_pos_eq. -rewrite ulp_DN_UP with (1 := Hx). -apply Rplus_lt_reg_r with (x - ulp x)%R. -ring_simplify. -assert (Hd: (round beta fexp Zfloor x <= x)%R). -apply round_DN_pt... -destruct Hd as [Hd|Hd]. -exact Hd. -elim Hx. -rewrite <- Hd. -apply generic_format_round... -apply Rle_0_minus. -apply round_UP_pt... +Theorem generic_format_pred : + forall x, F x -> + F (pred x). +Proof. +intros x Fx. +unfold pred. +apply generic_format_opp. +apply generic_format_succ. +now apply generic_format_opp. Qed. -Theorem ulp_half_error : - forall choice x, - (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp x)%R. -Proof with auto with typeclass_instances. -intros choice x. -destruct (generic_format_EM beta fexp x) as [Hx|Hx]. -(* x = rnd x *) -rewrite round_generic... -unfold Rminus. -rewrite Rplus_opp_r, Rabs_R0. -apply Rmult_le_pos. -apply Rlt_le. -apply Rinv_0_lt_compat. -now apply (Z2R_lt 0 2). -apply bpow_ge_0. -(* x <> rnd x *) -set (d := round beta fexp Zfloor x). -destruct (round_N_pt beta fexp choice x) as (Hr1, Hr2). -destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H]. -(* . rnd(x) = rndd(x) *) -apply Rle_trans with (Rabs (d - x)). -apply Hr2. -apply (round_DN_pt beta fexp x). -rewrite Rabs_left1. -rewrite Ropp_minus_distr. -apply Rmult_le_reg_r with 2%R. -now apply (Z2R_lt 0 2). -apply Rplus_le_reg_r with (d - x)%R. -ring_simplify. -apply Rle_trans with (1 := H). -right. field. -apply Rle_minus. -apply (round_DN_pt beta fexp x). -(* . rnd(x) = rndu(x) *) -assert (Hu: (d + ulp x)%R = round beta fexp Zceil x). -unfold d. -now rewrite <- ulp_DN_UP. -apply Rle_trans with (Rabs (d + ulp x - x)). -apply Hr2. -rewrite Hu. -apply (round_UP_pt beta fexp x). -rewrite Rabs_pos_eq. -apply Rmult_le_reg_r with 2%R. -now apply (Z2R_lt 0 2). -apply Rplus_le_reg_r with (- (d + ulp x - x))%R. -ring_simplify. -apply Rlt_le. -apply Rlt_le_trans with (1 := H). -right. field. -apply Rle_0_minus. -rewrite Hu. -apply (round_UP_pt beta fexp x). + + +Theorem pred_pos_lt_id : + forall x, (x <> 0)%R -> + (pred_pos x < x)%R. +Proof. +intros x Zx. +unfold pred_pos. +case Req_bool_spec; intros H. +(* *) +rewrite <- Rplus_0_r. +apply Rplus_lt_compat_l. +rewrite <- Ropp_0. +apply Ropp_lt_contravar. +apply bpow_gt_0. +(* *) +rewrite <- Rplus_0_r. +apply Rplus_lt_compat_l. +rewrite <- Ropp_0. +apply Ropp_lt_contravar. +rewrite ulp_neq_0; trivial. +apply bpow_gt_0. Qed. -Theorem ulp_le : - forall { Hm : Monotone_exp fexp }, - forall x y: R, - (0 < x)%R -> (x <= y)%R -> - (ulp x <= ulp y)%R. +Theorem succ_gt_id : + forall x, (x <> 0)%R -> + (x < succ x)%R. Proof. -intros Hm x y Hx Hxy. -apply bpow_le. -apply Hm. -now apply ln_beta_le. +intros x Zx; unfold succ. +case Rle_bool_spec; intros Hx. +pattern x at 1; rewrite <- (Rplus_0_r x). +apply Rplus_lt_compat_l. +rewrite ulp_neq_0; trivial. +apply bpow_gt_0. +pattern x at 1; rewrite <- (Ropp_involutive x). +apply Ropp_lt_contravar. +apply pred_pos_lt_id. +now auto with real. Qed. -Theorem ulp_bpow : - forall e, ulp (bpow e) = bpow (fexp (e + 1)). -intros e. -unfold ulp. -apply f_equal. -apply canonic_exp_fexp. -rewrite Rabs_pos_eq. -split. -ring_simplify (e + 1 - 1)%Z. -apply Rle_refl. -apply bpow_lt. -apply Zlt_succ. -apply bpow_ge_0. -Qed. -Theorem ulp_DN : - forall x, - (0 < round beta fexp Zfloor x)%R -> - ulp (round beta fexp Zfloor x) = ulp x. +Theorem pred_lt_id : + forall x, (x <> 0)%R -> + (pred x < x)%R. Proof. -intros x Hd. -unfold ulp. -now rewrite canonic_exp_DN with (2 := Hd). +intros x Zx; unfold pred. +pattern x at 2; rewrite <- (Ropp_involutive x). +apply Ropp_lt_contravar. +apply succ_gt_id. +now auto with real. Qed. -Theorem ulp_error_f : - forall { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x, - (round beta fexp rnd x <> 0)%R -> - (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R. -Proof with auto with typeclass_instances. -intros Hm rnd Zrnd x Hfx. -case (round_DN_or_UP beta fexp rnd x); intros Hx. -(* *) -case (Rle_or_lt 0 (round beta fexp Zfloor x)). -intros H; destruct H. -rewrite Hx at 2. -rewrite ulp_DN; trivial. -apply ulp_error... -rewrite Hx in Hfx; contradict Hfx; auto with real. -intros H. -apply Rlt_le_trans with (1:=ulp_error _ _). -rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp rnd x)). -apply ulp_le; trivial. -apply Ropp_0_gt_lt_contravar; apply Rlt_gt. -case (Rle_or_lt 0 x); trivial. -intros H1; contradict H. -apply Rle_not_lt. -apply round_ge_generic... -apply generic_format_0. -apply Ropp_le_contravar; rewrite Hx. -apply (round_DN_pt beta fexp x). -(* *) -rewrite Hx; case (Rle_or_lt 0 (round beta fexp Zceil x)). -intros H; destruct H. -apply Rlt_le_trans with (1:=ulp_error _ _). -apply ulp_le; trivial. -case (Rle_or_lt x 0); trivial. -intros H1; contradict H. -apply Rle_not_lt. -apply round_le_generic... -apply generic_format_0. -apply round_UP_pt... -rewrite Hx in Hfx; contradict Hfx; auto with real. -intros H. -rewrite <- (ulp_opp (round beta fexp Zceil x)). -rewrite <- round_DN_opp. -rewrite ulp_DN; trivial. -replace (round beta fexp Zceil x - x)%R with (-((round beta fexp Zfloor (-x) - (-x))))%R. -rewrite Rabs_Ropp. -apply ulp_error... -rewrite round_DN_opp; ring. -rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. +Theorem succ_ge_id : + forall x, (x <= succ x)%R. +Proof. +intros x; case (Req_dec x 0). +intros V; rewrite V. +unfold succ; rewrite Rle_bool_true;[idtac|now right]. +rewrite Rplus_0_l; apply ulp_ge_0. +intros; left; now apply succ_gt_id. Qed. -Theorem ulp_half_error_f : - forall { Hm : Monotone_exp fexp }, - forall choice x, - (round beta fexp (Znearest choice) x <> 0)%R -> - (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp (round beta fexp (Znearest choice) x))%R. -Proof with auto with typeclass_instances. -intros Hm choice x Hfx. -case (round_DN_or_UP beta fexp (Znearest choice) x); intros Hx. -(* *) -case (Rle_or_lt 0 (round beta fexp Zfloor x)). -intros H; destruct H. -rewrite Hx at 2. -rewrite ulp_DN; trivial. -apply ulp_half_error. -rewrite Hx in Hfx; contradict Hfx; auto with real. -intros H. -apply Rle_trans with (1:=ulp_half_error _ _). -apply Rmult_le_compat_l. -auto with real. -rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp (Znearest choice) x)). -apply ulp_le; trivial. -apply Ropp_0_gt_lt_contravar; apply Rlt_gt. -case (Rle_or_lt 0 x); trivial. -intros H1; contradict H. -apply Rle_not_lt. -apply round_ge_generic... -apply generic_format_0. -apply Ropp_le_contravar; rewrite Hx. -apply (round_DN_pt beta fexp x). -(* *) -case (Rle_or_lt 0 (round beta fexp Zceil x)). -intros H; destruct H. -apply Rle_trans with (1:=ulp_half_error _ _). -apply Rmult_le_compat_l. -auto with real. -apply ulp_le; trivial. -case (Rle_or_lt x 0); trivial. -intros H1; contradict H. -apply Rle_not_lt. -apply round_le_generic... -apply generic_format_0. -rewrite Hx; apply (round_UP_pt beta fexp x). -rewrite Hx in Hfx; contradict Hfx; auto with real. -intros H. -rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp Zceil x)). -rewrite <- round_DN_opp. -rewrite ulp_DN; trivial. -pattern x at 1 2; rewrite <- Ropp_involutive. -rewrite round_N_opp. -unfold Rminus. -rewrite <- Ropp_plus_distr, Rabs_Ropp. -apply ulp_half_error. -rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. + +Theorem pred_le_id : + forall x, (pred x <= x)%R. +Proof. +intros x; unfold pred. +pattern x at 2; rewrite <- (Ropp_involutive x). +apply Ropp_le_contravar. +apply succ_ge_id. Qed. -(** Predecessor *) -Definition pred x := - if Req_bool x (bpow (ln_beta beta x - 1)) then - (x - bpow (fexp (ln_beta beta x - 1)))%R - else - (x - ulp x)%R. -Theorem pred_ge_bpow : - forall x e, F x -> - x <> ulp x -> - (bpow e < x)%R -> - (bpow e <= x - ulp x)%R. +Theorem pred_pos_ge_0 : + forall x, + (0 < x)%R -> F x -> (0 <= pred_pos x)%R. Proof. -intros x e Fx Hx' Hx. -(* *) -assert (1 <= Ztrunc (scaled_mantissa beta fexp x))%Z. -assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. -apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). -rewrite <- Fx. -apply Rle_lt_trans with (2:=Hx). -apply bpow_ge_0. -omega. -case (Zle_lt_or_eq _ _ H); intros Hm. -(* *) -pattern x at 1 ; rewrite Fx. -unfold ulp, F2R. simpl. -pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. -rewrite <- Rmult_minus_distr_r. -change 1%R with (Z2R 1). -rewrite <- Z2R_minus. -change (bpow e <= F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) - 1) (canonic_exp beta fexp x)))%R. -apply bpow_le_F2R_m1; trivial. -now rewrite <- Fx. +intros x Zx Fx. +unfold pred_pos. +case Req_bool_spec; intros H. (* *) -contradict Hx'. -pattern x at 1; rewrite Fx. -rewrite <- Hm. -unfold ulp, F2R; simpl. -now rewrite Rmult_1_l. +apply Rle_0_minus. +rewrite H. +apply bpow_le. +destruct (ln_beta beta x) as (ex,Ex) ; simpl. +rewrite ln_beta_bpow. +ring_simplify (ex - 1 + 1 - 1)%Z. +apply generic_format_bpow_inv with beta; trivial. +simpl in H. +rewrite <- H; assumption. +apply Rle_0_minus. +now apply ulp_le_id. +Qed. + +Theorem pred_ge_0 : + forall x, + (0 < x)%R -> F x -> (0 <= pred x)%R. +Proof. +intros x Zx Fx. +rewrite pred_eq_pos. +now apply pred_pos_ge_0. +now left. Qed. -Lemma generic_format_pred_1: + +Lemma pred_pos_plus_ulp_aux1 : forall x, (0 < x)%R -> F x -> x <> bpow (ln_beta beta x - 1) -> - F (x - ulp x). + ((x - ulp x) + ulp (x-ulp x) = x)%R. Proof. intros x Zx Fx Hx. -destruct (ln_beta beta x) as (ex, Ex). -simpl in Hx. -specialize (Ex (Rgt_not_eq _ _ Zx)). -assert (Ex' : (bpow (ex - 1) < x < bpow ex)%R). -rewrite Rabs_pos_eq in Ex. -destruct Ex as (H,H'); destruct H; split; trivial. -contradict Hx; easy. -now apply Rlt_le. -unfold generic_format, scaled_mantissa, canonic_exp. -rewrite ln_beta_unique with beta (x - ulp x)%R ex. -pattern x at 1 3 ; rewrite Fx. -unfold ulp, scaled_mantissa. -rewrite canonic_exp_fexp with (1 := Ex). -unfold F2R. simpl. -rewrite Rmult_minus_distr_r. -rewrite Rmult_assoc. -rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r. -change (bpow 0) with (Z2R 1). -rewrite <- Z2R_minus. -rewrite Ztrunc_Z2R. -rewrite Z2R_minus. -rewrite Rmult_minus_distr_r. -now rewrite Rmult_1_l. -rewrite Rabs_pos_eq. +replace (ulp (x - ulp x)) with (ulp x). +ring. +assert (H:(x <> 0)%R) by auto with real. +assert (H':(x <> bpow (canonic_exp beta fexp x))%R). +unfold canonic_exp; intros M. +case_eq (ln_beta beta x); intros ex Hex T. +assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z). +rewrite T; reflexivity. +rewrite Lex in *. +clear T; simpl in *; specialize (Hex H). +rewrite Rabs_right in Hex. +2: apply Rle_ge; apply Rlt_le; easy. +assert (ex-1 < fexp ex < ex)%Z. +split ; apply (lt_bpow beta); rewrite <- M;[idtac|easy]. +destruct (proj1 Hex);[trivial|idtac]. +contradict Hx; auto with real. +omega. +rewrite 2!ulp_neq_0; try auto with real. +apply f_equal. +unfold canonic_exp; apply f_equal. +case_eq (ln_beta beta x); intros ex Hex T. +assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z). +rewrite T; reflexivity. +rewrite Lex in *; simpl in *; clear T. +specialize (Hex H). +apply sym_eq, ln_beta_unique. +rewrite Rabs_right. +rewrite Rabs_right in Hex. +2: apply Rle_ge; apply Rlt_le; easy. split. -apply pred_ge_bpow; trivial. -unfold ulp; intro H. -assert (ex-1 < canonic_exp beta fexp x < ex)%Z. -split ; apply (lt_bpow beta) ; rewrite <- H ; easy. -clear -H0. omega. -apply Ex'. -apply Rle_lt_trans with (2 := proj2 Ex'). -pattern x at 3 ; rewrite <- Rplus_0_r. +destruct Hex as ([H1|H1],H2). +apply Rle_trans with (x-ulp x)%R. +apply id_m_ulp_ge_bpow; trivial. +rewrite ulp_neq_0; trivial. +rewrite ulp_neq_0; trivial. +right; unfold canonic_exp; now rewrite Lex. +contradict Hx; auto with real. +apply Rle_lt_trans with (2:=proj2 Hex). +rewrite <- Rplus_0_r. apply Rplus_le_compat_l. -rewrite <-Ropp_0. +rewrite <- Ropp_0. apply Ropp_le_contravar. apply bpow_ge_0. +apply Rle_ge. apply Rle_0_minus. -pattern x at 2; rewrite Fx. -unfold ulp, F2R; simpl. -pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l. +rewrite Fx. +unfold F2R, canonic_exp; simpl. +rewrite Lex. +pattern (bpow (fexp ex)) at 1; rewrite <- Rmult_1_l. apply Rmult_le_compat_r. apply bpow_ge_0. -replace 1%R with (Z2R 1) by reflexivity. +replace 1%R with (Z2R (Zsucc 0)) by reflexivity. apply Z2R_le. -assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. +apply Zlt_le_succ. apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). -rewrite <- Fx. -apply Rle_lt_trans with (2:=proj1 Ex'). -apply bpow_ge_0. -omega. +now rewrite <- Fx. Qed. -Lemma generic_format_pred_2 : + +Lemma pred_pos_plus_ulp_aux2 : forall x, (0 < x)%R -> F x -> let e := ln_beta_val beta x (ln_beta beta x) in x = bpow (e - 1) -> - F (x - bpow (fexp (e - 1))). + (x - bpow (fexp (e-1)) <> 0)%R -> + ((x - bpow (fexp (e-1))) + ulp (x - bpow (fexp (e-1))) = x)%R. Proof. -intros x Zx Fx e Hx. -pose (f:=(x - bpow (fexp (e - 1)))%R). -fold f. +intros x Zx Fx e Hxe Zp. +replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))). +ring. assert (He:(fexp (e-1) <= e-1)%Z). apply generic_format_bpow_inv with beta; trivial. -rewrite <- Hx; assumption. +rewrite <- Hxe; assumption. case (Zle_lt_or_eq _ _ He); clear He; intros He. -assert (f = F2R (Float beta (Zpower beta (e-1-(fexp (e-1))) -1) (fexp (e-1))))%R. -unfold f; rewrite Hx. -unfold F2R; simpl. -rewrite Z2R_minus, Z2R_Zpower. -rewrite Rmult_minus_distr_r, Rmult_1_l. -rewrite <- bpow_plus. -now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring. -omega. -rewrite H. -apply generic_format_F2R. -intros _. -apply Zeq_le. -apply canonic_exp_fexp. -rewrite <- H. -unfold f; rewrite Hx. +(* *) +rewrite ulp_neq_0; trivial. +apply f_equal. +unfold canonic_exp; apply f_equal. +apply sym_eq. +apply ln_beta_unique. rewrite Rabs_right. split. apply Rplus_le_reg_l with (bpow (fexp (e-1))). ring_simplify. apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. -apply Rplus_le_compat ; apply bpow_le ; omega. +apply Rplus_le_compat; apply bpow_le; omega. apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. @@ -697,308 +926,285 @@ now rewrite Zmult_1_r. rewrite <- bpow_plus. replace (1+(e-2))%Z with (e-1)%Z by ring. now right. -rewrite <- Rplus_0_r. +rewrite <- Rplus_0_r, Hxe. apply Rplus_lt_compat_l. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply bpow_gt_0. apply Rle_ge; apply Rle_0_minus. +rewrite Hxe. apply bpow_le. omega. -replace f with 0%R. -apply generic_format_0. -unfold f. -rewrite Hx, He. -ring. -Qed. - -Theorem generic_format_pred : +(* *) +contradict Zp. +rewrite Hxe, He; ring. +Qed. + +Lemma pred_pos_plus_ulp_aux3 : forall x, (0 < x)%R -> F x -> - F (pred x). + let e := ln_beta_val beta x (ln_beta beta x) in + x = bpow (e - 1) -> + (x - bpow (fexp (e-1)) = 0)%R -> + (ulp 0 = x)%R. Proof. -intros x Zx Fx. -unfold pred. -case Req_bool_spec; intros H. -now apply generic_format_pred_2. -now apply generic_format_pred_1. +intros x Hx Fx e H1 H2. +assert (H3:(x = bpow (fexp (e - 1)))). +now apply Rminus_diag_uniq. +assert (H4: (fexp (e-1) = e-1)%Z). +apply bpow_inj with beta. +now rewrite <- H1. +unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros K. +specialize (K (e-1)%Z). +contradict K; omega. +intros n Hn. +rewrite H3; apply f_equal. +case (Zle_or_lt n (e-1)); intros H6. +apply valid_exp; omega. +apply sym_eq, valid_exp; omega. Qed. -Theorem generic_format_plus_ulp : - forall { monotone_exp : Monotone_exp fexp }, - forall x, (x <> 0)%R -> - F x -> F (x + ulp x). -Proof with auto with typeclass_instances. -intros monotone_exp x Zx Fx. -destruct (Rtotal_order x 0) as [Hx|[Hx|Hx]]. -rewrite <- Ropp_involutive. -apply generic_format_opp. -rewrite Ropp_plus_distr, <- ulp_opp. -apply generic_format_opp in Fx. -destruct (Req_dec (-x) (bpow (ln_beta beta (-x) - 1))) as [Hx'|Hx']. -rewrite Hx' in Fx |- *. -apply generic_format_bpow_inv' in Fx... -unfold ulp, canonic_exp. -rewrite ln_beta_bpow. -revert Fx. -generalize (ln_beta_val _ _ (ln_beta beta (-x)) - 1)%Z. -clear -monotone_exp valid_exp. -intros e He. -destruct (Zle_lt_or_eq _ _ He) as [He1|He1]. -assert (He2 : e = (e - fexp (e + 1) + fexp (e + 1))%Z) by ring. -rewrite He2 at 1. -rewrite bpow_plus. -assert (Hb := Z2R_Zpower beta _ (Zle_minus_le_0 _ _ He)). -match goal with |- F (?a * ?b + - ?b) => - replace (a * b + -b)%R with ((a - 1) * b)%R by ring end. -rewrite <- Hb. -rewrite <- (Z2R_minus _ 1). -change (F (F2R (Float beta (Zpower beta (e - fexp (e + 1)) - 1) (fexp (e + 1))))). -apply generic_format_F2R. -intros Zb. -unfold canonic_exp. -rewrite ln_beta_F2R with (1 := Zb). -rewrite (ln_beta_unique beta _ (e - fexp (e + 1))). -apply monotone_exp. -rewrite <- He2. -apply Zle_succ. -rewrite Rabs_pos_eq. -rewrite Z2R_minus, Hb. -split. -apply Rplus_le_reg_r with (- bpow (e - fexp (e + 1) - 1) + Z2R 1)%R. -apply Rmult_le_reg_r with (bpow (-(e - fexp (e+1) - 1))). -apply bpow_gt_0. -ring_simplify. -apply Rle_trans with R1. -rewrite Rmult_1_l. -apply (bpow_le _ _ 0). -clear -He1 ; omega. -rewrite Ropp_mult_distr_l_reverse. -rewrite <- 2!bpow_plus. -ring_simplify (e - fexp (e + 1) - 1 + - (e - fexp (e + 1) - 1))%Z. -ring_simplify (- (e - fexp (e + 1) - 1) + (e - fexp (e + 1)))%Z. -rewrite bpow_1. -rewrite <- (Z2R_plus (-1) _). -apply (Z2R_le 1). -generalize (Zle_bool_imp_le _ _ (radix_prop beta)). -clear ; omega. -rewrite <- (Rplus_0_r (bpow (e - fexp (e + 1)))) at 2. -apply Rplus_lt_compat_l. -now apply (Z2R_lt (-1) 0). -rewrite Z2R_minus. -apply Rle_0_minus. -rewrite Hb. -apply (bpow_le _ 0). -now apply Zle_minus_le_0. -rewrite He1, Rplus_opp_r. -apply generic_format_0. -apply generic_format_pred_1 ; try easy. -rewrite <- Ropp_0. -now apply Ropp_lt_contravar. -now elim Zx. -now apply generic_format_succ. -Qed. -Theorem generic_format_minus_ulp : - forall { monotone_exp : Monotone_exp fexp }, - forall x, (x <> 0)%R -> - F x -> F (x - ulp x). + + +(** The following one is false for x = 0 in FTZ *) + +Theorem pred_pos_plus_ulp : + forall x, (0 < x)%R -> F x -> + (pred_pos x + ulp (pred_pos x) = x)%R. Proof. -intros monotone_exp x Zx Fx. -replace (x - ulp x)%R with (-(-x + ulp x))%R by ring. -apply generic_format_opp. -rewrite <- ulp_opp. -apply generic_format_plus_ulp. -contradict Zx. -rewrite <- (Ropp_involutive x), Zx. -apply Ropp_0. -now apply generic_format_opp. +intros x Zx Fx. +unfold pred_pos. +case Req_bool_spec; intros H. +case (Req_EM_T (x - bpow (fexp (ln_beta_val beta x (ln_beta beta x) -1))) 0); intros H1. +rewrite H1, Rplus_0_l. +now apply pred_pos_plus_ulp_aux3. +now apply pred_pos_plus_ulp_aux2. +now apply pred_pos_plus_ulp_aux1. Qed. -Lemma pred_plus_ulp_1 : + + + +(** Rounding x + small epsilon *) + +Theorem ln_beta_plus_eps: forall x, (0 < x)%R -> F x -> - x <> bpow (ln_beta beta x - 1) -> - ((x - ulp x) + ulp (x-ulp x) = x)%R. + forall eps, (0 <= eps < ulp x)%R -> + ln_beta beta (x + eps) = ln_beta beta x :> Z. Proof. -intros x Zx Fx Hx. -replace (ulp (x - ulp x)) with (ulp x). -ring. -unfold ulp at 1 2; apply f_equal. -unfold canonic_exp; apply f_equal. -destruct (ln_beta beta x) as (ex, Hex). -simpl in *. -assert (x <> 0)%R by auto with real. -specialize (Hex H). -apply sym_eq. +intros x Zx Fx eps Heps. +destruct (ln_beta beta x) as (ex, He). +simpl. +specialize (He (Rgt_not_eq _ _ Zx)). apply ln_beta_unique. -rewrite Rabs_right. -rewrite Rabs_right in Hex. -2: apply Rle_ge; apply Rlt_le; easy. +rewrite Rabs_pos_eq. +rewrite Rabs_pos_eq in He. split. -destruct Hex as ([H1|H1],H2). -apply pred_ge_bpow; trivial. -unfold ulp; intros H3. -assert (ex-1 < canonic_exp beta fexp x < ex)%Z. -split ; apply (lt_bpow beta) ; rewrite <- H3 ; easy. -omega. -contradict Hx; auto with real. -apply Rle_lt_trans with (2:=proj2 Hex). -rewrite <- Rplus_0_r. -apply Rplus_le_compat_l. -rewrite <- Ropp_0. -apply Ropp_le_contravar. -apply bpow_ge_0. -apply Rle_ge. -apply Rle_0_minus. -pattern x at 2; rewrite Fx. -unfold ulp, F2R; simpl. -pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l. -apply Rmult_le_compat_r. -apply bpow_ge_0. -replace 1%R with (Z2R (Zsucc 0)) by reflexivity. -apply Z2R_le. -apply Zlt_le_succ. +apply Rle_trans with (1 := proj1 He). +pattern x at 1 ; rewrite <- Rplus_0_r. +now apply Rplus_le_compat_l. +apply Rlt_le_trans with (x + ulp x)%R. +now apply Rplus_lt_compat_l. +pattern x at 1 ; rewrite Fx. +rewrite ulp_neq_0. +unfold F2R. simpl. +pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. +rewrite <- Rmult_plus_distr_r. +change 1%R with (Z2R 1). +rewrite <- Z2R_plus. +change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R. +apply F2R_p1_le_bpow. apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). now rewrite <- Fx. +now rewrite <- Fx. +now apply Rgt_not_eq. +now apply Rlt_le. +apply Rplus_le_le_0_compat. +now apply Rlt_le. +apply Heps. Qed. -Lemma pred_plus_ulp_2 : - forall x, (0 < x)%R -> F x -> - let e := ln_beta_val beta x (ln_beta beta x) in - x = bpow (e - 1) -> - (x - bpow (fexp (e-1)) <> 0)%R -> - ((x - bpow (fexp (e-1))) + ulp (x - bpow (fexp (e-1))) = x)%R. +Theorem round_DN_plus_eps_pos: + forall x, (0 <= x)%R -> F x -> + forall eps, (0 <= eps < ulp x)%R -> + round beta fexp Zfloor (x + eps) = x. Proof. -intros x Zx Fx e Hxe Zp. -replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))). -ring. -assert (He:(fexp (e-1) <= e-1)%Z). -apply generic_format_bpow_inv with beta; trivial. -rewrite <- Hxe; assumption. -case (Zle_lt_or_eq _ _ He); clear He; intros He. -(* *) -unfold ulp; apply f_equal. -unfold canonic_exp; apply f_equal. -apply sym_eq. -apply ln_beta_unique. -rewrite Rabs_right. +intros x Zx Fx eps Heps. +destruct Zx as [Zx|Zx]. +(* . 0 < x *) +pattern x at 2 ; rewrite Fx. +unfold round. +unfold scaled_mantissa. simpl. +unfold canonic_exp at 1 2. +rewrite ln_beta_plus_eps ; trivial. +apply (f_equal (fun m => F2R (Float beta m _))). +rewrite Ztrunc_floor. +apply Zfloor_imp. split. -apply Rplus_le_reg_l with (bpow (fexp (e-1))). -ring_simplify. -apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. -apply Rplus_le_compat; apply bpow_le; omega. -apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. -apply Rle_trans with (bpow 1*bpow (e - 2))%R. +apply (Rle_trans _ _ _ (Zfloor_lb _)). apply Rmult_le_compat_r. apply bpow_ge_0. -replace 2%R with (Z2R 2) by reflexivity. -replace (bpow 1) with (Z2R beta). -apply Z2R_le. -apply <- Zle_is_le_bool. -now destruct beta. -simpl. -unfold Zpower_pos; simpl. -now rewrite Zmult_1_r. +pattern x at 1 ; rewrite <- Rplus_0_r. +now apply Rplus_le_compat_l. +apply Rlt_le_trans with ((x + ulp x) * bpow (- canonic_exp beta fexp x))%R. +apply Rmult_lt_compat_r. +apply bpow_gt_0. +now apply Rplus_lt_compat_l. +rewrite Rmult_plus_distr_r. +rewrite Z2R_plus. +apply Rplus_le_compat. +pattern x at 1 3 ; rewrite Fx. +unfold F2R. simpl. +rewrite Rmult_assoc. rewrite <- bpow_plus. -replace (1+(e-2))%Z with (e-1)%Z by ring. -now right. -rewrite <- Rplus_0_r, Hxe. -apply Rplus_lt_compat_l. -rewrite <- Ropp_0. -apply Ropp_lt_contravar. +rewrite Zplus_opp_r. +rewrite Rmult_1_r. +rewrite Zfloor_Z2R. +apply Rle_refl. +rewrite ulp_neq_0. +2: now apply Rgt_not_eq. +rewrite <- bpow_plus. +rewrite Zplus_opp_r. +apply Rle_refl. +apply Rmult_le_pos. +now apply Rlt_le. +apply bpow_ge_0. +(* . x=0 *) +rewrite <- Zx, Rplus_0_l; rewrite <- Zx in Heps. +case (proj1 Heps); intros P. +unfold round, scaled_mantissa, canonic_exp. +revert Heps; unfold ulp. +rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros _ (H1,H2). +absurd (0 < 0)%R; auto with real. +now apply Rle_lt_trans with (1:=H1). +intros n Hn H. +assert (fexp (ln_beta beta eps) = fexp n). +apply valid_exp; try assumption. +assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega]. +apply lt_bpow with beta. +apply Rle_lt_trans with (2:=proj2 H). +destruct (ln_beta beta eps) as (e,He). +simpl; rewrite Rabs_pos_eq in He. +now apply He, Rgt_not_eq. +now left. +replace (Zfloor (eps * bpow (- fexp (ln_beta beta eps)))) with 0%Z. +unfold F2R; simpl; ring. +apply sym_eq, Zfloor_imp. +split. +apply Rmult_le_pos. +now left. +apply bpow_ge_0. +apply Rmult_lt_reg_r with (bpow (fexp n)). apply bpow_gt_0. -apply Rle_ge; apply Rle_0_minus. -rewrite Hxe. -apply bpow_le. -omega. -(* *) -contradict Zp. -rewrite Hxe, He; ring. +rewrite Rmult_assoc, <- bpow_plus. +rewrite H0; ring_simplify (-fexp n + fexp n)%Z. +simpl; rewrite Rmult_1_l, Rmult_1_r. +apply H. +rewrite <- P, round_0; trivial. +apply valid_rnd_DN. Qed. -Theorem pred_plus_ulp : - forall x, (0 < x)%R -> F x -> - (pred x <> 0)%R -> - (pred x + ulp (pred x) = x)%R. -Proof. -intros x Zx Fx. -unfold pred. -case Req_bool_spec; intros H Zp. -now apply pred_plus_ulp_2. -now apply pred_plus_ulp_1. -Qed. -Theorem pred_lt_id : - forall x, - (pred x < x)%R. -Proof. -intros. -unfold pred. -case Req_bool_spec; intros H. -(* *) -rewrite <- Rplus_0_r. -apply Rplus_lt_compat_l. -rewrite <- Ropp_0. -apply Ropp_lt_contravar. +Theorem round_UP_plus_eps_pos : + forall x, (0 <= x)%R -> F x -> + forall eps, (0 < eps <= ulp x)%R -> + round beta fexp Zceil (x + eps) = (x + ulp x)%R. +Proof with auto with typeclass_instances. +intros x Zx Fx eps. +case Zx; intros Zx1. +(* . 0 < x *) +intros (Heps1,[Heps2|Heps2]). +assert (Heps: (0 <= eps < ulp x)%R). +split. +now apply Rlt_le. +exact Heps2. +assert (Hd := round_DN_plus_eps_pos x Zx Fx eps Heps). +rewrite round_UP_DN_ulp. +rewrite Hd. +rewrite 2!ulp_neq_0. +unfold canonic_exp. +now rewrite ln_beta_plus_eps. +now apply Rgt_not_eq. +now apply Rgt_not_eq, Rplus_lt_0_compat. +intros Fs. +rewrite round_generic in Hd... +apply Rgt_not_eq with (2 := Hd). +pattern x at 2 ; rewrite <- Rplus_0_r. +now apply Rplus_lt_compat_l. +rewrite Heps2. +apply round_generic... +now apply generic_format_succ_aux1. +(* . x=0 *) +rewrite <- Zx1, 2!Rplus_0_l. +intros Heps. +case (proj2 Heps). +unfold round, scaled_mantissa, canonic_exp. +unfold ulp. +rewrite Req_bool_true; trivial. +case negligible_exp_spec. +intros H2. +intros J; absurd (0 < 0)%R; auto with real. +apply Rlt_trans with eps; try assumption; apply Heps. +intros n Hn H. +assert (fexp (ln_beta beta eps) = fexp n). +apply valid_exp; try assumption. +assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega]. +apply lt_bpow with beta. +apply Rle_lt_trans with (2:=H). +destruct (ln_beta beta eps) as (e,He). +simpl; rewrite Rabs_pos_eq in He. +now apply He, Rgt_not_eq. +now left. +replace (Zceil (eps * bpow (- fexp (ln_beta beta eps)))) with 1%Z. +unfold F2R; simpl; rewrite H0; ring. +apply sym_eq, Zceil_imp. +split. +simpl; apply Rmult_lt_0_compat. +apply Heps. apply bpow_gt_0. -(* *) -rewrite <- Rplus_0_r. -apply Rplus_lt_compat_l. -rewrite <- Ropp_0. -apply Ropp_lt_contravar. +apply Rmult_le_reg_r with (bpow (fexp n)). apply bpow_gt_0. +rewrite Rmult_assoc, <- bpow_plus. +rewrite H0; ring_simplify (-fexp n + fexp n)%Z. +simpl; rewrite Rmult_1_l, Rmult_1_r. +now left. +intros P; rewrite P. +apply round_generic... +apply generic_format_ulp_0. Qed. -Theorem pred_ge_0 : - forall x, - (0 < x)%R -> F x -> (0 <= pred x)%R. -intros x Zx Fx. -unfold pred. -case Req_bool_spec; intros H. -(* *) -apply Rle_0_minus. -rewrite H. -apply bpow_le. -destruct (ln_beta beta x) as (ex,Ex) ; simpl. -rewrite ln_beta_bpow. -ring_simplify (ex - 1 + 1 - 1)%Z. -apply generic_format_bpow_inv with beta; trivial. -simpl in H. -rewrite <- H; assumption. -apply Rle_0_minus. -now apply ulp_le_id. -Qed. -Theorem round_UP_pred : - forall x, (0 < pred x)%R -> F x -> +Theorem round_UP_pred_plus_eps_pos : + forall x, (0 < x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x) )%R -> round beta fexp Zceil (pred x + eps) = x. Proof. intros x Hx Fx eps Heps. -rewrite round_UP_succ; trivial. -apply pred_plus_ulp; trivial. -apply Rlt_trans with (1:=Hx). -apply pred_lt_id. -now apply Rgt_not_eq. +rewrite round_UP_plus_eps_pos; trivial. +rewrite pred_eq_pos. +apply pred_pos_plus_ulp; trivial. +now left. +now apply pred_ge_0. apply generic_format_pred; trivial. -apply Rlt_trans with (1:=Hx). -apply pred_lt_id. Qed. -Theorem round_DN_pred : - forall x, (0 < pred x)%R -> F x -> +Theorem round_DN_minus_eps_pos : + forall x, (0 < x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x))%R -> round beta fexp Zfloor (x - eps) = pred x. Proof. -intros x Hpx Fx eps Heps. -assert (Hx:(0 < x)%R). -apply Rlt_trans with (1:=Hpx). -apply pred_lt_id. -replace (x-eps)%R with (pred x + (ulp (pred x)-eps))%R. -2: pattern x at 3; rewrite <- (pred_plus_ulp x); trivial. +intros x Hpx Fx eps. +rewrite pred_eq_pos;[intros Heps|now left]. +replace (x-eps)%R with (pred_pos x + (ulp (pred_pos x)-eps))%R. +2: pattern x at 3; rewrite <- (pred_pos_plus_ulp x); trivial. 2: ring. -2: now apply Rgt_not_eq. -rewrite round_DN_succ; trivial. -now apply generic_format_pred. +rewrite round_DN_plus_eps_pos; trivial. +now apply pred_pos_ge_0. +now apply generic_format_pred_pos. split. apply Rle_0_minus. now apply Heps. @@ -1009,15 +1215,96 @@ apply Ropp_lt_contravar. now apply Heps. Qed. -Lemma le_pred_lt_aux : + +Theorem round_DN_plus_eps: + forall x, F x -> + forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x) + else (ulp (pred (-x))))%R -> + round beta fexp Zfloor (x + eps) = x. +Proof. +intros x Fx eps Heps. +case (Rle_or_lt 0 x); intros Zx. +apply round_DN_plus_eps_pos; try assumption. +split; try apply Heps. +rewrite Rle_bool_true in Heps; trivial. +now apply Heps. +(* *) +rewrite Rle_bool_false in Heps; trivial. +rewrite <- (Ropp_involutive (x+eps)). +pattern x at 2; rewrite <- (Ropp_involutive x). +rewrite round_DN_opp. +apply f_equal. +replace (-(x+eps))%R with (pred (-x) + (ulp (pred (-x)) - eps))%R. +rewrite round_UP_pred_plus_eps_pos; try reflexivity. +now apply Ropp_0_gt_lt_contravar. +now apply generic_format_opp. +split. +apply Rplus_lt_reg_l with eps; ring_simplify. +apply Heps. +apply Rplus_le_reg_l with (eps-ulp (pred (- x)))%R; ring_simplify. +apply Heps. +unfold pred. +rewrite Ropp_involutive. +unfold succ; rewrite Rle_bool_false; try assumption. +rewrite Ropp_involutive; unfold Rminus. +rewrite <- Rplus_assoc, pred_pos_plus_ulp. +ring. +now apply Ropp_0_gt_lt_contravar. +now apply generic_format_opp. +Qed. + + +Theorem round_UP_plus_eps : + forall x, F x -> + forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x) + else (ulp (pred (-x))))%R -> + round beta fexp Zceil (x + eps) = (succ x)%R. +Proof with auto with typeclass_instances. +intros x Fx eps Heps. +case (Rle_or_lt 0 x); intros Zx. +rewrite succ_eq_pos; try assumption. +rewrite Rle_bool_true in Heps; trivial. +apply round_UP_plus_eps_pos; assumption. +(* *) +rewrite Rle_bool_false in Heps; trivial. +rewrite <- (Ropp_involutive (x+eps)). +rewrite <- (Ropp_involutive (succ x)). +rewrite round_UP_opp. +apply f_equal. +replace (-(x+eps))%R with (-succ x + (-eps + ulp (pred (-x))))%R. +apply round_DN_plus_eps_pos. +rewrite <- pred_opp. +apply pred_ge_0. +now apply Ropp_0_gt_lt_contravar. +now apply generic_format_opp. +now apply generic_format_opp, generic_format_succ. +split. +apply Rplus_le_reg_l with eps; ring_simplify. +apply Heps. +unfold pred; rewrite Ropp_involutive. +apply Rplus_lt_reg_l with (eps-ulp (- succ x))%R; ring_simplify. +apply Heps. +unfold succ; rewrite Rle_bool_false; try assumption. +apply trans_eq with (-x +-eps)%R;[idtac|ring]. +pattern (-x)%R at 3; rewrite <- (pred_pos_plus_ulp (-x)). +rewrite pred_eq_pos. +ring. +left; now apply Ropp_0_gt_lt_contravar. +now apply Ropp_0_gt_lt_contravar. +now apply generic_format_opp. +Qed. + + +Lemma le_pred_pos_lt : forall x y, F x -> F y -> - (0 < x < y)%R -> - (x <= pred y)%R. + (0 <= x < y)%R -> + (x <= pred_pos y)%R. Proof with auto with typeclass_instances. -intros x y Hx Hy H. +intros x y Fx Fy H. +case (proj1 H); intros V. assert (Zy:(0 < y)%R). -apply Rlt_trans with (1:=proj1 H). +apply Rle_lt_trans with (1:=proj1 H). apply H. (* *) assert (Zp: (0 < pred y)%R). @@ -1025,7 +1312,8 @@ assert (Zp:(0 <= pred y)%R). apply pred_ge_0 ; trivial. destruct Zp; trivial. generalize H0. -unfold pred. +rewrite pred_eq_pos;[idtac|now left]. +unfold pred_pos. destruct (ln_beta beta y) as (ey,Hey); simpl. case Req_bool_spec; intros Hy2. (* . *) @@ -1048,124 +1336,758 @@ now apply Rgt_ge. now apply Rgt_ge. apply Hey. now apply Rgt_not_eq. -case (Zle_lt_or_eq _ _ H2); intros Hexy. -assert (fexp ex = fexp (ey-1))%Z. -apply valid_exp. -omega. -rewrite <- H1. -omega. -absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z. -omega. -split. -apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). -now rewrite <- Hx. -apply lt_Z2R. -apply Rmult_lt_reg_r with (bpow (canonic_exp beta fexp x)). +case (Zle_lt_or_eq _ _ H2); intros Hexy. +assert (fexp ex = fexp (ey-1))%Z. +apply valid_exp. +omega. +rewrite <- H1. +omega. +absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z. +omega. +split. +apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). +now rewrite <- Fx. +apply lt_Z2R. +apply Rmult_lt_reg_r with (bpow (canonic_exp beta fexp x)). +apply bpow_gt_0. +replace (Z2R (Ztrunc (scaled_mantissa beta fexp x)) * + bpow (canonic_exp beta fexp x))%R with x. +rewrite Rmult_1_l. +unfold canonic_exp. +rewrite ln_beta_unique with beta x ex. +rewrite H3,<-H1, <- Hy2. +apply H. +exact Hex. +absurd (y <= x)%R. +now apply Rlt_not_le. +rewrite Rabs_right in Hex. +apply Rle_trans with (2:=proj1 Hex). +rewrite Hexy, Hy2. +now apply Rle_refl. +now apply Rgt_ge. +(* . *) +intros Hy3. +assert (y = bpow (fexp ey))%R. +apply Rminus_diag_uniq. +rewrite Hy3. +rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. +unfold canonic_exp. +rewrite (ln_beta_unique beta y ey); trivial. +apply Hey. +now apply Rgt_not_eq. +contradict Hy2. +rewrite H1. +apply f_equal. +apply Zplus_reg_l with 1%Z. +ring_simplify. +apply trans_eq with (ln_beta beta y). +apply sym_eq; apply ln_beta_unique. +rewrite H1, Rabs_right. +split. +apply bpow_le. +omega. +apply bpow_lt. +omega. +apply Rle_ge; apply bpow_ge_0. +apply ln_beta_unique. +apply Hey. +now apply Rgt_not_eq. +(* *) +case (Rle_or_lt (ulp (pred_pos y)) (y-x)); intros H1. +(* . *) +apply Rplus_le_reg_r with (-x + ulp (pred_pos y))%R. +ring_simplify (x+(-x+ulp (pred_pos y)))%R. +apply Rle_trans with (1:=H1). +rewrite <- (pred_pos_plus_ulp y) at 1; trivial. +apply Req_le; ring. +(* . *) +replace x with (y-(y-x))%R by ring. +rewrite <- pred_eq_pos;[idtac|now left]. +rewrite <- round_DN_minus_eps_pos with (eps:=(y-x)%R); try easy. +ring_simplify (y-(y-x))%R. +apply Req_le. +apply sym_eq. +apply round_generic... +split; trivial. +now apply Rlt_Rminus. +rewrite pred_eq_pos;[idtac|now left]. +now apply Rlt_le. +rewrite <- V; apply pred_pos_ge_0; trivial. +apply Rle_lt_trans with (1:=proj1 H); apply H. +Qed. + +Theorem succ_le_lt_aux: + forall x y, + F x -> F y -> + (0 <= x)%R -> (x < y)%R -> + (succ x <= y)%R. +Proof with auto with typeclass_instances. +intros x y Hx Hy Zx H. +rewrite succ_eq_pos; trivial. +case (Rle_or_lt (ulp x) (y-x)); intros H1. +apply Rplus_le_reg_r with (-x)%R. +now ring_simplify (x+ulp x + -x)%R. +replace y with (x+(y-x))%R by ring. +absurd (x < y)%R. +2: apply H. +apply Rle_not_lt; apply Req_le. +rewrite <- round_DN_plus_eps_pos with (eps:=(y-x)%R); try easy. +ring_simplify (x+(y-x))%R. +apply sym_eq. +apply round_generic... +split; trivial. +apply Rlt_le; now apply Rlt_Rminus. +Qed. + +Theorem succ_le_lt: + forall x y, + F x -> F y -> + (x < y)%R -> + (succ x <= y)%R. +Proof with auto with typeclass_instances. +intros x y Fx Fy H. +destruct (Rle_or_lt 0 x) as [Hx|Hx]. +now apply succ_le_lt_aux. +unfold succ; rewrite Rle_bool_false; try assumption. +case (Rle_or_lt y 0); intros Hy. +rewrite <- (Ropp_involutive y). +apply Ropp_le_contravar. +apply le_pred_pos_lt. +now apply generic_format_opp. +now apply generic_format_opp. +split. +rewrite <- Ropp_0; now apply Ropp_le_contravar. +now apply Ropp_lt_contravar. +apply Rle_trans with (-0)%R. +apply Ropp_le_contravar. +apply pred_pos_ge_0. +rewrite <- Ropp_0; now apply Ropp_lt_contravar. +now apply generic_format_opp. +rewrite Ropp_0; now left. +Qed. + +Theorem le_pred_lt : + forall x y, + F x -> F y -> + (x < y)%R -> + (x <= pred y)%R. +Proof. +intros x y Fx Fy Hxy. +rewrite <- (Ropp_involutive x). +unfold pred; apply Ropp_le_contravar. +apply succ_le_lt. +now apply generic_format_opp. +now apply generic_format_opp. +now apply Ropp_lt_contravar. +Qed. + + +Theorem lt_succ_le: + forall x y, + F x -> F y -> (y <> 0)%R -> + (x <= y)%R -> + (x < succ y)%R. +Proof. +intros x y Fx Fy Zy Hxy. +case (Rle_or_lt (succ y) x); trivial; intros H. +absurd (succ y = y)%R. +apply Rgt_not_eq. +now apply succ_gt_id. +apply Rle_antisym. +now apply Rle_trans with x. +apply succ_ge_id. +Qed. + + +Theorem succ_pred_aux : forall x, F x -> (0 < x)%R -> succ (pred x)=x. +Proof. +intros x Fx Hx. +rewrite pred_eq_pos;[idtac|now left]. +rewrite succ_eq_pos. +2: now apply pred_pos_ge_0. +now apply pred_pos_plus_ulp. +Qed. + +Theorem pred_succ_aux_0 : (pred (succ 0)=0)%R. +Proof. +unfold succ; rewrite Rle_bool_true. +2: apply Rle_refl. +rewrite Rplus_0_l. +rewrite pred_eq_pos. +2: apply ulp_ge_0. +unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec'. +(* *) +intros (H1,H2); rewrite H1. +unfold pred_pos; rewrite Req_bool_false. +2: apply Rlt_not_eq, bpow_gt_0. +unfold ulp; rewrite Req_bool_true; trivial. +rewrite H1; ring. +(* *) +intros (n,(H1,H2)); rewrite H1. +unfold pred_pos. +rewrite ln_beta_bpow. +replace (fexp n + 1 - 1)%Z with (fexp n) by ring. +rewrite Req_bool_true; trivial. +apply Rminus_diag_eq, f_equal. +apply sym_eq, valid_exp; omega. +Qed. + +Theorem pred_succ_aux : forall x, F x -> (0 < x)%R -> pred (succ x)=x. +Proof. +intros x Fx Hx. +rewrite succ_eq_pos;[idtac|now left]. +rewrite pred_eq_pos. +2: apply Rplus_le_le_0_compat;[now left| apply ulp_ge_0]. +unfold pred_pos. +case Req_bool_spec; intros H1. +(* *) +pose (l:=(ln_beta beta (x+ulp x))). +rewrite H1 at 1; fold l. +apply Rplus_eq_reg_r with (ulp x). +rewrite H1; fold l. +rewrite (ulp_neq_0 x) at 3. +2: now apply Rgt_not_eq. +unfold canonic_exp. +replace (fexp (ln_beta beta x)) with (fexp (l-1))%Z. +ring. +apply f_equal, sym_eq. +apply Zle_antisym. +assert (ln_beta beta x - 1 < l - 1)%Z;[idtac|omega]. +apply lt_bpow with beta. +unfold l; rewrite <- H1. +apply Rle_lt_trans with x. +destruct (ln_beta beta x) as (e,He); simpl. +rewrite <- (Rabs_right x) at 1. +2: apply Rle_ge; now left. +now apply He, Rgt_not_eq. +apply Rplus_lt_reg_l with (-x)%R; ring_simplify. +rewrite ulp_neq_0. +apply bpow_gt_0. +now apply Rgt_not_eq. +apply le_bpow with beta. +unfold l; rewrite <- H1. +apply id_p_ulp_le_bpow; trivial. +rewrite <- (Rabs_right x) at 1. +2: apply Rle_ge; now left. +apply bpow_ln_beta_gt. +(* *) +replace (ulp (x+ ulp x)) with (ulp x). +ring. +rewrite ulp_neq_0 at 1. +2: now apply Rgt_not_eq. +rewrite ulp_neq_0 at 1. +2: apply Rgt_not_eq, Rlt_gt. +2: apply Rlt_le_trans with (1:=Hx). +2: apply Rplus_le_reg_l with (-x)%R; ring_simplify. +2: apply ulp_ge_0. +apply f_equal; unfold canonic_exp; apply f_equal. +apply sym_eq, ln_beta_unique. +rewrite Rabs_right. +2: apply Rle_ge; left. +2: apply Rlt_le_trans with (1:=Hx). +2: apply Rplus_le_reg_l with (-x)%R; ring_simplify. +2: apply ulp_ge_0. +destruct (ln_beta beta x) as (e,He); simpl. +rewrite Rabs_right in He. +2: apply Rle_ge; now left. +split. +apply Rle_trans with x. +apply He, Rgt_not_eq; assumption. +apply Rplus_le_reg_l with (-x)%R; ring_simplify. +apply ulp_ge_0. +case (Rle_lt_or_eq_dec (x+ulp x) (bpow e)); trivial. +apply id_p_ulp_le_bpow; trivial. +apply He, Rgt_not_eq; assumption. +intros K; contradict H1. +rewrite K, ln_beta_bpow. +apply f_equal; ring. +Qed. + + + +Theorem succ_pred : forall x, F x -> succ (pred x)=x. +Proof. +intros x Fx. +case (Rle_or_lt 0 x); intros Hx. +destruct Hx as [Hx|Hx]. +now apply succ_pred_aux. +rewrite <- Hx. +rewrite pred_eq_opp_succ_opp, succ_opp, Ropp_0. +rewrite pred_succ_aux_0; ring. +rewrite pred_eq_opp_succ_opp, succ_opp. +rewrite pred_succ_aux. +ring. +now apply generic_format_opp. +now apply Ropp_0_gt_lt_contravar. +Qed. + +Theorem pred_succ : forall x, F x -> pred (succ x)=x. +Proof. +intros x Fx. +case (Rle_or_lt 0 x); intros Hx. +destruct Hx as [Hx|Hx]. +now apply pred_succ_aux. +rewrite <- Hx. +apply pred_succ_aux_0. +rewrite succ_eq_opp_pred_opp, pred_opp. +rewrite succ_pred_aux. +ring. +now apply generic_format_opp. +now apply Ropp_0_gt_lt_contravar. +Qed. + + +Theorem round_UP_pred_plus_eps : + forall x, F x -> + forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x) + else (ulp (pred x)))%R -> + round beta fexp Zceil (pred x + eps) = x. +Proof. +intros x Fx eps Heps. +rewrite round_UP_plus_eps. +now apply succ_pred. +now apply generic_format_pred. +unfold pred at 4. +rewrite Ropp_involutive, pred_succ. +rewrite ulp_opp. +generalize Heps; case (Rle_bool_spec x 0); intros H1 H2. +rewrite Rle_bool_false; trivial. +case H1; intros H1'. +apply Rlt_le_trans with (2:=H1). +apply pred_lt_id. +now apply Rlt_not_eq. +rewrite H1'; unfold pred, succ. +rewrite Ropp_0; rewrite Rle_bool_true;[idtac|now right]. +rewrite Rplus_0_l. +rewrite <- Ropp_0; apply Ropp_lt_contravar. +apply Rlt_le_trans with (1:=proj1 H2). +apply Rle_trans with (1:=proj2 H2). +rewrite Ropp_0, H1'. +now right. +rewrite Rle_bool_true; trivial. +now apply pred_ge_0. +now apply generic_format_opp. +Qed. + + +Theorem round_DN_minus_eps: + forall x, F x -> + forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x) + else (ulp (pred x)))%R -> + round beta fexp Zfloor (x - eps) = pred x. +Proof. +intros x Fx eps Heps. +replace (x-eps)%R with (-(-x+eps))%R by ring. +rewrite round_DN_opp. +unfold pred; apply f_equal. +pattern (-x)%R at 1; rewrite <- (pred_succ (-x)). +apply round_UP_pred_plus_eps. +now apply generic_format_succ, generic_format_opp. +rewrite pred_succ. +rewrite ulp_opp. +generalize Heps; case (Rle_bool_spec x 0); intros H1 H2. +rewrite Rle_bool_false; trivial. +case H1; intros H1'. +apply Rlt_le_trans with (-x)%R. +now apply Ropp_0_gt_lt_contravar. +apply succ_ge_id. +rewrite H1', Ropp_0, succ_eq_pos;[idtac|now right]. +rewrite Rplus_0_l. +apply Rlt_le_trans with (1:=proj1 H2). +rewrite H1' in H2; apply H2. +rewrite Rle_bool_true. +now rewrite succ_opp, ulp_opp. +rewrite succ_opp. +rewrite <- Ropp_0; apply Ropp_le_contravar. +now apply pred_ge_0. +now apply generic_format_opp. +now apply generic_format_opp. +Qed. + +(** Error of a rounding, expressed in number of ulps *) +(** false for x=0 in the FLX format *) +(* was ulp_error *) +Theorem error_lt_ulp : + forall rnd { Zrnd : Valid_rnd rnd } x, + (x <> 0)%R -> + (Rabs (round beta fexp rnd x - x) < ulp x)%R. +Proof with auto with typeclass_instances. +intros rnd Zrnd x Zx. +destruct (generic_format_EM beta fexp x) as [Hx|Hx]. +(* x = rnd x *) +rewrite round_generic... +unfold Rminus. +rewrite Rplus_opp_r, Rabs_R0. +rewrite ulp_neq_0; trivial. +apply bpow_gt_0. +(* x <> rnd x *) +destruct (round_DN_or_UP beta fexp rnd x) as [H|H] ; rewrite H ; clear H. +(* . *) +rewrite Rabs_left1. +rewrite Ropp_minus_distr. +apply Rplus_lt_reg_l with (round beta fexp Zfloor x). +rewrite <- round_UP_DN_ulp with (1 := Hx). +ring_simplify. +assert (Hu: (x <= round beta fexp Zceil x)%R). +apply round_UP_pt... +destruct Hu as [Hu|Hu]. +exact Hu. +elim Hx. +rewrite Hu. +apply generic_format_round... +apply Rle_minus. +apply round_DN_pt... +(* . *) +rewrite Rabs_pos_eq. +rewrite round_UP_DN_ulp with (1 := Hx). +apply Rplus_lt_reg_r with (x - ulp x)%R. +ring_simplify. +assert (Hd: (round beta fexp Zfloor x <= x)%R). +apply round_DN_pt... +destruct Hd as [Hd|Hd]. +exact Hd. +elim Hx. +rewrite <- Hd. +apply generic_format_round... +apply Rle_0_minus. +apply round_UP_pt... +Qed. + +(* was ulp_error_le *) +Theorem error_le_ulp : + forall rnd { Zrnd : Valid_rnd rnd } x, + (Rabs (round beta fexp rnd x - x) <= ulp x)%R. +Proof with auto with typeclass_instances. +intros rnd Zrnd x. +case (Req_dec x 0). +intros Zx; rewrite Zx, round_0... +unfold Rminus; rewrite Rplus_0_l, Ropp_0, Rabs_R0. +apply ulp_ge_0. +intros Zx; left. +now apply error_lt_ulp. +Qed. + +(* was ulp_half_error *) +Theorem error_le_half_ulp : + forall choice x, + (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp x)%R. +Proof with auto with typeclass_instances. +intros choice x. +destruct (generic_format_EM beta fexp x) as [Hx|Hx]. +(* x = rnd x *) +rewrite round_generic... +unfold Rminus. +rewrite Rplus_opp_r, Rabs_R0. +apply Rmult_le_pos. +apply Rlt_le. +apply Rinv_0_lt_compat. +now apply (Z2R_lt 0 2). +apply ulp_ge_0. +(* x <> rnd x *) +set (d := round beta fexp Zfloor x). +destruct (round_N_pt beta fexp choice x) as (Hr1, Hr2). +destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H]. +(* . rnd(x) = rndd(x) *) +apply Rle_trans with (Rabs (d - x)). +apply Hr2. +apply (round_DN_pt beta fexp x). +rewrite Rabs_left1. +rewrite Ropp_minus_distr. +apply Rmult_le_reg_r with 2%R. +now apply (Z2R_lt 0 2). +apply Rplus_le_reg_r with (d - x)%R. +ring_simplify. +apply Rle_trans with (1 := H). +right. field. +apply Rle_minus. +apply (round_DN_pt beta fexp x). +(* . rnd(x) = rndu(x) *) +assert (Hu: (d + ulp x)%R = round beta fexp Zceil x). +unfold d. +now rewrite <- round_UP_DN_ulp. +apply Rle_trans with (Rabs (d + ulp x - x)). +apply Hr2. +rewrite Hu. +apply (round_UP_pt beta fexp x). +rewrite Rabs_pos_eq. +apply Rmult_le_reg_r with 2%R. +now apply (Z2R_lt 0 2). +apply Rplus_le_reg_r with (- (d + ulp x - x))%R. +ring_simplify. +apply Rlt_le. +apply Rlt_le_trans with (1 := H). +right. field. +apply Rle_0_minus. +rewrite Hu. +apply (round_UP_pt beta fexp x). +Qed. + + +Theorem ulp_DN : + forall x, + (0 < round beta fexp Zfloor x)%R -> + ulp (round beta fexp Zfloor x) = ulp x. +Proof with auto with typeclass_instances. +intros x Hd. +rewrite 2!ulp_neq_0. +now rewrite canonic_exp_DN with (2 := Hd). +intros T; contradict Hd; rewrite T, round_0... +apply Rlt_irrefl. +now apply Rgt_not_eq. +Qed. + +Theorem round_neq_0_negligible_exp: + negligible_exp=None -> forall rnd { Zrnd : Valid_rnd rnd } x, + (x <> 0)%R -> (round beta fexp rnd x <> 0)%R. +Proof with auto with typeclass_instances. +intros H rndn Hrnd x Hx K. +case negligible_exp_spec'. +intros (_,Hn). +destruct (ln_beta beta x) as (e,He). +absurd (fexp e < e)%Z. +apply Zle_not_lt. +apply exp_small_round_0 with beta rndn x... +apply (Hn e). +intros (n,(H1,_)). +rewrite H in H1; discriminate. +Qed. + + +(** allows rnd x to be 0 *) +(* was ulp_error_f *) +Theorem error_lt_ulp_round : + forall { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x, + ( x <> 0)%R -> + (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R. +Proof with auto with typeclass_instances. +intros Hm. +(* wlog *) +cut (forall rnd : R -> Z, Valid_rnd rnd -> forall x : R, (0 < x)%R -> + (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R). +intros M rnd Hrnd x Zx. +case (Rle_or_lt 0 x). +intros H; destruct H. +now apply M. +contradict H; now apply sym_not_eq. +intros H. +rewrite <- (Ropp_involutive x). +rewrite round_opp, ulp_opp. +replace (- round beta fexp (Zrnd_opp rnd) (- x) - - - x)%R with + (-(round beta fexp (Zrnd_opp rnd) (- x) - (-x)))%R by ring. +rewrite Rabs_Ropp. +apply M. +now apply valid_rnd_opp. +now apply Ropp_0_gt_lt_contravar. +(* 0 < x *) +intros rnd Hrnd x Hx. +case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)). +apply round_ge_generic... +apply generic_format_0. +now left. +(* . 0 < round Zfloor x *) +intros Hx2. +apply Rlt_le_trans with (ulp x). +apply error_lt_ulp... +now apply Rgt_not_eq. +rewrite <- ulp_DN; trivial. +apply ulp_le_pos. +now left. +case (round_DN_or_UP beta fexp rnd x); intros V; rewrite V. +apply Rle_refl. +apply Rle_trans with x. +apply round_DN_pt... +apply round_UP_pt... +(* . 0 = round Zfloor x *) +intros Hx2. +case (round_DN_or_UP beta fexp rnd x); intros V; rewrite V; clear V. +(* .. round down -- difficult case *) +rewrite <- Hx2. +unfold Rminus; rewrite Rplus_0_l, Rabs_Ropp. +unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec. +(* without minimal exponent *) +intros K; contradict Hx2. +apply Rlt_not_eq. +apply F2R_gt_0_compat; simpl. +apply Zlt_le_trans with 1%Z. +apply Pos2Z.is_pos. +apply Zfloor_lub. +simpl; unfold scaled_mantissa, canonic_exp. +destruct (ln_beta beta x) as (e,He); simpl. +apply Rle_trans with (bpow (e-1) * bpow (- fexp e))%R. +rewrite <- bpow_plus. +replace 1%R with (bpow 0) by reflexivity. +apply bpow_le. +specialize (K e); omega. +apply Rmult_le_compat_r. +apply bpow_ge_0. +rewrite <- (Rabs_pos_eq x). +now apply He, Rgt_not_eq. +now left. +(* with a minimal exponent *) +intros n Hn. +rewrite Rabs_pos_eq;[idtac|now left]. +case (Rle_or_lt (bpow (fexp n)) x); trivial. +intros K; contradict Hx2. +apply Rlt_not_eq. +apply Rlt_le_trans with (bpow (fexp n)). apply bpow_gt_0. -replace (Z2R (Ztrunc (scaled_mantissa beta fexp x)) * - bpow (canonic_exp beta fexp x))%R with x. -rewrite Rmult_1_l. -unfold canonic_exp. -rewrite ln_beta_unique with beta x ex. -rewrite H3,<-H1, <- Hy2. -apply H. -exact Hex. -absurd (y <= x)%R. -now apply Rlt_not_le. -rewrite Rabs_right in Hex. -apply Rle_trans with (2:=proj1 Hex). -rewrite Hexy, Hy2. -now apply Rle_refl. -now apply Rgt_ge. -(* . *) -intros Hy3. -assert (y = bpow (fexp ey))%R. -apply Rminus_diag_uniq. -rewrite Hy3. -unfold ulp, canonic_exp. -rewrite (ln_beta_unique beta y ey); trivial. -apply Hey. +apply round_ge_generic... +apply generic_format_bpow. +now apply valid_exp. +(* .. round up *) +apply Rlt_le_trans with (ulp x). +apply error_lt_ulp... now apply Rgt_not_eq. -contradict Hy2. -rewrite H1. +apply ulp_le_pos. +now left. +apply round_UP_pt... +Qed. + +(** allows both x and rnd x to be 0 *) +(* was ulp_half_error_f *) +Theorem error_le_half_ulp_round : + forall { Hm : Monotone_exp fexp }, + forall choice x, + (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp (round beta fexp (Znearest choice) x))%R. +Proof with auto with typeclass_instances. +intros Hm choice x. +case (Req_dec (round beta fexp (Znearest choice) x) 0); intros Hfx. +(* *) +case (Req_dec x 0); intros Hx. +apply Rle_trans with (1:=error_le_half_ulp _ _). +rewrite Hx, round_0... +right; ring. +generalize (error_le_half_ulp choice x). +rewrite Hfx. +unfold Rminus; rewrite Rplus_0_l, Rabs_Ropp. +intros N. +unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec'. +intros (H1,H2). +contradict Hfx. +apply round_neq_0_negligible_exp... +intros (n,(H1,Hn)); rewrite H1. +apply Rle_trans with (1:=N). +right; apply f_equal. +rewrite ulp_neq_0; trivial. apply f_equal. -apply Zplus_reg_l with 1%Z. -ring_simplify. -apply trans_eq with (ln_beta beta y). -apply sym_eq; apply ln_beta_unique. -rewrite H1, Rabs_right. -split. -apply bpow_le. -omega. -apply bpow_lt. -omega. -apply Rle_ge; apply bpow_ge_0. -apply ln_beta_unique. -apply Hey. -now apply Rgt_not_eq. +unfold canonic_exp. +apply valid_exp; trivial. +assert (ln_beta beta x -1 < fexp n)%Z;[idtac|omega]. +apply lt_bpow with beta. +destruct (ln_beta beta x) as (e,He). +simpl. +apply Rle_lt_trans with (Rabs x). +now apply He. +apply Rle_lt_trans with (Rabs (round beta fexp (Znearest choice) x - x)). +right; rewrite Hfx; unfold Rminus; rewrite Rplus_0_l. +apply sym_eq, Rabs_Ropp. +apply Rlt_le_trans with (ulp 0). +rewrite <- Hfx. +apply error_lt_ulp_round... +unfold ulp; rewrite Req_bool_true, H1; trivial. +now right. (* *) -case (Rle_or_lt (ulp (pred y)) (y-x)); intros H1. +case (round_DN_or_UP beta fexp (Znearest choice) x); intros Hx. (* . *) -apply Rplus_le_reg_r with (-x + ulp (pred y))%R. -ring_simplify (x+(-x+ulp (pred y)))%R. -apply Rle_trans with (1:=H1). -rewrite <- (pred_plus_ulp y) at 1; trivial. -apply Req_le; ring. -now apply Rgt_not_eq. +case (Rle_or_lt 0 (round beta fexp Zfloor x)). +intros H; destruct H. +rewrite Hx at 2. +rewrite ulp_DN; trivial. +apply error_le_half_ulp. +rewrite Hx in Hfx; contradict Hfx; auto with real. +intros H. +apply Rle_trans with (1:=error_le_half_ulp _ _). +apply Rmult_le_compat_l. +auto with real. +apply ulp_le. +rewrite Hx; rewrite (Rabs_left1 x), Rabs_left; try assumption. +apply Ropp_le_contravar. +apply (round_DN_pt beta fexp x). +case (Rle_or_lt x 0); trivial. +intros H1; contradict H. +apply Rle_not_lt. +apply round_ge_generic... +apply generic_format_0. +now left. (* . *) -replace x with (y-(y-x))%R by ring. -rewrite <- round_DN_pred with (eps:=(y-x)%R); try easy. -ring_simplify (y-(y-x))%R. -apply Req_le. -apply sym_eq. -apply round_generic... -split; trivial. -now apply Rlt_Rminus. -now apply Rlt_le. +case (Rle_or_lt 0 (round beta fexp Zceil x)). +intros H; destruct H. +apply Rle_trans with (1:=error_le_half_ulp _ _). +apply Rmult_le_compat_l. +auto with real. +apply ulp_le_pos; trivial. +case (Rle_or_lt 0 x); trivial. +intros H1; contradict H. +apply Rle_not_lt. +apply round_le_generic... +apply generic_format_0. +now left. +rewrite Hx; apply (round_UP_pt beta fexp x). +rewrite Hx in Hfx; contradict Hfx; auto with real. +intros H. +rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp Zceil x)). +rewrite <- round_DN_opp. +rewrite ulp_DN; trivial. +pattern x at 1 2; rewrite <- Ropp_involutive. +rewrite round_N_opp. +unfold Rminus. +rewrite <- Ropp_plus_distr, Rabs_Ropp. +apply error_le_half_ulp. +rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption. Qed. -Theorem le_pred_lt : - forall x y, - F x -> F y -> - (0 < y)%R -> - (x < y)%R -> - (x <= pred y)%R. + +Theorem pred_le: forall x y, + F x -> F y -> (x <= y)%R -> (pred x <= pred y)%R. Proof. -intros x y Fx Fy Hy Hxy. -destruct (Rle_or_lt x 0) as [Hx|Hx]. -apply Rle_trans with (1 := Hx). -now apply pred_ge_0. -apply le_pred_lt_aux ; try easy. -now split. +intros x y Fx Fy Hxy. +assert (V:( ((x = 0) /\ (y = 0)) \/ (x <>0 \/ x < y))%R). +case (Req_dec x 0); intros Zx. +case Hxy; intros Zy. +now right; right. +left; split; trivial; now rewrite <- Zy. +now right; left. +destruct V as [(V1,V2)|V]. +rewrite V1,V2; now right. +apply le_pred_lt; try assumption. +apply generic_format_pred; try assumption. +case V; intros V1. +apply Rlt_le_trans with (2:=Hxy). +now apply pred_lt_id. +apply Rle_lt_trans with (2:=V1). +now apply pred_le_id. Qed. +Theorem succ_le: forall x y, + F x -> F y -> (x <= y)%R -> (succ x <= succ y)%R. +Proof. +intros x y Fx Fy Hxy. +rewrite 2!succ_eq_opp_pred_opp. +apply Ropp_le_contravar, pred_le; try apply generic_format_opp; try assumption. +now apply Ropp_le_contravar. +Qed. -Theorem pred_succ : forall { monotone_exp : Monotone_exp fexp }, - forall x, F x -> (0 < x)%R -> pred (x + ulp x)=x. +Theorem pred_le_inv: forall x y, F x -> F y + -> (pred x <= pred y)%R -> (x <= y)%R. Proof. -intros L x Fx Hx. -assert (x <= pred (x + ulp x))%R. -apply le_pred_lt. -assumption. -now apply generic_format_succ. -replace 0%R with (0+0)%R by ring; apply Rplus_lt_compat; try apply Hx. -apply bpow_gt_0. -apply Rplus_lt_reg_r with (-x)%R; ring_simplify. -apply bpow_gt_0. -apply Rle_antisym; trivial. -apply Rplus_le_reg_r with (ulp (pred (x + ulp x))). -rewrite pred_plus_ulp. -apply Rplus_le_compat_l. -now apply ulp_le. -replace 0%R with (0+0)%R by ring; apply Rplus_lt_compat; try apply Hx. -apply bpow_gt_0. -now apply generic_format_succ. -apply Rgt_not_eq. -now apply Rlt_le_trans with x. +intros x y Fx Fy Hxy. +rewrite <- (succ_pred x), <- (succ_pred y); try assumption. +apply succ_le; trivial; now apply generic_format_pred. Qed. +Theorem succ_le_inv: forall x y, F x -> F y + -> (succ x <= succ y)%R -> (x <= y)%R. +Proof. +intros x y Fx Fy Hxy. +rewrite <- (pred_succ x), <- (pred_succ y); try assumption. +apply pred_le; trivial; now apply generic_format_succ. +Qed. -Theorem lt_UP_le_DN : +(* was lt_UP_le_DN *) +Theorem le_round_DN_lt_UP : forall x y, F y -> (y < round beta fexp Zceil x -> y <= round beta fexp Zfloor x)%R. Proof with auto with typeclass_instances. @@ -1178,26 +2100,58 @@ apply round_UP_pt... now apply Rlt_le. Qed. +(* was lt_DN_le_UP *) +Theorem round_UP_le_gt_DN : + forall x y, F y -> + (round beta fexp Zfloor x < y -> round beta fexp Zceil x <= y)%R. +Proof with auto with typeclass_instances. +intros x y Fy Hlt. +apply round_UP_pt... +apply Rnot_lt_le. +contradict Hlt. +apply RIneq.Rle_not_lt. +apply round_DN_pt... +now apply Rlt_le. +Qed. + + + Theorem pred_UP_le_DN : - forall x, (0 < round beta fexp Zceil x)%R -> - (pred (round beta fexp Zceil x) <= round beta fexp Zfloor x)%R. + forall x, (pred (round beta fexp Zceil x) <= round beta fexp Zfloor x)%R. Proof with auto with typeclass_instances. -intros x Pxu. +intros x. destruct (generic_format_EM beta fexp x) as [Fx|Fx]. rewrite !round_generic... -now apply Rlt_le; apply pred_lt_id. +apply pred_le_id. +case (Req_dec (round beta fexp Zceil x) 0); intros Zx. +rewrite Zx; unfold pred; rewrite Ropp_0. +unfold succ; rewrite Rle_bool_true;[idtac|now right]. +rewrite Rplus_0_l; unfold ulp; rewrite Req_bool_true; trivial. +case negligible_exp_spec'. +intros (H1,H2). +contradict Zx; apply round_neq_0_negligible_exp... +intros L; apply Fx; rewrite L; apply generic_format_0. +intros (n,(H1,Hn)); rewrite H1. +case (Rle_or_lt (- bpow (fexp n)) (round beta fexp Zfloor x)); trivial; intros K. +absurd (round beta fexp Zceil x <= - bpow (fexp n))%R. +apply Rlt_not_le. +rewrite Zx, <- Ropp_0. +apply Ropp_lt_contravar, bpow_gt_0. +apply round_UP_le_gt_DN; try assumption. +apply generic_format_opp, generic_format_bpow. +now apply valid_exp. assert (let u := round beta fexp Zceil x in pred u < u)%R as Hup. - now apply pred_lt_id. -apply lt_UP_le_DN... +now apply pred_lt_id. +apply le_round_DN_lt_UP... apply generic_format_pred... now apply round_UP_pt. Qed. Theorem pred_UP_eq_DN : - forall x, (0 < round beta fexp Zceil x)%R -> ~ F x -> + forall x, ~ F x -> (pred (round beta fexp Zceil x) = round beta fexp Zfloor x)%R. Proof with auto with typeclass_instances. -intros x Px Fx. +intros x Fx. apply Rle_antisym. now apply pred_UP_le_DN. apply le_pred_lt; try apply generic_format_round... @@ -1205,212 +2159,200 @@ pose proof round_DN_UP_lt _ _ _ Fx as HE. now apply Rlt_trans with (1 := proj1 HE) (2 := proj2 HE). Qed. +Theorem succ_DN_eq_UP : + forall x, ~ F x -> + (succ (round beta fexp Zfloor x) = round beta fexp Zceil x)%R. +Proof with auto with typeclass_instances. +intros x Fx. +rewrite <- pred_UP_eq_DN; trivial. +rewrite succ_pred; trivial. +apply generic_format_round... +Qed. + + +(* was betw_eq_DN *) +Theorem round_DN_eq_betw: forall x d, F d + -> (d <= x < succ d)%R + -> round beta fexp Zfloor x = d. +Proof with auto with typeclass_instances. +intros x d Fd (Hxd1,Hxd2). +generalize (round_DN_pt beta fexp x); intros (T1,(T2,T3)). +apply sym_eq, Rle_antisym. +now apply T3. +destruct (generic_format_EM beta fexp x) as [Fx|NFx]. +rewrite round_generic... +apply succ_le_inv; try assumption. +apply succ_le_lt; try assumption. +apply generic_format_succ... +apply succ_le_inv; try assumption. +rewrite succ_DN_eq_UP; trivial. +apply round_UP_pt... +apply generic_format_succ... +now left. +Qed. + +(* was betw_eq_UP *) +Theorem round_UP_eq_betw: forall x u, F u + -> (pred u < x <= u)%R + -> round beta fexp Zceil x = u. +Proof with auto with typeclass_instances. +intros x u Fu Hux. +rewrite <- (Ropp_involutive (round beta fexp Zceil x)). +rewrite <- round_DN_opp. +rewrite <- (Ropp_involutive u). +apply f_equal. +apply round_DN_eq_betw; try assumption. +now apply generic_format_opp. +split;[now apply Ropp_le_contravar|idtac]. +rewrite succ_opp. +now apply Ropp_lt_contravar. +Qed. (** Properties of rounding to nearest and ulp *) -Theorem rnd_N_le_half_an_ulp: forall choice u v, - F u -> (0 < u)%R -> (v < u + (ulp u)/2)%R +Theorem round_N_le_midp: forall choice u v, + F u -> (v < (u + succ u)/2)%R -> (round beta fexp (Znearest choice) v <= u)%R. Proof with auto with typeclass_instances. -intros choice u v Fu Hu H. -(* . *) -assert (0 < ulp u / 2)%R. -unfold Rdiv; apply Rmult_lt_0_compat. -unfold ulp; apply bpow_gt_0. -auto with real. +intros choice u v Fu H. (* . *) -assert (ulp u / 2 < ulp u)%R. -apply Rlt_le_trans with (ulp u *1)%R;[idtac|right; ring]. -unfold Rdiv; apply Rmult_lt_compat_l. -apply bpow_gt_0. +assert (V: ((succ u = 0 /\ u = 0) \/ u < succ u)%R). +specialize (succ_ge_id u); intros P; destruct P as [P|P]. +now right. +case (Req_dec u 0); intros Zu. +left; split; trivial. +now rewrite <- P. +right; now apply succ_gt_id. +(* *) +destruct V as [(V1,V2)|V]. +rewrite V2; apply round_le_generic... +apply generic_format_0. +left; apply Rlt_le_trans with (1:=H). +rewrite V1,V2; right; field. +(* *) +assert (T: (u < (u + succ u) / 2 < succ u)%R). +split. apply Rmult_lt_reg_l with 2%R. -auto with real. -apply Rle_lt_trans with 1%R. +now auto with real. +apply Rplus_lt_reg_l with (-u)%R. +apply Rle_lt_trans with u;[right; ring|idtac]. +apply Rlt_le_trans with (1:=V). right; field. -rewrite Rmult_1_r; auto with real. +apply Rmult_lt_reg_l with 2%R. +now auto with real. +apply Rplus_lt_reg_l with (-succ u)%R. +apply Rle_lt_trans with u;[right; field|idtac]. +apply Rlt_le_trans with (1:=V). +right; ring. (* *) -apply Rnd_N_pt_monotone with F v (u + ulp u / 2)%R... +destruct T as (T1,T2). +apply Rnd_N_pt_monotone with F v ((u + succ u) / 2)%R... apply round_N_pt... -apply Rnd_DN_pt_N with (u+ulp u)%R. -pattern u at 3; replace u with (round beta fexp Zfloor (u + ulp u / 2)). +apply Rnd_DN_pt_N with (succ u)%R. +pattern u at 3; replace u with (round beta fexp Zfloor ((u + succ u) / 2)). apply round_DN_pt... -apply round_DN_succ; try assumption. +apply round_DN_eq_betw; trivial. split; try left; assumption. -replace (u+ulp u)%R with (round beta fexp Zceil (u + ulp u / 2)). +pattern (succ u) at 2; replace (succ u) with (round beta fexp Zceil ((u + succ u) / 2)). apply round_UP_pt... -apply round_UP_succ; try assumption... +apply round_UP_eq_betw; trivial. +apply generic_format_succ... +rewrite pred_succ; trivial. split; try left; assumption. right; field. Qed. -Theorem rnd_N_ge_half_an_ulp_pred: forall choice u v, - F u -> (0 < pred u)%R -> (u - (ulp (pred u))/2 < v)%R +Theorem round_N_ge_midp: forall choice u v, + F u -> ((u + pred u)/2 < v)%R -> (u <= round beta fexp (Znearest choice) v)%R. Proof with auto with typeclass_instances. -intros choice u v Fu Hu H. -(* . *) -assert (0 < u)%R. -apply Rlt_trans with (1:= Hu). -apply pred_lt_id. -assert (0 < ulp (pred u) / 2)%R. -unfold Rdiv; apply Rmult_lt_0_compat. -unfold ulp; apply bpow_gt_0. -auto with real. -assert (ulp (pred u) / 2 < ulp (pred u))%R. -apply Rlt_le_trans with (ulp (pred u) *1)%R;[idtac|right; ring]. -unfold Rdiv; apply Rmult_lt_compat_l. -apply bpow_gt_0. -apply Rmult_lt_reg_l with 2%R. -auto with real. -apply Rle_lt_trans with 1%R. -right; field. -rewrite Rmult_1_r; auto with real. -(* *) -apply Rnd_N_pt_monotone with F (u - ulp (pred u) / 2)%R v... -2: apply round_N_pt... -apply Rnd_UP_pt_N with (pred u). -pattern (pred u) at 2; replace (pred u) with (round beta fexp Zfloor (u - ulp (pred u) / 2)). -apply round_DN_pt... -replace (u - ulp (pred u) / 2)%R with (pred u + ulp (pred u) / 2)%R. -apply round_DN_succ; try assumption. -apply generic_format_pred; assumption. -split; [left|idtac]; assumption. -pattern u at 3; rewrite <- (pred_plus_ulp u); try assumption. -field. -now apply Rgt_not_eq. -pattern u at 3; replace u with (round beta fexp Zceil (u - ulp (pred u) / 2)). -apply round_UP_pt... -replace (u - ulp (pred u) / 2)%R with (pred u + ulp (pred u) / 2)%R. -apply trans_eq with (pred u +ulp(pred u))%R. -apply round_UP_succ; try assumption... -apply generic_format_pred; assumption. -split; [idtac|left]; assumption. -apply pred_plus_ulp; try assumption. -now apply Rgt_not_eq. -pattern u at 3; rewrite <- (pred_plus_ulp u); try assumption. -field. -now apply Rgt_not_eq. -pattern u at 4; rewrite <- (pred_plus_ulp u); try assumption. +intros choice u v Fu H. +rewrite <- (Ropp_involutive v). +rewrite round_N_opp. +rewrite <- (Ropp_involutive u). +apply Ropp_le_contravar. +apply round_N_le_midp. +now apply generic_format_opp. +apply Ropp_lt_cancel. +rewrite Ropp_involutive. +apply Rle_lt_trans with (2:=H). +unfold pred. right; field. -now apply Rgt_not_eq. Qed. -Theorem rnd_N_ge_half_an_ulp: forall choice u v, - F u -> (0 < u)%R -> (u <> bpow (ln_beta beta u - 1))%R - -> (u - (ulp u)/2 < v)%R - -> (u <= round beta fexp (Znearest choice) v)%R. +Lemma round_N_eq_DN: forall choice x, + let d:=round beta fexp Zfloor x in + let u:=round beta fexp Zceil x in + (x<(d+u)/2)%R -> + round beta fexp (Znearest choice) x = d. Proof with auto with typeclass_instances. -intros choice u v Fu Hupos Hu H. -(* *) -assert (bpow (ln_beta beta u-1) <= pred u)%R. -apply le_pred_lt; try assumption. -apply generic_format_bpow. -assert (canonic_exp beta fexp u < ln_beta beta u)%Z. -apply ln_beta_generic_gt; try assumption. -now apply Rgt_not_eq. -unfold canonic_exp in H0. -ring_simplify (ln_beta beta u - 1 + 1)%Z. -omega. -destruct ln_beta as (e,He); simpl in *. -assert (bpow (e - 1) <= Rabs u)%R. -apply He. -now apply Rgt_not_eq. -rewrite Rabs_right in H0. -case H0; auto. -intros T; contradict T. -now apply sym_not_eq. -apply Rle_ge; now left. -assert (Hu2:(ulp (pred u) = ulp u)). -unfold ulp, canonic_exp. -apply f_equal; apply f_equal. -apply ln_beta_unique. -rewrite Rabs_right. -split. -assumption. -apply Rlt_trans with (1:=pred_lt_id _). -destruct ln_beta as (e,He); simpl in *. -rewrite Rabs_right in He. -apply He. -now apply Rgt_not_eq. -apply Rle_ge; now left. -apply Rle_ge, pred_ge_0; assumption. -apply rnd_N_ge_half_an_ulp_pred; try assumption. -apply Rlt_le_trans with (2:=H0). -apply bpow_gt_0. -rewrite Hu2; assumption. +intros choice x d u H. +apply Rle_antisym. +destruct (generic_format_EM beta fexp x) as [Fx|Fx]. +rewrite round_generic... +apply round_DN_pt; trivial; now right. +apply round_N_le_midp. +apply round_DN_pt... +apply Rlt_le_trans with (1:=H). +right; apply f_equal2; trivial; apply f_equal. +now apply sym_eq, succ_DN_eq_UP. +apply round_ge_generic; try apply round_DN_pt... Qed. - -Lemma round_N_DN_betw: forall choice x d u, - Rnd_DN_pt (generic_format beta fexp) x d -> - Rnd_UP_pt (generic_format beta fexp) x u -> - (d<=x<(d+u)/2)%R -> +Lemma round_N_eq_DN_pt: forall choice x d u, + Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> + (x<(d+u)/2)%R -> round beta fexp (Znearest choice) x = d. Proof with auto with typeclass_instances. intros choice x d u Hd Hu H. -apply Rnd_N_pt_unicity with (generic_format beta fexp) x d u; try assumption. -intros Y. -absurd (x < (d+u)/2)%R; try apply H. -apply Rle_not_lt; right. -apply Rplus_eq_reg_r with (-x)%R. -apply trans_eq with (- (x-d)/2 + (u-x)/2)%R. -field. -rewrite Y; field. -apply round_N_pt... -apply Rnd_DN_UP_pt_N with d u... -apply Hd. -right; apply trans_eq with (-(d-x))%R;[idtac|ring]. -apply Rabs_left1. -apply Rplus_le_reg_l with x; ring_simplify. -apply H. -rewrite Rabs_left1. -apply Rplus_le_reg_l with (d+x)%R. -apply Rmult_le_reg_l with (/2)%R. -auto with real. -apply Rle_trans with x. -right; field. -apply Rle_trans with ((d+u)/2)%R. -now left. -right; field. -apply Rplus_le_reg_l with x; ring_simplify. -apply H. +assert (H0:(d = round beta fexp Zfloor x)%R). +apply Rnd_DN_pt_unicity with (1:=Hd). +apply round_DN_pt... +rewrite H0. +apply round_N_eq_DN. +rewrite <- H0. +rewrite Rnd_UP_pt_unicity with F x (round beta fexp Zceil x) u; try assumption. +apply round_UP_pt... Qed. +Lemma round_N_eq_UP: forall choice x, + let d:=round beta fexp Zfloor x in + let u:=round beta fexp Zceil x in + ((d+u)/2 < x)%R -> + round beta fexp (Znearest choice) x = u. +Proof with auto with typeclass_instances. +intros choice x d u H. +apply Rle_antisym. +apply round_le_generic; try apply round_UP_pt... +destruct (generic_format_EM beta fexp x) as [Fx|Fx]. +rewrite round_generic... +apply round_UP_pt; trivial; now right. +apply round_N_ge_midp. +apply round_UP_pt... +apply Rle_lt_trans with (2:=H). +right; apply f_equal2; trivial; rewrite Rplus_comm; apply f_equal2; trivial. +now apply pred_UP_eq_DN. +Qed. -Lemma round_N_UP_betw: forall choice x d u, - Rnd_DN_pt (generic_format beta fexp) x d -> - Rnd_UP_pt (generic_format beta fexp) x u -> - ((d+u)/2 < x <= u)%R -> +Lemma round_N_eq_UP_pt: forall choice x d u, + Rnd_DN_pt F x d -> Rnd_UP_pt F x u -> + ((d+u)/2 < x)%R -> round beta fexp (Znearest choice) x = u. Proof with auto with typeclass_instances. intros choice x d u Hd Hu H. -rewrite <- (Ropp_involutive (round beta fexp (Znearest choice) x )), - <- (Ropp_involutive u) . -apply f_equal. -rewrite <- (Ropp_involutive x) . -rewrite round_N_opp, Ropp_involutive. -apply round_N_DN_betw with (-d)%R. -replace u with (round beta fexp Zceil x). -rewrite <- round_DN_opp. -apply round_DN_pt... -apply Rnd_UP_pt_unicity with (generic_format beta fexp) x... -apply round_UP_pt... -replace d with (round beta fexp Zfloor x). -rewrite <- round_UP_opp. +assert (H0:(u = round beta fexp Zceil x)%R). +apply Rnd_UP_pt_unicity with (1:=Hu). apply round_UP_pt... -apply Rnd_DN_pt_unicity with (generic_format beta fexp) x... +rewrite H0. +apply round_N_eq_UP. +rewrite <- H0. +rewrite Rnd_DN_pt_unicity with F x (round beta fexp Zfloor x) d; try assumption. apply round_DN_pt... -split. -apply Ropp_le_contravar, H. -apply Rlt_le_trans with (-((d + u) / 2))%R. -apply Ropp_lt_contravar, H. -unfold Rdiv; right; ring. Qed. - End Fcore_ulp. diff --git a/flocq/Flocq_version.v b/flocq/Flocq_version.v index d2d9d3fb..c391f590 100644 --- a/flocq/Flocq_version.v +++ b/flocq/Flocq_version.v @@ -25,7 +25,8 @@ Definition Flocq_version := Eval vm_compute in let fix parse s major minor := match s with | String "."%char t => parse t (major * 100 + minor)%N N0 - | String h t => parse t major (minor + N_of_ascii h - N_of_ascii "0"%char)%N + | String h t => + parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N | Empty_string => (major * 100 + minor)%N end in - parse "2.4.0"%string N0 N0. + parse "2.5.0"%string N0 N0. diff --git a/flocq/Prop/Fprop_div_sqrt_error.v b/flocq/Prop/Fprop_div_sqrt_error.v index ec00ca4e..9d29001d 100644 --- a/flocq/Prop/Fprop_div_sqrt_error.v +++ b/flocq/Prop/Fprop_div_sqrt_error.v @@ -95,9 +95,6 @@ intros e; apply Zle_refl. now rewrite F2R_opp, F2R_mult, <- Hr1, <- Hy1. (* *) destruct (relative_error_FLX_ex beta prec (prec_gt_0 prec) rnd (x / y)%R) as (eps,(Heps1,Heps2)). -apply Rmult_integral_contrapositive_currified. -exact Zx. -now apply Rinv_neq_0_compat. rewrite Heps2. rewrite <- Rabs_Ropp. replace (-(x + - (x / y * (1 + eps) * y)))%R with (x * eps)%R by now field. @@ -135,8 +132,11 @@ now apply Rabs_pos_lt. rewrite Rabs_Ropp. replace (bpow (Fexp fr)) with (ulp beta (FLX_exp prec) (F2R fr)). rewrite <- Hr1. -apply ulp_error_f... -unfold ulp; apply f_equal. +apply error_lt_ulp_round... +apply Rmult_integral_contrapositive_currified; try apply Rinv_neq_0_compat; assumption. +rewrite ulp_neq_0. +2: now rewrite <- Hr1. +apply f_equal. now rewrite Hr2, <- Hr1. replace (prec+(Fexp fr+Fexp fy))%Z with ((prec+Fexp fy)+Fexp fr)%Z by ring. rewrite bpow_plus. @@ -246,8 +246,10 @@ apply Rmult_le_compat_r. apply Rabs_pos. apply Rle_trans with (/2*ulp beta (FLX_exp prec) (F2R fr))%R. rewrite <- Hr1. -apply ulp_half_error_f... -right; unfold ulp; apply f_equal. +apply error_le_half_ulp_round... +right; rewrite ulp_neq_0. +2: now rewrite <- Hr1. +apply f_equal. rewrite Hr2, <- Hr1; trivial. rewrite Rmult_assoc, Rmult_comm. replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring. diff --git a/flocq/Prop/Fprop_mult_error.v b/flocq/Prop/Fprop_mult_error.v index e84e80b4..7c71627b 100644 --- a/flocq/Prop/Fprop_mult_error.v +++ b/flocq/Prop/Fprop_mult_error.v @@ -126,8 +126,9 @@ apply Zplus_le_compat_r. rewrite ln_beta_unique with (1 := Hexy). apply ln_beta_le_bpow with (1 := Hz). replace (bpow (exy - prec)) with (ulp beta (FLX_exp prec) (x * y)). -apply ulp_error... -unfold ulp, canonic_exp. +apply error_lt_ulp... +rewrite ulp_neq_0; trivial. +unfold canonic_exp. now rewrite ln_beta_unique with (1 := Hexy). apply Hc1. reflexivity. diff --git a/flocq/Prop/Fprop_relative.v b/flocq/Prop/Fprop_relative.v index f0a8f344..585b71da 100644 --- a/flocq/Prop/Fprop_relative.v +++ b/flocq/Prop/Fprop_relative.v @@ -35,7 +35,7 @@ Section relative_error_conversion. Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. -Lemma relative_error_lt_conversion' : +Lemma relative_error_lt_conversion : forall x b, (0 < b)%R -> (x <> 0 -> Rabs (round beta fexp rnd x - x) < b * Rabs x)%R -> exists eps, @@ -62,19 +62,6 @@ rewrite Rinv_l with (1 := Hx0). now rewrite Rabs_R1, Rmult_1_r. Qed. -(* TODO: remove *) -Lemma relative_error_lt_conversion : - forall x b, (0 < b)%R -> - (Rabs (round beta fexp rnd x - x) < b * Rabs x)%R -> - exists eps, - (Rabs eps < b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R. -Proof. -intros x b Hb0 Hxb. -apply relative_error_lt_conversion'. -exact Hb0. -now intros _. -Qed. - Lemma relative_error_le_conversion : forall x b, (0 <= b)%R -> (Rabs (round beta fexp rnd x - x) <= b * Rabs x)%R -> @@ -113,16 +100,15 @@ Theorem relative_error : forall x, (bpow emin <= Rabs x)%R -> (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R. -Proof. +Proof with auto with typeclass_instances. intros x Hx. -apply Rlt_le_trans with (ulp beta fexp x)%R. -now apply ulp_error. -unfold ulp, canonic_exp. assert (Hx': (x <> 0)%R). -intros H. -apply Rlt_not_le with (2 := Hx). -rewrite H, Rabs_R0. -apply bpow_gt_0. +intros T; contradict Hx; rewrite T, Rabs_R0. +apply Rlt_not_le, bpow_gt_0. +apply Rlt_le_trans with (ulp beta fexp x)%R. +now apply error_lt_ulp... +rewrite ulp_neq_0; trivial. +unfold canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). @@ -150,6 +136,7 @@ Proof with auto with typeclass_instances. intros x Hx. apply relative_error_lt_conversion... apply bpow_gt_0. +intros _. now apply relative_error. Qed. @@ -168,28 +155,17 @@ rewrite F2R_0, F2R_Zabs. now apply Rabs_pos_lt. Qed. -Theorem relative_error_F2R_emin_ex' : +Theorem relative_error_F2R_emin_ex : forall m, let x := F2R (Float beta m emin) in exists eps, (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R. Proof with auto with typeclass_instances. intros m x. -apply relative_error_lt_conversion'... +apply relative_error_lt_conversion... apply bpow_gt_0. now apply relative_error_F2R_emin. Qed. -(* TODO: remove *) -Theorem relative_error_F2R_emin_ex : - forall m, let x := F2R (Float beta m emin) in - (x <> 0)%R -> - exists eps, - (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R. -Proof with auto with typeclass_instances. -intros m x _. -apply relative_error_F2R_emin_ex'. -Qed. - Theorem relative_error_round : (0 < p)%Z -> forall x, @@ -197,14 +173,13 @@ Theorem relative_error_round : (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs (round beta fexp rnd x))%R. Proof with auto with typeclass_instances. intros Hp x Hx. -apply Rlt_le_trans with (ulp beta fexp x)%R. -now apply ulp_error. assert (Hx': (x <> 0)%R). -intros H. -apply Rlt_not_le with (2 := Hx). -rewrite H, Rabs_R0. -apply bpow_gt_0. -unfold ulp, canonic_exp. +intros T; contradict Hx; rewrite T, Rabs_R0. +apply Rlt_not_le, bpow_gt_0. +apply Rlt_le_trans with (ulp beta fexp x)%R. +now apply error_lt_ulp. +rewrite ulp_neq_0; trivial. +unfold canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). @@ -222,7 +197,7 @@ apply bpow_ge_0. generalize He. apply round_abs_abs... clear rnd valid_rnd x Hx Hx' He. -intros rnd valid_rnd x Hx. +intros rnd valid_rnd x _ Hx. rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))). now apply round_le. apply generic_format_bpow. @@ -257,7 +232,7 @@ Theorem relative_error_N : Proof. intros x Hx. apply Rle_trans with (/2 * ulp beta fexp x)%R. -now apply ulp_half_error. +now apply error_le_half_ulp. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Rlt_le. @@ -268,7 +243,8 @@ intros H. apply Rlt_not_le with (2 := Hx). rewrite H, Rabs_R0. apply bpow_gt_0. -unfold ulp, canonic_exp. +rewrite ulp_neq_0; trivial. +unfold canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). @@ -348,7 +324,7 @@ Theorem relative_error_N_round : Proof with auto with typeclass_instances. intros Hp x Hx. apply Rle_trans with (/2 * ulp beta fexp x)%R. -now apply ulp_half_error. +now apply error_le_half_ulp. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Rlt_le. @@ -359,7 +335,8 @@ intros H. apply Rlt_not_le with (2 := Hx). rewrite H, Rabs_R0. apply bpow_gt_0. -unfold ulp, canonic_exp. +rewrite ulp_neq_0; trivial. +unfold canonic_exp. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He Hx'). @@ -377,7 +354,7 @@ apply bpow_ge_0. generalize He. apply round_abs_abs... clear rnd valid_rnd x Hx Hx' He. -intros rnd valid_rnd x Hx. +intros rnd valid_rnd x _ Hx. rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))). now apply round_le. apply generic_format_bpow. @@ -428,17 +405,6 @@ Qed. Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. -(* TODO: remove *) -Theorem relative_error_FLT_F2R_emin : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (x <> 0)%R -> - (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. -Proof with auto with typeclass_instances. -intros m x Hx. -apply relative_error_F2R_emin... -apply relative_error_FLT_aux. -Qed. - Theorem relative_error_FLT : forall x, (bpow (emin + prec - 1) <= Rabs x)%R -> @@ -449,7 +415,7 @@ apply relative_error with (emin + prec - 1)%Z... apply relative_error_FLT_aux. Qed. -Theorem relative_error_FLT_F2R_emin' : +Theorem relative_error_FLT_F2R_emin : forall m, let x := F2R (Float beta m emin) in (x <> 0)%R -> (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R. @@ -472,26 +438,13 @@ now exists (Float beta m emin). now apply relative_error_FLT. Qed. -Theorem relative_error_FLT_F2R_emin_ex' : +Theorem relative_error_FLT_F2R_emin_ex : forall m, let x := F2R (Float beta m emin) in exists eps, (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R. Proof with auto with typeclass_instances. intros m x. -apply relative_error_lt_conversion'... -apply bpow_gt_0. -now apply relative_error_FLT_F2R_emin'. -Qed. - -(* TODO: remove *) -Theorem relative_error_FLT_F2R_emin_ex : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (x <> 0)%R -> - exists eps, - (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R. -Proof with auto with typeclass_instances. -intros m x _. -apply relative_error_lt_conversion'... +apply relative_error_lt_conversion... apply bpow_gt_0. now apply relative_error_FLT_F2R_emin. Qed. @@ -506,7 +459,7 @@ Proof with auto with typeclass_instances. intros x Hx. apply relative_error_lt_conversion... apply bpow_gt_0. -now apply relative_error_FLT. +intros _; now apply relative_error_FLT. Qed. Variable choice : Z -> bool. @@ -548,7 +501,7 @@ apply relative_error_N_round with (emin + prec - 1)%Z... apply relative_error_FLT_aux. Qed. -Theorem relative_error_N_FLT_F2R_emin' : +Theorem relative_error_N_FLT_F2R_emin : forall m, let x := F2R (Float beta m emin) in (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. Proof with auto with typeclass_instances. @@ -573,17 +526,7 @@ now exists (Float beta m emin). now apply relative_error_N_FLT. Qed. -(* TODO: remove *) -Theorem relative_error_N_FLT_F2R_emin : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R. -Proof with auto with typeclass_instances. -intros m x. -apply relative_error_N_F2R_emin... -apply relative_error_FLT_aux. -Qed. - -Theorem relative_error_N_FLT_F2R_emin_ex' : +Theorem relative_error_N_FLT_F2R_emin_ex : forall m, let x := F2R (Float beta m emin) in exists eps, (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R. @@ -594,26 +537,11 @@ apply Rmult_le_pos. apply Rlt_le. apply (RinvN_pos 1). apply bpow_ge_0. -now apply relative_error_N_FLT_F2R_emin'. -Qed. - -(* TODO: remove *) -Theorem relative_error_N_FLT_F2R_emin_ex : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - exists eps, - (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R. -Proof with auto with typeclass_instances. -intros m x. -apply relative_error_le_conversion... -apply Rlt_le. -apply Rmult_lt_0_compat. -apply Rinv_0_lt_compat. -now apply (Z2R_lt 0 2). -apply bpow_gt_0. now apply relative_error_N_FLT_F2R_emin. Qed. -Theorem relative_error_N_FLT_round_F2R_emin' : + +Theorem relative_error_N_FLT_round_F2R_emin : forall m, let x := F2R (Float beta m emin) in (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R. Proof with auto with typeclass_instances. @@ -639,16 +567,6 @@ apply relative_error_N_round with (emin := (emin + prec - 1)%Z)... apply relative_error_FLT_aux. Qed. -(* TODO: remove *) -Theorem relative_error_N_FLT_round_F2R_emin : - forall m, let x := F2R (Float beta m (emin + prec - 1)) in - (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R. -Proof with auto with typeclass_instances. -intros m x. -apply relative_error_N_round_F2R_emin... -apply relative_error_FLT_aux. -Qed. - Lemma error_N_FLT_aux : forall x, (0 < x)%R -> @@ -682,10 +600,11 @@ auto with real. apply bpow_ge_0. split. apply Rle_trans with (/2*ulp beta (FLT_exp emin prec) x)%R. -apply ulp_half_error. +apply error_le_half_ulp. now apply FLT_exp_valid. apply Rmult_le_compat_l; auto with real. -unfold ulp. +rewrite ulp_neq_0. +2: now apply Rgt_not_eq. apply bpow_le. unfold FLT_exp, canonic_exp. rewrite Zmax_right. @@ -770,28 +689,17 @@ apply He. Qed. (** 1+#ε# property in any rounding in FLX *) -Theorem relative_error_FLX_ex' : +Theorem relative_error_FLX_ex : forall x, exists eps, (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R. Proof with auto with typeclass_instances. intros x. -apply relative_error_lt_conversion'... +apply relative_error_lt_conversion... apply bpow_gt_0. now apply relative_error_FLX. Qed. -(* TODO: remove *) -Theorem relative_error_FLX_ex : - forall x, - (x <> 0)%R -> - exists eps, - (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R. -Proof with auto with typeclass_instances. -intros x _. -apply relative_error_FLX_ex'. -Qed. - Theorem relative_error_FLX_round : forall x, (x <> 0)%R -> -- cgit