proposition: Theorem FmaErr: (a*x+y=r1+ga+al2)%R.
proof: Proof. case Exp1; intros I1. case Exp2; intros I2. case Exp3; intros I3. case Exp4; intros I4. elim errorBoundedPlus with bo radix p u1 al1 be1; auto with zarith. 2: elim u1Def; auto. 2: elim al1Def; auto. fold FtoRradix; intros be2' T; elim T; intros J1 T'; elim T'; intros J2 J3; clear T T'. unfold FtoRradix; apply FmaErr_aux with bo p P u1 u2 al1 be1 be2' gat; auto. elim Nbe1; intros; auto. elim H; intros T1 T2; elim T2; intros T3 T4; contradict T3; auto with zarith. fold FtoRradix; rewrite J1; rewrite <- be2Def; auto. assert (a*x+y=0)%R. apply ClosestZero1 with r1 (Fplus radix (Fmult a x) y); auto. unfold FtoRradix; rewrite Fplus_correct; auto; rewrite Fmult_correct; auto with real zarith. simpl; apply Zmin_Zle; auto with zarith. elim Fy; auto. rewrite H. assert (FtoRradix r1=0)%R. apply ClosestZero2 with (a*x+y)%R; auto; elim r1DefE; auto. assert (FtoRradix u1= (Fopp y))%R. 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 y)) with (a*x)%R; auto. rewrite Fopp_correct; fold FtoRradix; auto with real. apply Rplus_eq_reg_l with y; rewrite Rplus_comm; rewrite H; ring. assert (FtoRradix u2=0)%R. rewrite u2Def; rewrite H1; unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix. rewrite <- H; ring. assert (FtoRradix al1= y)%R. unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix y) with (y+u2)%R; auto with real. rewrite H2; auto with real. assert (FtoRradix al2=0)%R. rewrite al2Def; rewrite H2; rewrite H3; ring. assert (FtoRradix be1=0)%R. apply ClosestZero2 with (u1+al1)%R; auto. rewrite H3; rewrite H1; unfold FtoRradix; rewrite Fopp_correct; ring. assert (FtoRradix be2=0)%R. rewrite be2Def; rewrite H1; rewrite H3; rewrite H5; unfold FtoRradix; rewrite Fopp_correct; ring. assert (FtoRradix gat=0)%R. apply ClosestZero2 with (be1-r1)%R; auto. rewrite H5; rewrite H0; ring. assert (FtoRradix ga=0)%R. apply ClosestZero2 with (gat+be2)%R; auto. rewrite H7; rewrite H6; ring. rewrite H0; rewrite H8; rewrite H4; ring. assert (u1 + al1=0)%R. apply ClosestZero1 with be1 (Fplus radix u1 al1); auto. unfold FtoRradix; rewrite Fplus_correct; auto. simpl; apply Zmin_Zle. elim u1Def; intros T1 T2; elim T1; auto. elim al1Def; intros T1 T2; elim T1; auto. assert (FtoRradix be2=0)%R. rewrite be2Def; rewrite I3; rewrite H; ring. assert (FtoRradix gat= (Fopp r1))%R. 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. assert (T:(Closest bo radix (a*x+y)%R r1)); auto; elim T; auto. replace (FtoR radix (Fopp r1)) with (be1-r1)%R; auto. rewrite I3; rewrite Fopp_correct; fold FtoRradix; auto with real. assert (FtoRradix ga= gat)%R. unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. elim gatDef; auto. replace (FtoR radix gat) with (gat+be2)%R; auto. rewrite H0; auto with real. apply sym_eq; apply trans_eq with (FtoRradix al2). rewrite H2; rewrite H1; unfold FtoRradix; rewrite Fopp_correct; ring. rewrite al2Def; rewrite u2Def. apply trans_eq with (y+a*x-(u1+al1))%R;[idtac|rewrite H]; ring. assert (a*x=0)%R. apply ClosestZero1 with u1 (Fmult a x); auto. unfold FtoRradix; rewrite Fmult_correct; auto. assert (FtoRradix r1=y). unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix y) with (a*x+y)%R;[idtac|rewrite H]; auto with real. assert (FtoRradix u2=0)%R. rewrite u2Def; rewrite I2; rewrite H; ring. assert (FtoRradix al1=y). unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix y) with (y+u2)%R;[idtac|rewrite H1]; auto with real. assert (FtoRradix al2=0)%R. rewrite al2Def; rewrite H1; rewrite H2; ring. assert (FtoRradix be1=y). unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix y) with (u1+al1)%R;[idtac|rewrite I2; rewrite H2]; auto with real. assert (FtoRradix gat=0). apply ClosestZero2 with (be1-r1)%R; auto. rewrite H4; rewrite H0; ring. assert (FtoRradix ga=0). apply ClosestZero2 with (gat+be2)%R; auto. rewrite be2Def;rewrite H5; rewrite I2; rewrite H2; rewrite H4; simpl; ring. rewrite H; rewrite H0; rewrite H6; rewrite H3;simpl; ring. assert (y + u2=0)%R. elim errorBoundedMult with bo radix p (Closest bo radix) a x u1; auto with zarith. fold FtoRradix; intros u2' T; elim T; intros H1 T'; elim T'; intros H2 H3; clear T T'. apply ClosestZero1 with al1 (Fplus radix y u2'); auto. unfold FtoRradix; rewrite Fplus_correct; auto; fold FtoRradix; rewrite H1; rewrite u2Def; ring. simpl; apply Zmin_Zle; auto with zarith; apply Fy. apply ClosestRoundedModeP with p; auto with zarith. assert (FtoRradix be1=u1). unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. elim u1Def; auto. replace (FtoR radix u1) with (u1+al1)%R;[idtac|rewrite I1]; auto with real. assert (FtoRradix r1=u1). unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. elim u1Def; auto. replace (FtoR radix u1) with (a*x+y)%R;[idtac|idtac]; auto with real. fold FtoRradix; apply trans_eq with (u1+(y+u2))%R;[rewrite u2Def| rewrite H]; ring. assert (FtoRradix gat=0)%R. apply ClosestZero2 with (be1-r1)%R; auto; rewrite H0; rewrite H1; auto with real. assert (FtoRradix ga=0)%R. apply ClosestZero2 with (gat+be2)%R; auto. rewrite H2; rewrite be2Def; rewrite I1; rewrite H0; ring. rewrite H1; rewrite H3; rewrite al2Def; rewrite u2Def; rewrite I1; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz