proposition: Theorem discri16: (FtoRradix d=0)%R \/ (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. assert (Fq:(Fbounded bo q)). elim Roundq; intros A1 A2; elim A1; auto with zarith. assert (Fp:(Fbounded bo p)). elim Roundp; intros A1 A2; elim A1; auto with zarith. assert (Fd:(Fbounded bo d)). case (Rle_or_lt v u); intros. elim FRoundd; auto; intros L; elim L; intros A1 A2; elim A1; auto with zarith. elim SRoundd; auto; intros L; elim L; intros A1 A2; elim A1; auto with zarith. generalize cases; intros C. case C; clear C; intros C. assert (FtoRradix p=0)%R; auto with real. assert (0 <= p)%R. unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (b*b)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto with zarith. rewrite C; right; ring. assert (p <= 0)%R; auto with real. unfold FtoRradix; apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (b*b)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto with zarith. rewrite C; right; ring. assert (FtoRradix d=(Fopp q))%R. apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo precision (EvenClosest bo radix precision); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. apply oppBounded; auto. replace (FtoR radix (Fopp q)) with (p-q)%R; [apply FRoundd| rewrite Fopp_correct; fold FtoRradix; rewrite H; ring]. unfold FtoRradix; apply EvenClosestMonotone2 with bo precision (p+q)%R (3*Rabs t)%R; auto. replace (FtoRradix t) with (FtoRradix (Fopp q)). unfold FtoRradix; rewrite Fopp_correct;auto; fold FtoRradix. rewrite H; ring_simplify (0+q)%R. rewrite Rabs_Ropp; apply Rle_trans with (1:=(RRle_abs q)). apply Rle_trans with (1*(Rabs q))%R; auto with real. apply Rmult_le_compat_r; auto with real; apply Rabs_pos. unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo precision (EvenClosest bo radix precision); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. apply oppBounded; auto. replace (FtoR radix (Fopp q)) with (p-q)%R; [auto| rewrite Fopp_correct; fold FtoRradix; rewrite H; ring]. right; unfold delta; rewrite H0. unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix. replace (-q-(b*b-a*c))%R with ((a*c-q))%R;[idtac|rewrite C; ring]. apply Rle_trans with (/2*(Fulp bo radix precision q))%R. apply Rmult_le_reg_l with (2)%R; auto with real zarith. apply Rle_trans with (Fulp bo radix precision q);[idtac|simpl; right; field; auto with real]. unfold FtoRradix; apply ClosestUlp; auto. elim Roundq; auto. apply Rle_trans with (2 * Fulp bo radix precision q)%R; [apply Rmult_le_compat_r; auto with real|idtac]. unfold Fulp; auto with real zarith. apply powerRZ_le; try apply IZR_lt; auto with zarith. lra. apply Rmult_le_compat_l; auto with real; right. apply trans_eq with (Fulp bo radix precision (Fopp q)). unfold Fulp; rewrite Fnormalize_Fopp; auto with real zarith. apply FulpComp; auto with zarith. apply oppBounded; auto. case C; clear C; intros C. assert (FtoRradix q=0)%R; auto with real. assert (0 <= q)%R. unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (a*c)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto with zarith. assert (q <= 0)%R; auto with real. unfold FtoRradix; apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (a*c)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto with zarith. assert (FtoRradix d=p)%R. apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo precision (EvenClosest bo radix precision); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. replace (FtoR radix p) with (p-q)%R; [apply FRoundd| fold FtoRradix; rewrite H; ring]. unfold FtoRradix; apply EvenClosestMonotone2 with bo precision (p+q)%R (3*Rabs t)%R; auto. replace (FtoRradix t) with (FtoRradix p). rewrite H; ring_simplify (p+0)%R; apply Rle_trans with (1:=(RRle_abs p)). apply Rle_trans with (1*(Rabs p))%R; auto with real. apply Rmult_le_compat_r; auto with real; apply Rabs_pos. unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo precision (EvenClosest bo radix precision); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. replace (FtoR radix p) with (p-q)%R; [auto| fold FtoRradix; rewrite H; ring]. right; unfold delta; rewrite H0. replace (p-(b*b-a*c))%R with ((-(b*b-p)))%R;[idtac|rewrite C; ring]. apply Rle_trans with (/2*(Fulp bo radix precision p))%R. apply Rmult_le_reg_l with (2)%R; auto with real zarith. apply Rle_trans with (Fulp bo radix precision p);[idtac|simpl; right; field; auto with real]. rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto. elim Roundp; auto. rewrite FulpComp with bo radix precision d p; auto with zarith. apply Rmult_le_compat_r; auto with real. unfold Fulp; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. lra. case (Req_dec v 0)%R. clear C; intros C. assert (v <= u)%R. rewrite C; unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (3*Rabs t)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto with zarith. apply Rle_trans with (0*0)%R; auto with real; apply Rmult_le_compat; auto with real. apply Rabs_pos. assert (FtoRradix q=-p)%R. assert (FtoRradix v=p+q)%R. unfold FtoRradix; apply plusExactR0 with bo precision; auto with real. elim Roundv; auto. apply Rplus_eq_reg_l with p. rewrite <- H0; rewrite C; ring. assert (FtoRradix d=2*p)%R. assert (exists f:float, Fbounded bo f /\ (FtoRradix f=2*p)%R). exists (Float (Fnum p) (Fexp p+1)); split. elim Fp; intros; split; simpl; auto with zarith. unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; ring. elim H1; intros f T; elim T; intros; clear T H1. rewrite <- H3; unfold FtoRradix; apply sym_eq. apply RoundedModeProjectorIdemEq with bo precision (EvenClosest bo radix precision); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. replace (FtoR radix f) with (p-q)%R; auto. fold FtoRradix; rewrite H3; rewrite H0; ring. right; unfold delta. replace (d - (b * b - a * c))%R with (-(b*b-p)+(a*c-q))%R; [idtac|rewrite H1; rewrite H0; ring]. apply Rle_trans with (Rabs (- (b * b - p)) + Rabs ((a * c - q)))%R; [apply Rabs_triang|idtac]. apply Rle_trans with (/2*(Fulp bo radix precision p) +/2*(Fulp bo radix precision q))%R. apply Rplus_le_compat; apply Rmult_le_reg_l with (2)%R; auto with real zarith. apply Rle_trans with (Fulp bo radix precision p); [idtac|simpl; right; field; auto with real]. rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto. elim Roundp; auto. apply Rle_trans with (Fulp bo radix precision q); [idtac|simpl; right; field; auto with real]. unfold FtoRradix; apply ClosestUlp; auto. elim Roundq; auto. replace (Fulp bo radix precision q) with (Fulp bo radix precision p). apply Rle_trans with (Fulp bo radix precision p); [right; field; auto with real|idtac]. apply Rle_trans with (1*(Fulp bo radix precision d))%R; [idtac|apply Rmult_le_compat_r; unfold Fulp; auto with real zarith]. apply Rle_trans with (Fulp bo radix precision d); auto with real. assert (0 <= p)%R. apply P_positive with bo precision b b; auto. fold FtoRradix; apply Rle_trans with (Rsqr b); auto with real. apply LeFulpPos; auto with real zarith. fold FtoRradix; rewrite H1; apply Rle_trans with (1*p)%R; auto with real. apply powerRZ_le, IZR_lt; auto with zarith. apply trans_eq with (Fulp bo radix precision (Fopp p)). unfold Fulp; rewrite Fnormalize_Fopp; auto with real zarith. apply FulpComp; auto with zarith. apply oppBounded; auto. rewrite Fopp_correct; auto with real zarith. intros C'. case (Req_dec t 0). clear C; intros C. assert (FtoRradix p=q)%R. assert (FtoRradix t=p+ Fopp q)%R. unfold FtoRradix; apply plusExactR0 with bo precision; auto with real zarith. apply oppBounded; auto. elim Roundt; intros; rewrite Fopp_correct; auto with real. apply Rplus_eq_reg_l with (Fopp q); rewrite Rplus_comm. rewrite <- H; rewrite C; unfold FtoRradix; rewrite Fopp_correct; auto; ring. assert (FtoRradix v=2*p)%R. assert (exists f:float, Fbounded bo f /\ (FtoRradix f=2*p)%R). exists (Float (Fnum p) (Fexp p+1)); split. elim Fp; intros; split; simpl; auto with zarith. unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix ; ring. elim H0; intros f T; elim T; intros; clear T H0. rewrite <- H2; unfold FtoRradix; apply sym_eq. apply RoundedModeProjectorIdemEq with bo precision (EvenClosest bo radix precision); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. replace (FtoR radix f) with (p+q)%R; auto. fold FtoRradix; rewrite H2; rewrite H; ring. assert (FtoRradix u=0)%R. assert (0 <= u)%R. unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (3*Rabs t)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto with zarith. rewrite C; rewrite Rabs_R0; right; ring. assert (u <= 0)%R; auto with real. unfold FtoRradix; apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (3*Rabs t)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto with zarith. rewrite C; rewrite Rabs_R0; right; ring. assert (u < v)%R. rewrite H1; assert (0 <= v)%R; auto with real. rewrite H0; apply Rle_trans with (0*0)%R; auto with real. apply Rmult_le_compat; auto with real. apply P_positive with bo precision b b; auto. apply Rle_trans with (Rsqr (FtoR radix b)); auto with real. case H2; auto with real. intros T; absurd (FtoRradix v=0)%R; auto with real. assert (FtoRradix d=s)%R. unfold FtoRradix; apply sym_eq. apply RoundedModeProjectorIdemEq with bo precision (EvenClosest bo radix precision); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. elim SRounds; auto; intros A1 A2; elim A1; auto. replace (FtoR radix s) with (t+s)%R; auto. fold FtoRradix; rewrite C; ring. right; unfold delta. replace (d - (b * b - a * c))%R with (-((dp-dq)-s))%R; [idtac|rewrite dpEq; auto; rewrite dqEq; auto; rewrite H3; rewrite H; ring]. apply Rle_trans with (/2*(Fulp bo radix precision s))%R. apply Rmult_le_reg_l with (2)%R; auto with real zarith. apply Rle_trans with (Fulp bo radix precision s); [idtac|simpl; right; field; auto with real]. rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto. elim SRounds; auto. rewrite FulpComp with bo radix precision d s; auto with zarith real. 2: elim SRounds; auto; intros A1 A2; elim A1; auto. apply Rmult_le_compat_r. unfold Fulp; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. lra. intros C''. case (Rle_or_lt v u); intros. case C; clear C; intros C; auto with real. case C; clear C; intros C; auto with real. absurd (FtoRradix v=0)%R; auto with real. case C; clear C; intros C; auto with real. absurd (FtoRradix t=0)%R; auto with real. elim C; intros Y1 C1; elim C1; intros Y2 C2; elim C2; intros Y3 C3; clear C C1 C2. elim C3; intros Y4 C4; elim C4; intros Y5 Y6; clear C3 C4. right; unfold delta;apply discri15 with p q t dp dq s u v; auto with real zarith. case C; clear C; intros C; auto with real. case C; clear C; intros C; auto with real. absurd (FtoRradix v=0)%R; auto with real. case C; clear C; intros C; auto with real. absurd (FtoRradix t=0)%R; auto with real. elim C; intros Y1 C1; elim C1; intros Y2 C2; elim C2; intros Y3 C3; clear C C1 C2. elim C3; intros Y4 C4; elim C4; intros Y5 Y6; clear C3 C4. right; unfold delta;apply discri15 with p q t dp dq s u v; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz