proposition: Lemma err_add_no_err: forall x1 x2, format x1 -> format x2 -> err (round_flt (x1+x2)) (x1+x2) eps.
proof: Proof. Proof with auto with typeclass_instances. intros x1 x2 Fx1 Fx2. case (Rle_or_lt (bpow (emin+prec-1)) (Rabs (x1+x2))); intros Y. replace eps with (/ 2 * Raux.bpow beta (- prec + 1)). apply relative_error_N_FLT... apply f_equal; apply f_equal; ring. replace (round_flt (x1 + x2)) with (x1+x2). apply err_aux with 0. apply err_0. apply epsPos. apply sym_eq, round_generic... apply generic_format_FLT. apply FLT_format_generic in Fx1; apply FLT_format_generic in Fx2... destruct Fx1 as [f Hf1 Hf2 Hf3]. destruct Fx2 as [g Hg1 Hg2 Hg3]. exists (Fplus f g). now rewrite F2R_plus, Hf1, Hg1. apply lt_IZR. rewrite abs_IZR. rewrite IZR_Zpower. 2: auto with zarith. apply Rmult_lt_reg_r with (bpow (Fexp (Fplus f g))). apply bpow_gt_0. apply Rle_lt_trans with (Rabs (F2R (Fplus f g))). right; unfold F2R; rewrite Rabs_mult. apply f_equal. apply sym_eq, Rabs_right. apply Rle_ge, bpow_ge_0. rewrite F2R_plus, <- Hf1, <- Hg1. apply Rlt_le_trans with (1:=Y). rewrite <- bpow_plus. apply bpow_le. assert (emin <= Fexp (Fplus f g))%Z. rewrite Fexp_Fplus. now apply Z.min_case. lia. rewrite Fexp_Fplus. now apply Z.min_case. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)