proposition: Lemma ErrFMA_correct_simpl: a*x+y = r1+r2+r3.
proof: Proof. Proof with auto with typeclass_instances. case (Req_dec (a*x) 0); intros Zax. unfold r3, r2, gamma, alpha2, beta2, beta1, r1, u1, alpha1, alpha2,u2,u1. rewrite Zax, round_0... unfold Rminus; repeat rewrite Rplus_0_l. rewrite Ropp_0, Rplus_0_r. repeat rewrite (round_generic _ _ _ y)... replace (y+-y) with 0 by ring. rewrite round_0, Rplus_0_l... rewrite round_0, Rplus_0_l... rewrite round_0, Rplus_0_l... ring. case (Req_dec u2 0); intros Zu2. unfold r3, r2, gamma, alpha2, beta2, beta1, r1, u1, alpha1, alpha2. rewrite Zu2, Rplus_0_r. repeat rewrite (round_generic _ _ _ y)... ring_simplify. assert (G:round_flt (a * x) = a*x). apply trans_eq with (u1+u2). now rewrite Zu2, Rplus_0_r. unfold u2, u1; ring. rewrite G. replace (round_flt (a * x + y) - round_flt (a * x + y)) with 0 by ring. rewrite round_0, Rplus_0_l... rewrite (round_generic _ _ _ (a * x + y - round_flt (a * x + y))). ring. replace (a * x + y - round_flt (a * x + y)) with (- (round_flt (a * x + y) -(a*x+y))) by ring. apply generic_format_opp. rewrite <- G. apply plus_error... apply generic_format_round... case (Req_dec y 0); intros Zy. assert (Fu2: format u2). replace (u2) with (-(u1-(a*x))) by (unfold u2; ring). apply generic_format_opp. apply mult_error_FLT... intros L; case U1; intros H; try easy. apply Rle_trans with (2:=H); apply bpow_le. lia. unfold r3, r2, gamma, alpha2, beta2, beta1, r1, alpha1, alpha2. rewrite Zy, Rplus_0_r, Rplus_0_l; fold u1. rewrite (round_generic _ _ _ u2)... replace (u1+u2) with (a*x). 2: unfold u2, u1; ring. fold u1; ring_simplify (u1-u1). rewrite round_0... rewrite Rplus_0_l. fold u2; rewrite (round_generic _ _ _ u2)... ring_simplify (u2+(u2-u2)). rewrite (round_generic _ _ _ u2)... unfold u2,u1; ring. apply ErrFMA_correct; try assumption. case U1; intros H; [now left|right]. apply Rle_trans with (2:=H); apply bpow_le. lia. fold u1 u2 alpha1. now apply V2_Und2. fold u1 u2 alpha1 alpha2. now apply V2_Und4. now apply V2_Und5. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat