proposition: Theorem discri2: (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)) <= (Rabs (p-q)))%R -> (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. intros H1; unfold delta. apply Rle_trans with (1 * Fulp bo radix precision d)%R;[ring_simplify (1 * Fulp bo radix precision d)%R | unfold Fulp; auto with real zarith]. replace (d - (b * b' - a * c))%R with ((d-(t+s))+(t+s-b*b'+a*c))%R;[idtac|ring]. apply Rle_trans with (1:=Rabs_triang (d-(t+s))%R (t + s - b * b' + a * c)%R). apply Rmult_le_reg_l with 2%R; auto with real. rewrite Rmult_plus_distr_l. apply Rle_trans with (Fulp bo radix precision d+Fulp bo radix precision d)%R;[idtac|right;ring]. apply Rplus_le_compat. rewrite <- Rabs_Ropp; replace (- (d - (t + s)))%R with ((t+s)-d)%R;[idtac|ring]. unfold FtoRradix; apply ClosestUlp; auto. elim Roundd; auto. rewrite t_exact. replace (p - q + s - b * b' + a * c)%R with (-((dp-dq) - s))%R;[idtac|rewrite dpEq; rewrite dqEq; ring]. rewrite Rabs_Ropp; apply Rle_trans with (Fulp bo radix precision s). unfold FtoRradix; apply ClosestUlp; auto. elim Rounds; auto. rewrite FulpFabs; auto; rewrite FulpFabs with (f:=d); auto. apply LeFulpPos; auto with real zarith. apply absFBounded; auto. apply absFBounded; auto. rewrite Fabs_correct; auto with real. apply Rabs_pos. apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq)) (Rabs (t+s))%R; auto. 2: apply EvenClosestFabs; auto; left; auto. 2: apply EvenClosestFabs; auto; left; auto. cut (Rabs (dp - dq) <= (Rabs (p-q))/2)%R. intros H2; cut ((Rabs s) <= (Rabs t)/2)%R. intros H3; apply Rle_trans with (1:=H2). rewrite <- t_exact; apply Rle_trans with ((Rabs t)-(Rabs t)/2)%R. right; unfold Rdiv; field; auto with real. apply Rle_trans with ((Rabs t)-(Rabs s))%R; auto with real. unfold Rminus; apply Rplus_le_compat_l; auto with real. 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; auto with real. assert (t/2=(Float (Fnum t) (Z.pred (Fexp t))))%R. unfold FtoRradix, FtoR, Z.pred; simpl; rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 3; unfold radix; simpl; field. unfold Rdiv; rewrite <- (Rabs_right (/2)%R); auto with real. 2: apply Rle_ge; apply Rlt_le; auto with real. rewrite <- Rabs_mult; fold (Rdiv t 2%R). rewrite H; unfold FtoRradix; rewrite <- Fabs_correct; auto. rewrite <- Fabs_correct; auto. apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq))%R (Rabs (p-q)/2)%R; auto. apply EvenClosestFabs; auto; left; auto. replace (Rabs (p - q) / 2)%R with (FtoRradix (Fabs (Float (Fnum t) (Z.pred (Fexp t))))). unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto. apply EvenClosestRoundedModeP; auto. split; simpl; auto with zarith. rewrite Z.abs_eq; auto with zarith. apply Roundt. unfold FtoRradix; rewrite Fabs_correct; auto; fold FtoRradix; rewrite <- H. rewrite t_exact; unfold Rdiv; rewrite Rabs_mult; auto with real. rewrite (Rabs_right (/2)%R); auto with real. apply Rle_ge; apply Rlt_le; auto with real. apply Rle_trans with (1:=dp_dq_le). apply Rmult_le_reg_l with 2%R; auto with real; unfold Rdiv. rewrite <- Rmult_assoc. replace (2*(3*/2))%R with 3%R;[idtac|field; auto with real]. apply Rle_trans with (1:=H1). right; field; auto with real. apply Rmult_le_compat_r; auto with real. apply powerRZ_le, IZR_lt; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz