proposition: Theorem discri9: (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. assert (Square:(0<=b*b)%R). apply Rle_trans with (Rsqr b); auto with real. case (Rle_or_lt (p + q)%R (3 * Rabs (p - q))%R); intros. unfold delta;apply discri1 with p q; auto. case (Rle_or_lt (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)))%R (Rabs (p-q))%R); intros. unfold delta; apply discri2 with p q t dp dq s; auto. case (Zle_or_lt (Fexp q) (Fexp p)); intros. case (Zle_lt_or_eq (Fexp q) (Fexp p)); auto;intros. assert (Fexp q = Z.pred (Fexp p))%Z. cut (Z.le (Fexp q) (Z.pred (Fexp p))); auto with zarith. cut (Z.le (Z.pred (Fexp p)) (Fexp q)); auto with zarith. clear H1;apply Zle_powerRZ with radix; auto with real zarith. apply Rle_trans with (Fulp bo radix precision (Float (Fnum p) (Z.pred (Fexp p)))). rewrite CanonicFulp; auto. unfold FtoR; simpl; right; ring. left; split; auto with zarith. split; simpl; auto with zarith; try apply Np. apply Z.le_trans with (Fexp q); auto with zarith; apply Nq. simpl; elim Np; auto with zarith. apply Rle_trans with (Fulp bo radix precision q). apply LeFulpPos; auto with real zarith. split; simpl; auto with zarith; try apply Np. apply Z.le_trans with (Fexp q); auto with zarith; apply Nq. apply LeFnumZERO; simpl; auto with real zarith. apply LeR0Fnum with radix; auto with real zarith. apply P_positive with bo precision b b; auto. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (FtoRradix p). unfold FtoRradix, FtoR, Z.pred; simpl; rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2; simpl; unfold radix; right; field. apply P_le_two_Q with bo precision b b; auto. rewrite CanonicFulp; auto with zarith. unfold FtoR; simpl; right; ring. left; auto. clear H1 H2; assert (FtoRradix p=powerRZ radix (precision+Z.pred (Fexp p)))%R. case (Zle_lt_or_eq (Zpower_nat radix (pred precision)) (Fnum p)). elim Np; intros. apply Zmult_le_reg_r with radix; auto with zarith; try (apply Z.lt_gt; auto with zarith). apply Z.le_trans with (Zpower_nat radix precision). pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1). rewrite <- Zpower_nat_is_exp; auto with zarith. apply Zpower_nat_monotone_le; auto with zarith. simpl; auto with zarith. rewrite <- pGivesBound; apply Z.le_trans with (1:=H2). rewrite Z.abs_eq; auto with zarith. apply Z.mul_nonneg_nonneg; try unfold radix; auto with zarith. apply LeR0Fnum with radix; auto. apply P_positive with bo precision b b; auto. intros H1; contradict H0. apply Rle_not_lt. rewrite CanonicFulp; auto; [idtac|left; auto]. rewrite CanonicFulp; auto; [idtac|left; auto]. replace (FtoR radix (Float 1 (Fexp p))) with (powerRZ radix (Fexp p));[idtac|unfold FtoR; simpl; ring]. replace (FtoR radix (Float 1 (Fexp q))) with (powerRZ radix (Fexp q));[idtac|unfold FtoR; simpl; ring]. rewrite H3; unfold Rmin. case (Rle_dec (powerRZ radix (Fexp p)) (powerRZ radix (Z.pred (Fexp p)))); auto with real zarith; intros J. contradict J; apply Rlt_not_le; auto with real zarith. apply Rlt_powerRZ; try apply IZR_lt; auto with zarith. clear J; rewrite Rabs_right. unfold FtoRradix, FtoR, Rminus. apply Rle_trans with ((Z.succ (Zpower_nat radix (pred precision))*(powerRZ radix (Fexp p))+-((Z.pred (Zpower_nat radix precision))*(powerRZ radix (Fexp q)))))%R. unfold Z.pred, Z.succ; rewrite plus_IZR; rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ. rewrite inj_pred; auto with zarith. rewrite H3; unfold Z.pred; simpl; right;ring_simplify. repeat rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2 4 7 9; simpl; unfold radix; field. apply Rplus_le_compat;[apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; auto with zarith. apply IZR_le; auto with zarith. apply Ropp_le_contravar; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. apply Rle_trans with (1:=RRle_abs (Fnum q)). rewrite Rabs_Zabs; rewrite <- pGivesBound;auto with zarith. destruct Nq as ((T1,T2),T3); apply IZR_le; auto with zarith. apply Rle_ge; apply Rlt_le; apply Rplus_lt_reg_r with q. ring_simplify. unfold FtoRradix; apply FcanonicPosFexpRlt with bo precision; auto with zarith. apply Rlt_le; apply Q_positive with bo precision b b p; auto. apply P_positive with bo precision b b; auto. left; auto. left; auto. intros H1; unfold FtoRradix, FtoR; rewrite <- H1. rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith. rewrite inj_pred; auto with zarith. replace (Z.pred precision+Fexp p)%Z with (precision + Z.pred (Fexp p))%Z;[auto with real|unfold Z.pred; ring]. unfold delta; apply discri8 with p q t dp dq s (Z.pred (Fexp p)); auto. apply FcanonicUnique with radix bo precision; auto with zarith real. left; auto. left; split; [split;simpl|idtac]; auto with zarith. rewrite Z.abs_eq; auto with zarith. rewrite pGivesBound; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. apply Zpower_NR0; auto with zarith. apply Z.le_trans with (Fexp p); auto with zarith; apply Np. simpl (Fnum (Float (Zpower_nat 2 (pred precision)) (Z.succ (Z.pred (Fexp p))))). replace radix with (Zpower_nat radix 1);[idtac|simpl; auto with zarith]. rewrite <-Zpower_nat_is_exp; rewrite pGivesBound; auto with zarith. rewrite Z.abs_eq; auto with zarith. apply Zpower_nat_monotone_le; auto with zarith. apply Zpower_NR0; auto with zarith. fold FtoRradix; rewrite H1; unfold FtoRradix, FtoR, Z.pred, Z.succ; simpl. rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith. rewrite inj_pred; auto with zarith; unfold Z.pred. replace (precision + -1 + (Fexp p + -1 + 1))%Z with (precision+(Fexp p+-1))%Z; auto with real; ring. unfold delta;apply discri4 with p q t dp dq s; auto. assert (Fexp p = Z.pred (Fexp q))%Z. cut (Z.le (Fexp p) (Z.pred (Fexp q))); auto with zarith. cut (Z.le (Z.pred (Fexp q)) (Fexp p)); auto with zarith. clear H1;apply Zle_powerRZ with radix; auto with real zarith. apply Rle_trans with (Fulp bo radix precision (Float (Fnum q) (Z.pred (Fexp q)))). rewrite CanonicFulp; auto. unfold FtoR; simpl; right; ring. left; split; auto with zarith. split; simpl; auto with zarith. apply Nq. assert (exists s : float, Fbounded bo s /\ FtoR 2 s = (FtoR 2 a * FtoR 2 c - FtoR 2 q)%R /\ Fexp s = (Fexp q - precision)%Z /\ (Rabs (Fnum s) <= powerRZ (Zpos 2) (Z.pred precision))%R). apply errorBoundedMultClosest_Can; auto. elim Roundq; auto. left; auto. elim H1; intros s' T; elim T; intros T1 T2; elim T2; intros T3 T4; elim T4; intros. apply Z.le_trans with (Fexp q - precision)%Z; auto with zarith. rewrite <- H2; auto with zarith. apply T. simpl; elim Nq; auto with zarith. apply Rle_trans with (Fulp bo radix precision p). apply LeFulpPos; auto with real zarith. split; simpl; auto with zarith; try apply Nq. assert (exists s : float, Fbounded bo s /\ FtoR 2 s = (FtoR 2 a * FtoR 2 c - FtoR 2 q)%R /\ Fexp s = (Fexp q - precision)%Z /\ (Rabs (Fnum s) <= powerRZ (Zpos 2) (Z.pred precision))%R). apply errorBoundedMultClosest_Can; auto. elim Roundq; auto. left; auto. elim H1; intros s' T; elim T; intros T1 T2; elim T2; intros T3 T4; elim T4; intros. apply Z.le_trans with (Fexp q - precision)%Z; auto with zarith. rewrite <- H2; auto with zarith; apply T. apply LeFnumZERO; simpl; auto with real zarith. apply LeR0Fnum with radix; auto with real zarith. apply Rlt_le; apply Q_positive with bo precision b b p; auto. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (FtoRradix q). unfold FtoRradix, FtoR, Z.pred; simpl; rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2; simpl; unfold radix; right; field. apply Q_le_two_P with bo precision b b; auto. rewrite CanonicFulp; auto with zarith. unfold FtoR; simpl; right; ring. left; auto. clear H1; assert (FtoRradix q=powerRZ radix (precision+Z.pred (Fexp q)))%R. case (Zle_lt_or_eq (Zpower_nat radix (pred precision)) (Fnum q)). elim Nq; intros. apply Zmult_le_reg_r with radix; auto with zarith; try (apply Z.lt_gt; auto with zarith). apply Z.le_trans with (Zpower_nat radix precision). pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1). rewrite <- Zpower_nat_is_exp; auto with zarith. apply Zpower_nat_monotone_le; auto with zarith. simpl; auto with zarith. rewrite <- pGivesBound; apply Z.le_trans with (1:=H3). rewrite Z.abs_eq; auto with zarith. apply Z.mul_nonneg_nonneg; try unfold radix; auto with zarith. apply LeR0Fnum with radix; auto. apply Rlt_le; apply Q_positive with bo precision b b p; auto. intros H1; contradict H0. apply Rle_not_lt. rewrite CanonicFulp; auto; [idtac|left; auto]. rewrite CanonicFulp; auto; [idtac|left; auto]. replace (FtoR radix (Float 1 (Fexp p))) with (powerRZ radix (Fexp p));[idtac|unfold FtoR; simpl; ring]. replace (FtoR radix (Float 1 (Fexp q))) with (powerRZ radix (Fexp q));[idtac|unfold FtoR; simpl; ring]. rewrite H2; unfold Rmin. case (Rle_dec (powerRZ radix (Z.pred (Fexp q))) (powerRZ radix (Fexp q))); auto with real zarith; intros J. clear J; rewrite Rabs_left1. unfold FtoRradix, FtoR, Rminus. apply Rle_trans with (- ((Z.pred (Zpower_nat radix precision)) * powerRZ radix (Fexp p) + - ((Z.succ (Zpower_nat radix (pred precision))) * powerRZ radix (Fexp q))))%R. unfold Z.pred, Z.succ; rewrite plus_IZR; rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ. rewrite inj_pred; auto with zarith. rewrite H2; unfold Z.pred; simpl; right. repeat rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2 5 7; simpl; unfold radix; field. apply Ropp_le_contravar. apply Rplus_le_compat;[apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; auto with zarith. 2:apply Ropp_le_contravar; apply Rmult_le_compat_r; auto with real zarith. 2: apply powerRZ_le, IZR_lt; auto with zarith. apply Rle_trans with (1:=RRle_abs (Fnum p)). rewrite Rabs_Zabs; rewrite <- pGivesBound;auto with zarith. apply IZR_le, Zle_Zpred, Np. apply IZR_le; auto with zarith. apply Rlt_le; apply Rplus_lt_reg_r with q. ring_simplify. unfold FtoRradix; apply FcanonicPosFexpRlt with bo precision; auto with zarith. 2:apply Rlt_le; apply Q_positive with bo precision b b p; auto. apply P_positive with bo precision b b; auto. left; auto. left; auto. contradict J; auto with real zarith. apply Rle_powerRZ; try apply IZR_le; try unfold radix; auto with zarith. intros H1; unfold FtoRradix, FtoR; rewrite <- H1. rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith. rewrite inj_pred; auto with zarith. replace (Z.pred precision+Fexp q)%Z with (precision + Z.pred (Fexp q))%Z;[auto with real|unfold Z.pred; ring]. unfold delta; rewrite <-Rabs_Ropp. replace (- (d - (b * b - a * c)))%R with (Fopp d-(a*c-b*b))%R;[idtac|unfold FtoRradix; rewrite Fopp_correct; ring]. replace (Fulp bo radix precision d) with (Fulp bo radix precision (Fopp d)); auto with zarith. 2: unfold Fulp; rewrite Fnormalize_Fopp; unfold Fopp; simpl; auto with real zarith. apply discri8 with q p (Fopp t) dq dp (Fopp s) (Z.pred (Fexp q)); auto with zarith. apply oppBounded; auto. apply FcanonicFopp; auto. apply FnormalFop; auto. fold radix; fold FtoRradix; case (Rle_or_lt 0%R (a*c)%R); auto. intros H3; absurd (0 < q)%R. apply Rle_not_lt; unfold FtoRradix; apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (a*c)%R; auto with real. apply EvenClosestRoundedModeP; auto. apply Q_positive with bo precision b b p; auto. fold radix; fold FtoRradix; rewrite (Rplus_comm q p). replace (q-p)%R with (-(p-q))%R; auto with real; rewrite Rabs_Ropp; auto. fold radix; fold FtoRradix; replace (q-p)%R with (-(p-q))%R; auto with real. generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto. fold radix; fold FtoRradix; replace (dq-dp)%R with (-(dp-dq))%R;auto with real. generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto. fold radix; fold FtoRradix; replace (Fopp t+Fopp s)%R with (-(t+s))%R;[idtac|unfold FtoRradix; repeat rewrite Fopp_correct; ring]. generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto. apply FcanonicUnique with radix bo precision; auto with zarith real. left; auto. left; split; [split;simpl|idtac]; auto with zarith. rewrite Z.abs_eq; auto with zarith. rewrite pGivesBound; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. apply Zpower_NR0; auto with zarith. apply Z.le_trans with (Fexp q); auto with zarith; apply Fq. simpl (Fnum (Float (Zpower_nat 2 (pred precision)) (Z.succ (Z.pred (Fexp q))))). replace radix with (Zpower_nat radix 1);[idtac|simpl; auto with zarith]. rewrite <-Zpower_nat_is_exp; rewrite pGivesBound; auto with zarith. rewrite Z.abs_eq; auto with zarith. apply Zpower_nat_monotone_le; auto with zarith. apply Zpower_NR0; auto with zarith. fold FtoRradix; rewrite H1; unfold FtoRradix, FtoR, Z.pred, Z.succ; simpl. rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith. rewrite inj_pred; auto with zarith; unfold Z.pred. replace (precision + -1 + (Fexp q + -1 + 1))%Z with (precision+(Fexp q+-1))%Z; auto with real; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz