proposition: Theorem generic_format_plus : forall x y, format x -> format y -> (Rabs (x + y) <= bpow (Z.min (mag beta x) (mag beta y)))%R -> format (x + y)%R.
proof: Proof. intros x y Fx Fy Hxy. destruct (Req_dec (x + y) 0) as [Zxy|Zxy]. rewrite Zxy. apply generic_format_0. destruct (Req_dec x R0) as [Zx|Zx]. now rewrite Zx, Rplus_0_l. destruct (Req_dec y R0) as [Zy|Zy]. now rewrite Zy, Rplus_0_r. destruct Hxy as [Hxy|Hxy]. revert Hxy. destruct (mag beta x) as (ex, Ex). simpl. specialize (Ex Zx). destruct (mag beta y) as (ey, Ey). simpl. specialize (Ey Zy). intros Hxy. set (fx := Float beta (Ztrunc (scaled_mantissa beta fexp x)) (fexp ex)). assert (Hx: x = F2R fx). rewrite Fx at 1. unfold cexp. now rewrite mag_unique with (1 := Ex). set (fy := Float beta (Ztrunc (scaled_mantissa beta fexp y)) (fexp ey)). assert (Hy: y = F2R fy). rewrite Fy at 1. unfold cexp. now rewrite mag_unique with (1 := Ey). rewrite Hx, Hy. rewrite <- F2R_plus. apply generic_format_F2R. intros _. case_eq (Fplus fx fy). intros mxy exy Pxy; simpl. rewrite <- Pxy, F2R_plus, <- Hx, <- Hy. unfold cexp. replace exy with (fexp (Z.min ex ey)). apply monotone_exp. now apply mag_le_bpow. replace exy with (Fexp (Fplus fx fy)) by exact (f_equal Fexp Pxy). rewrite Fexp_Fplus. simpl. clear -monotone_exp. apply sym_eq. destruct (Zmin_spec ex ey) as [(H1,H2)|(H1,H2)] ; rewrite H2. apply Z.min_l. now apply monotone_exp. apply Z.min_r. apply monotone_exp. apply Zlt_le_weak. now apply Z.gt_lt. apply generic_format_abs_inv. rewrite Hxy. apply generic_format_bpow. apply valid_exp. case (Zmin_spec (mag beta x) (mag beta y)); intros (H1,H2); rewrite H2; now apply mag_generic_gt. Qed.
imports: Coq(ZArith Reals) Zaux Raux Defs Generic_fmt Operations