proposition: Theorem ErrFmaApprox_2: (Rabs (z+w-(a*x+b)) <= (3*radix/2+/2)*powerRZ radix (2-2*p)*Rabs z)%R.
proof: Proof. case Nv; intros I5. case Nz; intros I3. case Nph; intros I1. case Nuh; intros I2. case Nw; intros I4. unfold FtoRradix; apply ErrFmaApprox_2_aux with bo ph pl uh ul t v; auto. replace (z + w - (a * x + b))%R with (-(ul+pl-v))%R. apply Rmult_le_reg_l with 2; auto with real zarith; rewrite Rabs_Ropp. apply Rle_trans with (Fulp bo radix p v). unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite Rplus_comm; auto with real. apply Rle_trans with (Rabs v * powerRZ radix (Z.succ (- p)))%R; [unfold FtoRradix; apply FulpLe2; auto with zarith|idtac]. elim vDef; auto. rewrite FcanonicFnormalizeEq; auto with zarith; left; auto. assert (Rabs v <= powerRZ radix (Fexp z) * radix)%R. unfold FtoRradix; apply vLe with bo p a x b ph pl uh ul; auto. apply Rle_trans with ((powerRZ radix (Fexp z) * radix)* powerRZ radix (Z.succ (- p)))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with ((Rabs z * powerRZ radix (Z.succ (- p)))* radix * powerRZ radix (Z.succ (- p)))%R. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rmult_le_compat_r; auto with real zarith. apply IZR_le; lia. apply Rle_trans with (Fulp bo radix p z). unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto. unfold FtoRradix; apply FulpLe2; auto with zarith. elim zDef; auto. rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto. apply Rle_trans with (radix*powerRZ radix (2 - 2 * p) * Rabs z)%R. replace (2-2*p)%Z with (1+1-p-p)%Z;[idtac|ring]. unfold Z.succ, Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl. ring_simplify (radix*1)%R; right; ring. rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real. apply Rabs_pos. rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (3*radix+1)%R;[idtac|right; simpl; field; auto with real]. apply Rle_trans with (1*radix+0)%R;[right; ring|apply Rplus_le_compat; auto with real zarith]. apply Rmult_le_compat_r; try apply IZR_le; lia. rewrite ulDef; rewrite plDef. assert (t+v=0)%R. apply ClosestZero1 with bo radix p w (Fplus radix t v); auto with zarith. rewrite Fplus_correct; fold FtoRradix; auto. simpl; apply Zmin_Zle; auto with zarith. elim tDef; intros Y1 Y2; elim Y1; auto. elim vDef; intros Y1 Y2; elim Y1; auto. cut (uh-z=t)%R;[intros H'|idtac]. rewrite I4; simpl; rewrite <- H; rewrite <- H'; ring. 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 <- H1; unfold FtoRradix. apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; rewrite H1; auto. assert (ph+b=0)%R. apply ClosestZero1 with bo radix p uh (Fplus radix ph b); auto with zarith. rewrite Fplus_correct; fold FtoRradix; auto. simpl; apply Zmin_Zle; auto with zarith. elim phDef; intros Y1 Y2; elim Y1; auto. apply Fb. absurd (FtoRradix ul=0)%R; auto. rewrite ulDef; rewrite I2; rewrite H; simpl; ring. absurd (FtoRradix ul=0)%R; auto. rewrite ulDef; rewrite I1. cut (FtoRradix b=uh)%R; [intros Y; rewrite Y; simpl; ring|idtac]. unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix b) with (ph+b)%R; auto; rewrite I1; auto with real. assert (FtoRradix uh=0)%R. unfold FtoRradix; apply ClosestZero2 with bo p (ph+b)%R; auto with real zarith. cut (FtoRradix ph= (Fopp b)); [intros I;rewrite I; unfold FtoRradix; rewrite Fopp_correct; ring|idtac]. unfold FtoRradix; apply sym_eq. 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. rewrite Fopp_correct; fold FtoRradix; assert (a*x+b=0)%R; auto with real. 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. simpl; apply Zmin_Zle; auto with zarith. apply Fb. apply Rplus_eq_reg_l with (FtoRradix b); rewrite Rplus_comm; rewrite H;ring. assert (ph+b=0)%R. apply ClosestZero1 with bo radix p uh (Fplus radix ph b); auto with zarith. rewrite Fplus_correct; fold FtoRradix; auto. simpl; apply Zmin_Zle; auto with zarith. elim phDef; intros Y1 Y2; elim Y1; auto. apply Fb. absurd (FtoRradix ul=0)%R; auto. rewrite ulDef; rewrite H0; rewrite H; ring. 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]. assert (pl+ul=0)%R. elim errorBoundedPlus with bo radix p ph b uh; auto with zarith. 2: elim phDef; auto. fold FtoRradix; intros pl' T; elim T; intros Y1 T'; elim T'; intros Y2 Y3; clear T T'. elim errorBoundedMult with bo radix p (Closest bo radix) a x ph; auto with zarith. 2: apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; intros ul' T; elim T; intros Y1' T'; elim T'; intros Y2' Y3'; clear T T'. apply ClosestZero1 with bo radix p v (Fplus radix pl' ul'); auto with zarith. rewrite Fplus_correct; fold FtoRradix; auto. rewrite ulDef; rewrite plDef; rewrite Y1; rewrite Y1'; ring. simpl; apply Zmin_Zle; auto with zarith. apply Y2. rewrite H. replace (FtoRradix w) with (FtoRradix t). replace (FtoRradix t) with (uh-z)%R; [ring|idtac]. 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 <- H1; unfold FtoRradix. apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; rewrite H1; auto. unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. elim tDef; auto. replace (FtoR radix t) with (t+v)%R; auto; rewrite I5; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz