proposition: Theorem discri10: (q <= p)%R -> (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. intros G. case (Zle_lt_or_eq (Fexp d) (Fexp q)). apply Fcanonic_Rle_Zle with radix bo precision; auto with real zarith. left; auto. fold FtoRradix; rewrite Rabs_right. rewrite Rabs_right. rewrite dexact; apply Rplus_le_reg_l with q. ring_simplify; apply P_le_two_Q with bo precision b b'; auto. apply Rle_ge; left; apply Q_positive with bo precision b b' p; auto. apply Rle_ge; rewrite dexact; apply Rplus_le_reg_l with q. ring_simplify; auto with real. assert ( 0 < 2+(powerRZ radix (-precision)))%R. apply Rle_lt_trans with (0+0)%R; auto with real. apply Rplus_lt_compat; auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. assert ((q <= p * (1 + powerRZ radix (1 - precision)) / (2 + powerRZ radix (- precision)))%R). apply Rmult_le_reg_l with (2 + powerRZ radix (- precision))%R; auto with real. apply Rle_trans with (p * (1 + powerRZ radix (1 - precision)))%R;[idtac|right; field; auto with real]. apply Rmult_le_reg_l with 2%R; auto with real. apply Rplus_le_reg_l with (-2*p+p*(powerRZ radix (1-precision))-3*q*(powerRZ radix (1-precision)))%R. apply Rle_trans with ((powerRZ radix (1-precision))*(3*(p-q)))%R;[idtac|right; ring]. apply Rle_trans with ((4*q-2*p)*(1-powerRZ radix (-precision)))%R. right; unfold Zminus; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix ; ring. assert (0 < (1 - powerRZ radix (- precision)))%R. apply Rplus_lt_reg_r with (powerRZ radix (- precision)). ring_simplify. replace 1%R with (powerRZ radix 0); [ auto with real zarith | simpl in |- *; auto ]. apply Rlt_powerRZ; try apply IZR_lt; auto with zarith. apply Rmult_le_reg_l with (/ (1 - powerRZ radix (- precision)))%R; auto with real. apply Rle_trans with (4 * q - 2 * p)%R;[right; field; auto with real|idtac]. apply Rle_trans with (Fulp bo radix precision v). apply Rle_trans with (((p+q)-v) +- (3*(p-q)-v))%R;[right;ring|idtac]. apply Rle_trans with (Rabs (((p+q)-v) +- (3*(p-q)-v)));[apply RRle_abs|idtac]. apply Rle_trans with (Rabs (((p+q)-v)) +Rabs (- (3*(p-q)-v)))%R;[apply Rabs_triang|idtac]. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (2*(Rabs (((p+q)-v))) +2*Rabs (- (3*(p-q)-v)))%R;[right;ring|idtac]. apply Rle_trans with (Fulp bo radix precision v+Fulp bo radix precision v)%R;[idtac|right;ring]. rewrite Rabs_Ropp; auto with real zarith. apply Rplus_le_compat; unfold FtoRradix; apply ClosestUlp; auto with zarith. elim Roundv; auto. elim Roundu; intros Y1 Y2. apply ClosestCompatible with (1:=Y1); fold FtoRradix; auto. rewrite <- dDef; rewrite dexact. rewrite Rabs_right; auto with real. apply Rle_ge; apply Rplus_le_reg_l with q; auto with real. ring_simplify (q+0)%R; apply Rle_trans with (1:=G); right; ring. apply sym_eq; apply IneqEq. apply Rle_trans with (Rabs v * powerRZ radix (Z.succ (- precision)))%R. unfold FtoRradix; apply FulpLe2; auto. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. unfold Z.succ; replace (-precision+1)%Z with (1-precision)%Z; auto with zarith. apply Rle_trans with (((3 * (p - q))*/(1 - powerRZ radix (- precision)))* powerRZ radix (1 - precision))%R; [idtac|right; ring]. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. assert (0 <= p-q)%R. apply Rplus_le_reg_l with q; auto with real. ring_simplify (q+0)%R; apply Rle_trans with (1:=G); right; ring. apply Rle_trans with (Rabs (3 * Rabs t) / (1 - powerRZ radix (- precision)))%R. rewrite IneqEq. apply RoundLeNormal; auto. elim Roundu; auto. rewrite <- dDef; rewrite dexact. rewrite Rabs_right;[rewrite Rabs_right; auto with real; right; ring|idtac]. rewrite Rabs_right; auto with real. apply Rle_ge; apply Rle_trans with (3*0)%R; auto with real. intros W. case (Zle_lt_or_eq (Fexp q) (Fexp p)). apply Fcanonic_Rle_Zle with radix bo precision; auto with zarith. left; auto. left; auto. assert (0 <= q)%R. left; apply Q_positive with bo precision b b' p; auto. fold FtoRradix; repeat rewrite Rabs_right; auto with real. apply Rle_ge; apply Rle_trans with (1:=H1); auto with real. intros M. assert (exists qq:float, (FtoRradix qq=2*q)%R /\ Fbounded bo qq /\ Fnormal radix bo qq /\ Fnum qq=Fnum q /\ (Fexp qq=Fexp q+1)%Z). exists (Float (Fnum q) ((Fexp q)+1)). elim Nq; intros F1 F2; elim F1; intros. split;[unfold FtoRradix, FtoR; simpl|idtac]. rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; ring. repeat split; simpl; auto with zarith. elim H1; intros qq H1'; elim H1'; intros J1 H2; elim H2; intros J2 H3; elim H3; intros J3 H4; elim H4; intros J4 J5;clear H1' H1 H2 H3 H4. assert (2*q=FSucc bo radix precision p)%R. rewrite <- J1. assert ((FSucc bo radix precision p <= qq)%R /\ (qq <= FSucc bo radix precision p)%R). 2: elim H1; auto with real. split. unfold FtoRradix; apply FSuccProp; auto with real zarith. left; auto. left; auto. fold FtoRradix; rewrite J1. assert (p <= 2*q)%R. apply P_le_two_Q with bo precision b b'; auto. case H1; auto. intros A. absurd (3 * Rabs (p - q) < p + q)%R; auto. apply Rle_not_lt; rewrite A. ring_simplify (2*q-q)%R; rewrite Rabs_right. right; ring. apply Rle_ge; left; apply Q_positive with bo precision b b' p; auto. case (Rle_or_lt qq (FSucc bo radix precision p)); auto; intros N. absurd (FSucc bo radix precision (FSucc bo radix precision p) <= qq)%R. 2: unfold FtoRradix; apply FSuccProp; auto with zarith. 2: apply FSuccCanonic; auto with zarith. 2: left; auto. 2: left; auto. apply Rlt_not_le. apply Rle_lt_trans with (2*(p*(1+powerRZ radix (1-precision))/(2+(powerRZ radix (-precision)))))%R. rewrite J1; apply Rmult_le_compat_l; auto with real. assert (0 < (powerRZ radix precision) - 1)%R. apply Rplus_lt_reg_r with 1%R; ring_simplify. replace 1%R with (powerRZ radix 0); auto with real zarith. apply Rlt_powerRZ; try apply IZR_lt; auto with zarith. apply Rlt_le_trans with (p*(((powerRZ radix precision)+1)/((powerRZ radix precision) -1)))%R. apply Rle_lt_trans with (p*((2 + 2*powerRZ radix (1 - precision)) / (2 + powerRZ radix (- precision))))%R; [right; unfold Rdiv; ring|idtac]. apply Rmult_lt_compat_l. apply Rlt_le_trans with (2:=G). apply Q_positive with bo precision b b' p; auto. apply Rmult_lt_reg_l with (powerRZ radix precision - 1)%R; auto with real. apply Rlt_le_trans with (powerRZ radix precision + 1)%R;[idtac|right; field; auto with real]. apply Rmult_lt_reg_l with (2+powerRZ radix (-precision))%R; auto with real. apply Rle_lt_trans with ((powerRZ radix precision - 1) * ((2 + 2 * powerRZ radix (1 - precision))))%R;[right; field; auto with real|idtac]. apply Rle_lt_trans with (2*powerRZ radix precision+2+-2*powerRZ radix (1-precision))%R; [right; ring_simplify|idtac]. rewrite Rmult_assoc. repeat rewrite <- powerRZ_add; auto with real zarith. ring_simplify (precision+(1-precision))%Z; rewrite powerRZ_1; unfold radix; ring. apply Rlt_le_trans with (2 * powerRZ radix precision + 2 +1+powerRZ radix (-precision))%R. repeat rewrite Rplus_assoc; repeat apply Rplus_lt_compat_l. apply Rle_lt_trans with (1+0)%R; auto with real. ring_simplify (1+0)%R; apply Rle_trans with 0%R; auto with real. apply Ropp_le_cancel; ring_simplify ( - (-2 * powerRZ radix (1 - precision)))%R. apply Rle_trans with (2*0)%R; auto with real zarith. right; ring. apply Rmult_le_compat_l; auto with real. apply powerRZ_le, IZR_lt; auto with zarith. apply Rplus_lt_compat_l. apply powerRZ_lt, IZR_lt; auto with zarith. right; ring_simplify. rewrite <- powerRZ_add; auto with real zarith. ring_simplify (precision+-precision)%Z; simpl; ring. apply Rle_trans with (p+2*Fulp bo radix precision p)%R. apply Rmult_le_reg_l with (powerRZ radix precision - 1)%R; auto with real. apply Rle_trans with (p * ((powerRZ radix precision + 1)))%R;[right; field; auto with real|idtac]. apply Rle_trans with ((powerRZ radix precision -1)*p+2*p)%R;[right; ring|idtac]. apply Rle_trans with ((powerRZ radix precision -1)*p + 2*((powerRZ radix precision - 1)* Fulp bo radix precision p))%R;[idtac|right; ring]. apply Rplus_le_compat_l. apply Rmult_le_compat_l; auto with real. apply Rle_trans with (Rabs p);[apply RRle_abs|idtac]. unfold FtoRradix; apply FulpGe; auto. apply Rplus_le_reg_l with (-(FSucc bo radix precision p))%R. apply Rle_trans with (Fminus radix (FSucc bo radix precision (FSucc bo radix precision p)) (FSucc bo radix precision p));[idtac|unfold FtoRradix; rewrite Fminus_correct; auto; right; ring]. unfold FtoRradix; rewrite FSuccDiff1; auto with zarith. rewrite <- CanonicFulp with bo radix precision (FSucc bo radix precision p); auto with zarith. 2:apply FSuccCanonic; auto with zarith; left; auto. apply Rle_trans with (-(Fminus radix (FSucc bo radix precision p) p)+ 2 * Fulp bo radix precision p)%R; [unfold FtoRradix; rewrite Fminus_correct; auto; right; ring|idtac]. unfold FtoRradix; rewrite FSuccDiff1; auto with zarith. rewrite <- CanonicFulp with bo radix precision p; auto with zarith. 2: left; auto. ring_simplify. apply LeFulpPos; auto with zarith. apply FBoundedSuc; auto with zarith. fold FtoRradix; apply P_positive with bo precision b b'; auto. left; apply FSuccLt; auto with zarith. assert (0 < nNormMin radix precision)%Z;[apply nNormPos; auto with zarith|idtac]. assert (0 <= Fnum p)%Z; auto with zarith. apply LeR0Fnum with radix; auto with real zarith. apply P_positive with bo precision b b'; auto. assert (0 < nNormMin radix precision)%Z;[apply nNormPos; auto with zarith|idtac]. assert (0 <= Fnum (FSucc bo radix precision p))%Z; auto with zarith. apply LeR0Fnum with radix; auto with real zarith. apply Rle_trans with (FtoR radix p). apply P_positive with bo precision b b'; auto. left; apply FSuccLt; auto with zarith. assert (Fexp d = Fexp q-1)%Z. assert (Fexp q -1 <= Fexp d)%Z; auto with zarith. apply Z.le_trans with (Fexp p-2)%Z; auto with zarith. apply Z.le_trans with (Fexp (Float (Fnum p) (Fexp p-2))); auto with zarith. apply Fcanonic_Rle_Zle with radix bo precision; auto with real zarith. elim Np; intros Y1 Y2; elim Y1; intros; left; split;try split; simpl; auto with zarith. apply Rle_trans with (p/4)%R. unfold Rdiv, FtoRradix, FtoR; simpl. rewrite Rabs_mult; repeat rewrite Rabs_right. unfold Zminus; rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2; simpl; unfold radix; right; field. apply Rle_ge; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. apply Rle_ge; assert (0 <= Fnum p)%Z; auto with real zarith. apply LeR0Fnum with radix; auto with real zarith. fold FtoRradix; apply P_positive with bo precision b b'; auto. apply IZR_le; auto. fold FtoRradix; rewrite dexact. rewrite Rabs_right. 2: apply Rle_ge; apply Rplus_le_reg_l with q. 2: ring_simplify; auto with real. apply Rle_trans with (p- p * (1 + powerRZ radix (1 - precision)) / (2 + powerRZ radix (- precision)))%R; auto with real. 2: unfold Rminus; apply Rplus_le_compat_l; auto with real. unfold Rdiv; apply Rle_trans with (p*(1-(1 + powerRZ radix (1 - precision)) */ (2 + powerRZ radix (- precision))))%R;[idtac|right; ring]. apply Rmult_le_compat_l. apply P_positive with bo precision b b'; auto. apply Rmult_le_reg_l with 4%R; auto with real. apply Rmult_le_reg_l with (2 + powerRZ radix (- precision))%R; auto with real. apply Rle_trans with (2 + powerRZ radix (- precision))%R; [right; field|idtac]. assert (0 < 4)%R; [apply Rlt_le_trans with 2%R|idtac]; auto with real. apply Rle_trans with (4* (2 + powerRZ radix (- precision))- 4*(1 + powerRZ radix (1 - precision)))%R;[idtac|right;field; auto with real]. unfold Zminus; rewrite powerRZ_add; auto with real zarith; rewrite powerRZ_1. apply Rplus_le_reg_l with (-2+4*powerRZ radix (-precision))%R. apply Rle_trans with (5*powerRZ radix (-precision))%R;[right; ring|idtac]. apply Rle_trans with 2%R;[idtac|simpl; unfold radix; right; ring]. apply Rle_trans with (powerRZ radix 0); auto with real zarith. apply Rle_trans with (powerRZ radix (3-precision)); auto with real zarith. unfold Zminus; rewrite powerRZ_add; auto with real zarith. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. unfold powerRZ; simpl; unfold radix; repeat rewrite <- mult_IZR; auto with real zarith. apply Rle_powerRZ; auto with real zarith. simpl; auto with real. case (Zle_lt_or_eq (nNormMin radix precision) (Fnum q)). elim Nq; intros. apply Zmult_le_reg_r with radix. unfold radix; auto with zarith. rewrite Zmult_comm; rewrite <- PosNormMin with radix bo precision; auto with zarith. apply Z.le_trans with (1:=H4); rewrite Z.abs_eq; auto with zarith. apply Z.mul_nonneg_nonneg. unfold radix; lia. assert (0 < Fnum q)%Z; auto with zarith. apply LtR0Fnum with radix; auto with real zarith. apply Q_positive with bo precision b b' p; auto. intros P. assert (Fnum q < nNormMin radix precision+2)%Z. apply lt_IZR; rewrite plus_IZR; simpl. apply Rmult_lt_reg_l with (powerRZ radix (Fexp q)); auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. apply Rle_lt_trans with q;[unfold FtoRradix, FtoR; auto with real|idtac]. apply Rplus_lt_reg_r with (-2*powerRZ radix (Fexp q))%R. apply Rlt_le_trans with (powerRZ radix (Fexp q) * (nNormMin radix precision))%R; [idtac|right; ring]. apply Rle_lt_trans with d;[rewrite dexact|idtac]. apply Rplus_le_reg_l with q. ring_simplify (q + (p - q))%R;right. rewrite <- FPredSuc with bo radix precision p; auto with zarith. 2: left; auto. replace (FSucc bo radix precision p) with qq. rewrite FPredSimpl4; auto with zarith. unfold FtoRradix, FtoR, Z.pred; simpl; rewrite J4; rewrite J5; ring_simplify. rewrite plus_IZR; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; ring. assert (- pPred (vNum bo) < Fnum qq)%Z; auto with zarith. apply Z.lt_trans with (nNormMin radix precision); auto with zarith. assert (0 < pPred (vNum bo))%Z. apply pPredMoreThanOne with radix precision; auto with zarith. apply Z.lt_trans with 0%Z; auto with zarith. apply nNormPos; auto with zarith. apply FcanonicUnique with radix bo precision; auto with zarith real. left; auto. apply FSuccCanonic; auto with zarith. left; auto. fold FtoRradix; rewrite J1; auto with real. apply Rle_lt_trans with (Rabs d);[apply RRle_abs|idtac]. unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold Fabs, FtoR; simpl. apply Rlt_le_trans with (powerRZ 2 precision* powerRZ 2 (Fexp d))%R. apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. assert (Fbounded bo d);[rewrite dDef; elim Roundt; intros I1 I2; elim I1; auto|idtac]. elim H3; intros. apply Rlt_le_trans with (Zpos (vNum bo)); try apply IZR_lt; auto with real zarith. right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real. unfold nNormMin; repeat rewrite <- powerRZ_add; auto with real zarith. rewrite Zpower_nat_Z_powerRZ; repeat rewrite <- powerRZ_add; auto with real zarith. replace (Fexp q+pred precision)%Z with (precision+Fexp d)%Z by lia. apply Rle_refl. assert (Fnum q= nNormMin radix precision + 1)%Z; auto with zarith. clear P H3. assert (p=Float (nNormMin radix precision) (Fexp q+1)). rewrite <- FPredSuc with bo radix precision p; auto with zarith. 2: left; auto. replace (FSucc bo radix precision p) with qq. rewrite FPredSimpl4; auto with zarith. rewrite J4; rewrite J5; rewrite H4; unfold Z.pred; auto with zarith. ring_simplify (nNormMin radix precision + 1 + -1)%Z; auto. assert (- pPred (vNum bo) < Fnum qq)%Z; auto with zarith. rewrite J4; rewrite H4. apply Z.lt_trans with (nNormMin radix precision); auto with zarith. assert (0 < pPred (vNum bo))%Z. apply pPredMoreThanOne with radix precision; auto with zarith. apply Z.lt_trans with 0%Z; auto with zarith. apply nNormPos; auto with zarith. apply FcanonicUnique with radix bo precision; auto with zarith real. left; auto. apply FSuccCanonic; auto with zarith. left; auto. fold FtoRradix; rewrite J1; auto with real. contradict Case2; apply Rlt_not_le. assert (FtoRradix p=powerRZ radix (Fexp q)*powerRZ radix precision)%R. rewrite H3; unfold FtoRradix, FtoR; simpl. unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith. repeat rewrite <- powerRZ_add; auto with real zarith. replace (Fexp q+precision)%Z with (Z.pred precision+(Fexp q+1))%Z;unfold Z.pred; auto with real zarith. assert (FtoRradix q=powerRZ radix (Fexp q)*(powerRZ radix (precision-1)+1))%R. unfold FtoRradix, FtoR; rewrite H4; rewrite plus_IZR; simpl. unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith. unfold Z.pred, Zminus; simpl; ring. assert (exists w1:float, Fbounded bo w1 /\ (FtoRradix w1=powerRZ radix (Fexp q)* (powerRZ radix precision+powerRZ radix (precision-1)-2))%R). exists (Float (Zpower_nat radix (pred precision)+Zpower_nat radix (pred (pred precision))-1) (Fexp q+1)). split;[split; simpl|idtac]. rewrite Z.abs_eq; auto with zarith. rewrite pGivesBound; apply Z.lt_le_trans with (Zpower_nat radix (pred precision) + Zpower_nat radix (pred precision))%Z. unfold Zminus; rewrite <- Zplus_assoc; apply Zplus_lt_compat_l. apply Z.lt_le_trans with (Zpower_nat radix (pred (pred precision)) + Zpower_nat radix (pred (pred precision)))%Z. apply Zplus_lt_compat_l; auto with zarith. apply Z.lt_trans with 0%Z; auto with zarith. apply Zpower_nat_less; auto with zarith. pattern (pred precision) at 3; replace (pred precision) with (1+pred (pred precision)); auto with zarith. rewrite Zpower_nat_is_exp. replace (Zpower_nat radix 1) with 2%Z; auto with zarith. pattern precision at 3; replace precision with (1+pred precision); auto with zarith. rewrite Zpower_nat_is_exp. replace (Zpower_nat radix 1) with 2%Z; auto with zarith. assert (1 <= Zpower_nat radix (pred precision) + Zpower_nat radix (pred (pred precision)))%Z; auto with zarith. apply Z.le_trans with (Zpower_nat radix (pred precision)+0)%Z; auto with zarith. apply Z.le_trans with (Zpower_nat radix (pred precision))%Z; auto with zarith. apply Zpower_NR1; unfold radix; auto with zarith. apply Zplus_le_compat_l. apply Zpower_NR0; unfold radix; auto with zarith. elim J2; rewrite <- J5; auto. unfold FtoRradix, FtoR; simpl. unfold Zminus; repeat rewrite plus_IZR; simpl. repeat rewrite Zpower_nat_Z_powerRZ. repeat rewrite inj_pred; auto with zarith; unfold Z.pred. repeat rewrite powerRZ_add; auto with real zarith; simpl. unfold radix; ring_simplify (2*1)%R; field; auto with real. assert (0 < 4)%R;[apply Rlt_le_trans with 2%R|idtac]; auto with real. intros. elim H7; intros w1 T1; elim T1; intros W11 W12; clear H7 T1. apply Rle_lt_trans with w1. apply Rle_trans with (Rabs u);[apply RRle_abs|idtac];unfold FtoRradix. apply RoundAbsMonotoner with bo precision (EvenClosest bo radix precision) (3*Rabs t)%R; auto with zarith. apply EvenClosestRoundedModeP; auto. fold FtoRradix; rewrite <- dDef; rewrite dexact. rewrite Rabs_right. rewrite Rabs_right. rewrite H5; rewrite H6. apply Rle_trans with (w1-powerRZ radix (Fexp q))%R. rewrite W12; right; ring_simplify. unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; simpl. unfold radix; ring_simplify (2*1)%R; field; auto with real. apply Rle_trans with (w1-0)%R; auto with real. unfold Rminus; apply Rplus_le_compat_l; auto with real zarith. apply Ropp_le_contravar. apply powerRZ_le, IZR_lt; auto with zarith. apply Rle_ge; apply Rplus_le_reg_l with q. ring_simplify; auto with real. apply Rle_ge; apply Rle_trans with (3*0)%R; auto with real. apply Rmult_le_compat_l; auto with real. apply Rabs_pos. assert (exists w2:float, Fbounded bo w2 /\ (FtoRradix w2=powerRZ radix (Fexp q)* (powerRZ radix precision+powerRZ radix (precision-1)))%R). exists (Float (Zpower_nat radix (pred precision)+Zpower_nat radix (pred (pred precision))) (Fexp q+1)). split;[split; simpl|idtac]. rewrite Z.abs_eq; auto with zarith. rewrite pGivesBound; apply Z.lt_le_trans with (Zpower_nat radix (pred precision) + Zpower_nat radix (pred precision))%Z. apply Zplus_lt_compat_l; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. pattern precision at 3; replace precision with (1+pred precision); auto with zarith. rewrite Zpower_nat_is_exp. replace (Zpower_nat radix 1) with 2%Z; auto with zarith. apply Z.add_nonneg_nonneg; apply Zpower_NR0; unfold radix; auto with zarith. elim J2; rewrite <- J5; auto. unfold FtoRradix, FtoR; simpl. unfold Zminus; repeat rewrite plus_IZR; simpl. repeat rewrite Zpower_nat_Z_powerRZ. repeat rewrite inj_pred; auto with zarith; unfold Z.pred. repeat rewrite powerRZ_add; auto with real zarith; simpl. ring_simplify (2*1)%R; field; auto with real. assert (0 < 4)%R;[apply Rlt_le_trans with 2%R|idtac]; auto with real. elim H7; intros w2 T1; elim T1; intros W21 W22; clear H7 T1. apply Rlt_le_trans with w2. rewrite W12; rewrite W22; apply Rmult_lt_compat_l; auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. unfold Rminus; rewrite Rplus_assoc. apply Rplus_lt_compat_l; auto with real zarith. apply Rlt_le_trans with (powerRZ radix (precision - 1) + -0)%R; auto with real. right; ring. assert (0 <= p+q)%R. apply Rle_trans with (0+0)%R;auto with real; apply Rplus_le_compat. apply P_positive with bo precision b b'; auto. left; apply Q_positive with bo precision b b' p; auto. apply Rle_trans with (Rabs v). unfold FtoRradix; apply RoundAbsMonotonel with bo precision (EvenClosest bo radix precision) (p+q)%R;auto with zarith. apply EvenClosestRoundedModeP; auto. fold FtoRradix; rewrite Rabs_right; auto with real. apply Rle_trans with (w2+0)%R; auto with real zarith. apply Rle_trans with (w2+powerRZ radix (Fexp q))%R; auto with real zarith. apply Rplus_le_compat_l. apply powerRZ_le, IZR_lt; auto with zarith. rewrite W22; rewrite H5; rewrite H6; right;ring. rewrite Rabs_right; auto with real; apply Rle_ge. unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (p+q)%R; auto. apply EvenClosestRoundedModeP; auto. intros P. assert (p=Float (pPred (vNum bo)) (Fexp q)). rewrite <- FPredSuc with bo radix precision p; auto with zarith. 2: left; auto. replace (FSucc bo radix precision p) with qq. rewrite FPredSimpl2; auto with zarith. replace (Z.pred (Fexp qq)) with (Fexp q); auto. rewrite J5; unfold Z.pred; auto with zarith. rewrite J5; assert (-dExp bo <= Fexp q)%Z; auto with zarith; apply Fq. apply FcanonicUnique with radix bo precision; auto with zarith real. left; auto. apply FSuccCanonic; auto with zarith. left; auto. fold FtoRradix; rewrite J1; auto with real. contradict M. rewrite H3; simpl; auto with zarith. intros M. apply Rle_trans with (Rabs (-(dp-dq)))%R. unfold delta; replace (d - (b * b' - a * c))%R with (-(dp-dq))%R; auto with real. rewrite dexact; rewrite dpEq; rewrite dqEq; ring. rewrite Rabs_Ropp. unfold Rminus; apply Rle_trans with (Rabs dp + Rabs (-dq))%R;[apply Rabs_triang|rewrite Rabs_Ropp]. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (2*Rabs dp + 2*Rabs dq)%R;[right; simpl; ring|idtac]. apply Rle_trans with (Fulp bo radix precision p+Fulp bo radix precision q)%R; [apply Rplus_le_compat|idtac]. rewrite dpEq; unfold FtoRradix; apply ClosestUlp; auto with zarith. elim Roundp; auto. rewrite dqEq; unfold FtoRradix; apply ClosestUlp; auto with zarith. elim Roundq; auto. repeat rewrite CanonicFulp; auto with zarith. 2: left; auto. 2: left; auto. rewrite M; unfold FtoR;simpl. apply Rle_trans with (2* powerRZ radix (Fexp p))%R;[right; ring|idtac]. apply Rmult_le_compat_l; auto with real. apply Rle_trans with (powerRZ radix (Fexp d+1));[idtac| rewrite powerRZ_add; auto with real zarith; rewrite powerRZ_1; unfold radix; right; ring]. apply Rle_powerRZ; auto with real. assert (Fexp p-1 <= Fexp d)%Z; auto with zarith. assert (exists f:float, (Fexp f=Fexp p-1)%Z /\ (FtoRradix f=powerRZ radix (precision-2+Fexp p))%R /\ Fnormal radix bo f). exists (Float (nNormMin radix precision) (Fexp p -1)). split;simpl; auto with zarith. split;[unfold FtoRradix, FtoR, nNormMin; simpl|idtac]. rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith. rewrite <- powerRZ_add; auto with real zarith. replace (Z.pred precision + (Fexp p - 1))%Z with (precision - 2 + Fexp p)%Z; [auto with real|unfold Z.pred; ring]. split;[split;simpl; auto with zarith|idtac]. rewrite Z.abs_eq; auto with zarith. apply ZltNormMinVnum; auto with zarith. assert (0 < nNormMin radix precision)%Z; auto with zarith. apply nNormPos; auto with zarith. simpl (Fnum (Float (nNormMin radix precision) (Fexp p - 1))). rewrite <- PosNormMin with radix bo precision; auto with zarith. elim H1; intros f H1'; elim H1'; intros K1 H2; elim H2; intros K2 K3;clear H1' H1 H2. rewrite <- K1. apply Fcanonic_Rle_Zle with radix bo precision; auto with zarith. left; auto. fold FtoRradix; rewrite dexact; rewrite K2. rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith]. rewrite Rabs_right. 2:apply Rle_ge;apply Rplus_le_reg_l with q. 2: ring_simplify; auto with real. apply Rmult_le_reg_l with 3%R; auto with real. apply Rle_trans with ((2*powerRZ radix (precision-1+Fexp p))*(1-powerRZ radix (-precision)))%R. replace (powerRZ radix (precision - 1 + Fexp p)) with (2*powerRZ radix (precision - 2 + Fexp p))%R; [idtac|unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; simpl]. 2: unfold radix; ring_simplify (2*1)%R; field; auto with real. apply Rle_trans with ((2*2* (1 - powerRZ radix (- precision)))* powerRZ radix (precision - 2 + Fexp p))%R;[idtac|right; ring]. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. apply Rplus_le_reg_l with (-3+4*powerRZ radix (- precision))%R. ring_simplify. apply Rle_trans with (powerRZ radix (2+-precision)). rewrite powerRZ_add; auto with real zarith; unfold powerRZ at 2. simpl; unfold radix; right; ring. apply Rle_trans with (powerRZ radix 0); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; unfold radix; auto with zarith. 2: apply powerRZ_le; try apply IZR_lt; auto with zarith. assert (0 < (1 - powerRZ radix (- precision)))%R. apply Rplus_lt_reg_r with (powerRZ radix (- precision)). ring_simplify. replace 1%R with (powerRZ radix 0); [ auto with real zarith | simpl in |- *; auto ]. apply Rlt_powerRZ; try apply IZR_lt; auto with zarith. apply Rle_trans with (v* (1 - powerRZ radix (- precision)))%R. apply Rmult_le_compat_r; auto with real. assert (H3: exists g:float, Fbounded bo g /\ (FtoRradix g= 2 * powerRZ radix (precision - 1 + Fexp p))%R). exists (Float 1%Z (Fexp p +precision))%Z. split;[split; simpl; auto with zarith|idtac]. apply vNumbMoreThanOne with radix precision; auto with zarith. unfold FtoRradix, FtoR; simpl;unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith. simpl; unfold radix; ring_simplify (2*1)%R; field; auto with real. clear K1 K2 K3 f; elim H3; intros g H1'; elim H1'; intros K1 K2; clear H3 H1'. rewrite <- K2; unfold FtoRradix. apply EvenClosestMonotone2 with bo precision g (p+q)%R; auto with real zarith. rewrite K2; apply Rle_trans with ( powerRZ radix (precision - 1 + Fexp p)+ powerRZ radix (precision - 1 + Fexp p))%R;[right; ring|idtac]. assert (forall f:float, Fnormal radix bo f -> (0 <= f)%R -> (powerRZ radix (precision - 1 + Fexp f) <= f)%R). intros f Hf Hf'; rewrite powerRZ_add; auto with real zarith. unfold FtoRradix, FtoR; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le; try apply IZR_lt; auto with zarith. elim Hf; intros. apply Rmult_le_reg_l with (radix); auto with real zarith. apply Rle_trans with (Zpos (vNum bo)). rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ. unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl. ring_simplify (2*1)%R; right; field; auto with real. apply Rle_trans with (Z.abs (radix * Fnum f)); try apply IZR_le; auto with real zarith. rewrite Zabs_Zmult; repeat rewrite Z.abs_eq; auto with real zarith. rewrite mult_IZR; auto with real zarith. apply LeR0Fnum with radix; auto with real zarith. unfold radix; auto with zarith. apply Rplus_le_compat;[apply H2; auto|idtac]. apply P_positive with bo precision b b'; auto. rewrite <- M; apply H2; auto. left; apply Q_positive with bo precision b b' p; auto. unfold FtoRradix; apply RoundedModeProjectorIdem with bo; auto. apply EvenClosestRoundedModeP; auto with zarith. apply Rmult_le_reg_l with (/(1 - powerRZ radix (- precision)))%R; auto with real. apply Rle_trans with (FtoRradix v);[right; field; auto with real|idtac]. replace (3 * (p - q))%R with (Rabs (3*Rabs t)). apply Rle_trans with (Rabs (3*Rabs t) / (1 - powerRZ radix (- precision)))%R; [idtac|right; unfold Rdiv; ring]. apply Rle_trans with (Rabs v);[apply RRle_abs|idtac]. rewrite IneqEq. apply RoundLeNormal; auto. elim Roundu; auto. rewrite <- dDef; rewrite dexact; auto. rewrite Rabs_right;[idtac|apply Rle_ge]. rewrite Rabs_right;[idtac|apply Rle_ge]; auto with real. apply Rplus_le_reg_l with q. ring_simplify; auto with real. apply Rle_trans with (0*0)%R; auto with real; apply Rmult_le_compat; auto with real. apply Rabs_pos. intros M. apply Rle_trans with (Rabs (-(dp-dq)))%R. unfold delta; replace (d - (b * b' - a * c))%R with (-(dp-dq))%R; auto with real. rewrite dexact; rewrite dpEq; rewrite dqEq; ring. rewrite Rabs_Ropp. apply Rle_trans with (3 / 2 * Rmin (Fulp bo 2 precision p) (Fulp bo 2 precision q))%R. apply dp_dq_le with a b b' c; auto. replace (Rmin (Fulp bo 2 precision p) (Fulp bo 2 precision q)) with (Fulp bo 2 precision q). apply Rmult_le_compat; auto with real zarith. lra. unfold Fulp; auto with real zarith. apply powerRZ_le; try apply IZR_lt; auto with zarith. lra. repeat rewrite CanonicFulp; auto with zarith. right; rewrite M; auto with real. left; auto. repeat rewrite CanonicFulp; auto with zarith. 2: left; auto. 2: left; auto. rewrite Rmin_comm. unfold Rmin. case (Rle_dec (FtoR 2 (Float 1 (Fexp q))) (FtoR 2 (Float 1 (Fexp p)))); auto with real. intros N. absurd (Fexp q <= Fexp p)%Z. assert (Fexp p < Fexp q)%Z; auto with zarith. apply Zlt_powerRZ with radix; auto with real zarith. apply Rle_lt_trans with (FtoR 2 (Float 1 (Fexp p))); [right; unfold FtoR, radix; simpl; ring|idtac]. apply Rlt_le_trans with (FtoR 2 (Float 1 (Fexp q))); auto with real. right; unfold FtoR, radix; simpl; ring. apply Fcanonic_Rle_Zle with radix bo precision; auto with real zarith. left; auto. left; auto. fold FtoRradix; rewrite Rabs_right. rewrite Rabs_right; auto with real. apply Rle_ge; apply P_positive with bo precision b b'; auto. apply Rle_ge; left; apply Q_positive with bo precision b b' p; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz