diff --git a/src/Calc/Fcalc_bracket.v b/src/Calc/Fcalc_bracket.v index 371e58eb39ee6f575416a923a3a8d4507db5b50e..5aa474c00dc49bd3e9e38c39a40403aa07984c92 100644 --- a/src/Calc/Fcalc_bracket.v +++ b/src/Calc/Fcalc_bracket.v @@ -334,12 +334,7 @@ Variable Hstep : (0 < step)%R. Lemma double_div2 : ((start + start)/2 = start)%R. Proof. -rewrite <- (Rmult_1_r start). -unfold Rdiv. -rewrite <- Rmult_plus_distr_l, Rmult_assoc. -apply f_equal. -apply Rinv_r. -now apply (Z2R_neq 2 0). +field. Qed. Lemma ordered_steps : @@ -479,19 +474,9 @@ Lemma middle_odd : (((start + Z2R k * step) + (start + Z2R (k + 1) * step))/2 = start + Z2R nb_steps * step * /2)%R. Proof. intros k Hk. -apply Rminus_diag_uniq. -rewrite plus_Z2R. -simpl (Z2R 1). -unfold Rdiv. -match goal with -| |- ?v = R0 => replace v with (start * (2 * /2 + -1) + step * /2 * ((2 * Z2R k + 1) - Z2R nb_steps))%R by ring -end. -rewrite Rinv_r, Rplus_opp_r, Rmult_0_r, Rplus_0_l. -apply Rmult_eq_0_compat_l. -change (Z2R 2 * Z2R k + Z2R 1 - Z2R nb_steps = 0)%R. -rewrite <- mult_Z2R, <- plus_Z2R, <- minus_Z2R. -now rewrite Hk, Zminus_diag. -now apply (Z2R_neq 2 0). +rewrite <- Hk. +rewrite 2!plus_Z2R, mult_Z2R. +simpl. field. Qed. Theorem inbetween_step_Lo_Mi_odd : @@ -937,7 +922,7 @@ Theorem inbetween_float_DN : forall x m l, let e := canonic_exponent beta fexp x in inbetween_float m e x l -> - Rnd_DN_pt format x (F2R (Float beta m e)). + F2R (Float beta m e) = rounding beta fexp ZrndDN x. Proof. intros x m l e Hl. assert (Hb: (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R). @@ -945,7 +930,7 @@ apply inbetween_bounds_strict with (2 := Hl). apply F2R_lt_compat. apply Zlt_succ. replace m with (Zfloor (x * bpow (- e))). -now apply generic_DN_pt. +apply refl_equal. apply Zfloor_imp. split. apply Rmult_le_reg_r with (bpow e). @@ -970,7 +955,7 @@ Theorem inbetween_float_UP : forall x m l, let e := canonic_exponent beta fexp x in inbetween_float m e x l -> - Rnd_UP_pt format x (F2R (Float beta (cond_incr (round_UP l) m) e)). + F2R (Float beta (cond_incr (round_UP l) m) e) = rounding beta fexp ZrndUP x. Proof. intros x m l e Hl. assert (Hl': l = loc_Eq \/ l <> loc_Eq). @@ -981,7 +966,8 @@ rewrite Hl' in Hl. inversion_clear Hl. rewrite H, Hl'. simpl. -apply Rnd_UP_pt_refl. +rewrite rounding_generic. +apply refl_equal. apply generic_format_canonic. unfold canonic. now rewrite <- H. @@ -994,7 +980,7 @@ apply F2R_lt_compat. apply Zlt_succ. exact Hl'. replace (m + 1)%Z with (Zceil (x * bpow (- e))). -now apply generic_UP_pt. +apply refl_equal. apply Zceil_imp. ring_simplify (m + 1 - 1)%Z. split. @@ -1033,59 +1019,75 @@ assert (Hd := inbetween_float_DN _ _ _ Hl). unfold round_NE. generalize (inbetween_float_UP _ _ _ Hl). fold e in Hd |- *. +assert (Hd': Rnd_DN_pt format x (F2R (Float beta m e))). +rewrite Hd. +now apply generic_DN_pt. +assert (Hu': Rnd_UP_pt format x (rounding beta fexp ZrndUP x)). +now apply generic_UP_pt. destruct l ; simpl ; intros Hu. (* loc_Eq *) inversion_clear Hl. rewrite H. apply Rnd_NG_pt_refl. -apply Hd. +rewrite Hd. +now apply generic_format_rounding. (* loc_Lo *) split. -now apply (Rnd_N_pt_bracket_not_Hi _ _ _ _ Hd Hu loc_Lo). +rewrite <- Hu in Hu'. +now apply (Rnd_N_pt_bracket_not_Hi _ _ _ _ Hd' Hu' loc_Lo). right. intros g Hg. -destruct (Rnd_N_pt_DN_or_UP _ _ _ Hg) as [H|H]. -now apply Rnd_DN_pt_unicity with (1 := H). -rewrite (Rnd_UP_pt_unicity _ _ _ _ H Hu) in Hg. -now elim (Rnd_not_N_pt_bracket_Lo _ _ _ _ Hd Hl). +destruct (generic_N_pt_DN_or_UP _ _ prop_exp _ _ Hg) as [H|H]. +now rewrite Hd. +rewrite H in Hg. +elim (Rnd_not_N_pt_bracket_Lo _ _ _ _ Hd' Hl). +now rewrite Hu. (* loc_Mi *) assert (Hm: (0 <= m)%Z). apply Zlt_succ_le. apply F2R_gt_0_reg with beta e. apply Rlt_le_trans with (1 := Hx). -apply Hu. +unfold Zsucc. +rewrite Hu. +apply (generic_UP_pt beta fexp prop_exp x). destruct (Z_le_lt_eq_dec _ _ Hm) as [Hm'|Hm']. (* - 0 < m *) assert (Hcd : canonic beta fexp (Float beta m e)). unfold canonic. apply sym_eq. -apply canonic_exponent_DN_pt ; try easy. +rewrite Hd. +apply canonic_exponent_DN ; try easy. +rewrite <- Hd. now apply F2R_gt_0_compat. destruct (Zeven_odd_bool m) as ([|], Heo) ; simpl. split. -now apply (Rnd_N_pt_bracket_not_Hi _ _ _ _ Hd Hu loc_Mi). +apply (Rnd_N_pt_bracket_not_Hi _ _ _ _ Hd' Hu' loc_Mi). +easy. +now rewrite <- Hu. left. now eexists ; repeat split. split. -apply (Rnd_N_pt_bracket_Mi_Hi _ _ _ _ Hd Hu loc_Mi). +rewrite <- Hu in Hu'. +apply (Rnd_N_pt_bracket_Mi_Hi _ _ _ _ Hd' Hu' loc_Mi). now left. exact Hl. left. -generalize (proj1 Hu). +generalize (proj1 Hu'). +rewrite <- Hu. unfold generic_format. fold e. set (cu := Float beta (Ztrunc (scaled_mantissa beta fexp (F2R (Float beta (m + 1) e)))) (canonic_exponent beta fexp (F2R (Float beta (m + 1) e)))). -intros Hu'. +intros Hu''. assert (Hcu : canonic beta fexp cu). unfold canonic. -now rewrite <- Hu'. -rewrite Hu'. +now rewrite <- Hu''. +rewrite Hu''. eexists ; repeat split. exact Hcu. replace (Fnum cu) with (Fnum (Float beta m e) + Fnum cu + -Fnum (Float beta m e))%Z by ring. apply Zodd_plus_Zodd. -rewrite Hu' in Hu. +rewrite Hu'' in Hu. apply (DN_UP_parity_generic beta fexp prop_exp strong_fexp x (Float beta m e) cu) ; try easy. apply (generic_format_discrete beta fexp x m). apply inbetween_bounds_strict_not_Eq with (2 := Hl). @@ -1097,7 +1099,9 @@ now apply Zodd_mult_Zodd. (* - m = 0 *) destruct (Zeven_odd_bool m) as ([|], Heo) ; simpl. split. -now apply (Rnd_N_pt_bracket_not_Hi _ _ _ _ Hd Hu loc_Mi). +apply (Rnd_N_pt_bracket_not_Hi _ _ _ _ Hd' Hu' loc_Mi). +easy. +now rewrite <- Hu. left. rewrite <- Hm', F2R_0. exists (Float beta 0 (canonic_exponent beta fexp 0)). @@ -1108,15 +1112,18 @@ rewrite <- Hm' in Heo. elim Heo. (* loc_Hi *) split. -apply (Rnd_N_pt_bracket_Mi_Hi _ _ _ _ Hd Hu loc_Hi). +rewrite <- Hu in Hu'. +apply (Rnd_N_pt_bracket_Mi_Hi _ _ _ _ Hd' Hu' loc_Hi). now right. exact Hl. right. intros g Hg. -destruct (Rnd_N_pt_DN_or_UP _ _ _ Hg) as [H|H]. -rewrite (Rnd_DN_pt_unicity _ _ _ _ H Hd) in Hg. -now elim (Rnd_not_N_pt_bracket_Hi _ _ _ _ Hu Hl). -now apply Rnd_UP_pt_unicity with (1 := H). +destruct (generic_N_pt_DN_or_UP _ _ prop_exp _ _ Hg) as [H|H]. +rewrite H in Hg. +rewrite <- Hu in Hu'. +elim (Rnd_not_N_pt_bracket_Hi _ _ _ _ Hu' Hl). +now rewrite Hd. +now rewrite H. Qed. End Fcalc_bracket_generic. diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v index 7e3e3aa57415c758e29fcc8f131dd502b68120a7..a299aeff00bc8287a7cae8db450e858f2d91b847 100644 --- a/src/Core/Fcore_generic_fmt.v +++ b/src/Core/Fcore_generic_fmt.v @@ -346,6 +346,29 @@ Let Zrnd := Zrnd rnd. Let Zrnd_monotone := Zrnd_monotone rnd. Let Zrnd_Z2R := Zrnd_Z2R rnd. +Theorem Zrnd_DN_or_UP : + forall x, Zrnd x = Zfloor x \/ Zrnd x = Zceil x. +Proof. +intros x. +destruct (Zle_or_lt (Zrnd x) (Zfloor x)) as [Hx|Hx]. +left. +apply Zle_antisym with (1 := Hx). +rewrite <- (Zrnd_Z2R (Zfloor x)). +apply Zrnd_monotone. +apply Zfloor_lb. +right. +apply Zle_antisym. +rewrite <- (Zrnd_Z2R (Zceil x)). +apply Zrnd_monotone. +apply Zceil_ub. +rewrite Zceil_floor_neq. +omega. +intros H. +rewrite <- H in Hx. +rewrite Zfloor_Z2R, Zrnd_Z2R in Hx. +apply Zlt_irrefl with (1 := Hx). +Qed. + Definition rounding x := F2R (Float beta (Zrnd (scaled_mantissa x)) (canonic_exponent x)). @@ -455,6 +478,18 @@ End Fcore_generic_rounding_pos. Definition ZrndDN := mkZrounding Zfloor Zfloor_le Zfloor_Z2R. Definition ZrndUP := mkZrounding Zceil Zceil_le Zceil_Z2R. +Theorem rounding_DN_or_UP : + forall rnd x, + rounding rnd x = rounding ZrndDN x \/ rounding rnd x = rounding ZrndUP x. +Proof. +intros rnd x. +unfold rounding. +unfold Zrnd at 2 4. simpl. +destruct (Zrnd_DN_or_UP rnd (scaled_mantissa x)) as [Hx|Hx]. +left. now rewrite Hx. +right. now rewrite Hx. +Qed. + Section Fcore_generic_rounding. Theorem rounding_monotone : @@ -519,10 +554,10 @@ End Fcore_generic_rounding. Theorem generic_DN_pt_pos : forall x, (0 < x)%R -> - Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (scaled_mantissa x)) (canonic_exponent x))). + Rnd_DN_pt generic_format x (rounding ZrndDN x). Proof. intros x H0x. -unfold scaled_mantissa, canonic_exponent. +unfold rounding, scaled_mantissa, canonic_exponent. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He (Rgt_not_eq _ _ H0x)). @@ -621,10 +656,10 @@ Qed. Theorem generic_DN_pt_neg : forall x, (x < 0)%R -> - Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (scaled_mantissa x)) (canonic_exponent x))). + Rnd_DN_pt generic_format x (rounding ZrndDN x). Proof. intros x Hx0. -unfold scaled_mantissa, canonic_exponent. +unfold rounding, scaled_mantissa, canonic_exponent. destruct (ln_beta beta x) as (ex, He). simpl. specialize (He (Rlt_not_eq _ _ Hx0)). @@ -815,11 +850,12 @@ Qed. Theorem generic_DN_pt : forall x, - Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (x * bpow (- canonic_exponent x))) (canonic_exponent x))). + Rnd_DN_pt generic_format x (rounding ZrndDN x). Proof. intros x. destruct (total_order_T 0 x) as [[Hx|Hx]|Hx]. now apply generic_DN_pt_pos. +unfold rounding, scaled_mantissa. rewrite <- Hx, Rmult_0_l. fold (Z2R 0). rewrite Zfloor_Z2R, F2R_0. @@ -828,57 +864,93 @@ apply generic_format_0. now apply generic_DN_pt_neg. Qed. +Theorem generic_DN_opp : + forall x, + rounding ZrndDN (-x) = (- rounding ZrndUP x)%R. +Proof. +intros x. +unfold rounding. +rewrite scaled_mantissa_opp. +rewrite opp_F2R. +unfold Zrnd. simpl. +unfold Zceil. +rewrite Zopp_involutive. +now rewrite canonic_exponent_opp. +Qed. + +Theorem generic_UP_opp : + forall x, + rounding ZrndUP (-x) = (- rounding ZrndDN x)%R. +Proof. +intros x. +unfold rounding. +rewrite scaled_mantissa_opp. +rewrite opp_F2R. +unfold Zrnd. simpl. +unfold Zceil. +rewrite Ropp_involutive. +now rewrite canonic_exponent_opp. +Qed. + Theorem generic_UP_pt : forall x, - Rnd_UP_pt generic_format x (F2R (Float beta (Zceil (x * bpow (- canonic_exponent x))) (canonic_exponent x))). + Rnd_UP_pt generic_format x (rounding ZrndUP x). Proof. intros x. apply Rnd_DN_UP_pt_sym. apply generic_format_satisfies_any. -unfold Zceil. -rewrite <- Ropp_mult_distr_l_reverse. -rewrite opp_F2R, Zopp_involutive. -rewrite <- canonic_exponent_opp. +pattern x at 2 ; rewrite <- Ropp_involutive. +rewrite generic_UP_opp. +rewrite Ropp_involutive. apply generic_DN_pt. Qed. -Theorem generic_DN_pt_small_pos : +Theorem generic_format_rounding : + forall rnd x, + generic_format (rounding rnd x). +Proof. +intros rnd x. +destruct (rounding_DN_or_UP rnd x) as [H|H] ; rewrite H. +apply (generic_DN_pt x). +apply (generic_UP_pt x). +Qed. + +Theorem generic_DN_small_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> (ex <= fexp ex)%Z -> - Rnd_DN_pt generic_format x R0. + rounding ZrndDN x = R0. Proof. intros x ex Hx He. rewrite <- (F2R_0 beta (canonic_exponent x)). rewrite <- mantissa_DN_small_pos with (1 := Hx) (2 := He). -rewrite <- canonic_exponent_fexp_pos with (1 := Hx). -apply generic_DN_pt. +now rewrite <- canonic_exponent_fexp_pos with (1 := Hx). Qed. -Theorem generic_UP_pt_small_pos : +Theorem generic_UP_small_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> (ex <= fexp ex)%Z -> - Rnd_UP_pt generic_format x (bpow (fexp ex)). + rounding ZrndUP x = (bpow (fexp ex)). Proof. intros x ex Hx He. rewrite <- F2R_bpow. rewrite <- mantissa_UP_small_pos with (1 := Hx) (2 := He). -rewrite <- canonic_exponent_fexp_pos with (1 := Hx). -apply generic_UP_pt. +now rewrite <- canonic_exponent_fexp_pos with (1 := Hx). Qed. -Theorem generic_UP_pt_large_pos_le_pow : - forall x xu ex, +Theorem generic_UP_large_pos_le_pow : + forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> (fexp ex < ex)%Z -> - Rnd_UP_pt generic_format x xu -> - (xu <= bpow ex)%R. + (rounding ZrndUP x <= bpow ex)%R. Proof. -intros x xu ex Hx He (_, (_, Hu4)). -apply Hu4 with (2 := Rlt_le _ _ (proj2 Hx)). +intros x ex Hx He. +apply (generic_UP_pt x). apply generic_format_bpow. exact (proj1 (prop_exp _) He). +apply Rlt_le. +apply Hx. Qed. Theorem generic_format_EM : @@ -900,18 +972,17 @@ rewrite <- Hxd. apply Hd. Qed. -Theorem generic_DN_pt_large_pos_ge_pow : - forall x d e, - (0 < d)%R -> - Rnd_DN_pt generic_format x d -> +Theorem generic_DN_large_pos_ge_pow : + forall x e, + (0 < rounding ZrndDN x)%R -> (bpow e <= x)%R -> - (bpow e <= d)%R. + (bpow e <= rounding ZrndDN x)%R. Proof. -intros x d e Hd Hxd Hex. +intros x e Hd Hex. destruct (ln_beta beta x) as (ex, He). assert (Hx: (0 < x)%R). apply Rlt_le_trans with (1 := Hd). -apply Hxd. +apply (generic_DN_pt x). specialize (He (Rgt_not_eq _ _ Hx)). rewrite Rabs_pos_eq in He. 2: now apply Rlt_le. apply Rle_trans with (bpow (ex - 1)). @@ -919,38 +990,52 @@ apply -> bpow_le. cut (e < ex)%Z. omega. apply <- bpow_lt. now apply Rle_lt_trans with (2 := proj2 He). -apply Hxd with (2 := proj1 He). +apply (generic_DN_pt x) with (2 := proj1 He). apply generic_format_bpow. destruct (Zle_or_lt ex (fexp ex)). elim Rgt_not_eq with (1 := Hd). -apply Rnd_DN_pt_unicity with (1 := Hxd). -now apply generic_DN_pt_small_pos with (1 := He). +now apply generic_DN_small_pos with (1 := He). ring_simplify (ex - 1 + 1)%Z. omega. Qed. -Theorem canonic_exponent_DN_pt : - forall x d : R, - (0 < d)%R -> - Rnd_DN_pt generic_format x d -> - canonic_exponent d = canonic_exponent x. +Theorem canonic_exponent_DN : + forall x, + (0 < rounding ZrndDN x)%R -> + canonic_exponent (rounding ZrndDN x) = canonic_exponent x. Proof. -intros x d Hd Hxd. +intros x Hd. unfold canonic_exponent. apply f_equal. apply ln_beta_unique. -rewrite (Rabs_pos_eq d). 2: now apply Rlt_le. +rewrite (Rabs_pos_eq (rounding ZrndDN x)). 2: now apply Rlt_le. destruct (ln_beta beta x) as (ex, He). simpl. assert (Hx: (0 < x)%R). apply Rlt_le_trans with (1 := Hd). -apply Hxd. +apply (generic_DN_pt x). specialize (He (Rgt_not_eq _ _ Hx)). rewrite Rabs_pos_eq in He. 2: now apply Rlt_le. split. -now apply generic_DN_pt_large_pos_ge_pow with (2 := Hxd). +apply generic_DN_large_pos_ge_pow with (1 := Hd). +apply He. apply Rle_lt_trans with (2 := proj2 He). -apply Hxd. +apply (generic_DN_pt x). +Qed. + +Theorem generic_N_pt_DN_or_UP : + forall x f, + Rnd_N_pt generic_format x f -> + f = rounding ZrndDN x \/ f = rounding ZrndUP x. +Proof. +intros x f Hxf. +destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf). +left. +apply Rnd_DN_pt_unicity with (1 := H). +apply generic_DN_pt. +right. +apply Rnd_UP_pt_unicity with (1 := H). +apply generic_UP_pt. Qed. End RND_generic. diff --git a/src/Core/Fcore_rnd_ne.v b/src/Core/Fcore_rnd_ne.v index 6e1c28cfc318fa5cd365c54ffbf46ff4ad499bb4..a592038736bd999fb1d506aace0ebbecb959dc51 100644 --- a/src/Core/Fcore_rnd_ne.v +++ b/src/Core/Fcore_rnd_ne.v @@ -30,8 +30,8 @@ Definition DN_UP_parity_pos_prop := ~ format x -> canonic xd -> canonic xu -> - Rnd_DN_pt format x (F2R xd) -> - Rnd_UP_pt format x (F2R xu) -> + F2R xd = rounding beta fexp ZrndDN x -> + F2R xu = rounding beta fexp ZrndUP x -> Zodd (Fnum xd + Fnum xu). Definition DN_UP_parity_prop := @@ -39,8 +39,8 @@ Definition DN_UP_parity_prop := ~ format x -> canonic xd -> canonic xu -> - Rnd_DN_pt format x (F2R xd) -> - Rnd_UP_pt format x (F2R xu) -> + F2R xd = rounding beta fexp ZrndDN x -> + F2R xu = rounding beta fexp ZrndUP x -> Zodd (Fnum xd + Fnum xu). Theorem DN_UP_parity_aux : @@ -73,18 +73,12 @@ rewrite <- Ropp_involutive. now apply generic_format_opp. now apply canonic_opp. now apply canonic_opp. -apply Rnd_UP_DN_pt_sym. -apply generic_format_opp. -rewrite <- opp_F2R. -now rewrite 2!Ropp_involutive. -apply Rnd_DN_UP_pt_sym. -apply generic_format_opp. -rewrite <- opp_F2R. -now rewrite 2!Ropp_involutive. +rewrite generic_DN_opp, <- opp_F2R. +now apply f_equal. +rewrite generic_UP_opp, <- opp_F2R. +now apply f_equal. Qed. -Hypothesis valid_fexp : valid_exp fexp. - Definition NE_ex_prop := Zodd (radix_val beta) \/ forall e, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e). @@ -103,67 +97,63 @@ destruct (Zle_or_lt ex (fexp ex)) as [Hxe|Hxe]. assert (Hd3 : Fnum xd = Z0). apply F2R_eq_0_reg with beta (Fexp xd). change (F2R xd = R0). -apply Rnd_DN_pt_unicity with (1 := Hxd). -now apply generic_DN_pt_small_pos with (2 := Hex). +rewrite Hxd. +apply generic_DN_small_pos with (1 := Hex) (2 := Hxe). assert (Hu3 : xu = Float beta (1 * Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))). apply canonic_unicity with (1 := Hu). apply (f_equal fexp). rewrite <- F2R_change_exp. now rewrite F2R_bpow, ln_beta_bpow. -now eapply valid_fexp. +now eapply prop_exp. rewrite <- F2R_change_exp. rewrite F2R_bpow. apply sym_eq. -apply Rnd_UP_pt_unicity with (2 := Hxu). -now apply generic_UP_pt_small_pos. -now eapply valid_fexp. +rewrite Hxu. +apply sym_eq. +apply generic_UP_small_pos with (1 := Hex) (2 := Hxe). +now eapply prop_exp. rewrite Hd3, Hu3. rewrite Zmult_1_l. simpl. destruct strong_fexp as [H|H]. apply Zodd_Zpower with (2 := H). apply Zle_minus_le_0. -now eapply valid_fexp. +now eapply prop_exp. rewrite (proj2 (H ex)). now rewrite Zminus_diag. exact Hxe. (* large x *) assert (Hd4: (bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R). rewrite Rabs_pos_eq. +rewrite Hxd. split. -apply Hxd. +apply (generic_DN_pt beta fexp prop_exp x). apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. omega. apply Hex. apply Rle_lt_trans with (2 := proj2 Hex). -apply Hxd. -apply Hxd. +apply (generic_DN_pt beta fexp prop_exp x). +rewrite Hxd. +apply (generic_DN_pt beta fexp prop_exp x). apply generic_format_0. now apply Rlt_le. -assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now eapply valid_fexp. +assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now eapply prop_exp. assert (Hud: (F2R xu = F2R xd + ulp beta fexp x)%R). -apply Rnd_UP_pt_unicity with (1 := Hxu). -now apply ulp_DN_UP_pt. +rewrite Hxu, Hxd. +now apply ulp_DN_UP. destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2]. (* - xu > bpow ex *) elim (Rlt_not_le _ _ Hu2). -apply Rnd_UP_pt_monotone with (generic_format beta fexp) x (bpow ex). -exact Hxu. -split. -apply generic_format_bpow. -exact Hxe2. -split. -apply Rle_refl. -easy. -now apply Rlt_le. +rewrite Hxu. +now apply generic_UP_large_pos_le_pow. (* - xu = bpow ex *) assert (Hu3: xu = Float beta (1 * Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))). apply canonic_unicity with (1 := Hu). apply (f_equal fexp). rewrite <- F2R_change_exp. now rewrite F2R_bpow, ln_beta_bpow. -now eapply valid_fexp. +now eapply prop_exp. rewrite <- Hu2. apply sym_eq. rewrite <- F2R_change_exp. @@ -235,11 +225,13 @@ apply bpow_gt_0. rewrite Rabs_pos_eq. split. apply Rle_trans with (1 := proj1 Hex). -apply Hxu. +rewrite Hxu. +apply (generic_UP_pt beta fexp prop_exp x). exact Hu2. apply Rlt_le. apply Rlt_le_trans with (1 := H0x). -apply Hxu. +rewrite Hxu. +apply (generic_UP_pt beta fexp prop_exp x). Qed. Theorem DN_UP_parity_generic : @@ -285,8 +277,12 @@ unfold Fcore_generic_fmt.canonic. now rewrite <- Hd1. unfold Fcore_generic_fmt.canonic. now rewrite <- Hu1. -now rewrite <- Hd1. -now rewrite <- Hu1. +rewrite <- Hd1. +apply Rnd_DN_pt_unicity with (1 := Hd). +now apply generic_DN_pt. +rewrite <- Hu1. +apply Rnd_UP_pt_unicity with (1 := Hu). +now apply generic_UP_pt. now apply Zodd_mult_Zodd. Qed. @@ -309,8 +305,12 @@ intros Hf. apply Hx. apply sym_eq. now apply Rnd_DN_pt_idempotent with (1 := Hd). -now rewrite <- Hd1. -now rewrite <- Hu1. +rewrite <- Hd1. +apply Rnd_DN_pt_unicity with (1 := Hd). +now apply generic_DN_pt. +rewrite <- Hu1. +apply Rnd_UP_pt_unicity with (1 := Hu). +now apply generic_UP_pt. Qed. Theorem Rnd_NE_pt_rounding : diff --git a/src/Core/Fcore_ulp.v b/src/Core/Fcore_ulp.v index a18166d74b5e571604652848f6457b0f7dd36b5e..f4b3a4fb5e54ef80607a2ec10f37f125992f7ad6 100644 --- a/src/Core/Fcore_ulp.v +++ b/src/Core/Fcore_ulp.v @@ -18,21 +18,12 @@ Definition ulp x := bpow (canonic_exponent beta fexp x). Definition F := generic_format beta fexp. -Theorem ulp_DN_UP_pt : - forall x xd, - ~ F x -> - Rnd_DN_pt F x xd -> - Rnd_UP_pt F x (xd + ulp x)%R. +Theorem ulp_DN_UP : + forall x, ~ F x -> + rounding beta fexp ZrndUP x = (rounding beta fexp ZrndDN x + ulp x)%R. Proof. -intros x xd Fx Hd1. -set (ex := canonic_exponent beta fexp x). -assert (Hd2 := generic_DN_pt beta _ prop_exp x). -generalize (generic_UP_pt beta _ prop_exp x). -fold ex in Hd2 |- *. -replace (F2R (Float beta (Zceil (x * bpow (- ex))) ex)) with (xd + ulp x)%R. -easy. -rewrite (Rnd_DN_pt_unicity _ _ _ _ Hd1 Hd2). -unfold ulp. fold ex. +intros x Fx. +unfold rounding, Zrnd, ulp. simpl. unfold F2R. simpl. rewrite Zceil_floor_neq. rewrite plus_Z2R. simpl. @@ -41,62 +32,54 @@ intros H. apply Fx. unfold F, generic_format. unfold F2R. simpl. -unfold scaled_mantissa. -fold ex. rewrite <- H. rewrite Ztrunc_Z2R. rewrite H. -now rewrite Rmult_assoc, <- bpow_add, Zplus_opp_l, Rmult_1_r. +now rewrite scaled_mantissa_bpow. Qed. Theorem ulp_error : - forall rnd : R -> R, - Rounding_for_Format F rnd -> - forall x, - (Rabs (rnd x - x) < ulp x)%R. + forall Zrnd x, + (Rabs (rounding beta fexp Zrnd x - x) < ulp x)%R. Proof. -intros rnd Hrnd x. -assert (Hs := generic_format_satisfies_any beta _ prop_exp). -destruct (proj1 (satisfies_any_imp_DN F Hs) x) as (d, Hd). -destruct (Rle_lt_or_eq_dec d x) as [Hxd|Hxd]. +intros Zrnd x. +destruct (generic_format_EM beta fexp prop_exp x) as [Hx|Hx]. +(* x = rnd x *) +rewrite rounding_generic with (1 := Hx). +unfold Rminus. +rewrite Rplus_opp_r, Rabs_R0. +apply bpow_gt_0. (* x <> rnd x *) -apply Hd. -assert (Fx : ~F x). -intros Fx. -apply Rlt_not_le with (1 := Hxd). -apply Req_le. -apply sym_eq. -now apply Rnd_DN_pt_idempotent with (1 := Hd). -assert (Hu := ulp_DN_UP_pt _ _ Fx Hd). -set (u := (d + ulp x)%R). -assert (Hxu : (x < u)%R). -destruct (Rle_lt_or_eq_dec x u) as [Hxu|Hxu]. -apply Hu. -exact Hxu. -elim Fx. -rewrite Hxu. -apply Hu. -destruct (Rnd_DN_or_UP_pt _ _ Hrnd _ _ _ Hd Hu) as [Hr|Hr] ; - rewrite Hr ; clear Hr. -rewrite <- Ropp_minus_distr. -rewrite Rabs_Ropp, Rabs_pos_eq. -apply Rplus_lt_reg_r with d. -now replace (d + (x - d))%R with x by ring. -apply Rle_0_minus. -apply Hd. +destruct (rounding_DN_or_UP beta fexp Zrnd x) as [H|H] ; rewrite H ; clear H. +(* . *) +rewrite Rabs_left1. +rewrite Ropp_minus_distr. +apply Rplus_lt_reg_r with (rounding beta fexp ZrndDN x). +rewrite <- ulp_DN_UP with (1 := Hx). +ring_simplify. +assert (Hu: (x <= rounding beta fexp ZrndUP x)%R). +apply (generic_UP_pt beta fexp prop_exp x). +destruct Hu as [Hu|Hu]. +exact Hu. +elim Hx. +rewrite Hu. +now apply generic_format_rounding. +apply Rle_minus. +apply (generic_DN_pt beta fexp prop_exp x). +(* . *) rewrite Rabs_pos_eq. +rewrite ulp_DN_UP with (1 := Hx). apply Rplus_lt_reg_r with (x - ulp x)%R. -now ring_simplify. +ring_simplify. +assert (Hd: (rounding beta fexp ZrndDN x <= x)%R). +apply (generic_DN_pt beta fexp prop_exp x). +destruct Hd as [Hd|Hd]. +exact Hd. +elim Hx. +rewrite <- Hd. +now apply generic_format_rounding. apply Rle_0_minus. -apply Hu. -(* x = rnd x *) -rewrite Hxd in Hd. -rewrite (proj2 (proj2 Hrnd)). -unfold Rminus. -rewrite Rplus_opp_r. -rewrite Rabs_R0. -apply bpow_gt_0. -apply Hd. +apply (generic_UP_pt beta fexp prop_exp x). Qed. Theorem ulp_half_error_pt : @@ -105,63 +88,54 @@ Theorem ulp_half_error_pt : (Rabs (xr - x) <= /2 * ulp x)%R. Proof. intros x xr Hxr. -assert (Hs := generic_format_satisfies_any beta _ prop_exp). -destruct (proj1 (satisfies_any_imp_DN F Hs) x) as (d, Hd). -destruct (Rle_lt_or_eq_dec d x) as [Hxd|Hxd]. -(* x <> rnd x *) -apply Hd. -assert (Fx : ~F x). -intros Fx. -apply Rlt_not_le with (1 := Hxd). -apply Req_le. -apply sym_eq. -now apply Rnd_DN_pt_idempotent with (1 := Hd). -assert (Hu := ulp_DN_UP_pt _ _ Fx Hd). -destruct Hxr as (Hr1, Hr2). -assert (Hdx : (Rabs (d - x) = x - d)%R). -rewrite <- Ropp_minus_distr. -rewrite Rabs_Ropp. -apply Rabs_pos_eq. -apply Rle_0_minus. -apply Hd. -assert (Hux : (Rabs (d + ulp x - x) = d + ulp x - x)%R). -apply Rabs_pos_eq. -apply Rle_0_minus. -apply Hu. -destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H]. -(* . rnd(x) = rndd(x) *) -apply Rle_trans with (1 := Hr2 _ (proj1 Hd)). -rewrite Hdx. -apply Rmult_le_reg_l with 2%R. -now apply (Z2R_lt 0 2). -rewrite Rmult_plus_distr_r. -rewrite Rmult_1_l. -apply Rle_trans with (1 := Rplus_le_compat_l (x - d) _ _ H). -field_simplify. -apply Rle_refl. -(* . rnd(x) = rndu(x) *) -apply Rle_trans with (1 := Hr2 _ (proj1 Hu)). -rewrite Hux. -apply Rmult_le_reg_l with 2%R. -now apply (Z2R_lt 0 2). -rewrite Rmult_plus_distr_r. -rewrite Rmult_1_l. -apply Rlt_le. -apply Rlt_le_trans with (1 := Rplus_lt_compat_l (d + ulp x - x) _ _ H). -field_simplify. -apply Rle_refl. +destruct (generic_format_EM beta fexp prop_exp x) as [Hx|Hx]. (* x = rnd x *) -rewrite Hxd in Hd. rewrite Rnd_N_pt_idempotent with (1 := Hxr). unfold Rminus. -rewrite Rplus_opp_r. -rewrite Rabs_R0. +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. -apply Hd. +exact Hx. +(* x <> rnd x *) +set (d := rounding beta fexp ZrndDN x). +destruct Hxr 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 (generic_DN_pt beta fexp prop_exp 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 (generic_DN_pt beta fexp prop_exp x). +(* . rnd(x) = rndu(x) *) +assert (Hu: (d + ulp x)%R = rounding beta fexp ZrndUP x). +unfold d. +now rewrite <- ulp_DN_UP. +apply Rle_trans with (Rabs (d + ulp x - x)). +apply Hr2. +rewrite Hu. +apply (generic_UP_pt beta fexp prop_exp 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 (generic_UP_pt beta fexp prop_exp x). Qed. Theorem ulp_monotone : @@ -192,14 +166,13 @@ apply bpow_ge_0. Qed. Theorem ulp_DN_pt_eq : - forall x d : R, - (0 < d)%R -> - Rnd_DN_pt F x d -> - ulp d = ulp x. + forall x, + (0 < rounding beta fexp ZrndDN x)%R -> + ulp (rounding beta fexp ZrndDN x) = ulp x. Proof. -intros x d Hd Hxd. +intros x Hd. unfold ulp. -now rewrite canonic_exponent_DN_pt with (3 := Hxd). +now rewrite canonic_exponent_DN with (2 := Hd). Qed. End Fcore_ulp.