Replaced some Rnd_DN/UP_pt with explicit formulas for rounded values.

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.

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.