proposition: Theorem discri: (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. case Np; intros. 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. apply oppBounded; auto. replace (FtoR radix (Fopp q)) with (p-q)%R; [apply Firstcase|rewrite Fopp_correct; fold FtoRradix; rewrite H; ring]. rewrite H; ring_simplify (0-q)%R; 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 delta; rewrite H0. unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix. replace (-q-(b*b-a*c))%R with ((a*c-q)+(-(b*b)))%R;[idtac|ring]. apply Rle_trans with (1:=(Rabs_triang (a * c - q)%R (-(b*b))%R)). apply Rle_trans with (/2*(Fulp bo radix precision q)+/2*(Fulp bo radix precision p))%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 q);[idtac|simpl; right; field; auto with real]. unfold FtoRradix; apply ClosestUlp; auto. elim Roundq; auto. apply Rle_trans with (Fulp bo radix precision p);[idtac|simpl; right; field; auto with real]. replace (-(b*b))%R with (-(b*b-p))%R;[rewrite Rabs_Ropp|rewrite H;ring]. unfold FtoRradix; apply ClosestUlp; auto. elim Roundp; auto. apply Rle_trans with (/ 2 * Fulp bo radix precision q + / 2 * Fulp bo radix precision q)%R;[apply Rplus_le_compat; auto with real|idtac]. apply Rmult_le_compat_l; auto with real. rewrite Fulp_zero. unfold Fulp; apply Rle_powerRZ;auto with real zarith. apply FnormalizeBounded; auto with zarith. apply is_Fzero_rep2 with radix; auto with zarith. apply Rle_trans with (1 * Fulp bo radix precision q)%R;[right; field; auto with real|idtac]. apply Rmult_le_compat; auto with real zarith. unfold Fulp; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. 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 Nq; intros. 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. replace (FtoR radix p) with (p-q)%R; [apply Firstcase|fold FtoRradix; rewrite H0; ring]. rewrite H0; ring_simplify (p+0)%R; 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 delta; rewrite H1. replace (p-(b*b-a*c))%R with (a*c+(-(b*b-p)))%R;[idtac|ring]. apply Rle_trans with (1:=(Rabs_triang (a * c )%R (-(b*b-p))%R)). apply Rle_trans with (/2*(Fulp bo radix precision q)+/2*(Fulp bo radix precision p))%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 q);[idtac|simpl; right; field; auto with real]. replace (a*c)%R with (a*c-q)%R;[idtac|rewrite H0;ring]. unfold FtoRradix; apply ClosestUlp; auto. elim Roundq; auto. 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 (/ 2 * Fulp bo radix precision p + / 2 * Fulp bo radix precision p)%R;[apply Rplus_le_compat; auto with real|idtac]. apply Rmult_le_compat_l; auto with real. rewrite Fulp_zero. unfold Fulp; apply Rle_powerRZ;auto with real zarith. apply FnormalizeBounded; auto with zarith. apply is_Fzero_rep2 with radix; auto with zarith. apply Rle_trans with (1 * Fulp bo radix precision p)%R;[right; field; auto with real|idtac]. apply Rmult_le_compat; auto with real zarith. unfold Fulp; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. right; apply FulpComp; auto with zarith. case (Rle_or_lt (p + q)%R (3 * Rabs (p - q))%R); intros. unfold delta;apply discri1 with p q; auto. apply Rle_trans with (Rsqr (FtoR 2 b)) ; auto with real. case (Ns H1); intros. unfold delta; apply discri3 with p q t dp dq s; auto with real zarith. apply Rle_trans with (Rsqr (FtoR 2 b)) ; auto with real. 2:unfold delta; apply discri9 with p q t dp dq s; auto. exists (Float 0%Z 0%Z). split. unfold Fbounded; split; unfold Fexp; try lia; auto with zarith. apply trans_eq with 0%R. unfold FtoR; simpl; ring. fold radix; fold FtoRradix. rewrite <- H2. unfold FtoRradix; rewrite plusExactR0 with bo radix precision dp (Fopp dq) s; auto. rewrite Fopp_correct; ring. apply oppBounded; auto. replace (FtoR radix dp + FtoR radix (Fopp dq))%R with (dp - dq)%R; auto. elim SRounds; auto. unfold FtoRradix; rewrite Fopp_correct; auto with real. intros; left; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz