proposition: Theorem ErrFmaApprox_1: (Rabs (z+w-(a*x+b)) <= (3*radix/2+/2)*powerRZ radix (2-2*p)*Rabs z)%R.
proof: Proof. case Nz; intros I1. case Nw; intros I2. apply ErrFmaApprox_1_aux; auto. replace (z+w-(a*x+b))%R with 0%R. rewrite Rabs_R0; apply Rle_trans with (0*Rabs z)%R; [right; ring|apply Rmult_le_compat_r; auto with real]. apply Rabs_pos. apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith. apply Rle_lt_trans with (0+0)%R; auto with real; apply Rplus_lt_compat; auto with real. unfold Rdiv;repeat apply Rmult_lt_0_compat; auto with real zarith. apply IZR_lt; lia. apply powerRZ_lt, IZR_lt; lia. apply sym_eq; apply trans_eq with (z+w-uh-(pl+ul))%R;[rewrite plDef; rewrite ulDef; ring|idtac]. rewrite I2; rewrite Case1; simpl. ring_simplify. assert (FtoRradix t=uh-z)%R. elim tBounded with bo radix p a x b ph pl uh z; auto with zarith. fold FtoRradix; intros t' T; elim T; intros; clear T. rewrite <- H0; unfold FtoRradix; apply sym_eq. apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; rewrite H0; auto. cut (FtoRradix pl=-t)%R;[intros K; rewrite K; rewrite H; ring|idtac]. apply trans_eq with (FtoRradix v). unfold FtoRradix;apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix pl) with (pl+ul)%R; auto; rewrite Case1; auto with real. assert (t+v=0)%R; auto with real. apply ClosestZero1 with bo radix p w (Fplus radix t v); auto with zarith. rewrite Fplus_correct; fold FtoRradix; auto with real. simpl; apply Zmin_Zle. elim tDef; intros J1 J2; elim J1; auto. elim vDef; intros J1 J2; elim J1; auto. apply Rplus_eq_reg_l with t; rewrite H0; auto with real. replace (z+w-(a*x+b))%R with 0%R. rewrite Rabs_R0; apply Rle_trans with (0*Rabs z)%R; [right; ring|apply Rmult_le_compat_r; auto with real]. apply Rabs_pos. apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith. apply Rle_lt_trans with (0+0)%R; auto with real; apply Rplus_lt_compat; auto with real. unfold Rdiv;repeat apply Rmult_lt_0_compat; auto with real zarith. apply IZR_lt; lia. apply powerRZ_lt, IZR_lt; lia. assert (a*x+b=0)%R. apply ClosestZero1 with bo radix p z (Fplus radix (Fmult a x) b); auto with zarith. rewrite Fplus_correct; auto; rewrite Fmult_correct; fold FtoRradix; auto with real. simpl; apply Zmin_Zle; auto with zarith; apply Fb. rewrite I1; rewrite H; simpl; ring_simplify. apply sym_eq; unfold FtoRradix; apply ClosestZero2 with bo p (t+v)%R; auto. cut (FtoRradix uh=0);[intros M1|idtac]. replace (FtoRradix t) with 0%R. replace (FtoRradix v) with 0%R;[ring|idtac]. apply sym_eq; unfold FtoRradix; apply ClosestZero2 with bo p (pl+ul)%R; auto. rewrite plDef; rewrite ulDef. apply trans_eq with ((a*x+b)-uh)%R;[ring|rewrite H; rewrite M1; simpl; ring]. apply sym_eq; unfold FtoRradix; apply ClosestZero2 with bo p (uh-z)%R; auto. rewrite M1; rewrite I1; ring. unfold FtoRradix; apply ClosestZero2 with bo p (ph+b)%R; auto. replace (FtoRradix ph) with (FtoRradix (Fopp b));[unfold FtoRradix; rewrite Fopp_correct; ring|idtac]. unfold FtoRradix;apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply oppBounded; auto. replace (FtoR radix (Fopp b)) with (a*x)%R; auto. apply Rplus_eq_reg_l with (FtoRradix b); rewrite Rplus_comm; rewrite H; rewrite Fopp_correct;auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz