Proved Fplus_same_exp and Fminus_same_exp.

src/Calc/Fcalc_ops.v

@@ -102,6 +102,16 @@ rewrite Z2R_plus.
 apply Rmult_plus_distr_r.
 Qed.
 
+Theorem Fplus_same_exp :
+  forall m1 m2 e,
+  Fplus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 + m2) e.
+Proof.
+intros m1 m2 e.
+unfold Fplus.
+simpl.
+now rewrite Zle_bool_refl, Zminus_diag, Zmult_1_r.
+Qed.
+
 Theorem Fexp_Fplus :
   forall f1 f2 : float beta,
   Fexp (Fplus f1 f2) = Zmin (Fexp f1) (Fexp f2).
@@ -124,6 +134,15 @@ rewrite plus_F2R, Fopp_F2R.
 ring.
 Qed.
 
+Theorem Fminus_same_exp :
+  forall m1 m2 e,
+  Fminus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 - m2) e.
+Proof.
+intros m1 m2 e.
+unfold Fminus.
+apply Fplus_same_exp.
+Qed.
+
 Definition Fmult (f1 f2 : float beta) :=
   let '(Float m1 e1) := f1 in
   let '(Float m2 e2) := f2 in

src/Prop/Fprop_plus_error.v

@@ -102,15 +102,9 @@ now rewrite Zle_imp_le_bool with (1 := He).
 rewrite Hxy.
 destruct (round_repr_same_exp (Znearest choice) (mx + my * beta ^ (ey - ex)) ex) as (mxy, Hxy').
 rewrite Hxy'.
-assert (H: (F2R (Float beta mxy ex) -
-   F2R (Float beta (mx + my * beta ^ (ey - ex)) ex))%R = F2R
-     (Float beta
-        (- (mx + my * beta ^ (ey - ex)) +
-         mxy * beta ^ (ex - ex)) ex)).
-unfold Rminus.
-rewrite opp_F2R, Rplus_comm, <- plus_F2R.
-unfold Fplus. simpl.
-now rewrite Zle_bool_refl.
+assert (H: (F2R (Float beta mxy ex) - F2R (Float beta (mx + my * beta ^ (ey - ex)) ex))%R =
+  F2R (Float beta (mxy - (mx + my * beta ^ (ey - ex))) ex)).
+now rewrite <- minus_F2R, Fminus_same_exp.
 rewrite H.
 apply generic_format_canonic_exponent.
 apply monotone_exp.
@@ -170,12 +164,10 @@ specialize (Hexy H0).
 destruct (Zle_or_lt exy (fexp exy)) as [He'|He'].
 (* . *)
 assert (H: (x + y)%R = F2R (Float beta (Ztrunc (x * bpow (- fexp exy)) +
-  Ztrunc (y * bpow (- fexp exy)) * Zpower beta (fexp exy - fexp exy)) (fexp exy))).
+  Ztrunc (y * bpow (- fexp exy))) (fexp exy))).
 rewrite (subnormal_exponent beta fexp exy x He' Hx) at 1.
 rewrite (subnormal_exponent beta fexp exy y He' Hy) at 1.
-rewrite <- plus_F2R.
-unfold Fplus. simpl.
-now rewrite Zle_bool_refl.
+now rewrite <- plus_F2R, Fplus_same_exp.
 rewrite H in Hxy.
 rewrite round_generic in Hxy...
 now rewrite <- H in Hxy.