proposition: Theorem discri5: (0 < dp*dq)%R -> (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. intros. unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto. assert (forall f1 f2 g : float, Fbounded bo f1 -> Fbounded bo f2 -> Closest bo 2 (FtoR 2 f1 * FtoR 2 f2) g -> (powerRZ (Zpos 2) (- dExp bo + 2 * precision - 1) <= Rabs (FtoR 2 f1 * FtoR 2 f2))%R -> Fcanonic 2 bo g -> exists s : float, Fbounded bo s /\ FtoR 2 s = (FtoR 2 f1 * FtoR 2 f2 - FtoR 2 g)%R /\ Fexp s = (Fexp g - precision)%Z /\ (Rabs (Fnum s) <= powerRZ (Zpos 2) (Z.pred precision))%R). apply errorBoundedMultClosest_Can; auto. fold radix in H0; fold FtoRradix in H0. elim H0 with (f1:=b) (f2:=b') (g:=p); auto with zarith real. intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4 H5; clear T2 T3 T4. 2: elim Roundp; auto. elim H0 with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear H0. intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4. 2: elim Roundq; auto. 2: left; auto. 2: left; auto. fold radix; fold FtoRradix; rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'. exists (Fminus radix dp' dq'); split. 2: unfold FtoRradix; rewrite Fminus_correct; auto with real. unfold Fminus, Fopp, Fplus; simpl. repeat rewrite H4'; repeat rewrite q_eqExp; repeat rewrite H4. replace (Fexp p) with (Z.succ e); [idtac|rewrite p_eqF; auto]. rewrite Z.min_r; auto with zarith. split; auto with zarith. simpl; unfold Z.succ. ring_simplify (e + 1 - precision - (e - precision))%Z; ring_simplify (e - precision - (e - precision))%Z. simpl. unfold nat_of_P, Zpower_nat; simpl. replace ( - Fnum dq' * 1)%Z with (- Fnum dq')%Z; [idtac|ring]. apply lt_IZR. rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto. rewrite <- Rabs_Zabs; rewrite plus_IZR;rewrite mult_IZR;rewrite Ropp_Ropp_IZR. assert (forall (x y z:R), (0 < x*y)%R -> (Rabs x <= z)%R -> (Rabs y <= z)%R -> (Rabs (2*x-y) < 2*z)%R). intros. unfold Rabs; case (Rcase_abs (2*x-y)%R); case (Rle_or_lt 0%R x); intros. case H7; intros; replace (- (2 * x - y))%R with (-(2)*x+y)%R by ring. apply Rlt_le_trans with (-(2)*0+y)%R; auto with real. apply Rplus_lt_compat_r; repeat rewrite Ropp_mult_distr_l_reverse. apply Ropp_lt_contravar; auto with real. ring_simplify (-(2)*0+y)%R; apply Rle_trans with z; auto with real. apply Rle_trans with (2:=H6); apply RRle_abs. apply Rle_trans with (1*z)%R; auto with real. apply Rmult_le_compat_r; auto with real. apply Rle_trans with (2:=H1); auto with real. apply Rabs_pos. contradict H0; rewrite <- H8; auto with real. ring_simplify (0*y)%R; auto with real. ring_simplify (- (2 * x - y))%R. apply Rlt_le_trans with (-2*x+0)%R;[apply Rplus_lt_compat_l|idtac]. apply Rmult_lt_reg_l with (-x)%R; auto with real. apply Rle_lt_trans with (-(x*y))%R; auto with real. apply Rlt_le_trans with (-0)%R; auto with real; right;ring. apply Rle_trans with (2*(-x))%R;[right;ring|apply Rmult_le_compat_l; auto with real]. apply Rle_trans with (2:=H1); rewrite <- Rabs_Ropp; apply RRle_abs. apply Rlt_le_trans with (2*x-0)%R;[unfold Rminus; apply Rplus_lt_compat_l|idtac]. apply Ropp_lt_contravar; apply Rmult_lt_reg_l with x; auto with real. case H7; auto with real. intros H8; contradict H0; rewrite <- H8; ring_simplify (0*y)%R; auto with real. ring_simplify (x*0)%R; auto with real. apply Rle_trans with (2*x)%R;[right;ring|apply Rmult_le_compat_l; auto with real]. apply Rle_trans with (2:=H1); apply RRle_abs. apply Rlt_le_trans with (2*0-y)%R; [unfold Rminus; apply Rplus_lt_compat_r; apply Rmult_lt_compat_l; auto with real|idtac]. apply Rle_trans with (-y)%R;[right;ring|apply Rle_trans with z]. apply Rle_trans with (2:=H6); rewrite <- Rabs_Ropp; apply RRle_abs. apply Rle_trans with (1*z)%R;[right;ring|apply Rmult_le_compat_r; auto with real]. apply Rle_trans with (2:=H1); auto with real. apply Rabs_pos. replace (Fnum dp' * Zpos 2+-Fnum dq')%R with (2*(Fnum dp')-Fnum dq')%R; auto with real zarith. apply Rlt_le_trans with (2*powerRZ radix (Z.pred precision))%R. apply H0; auto. apply Rmult_lt_reg_l with (powerRZ radix (Fexp dq')); auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. apply Rmult_lt_reg_l with (powerRZ radix (Fexp dp')); auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. apply Rle_lt_trans with 0%R;[right;ring|apply Rlt_le_trans with (1:=H)]. rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'. unfold FtoRradix, FtoR; right; ring. right; unfold Z.pred, Zminus; rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2; simpl; unfold radix; field. simpl; ring. simpl;rewrite <-q_eqExp; rewrite <- H4'; auto with zarith. apply H2'. Qed.
imports: Reals ZArith List PeanoNat Psatz