proposition: Theorem discri12: (q <= p)%R -> (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. intros M. assert (0 < 3)%R. apply Rlt_le_trans with 2%R; auto with real. assert (0 <= p-q)%R. apply Rplus_le_reg_l with q. ring_simplify; auto. assert (0 <= p)%R. apply P_positive with bo precision b b'; auto. assert (0 < (1 - powerRZ radix (- precision)))%R; auto with real. 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. assert (p-q <= Rsqr (1+powerRZ radix (-precision))/(1-powerRZ radix (-precision))*/3*(p+Rabs q))%R. apply Rle_trans with (Rabs (p-q));[apply RRle_abs|idtac]. apply Rle_trans with (Rabs t * (1 + powerRZ radix (- precision)))%R. apply RoundGeNormal; auto. elim Roundt; auto. apply Rle_trans with (((((p + Rabs q)/(1 - powerRZ radix (- precision))) * (1 + powerRZ radix (- precision)))*/3)* (1 + powerRZ radix (- precision)))%R; [idtac|right; unfold Rdiv, Rsqr; ring]. apply Rmult_le_compat_r; auto with real. apply Rle_trans with (0+0)%R; try apply Rplus_le_compat; auto with real zarith. apply powerRZ_le; try apply IZR_lt; auto with zarith. apply Rle_trans with ((3*Rabs t)*/3)%R; [right; field; auto with real| apply Rmult_le_compat_r; auto with real]. apply Rle_trans with (Rabs (3*Rabs t));[apply RRle_abs|idtac]. apply Rle_trans with (Rabs u * (1 + powerRZ radix (- precision)))%R. apply RoundGeNormal; auto; elim Roundu; auto. apply Rmult_le_compat_r; auto with real. apply Rle_trans with (0+0)%R; try apply Rplus_le_compat; auto with real zarith. apply powerRZ_le; try apply IZR_lt; auto with zarith. apply Rle_trans with (Rabs v). cut (0 <= u)%R. intros; repeat rewrite Rabs_right; auto with real. apply Rle_ge; apply Rle_trans with (FtoRradix u); auto with real. unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (3 * Rabs t)%R; auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. apply Rle_trans with(3*0)%R; auto with real; apply Rmult_le_compat; auto with real. apply Rabs_pos. apply Rle_trans with (Rabs (p+q) / (1 - powerRZ radix (- precision)))%R. unfold FtoRradix; apply RoundLeNormal with bo; auto with zarith real. elim Roundv; auto. unfold Rdiv; apply Rmult_le_compat_r; auto with real. apply Rle_trans with (Rabs p+Rabs q)%R;[apply Rabs_triang|idtac]. apply Rplus_le_compat_r; rewrite Rabs_right; auto with real. case (Rle_or_lt q 0); intros. absurd (p <= q)%R. apply Rlt_not_le; case M; auto with real. intros; absurd (0 < v)%R. apply Rle_not_lt. unfold FtoRradix; apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (p+q)%R; auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. apply Rle_trans with (1:=Case1); rewrite H5. right; ring_simplify (p-p)%R; rewrite Rabs_R0; ring. apply Rle_lt_trans with (FtoRradix u); auto with real. unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (3 * Rabs t)%R; auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. apply Rle_trans with(3*0)%R; auto with real; apply Rmult_le_compat; auto with real. apply Rabs_pos. apply Rmult_le_reg_l with (1- Rsqr (1 + powerRZ radix (- precision)) / (1 - powerRZ radix (- precision)) * / 3)%R. apply Rplus_lt_reg_r with (Rsqr (1 + powerRZ radix (- precision)) / (1 - powerRZ radix (- precision)) * / 3)%R. ring_simplify. apply Rmult_lt_reg_l with 3%R; auto with real. apply Rmult_lt_reg_l with (1 - powerRZ radix (- precision))%R; auto with real. apply Rle_lt_trans with (Rsqr (1 + powerRZ radix (- precision))); [right; field; auto with real|ring_simplify (3*1)%R]. apply Rplus_lt_reg_r with (-1+3*powerRZ radix (- precision))%R. apply Rle_lt_trans with (5* powerRZ radix (- precision) + powerRZ radix (- precision)* powerRZ radix (- precision))%R;[right; unfold Rsqr; ring|idtac]. apply Rlt_le_trans with 2%R;[idtac|right; ring]. apply Rlt_le_trans with (5 * powerRZ radix (- precision) + 3*powerRZ radix (- precision))%R; [apply Rplus_lt_compat_l; apply Rmult_lt_compat_r; auto with real zarith|idtac]. apply powerRZ_lt; try apply IZR_lt; auto with zarith. apply Rle_lt_trans with (powerRZ radix 1); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; try unfold radix; auto with zarith. simpl; unfold radix; ring_simplify (2*1)%R; auto with real. apply Rle_trans with (8 * powerRZ radix (- precision))%R;[right; ring|idtac]. replace 8%R with (powerRZ radix 3);[idtac|unfold powerRZ, radix; simpl; ring]. replace 2%R with (powerRZ radix 1);[idtac|unfold powerRZ, radix; simpl; ring]. rewrite <- powerRZ_add; auto with real zarith. apply Rle_powerRZ; try apply IZR_le; try unfold radix; auto with zarith. apply Rplus_le_reg_l with (-q+ ((Rsqr (1 + powerRZ radix (- precision)) / (1 - powerRZ radix (- precision)) * / 3) * p))%R. apply Rle_trans with (p-q)%R;[right; ring|idtac]. apply Rle_trans with (1:=H3). apply Rle_trans with (Rsqr (1 + powerRZ radix (- precision)) / (1 - powerRZ radix (- precision)) * / 3 * (p - q))%R; [idtac|right; ring]. replace (Rabs q) with (-q)%R;[right; ring|rewrite Rabs_left1; auto with real]. assert (forall f1:float, forall f2:float, forall i:Z, (0 <= i)%Z -> Fbounded bo f1 -> Fnormal radix bo f2 -> (Rabs f1 <= powerRZ radix i*Rabs f2)%R -> (Fulp bo radix precision f1 <= powerRZ radix i*Fulp bo radix precision f2)%R). intros. rewrite CanonicFulp with bo radix precision f2; auto with zarith. 2: left; auto. unfold FtoR; simpl; ring_simplify ((1 * powerRZ radix (Fexp f2)))%R. unfold Fulp; rewrite <- powerRZ_add; auto with real zarith. apply Rle_powerRZ; auto with real zarith. apply Z.le_trans with (Fexp (Float (Fnum f2) (i + Fexp f2))); auto with zarith. apply Fcanonic_Rle_Zle with radix bo precision; auto with real zarith. apply FnormalizeCanonic; auto with real zarith. elim H7; intros Y1 Y2; elim Y1; intros Y3 Y4. left; split; try split; simpl; auto with zarith. rewrite FnormalizeCorrect; auto with real zarith. fold FtoRradix; apply Rle_trans with (1:=H8). unfold FtoRradix; repeat rewrite <- Fabs_correct; auto. unfold FtoR, Rabs; simpl. rewrite powerRZ_add; auto with real zarith; right; ring. assert (2*q <= p)%R. apply Rmult_le_reg_l with 2%R; auto with real. apply Rplus_le_reg_l with (-3*q+p)%R. apply Rle_trans with (p+q)%R;[right; ring|apply Rle_trans with (1:=Case1)]. rewrite Rabs_right;[right; ring|apply Rle_ge; auto with real]. assert (q <= t)%R. apply Rle_trans with (Rabs t);[idtac|rewrite Rabs_right; auto with real]. 2:unfold FtoRradix; apply Rle_ge; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (p-q)%R; auto with zarith. 2: apply EvenClosestRoundedModeP; auto with zarith. unfold FtoRradix; apply RoundAbsMonotonel with bo precision (EvenClosest bo radix precision) (p-q)%R; auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. fold FtoRradix; rewrite Rabs_right;[idtac|apply Rle_ge]; auto with real. apply Rplus_le_reg_l with q; ring_simplify (q+(p-q))%R. apply Rle_trans with (2*q)%R; auto with real; right; ring. assert (Rabs s <= 3*Fulp bo radix precision q)%R. assert (exists f:float, Fbounded bo f /\ (FtoRradix f= 3 * Fulp bo radix precision q)%R). exists (Float 3 (Fexp q)). split;[split; simpl; auto with zarith|idtac]. apply Z.lt_le_trans with (Zpower_nat radix 2); auto with zarith. rewrite pGivesBound; auto with zarith. apply Zpower_nat_monotone_le; auto with zarith. apply Fq. rewrite CanonicFulp; auto with real zarith. 2: left; auto. unfold FtoRradix, FtoR; simpl; ring. elim H8; intros f T; elim T; intros; clear T H8. rewrite <- H10. unfold FtoRradix; apply RoundAbsMonotoner with bo precision (EvenClosest bo radix precision) (dp-dq)%R; auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. fold FtoRradix; 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; 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. apply Rle_trans with (5*Fulp bo radix precision q+Fulp bo radix precision q)%R; [apply Rplus_le_compat_r|rewrite H10; simpl; right; ring]. apply Rle_trans with (powerRZ radix 2*Fulp bo radix precision q)%R; [idtac|apply Rmult_le_compat_r; auto with real zarith]. 2: unfold Fulp; auto with real zarith. 2: apply powerRZ_le; try apply IZR_lt; auto with zarith. 2: unfold powerRZ, radix; simpl; lra. apply H5; auto with zarith. apply Rle_trans with (3*Rabs q)%R; [idtac|apply Rmult_le_compat_r; auto with real zarith]. 2: apply Rabs_pos. 2: unfold powerRZ, radix; simpl; lra. apply Rmult_le_reg_l with (/2)%R; auto with real. apply Rplus_le_reg_l with (/2*Rabs p)%R. apply Rle_trans with (Rabs p);[right; field; auto with real|idtac]. rewrite Rabs_right;auto with real. apply Rle_trans with (/2*(p+Rabs q) +Rabs q)%R;[idtac|right; field; auto with real]. apply Rle_trans with ((p-q)+Rabs q)%R. rewrite Rabs_right; [right; ring|apply Rle_ge;auto with real]. apply Rplus_le_compat_r. apply Rle_trans with (1:=H3). apply Rmult_le_compat_r; auto with real. apply Rle_trans with (0+0)%R; try apply Rplus_le_compat; auto with real. apply Rabs_pos. apply Rmult_le_reg_l with 2%R; auto with real. apply Rmult_le_reg_l with 3%R; auto with real. apply Rmult_le_reg_l with (1 - powerRZ radix (- precision))%R; auto with real. apply Rle_trans with (Rsqr (1 + powerRZ radix (- precision))*2)%R; [right; field; auto with real|idtac]. apply Rle_trans with (3*(1 - powerRZ radix (- precision)))%R;[idtac|right; field; auto with real]. apply Rplus_le_reg_l with (-2+3*powerRZ radix (- precision))%R. apply Rle_trans with (7*powerRZ radix (- precision) +2*powerRZ radix (- precision)*powerRZ radix (- precision))%R;[right; unfold Rsqr; ring|idtac]. apply Rle_trans with 1%R;[idtac|right; ring]. apply Rle_trans with (7 * powerRZ radix (- precision) + powerRZ radix (- precision))%R; [apply Rplus_le_compat_l|idtac]. replace 2%R with (powerRZ radix 1); auto with real zarith. repeat rewrite <- powerRZ_add; auto with real zarith. apply Rle_powerRZ; try apply IZR_le; try unfold radix; auto with zarith. simpl; unfold radix; ring. apply Rle_trans with (powerRZ radix 3 * powerRZ radix (- precision))%R; [unfold powerRZ at 3; unfold radix; right; simpl; ring | idtac]. rewrite <- powerRZ_add; auto with real zarith. apply Rle_trans with (powerRZ radix 0); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; try unfold radix; auto with zarith. assert (t-3*Fulp bo radix precision t <= Rabs d)%R. assert (exists f:float, Fbounded bo f /\ (FtoRradix f= t-3 * Fulp bo radix precision t)%R). exists (Float (Fnum t-3) (Fexp t)). split;[split; simpl; auto with zarith|idtac]. assert (0 < Fnum t)%Z;[apply LtR0Fnum with radix; auto with real zarith|idtac]. fold FtoRradix; apply Rlt_le_trans with q; auto. case (Zle_or_lt 0 (Fnum t-3)%Z); intros. rewrite Z.abs_eq; auto. apply Z.le_lt_trans with (Z.abs (Fnum t)); try lia. apply Ft. rewrite <- Zabs_Zopp; rewrite Z.abs_eq; auto with zarith. apply Z.lt_le_trans with 3%Z; auto with zarith. apply Z.le_trans with (nNormMin radix precision); auto with zarith. unfold nNormMin; apply Z.le_trans with (Zpower_nat radix 2). easy. apply Zpower_nat_monotone_le; auto with zarith. apply nNrMMimLevNum; auto with zarith. rewrite CanonicFulp; auto with zarith. 2: left; auto. unfold FtoRradix, FtoR, Zminus; simpl; rewrite plus_IZR; simpl; ring. elim H9; intros f T; elim T; intros; clear H9 T. rewrite <- H11. unfold FtoRradix; apply RoundAbsMonotonel with bo precision (EvenClosest bo radix precision) (t+s)%R; auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. fold FtoRradix; replace (t+s)%R with (t-(-s))%R;[idtac|ring]. apply Rle_trans with (Rabs t -Rabs (-s))%R;[idtac|apply Rabs_triang_inv]. rewrite Rabs_Ropp; rewrite Rabs_right. rewrite H11; unfold Rminus; apply Rplus_le_compat_l; auto with real. apply Ropp_le_contravar; apply Rle_trans with (1:=H8). apply Rmult_le_compat_l; auto with real. apply LeFulpPos; auto with real. apply Rle_ge; apply Rle_trans with q; auto with real. assert (Fulp bo radix precision t <= 2*Fulp bo radix precision d)%R. replace 2%R with (powerRZ radix 1); auto with real zarith. apply H5; auto with zarith. apply Rmult_le_reg_l with (/2)%R; auto with real. apply Rle_trans with (Rabs d);[idtac|right; unfold powerRZ, radix; simpl; field; auto with real]. apply Rle_trans with (2:=H9). rewrite Rabs_right;[idtac|apply Rle_ge; apply Rle_trans with q; auto with real]. apply Rle_trans with (t-t/2)%R;[right; field; auto with real|idtac]. unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_contravar. apply Rle_trans with (3*(Rabs (FtoR radix t) * powerRZ radix (Z.succ (- precision))))%R. apply Rmult_le_compat_l; auto with real. apply FulpLe2; auto with real zarith. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. fold FtoRradix; apply Rle_trans with (Rabs t*(3*powerRZ radix (Z.succ (- precision))))%R; [right; ring|idtac]. rewrite Rabs_right;[idtac|apply Rle_ge; apply Rle_trans with q; auto with real]. unfold Rdiv; apply Rmult_le_compat_l; auto with real. apply Rle_trans with q; auto with real. apply Rle_trans with (4*powerRZ radix (Z.succ (- precision)))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le; try apply IZR_lt; auto with zarith. replace 4%R with (powerRZ radix 2). 2: unfold powerRZ, radix; simpl; ring. replace (/2)%R with (powerRZ radix (-1)). 2: unfold powerRZ, radix; ring_simplify (2*1)%R; auto with real. 2: unfold powerRZ, radix; simpl; ring. rewrite <- powerRZ_add; auto with real zarith. unfold Z.succ; apply Rle_powerRZ; auto with real zarith. unfold delta. replace (d-(b*b'-a*c))%R with (-((t+s)-d)+-((p-q)-t)+-((dp-dq)-s))%R;[idtac|rewrite dpEq; rewrite dqEq; ring]. apply Rle_trans with (Rabs (- (t + s - d) + (- (p - q - t))) + Rabs (- (dp - dq - s)))%R; [apply Rabs_triang|rewrite Rabs_Ropp]. apply Rle_trans with (Rabs (- (t + s - d)) + Rabs (- (p - q - t)) + Rabs ((dp - dq - s)))%R; [apply Rplus_le_compat_r; apply Rabs_triang|repeat rewrite Rabs_Ropp]. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (2*Rabs ((t + s - d)) + 2*Rabs ((p - q - t)) + 2*Rabs ((dp - dq - s)))%R;[right; ring|idtac]. apply Rle_trans with (Fulp bo radix precision d+Fulp bo radix precision t +Fulp bo radix precision s)%R;[apply Rplus_le_compat|idtac]. apply Rplus_le_compat. unfold FtoRradix; apply ClosestUlp; auto with zarith; elim Roundd; auto. unfold FtoRradix; apply ClosestUlp; auto with zarith; elim Roundt; auto. unfold FtoRradix; apply ClosestUlp; auto with zarith; elim Rounds; auto. apply Rle_trans with (Fulp bo radix precision d + 2*Fulp bo radix precision d + Fulp bo radix precision s)%R; auto with real. apply Rle_trans with (Fulp bo radix precision d + 2 * Fulp bo radix precision d + Fulp bo radix precision d)%R;[idtac|right; simpl; ring]. apply Rplus_le_compat_l. rewrite FulpFabs with bo radix precision s; auto. rewrite FulpFabs with bo radix precision d; auto. apply LeFulpPos; auto with zarith real. apply absFBounded; auto. apply absFBounded; auto. rewrite Fabs_correct; auto with real zarith. apply Rabs_pos. repeat rewrite Fabs_correct; auto; fold FtoRradix. apply Rle_trans with (1:=H8); apply Rle_trans with (2:=H9). apply Rle_trans with (3 * Fulp bo radix precision t)%R. apply Rmult_le_compat_l; auto with real. apply LeFulpPos; auto with zarith real. apply Rplus_le_reg_l with (3* Fulp bo radix precision t)%R. ring_simplify (3 * Fulp bo radix precision t + (t - 3 * Fulp bo radix precision t))%R. apply Rle_trans with (6*Fulp bo radix precision t)%R;[right; ring|idtac]. apply Rle_trans with (6*(Rabs (FtoR radix t) * powerRZ radix (Z.succ (- precision))))%R. apply Rmult_le_compat_l; auto with real. apply FulpLe2; auto with real zarith. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. fold FtoRradix; apply Rle_trans with (Rabs t*(6*powerRZ radix (Z.succ (- precision))))%R; [right; ring|idtac]. rewrite Rabs_right;[idtac|apply Rle_ge; apply Rle_trans with q; auto with real]. apply Rle_trans with (t*1)%R; auto with real. apply Rmult_le_compat_l; auto with real. apply Rle_trans with q; auto with real. apply Rle_trans with (8*powerRZ radix (Z.succ (- precision)))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le; try apply IZR_lt; auto with zarith. replace 8%R with (powerRZ radix 3). 2: unfold powerRZ, radix; simpl; ring. replace 1%R with (powerRZ radix 0). 2: simpl; auto with real. rewrite <- powerRZ_add; auto with real zarith. apply Rle_powerRZ; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz