proposition: Theorem discri7: (dp < 0)%R -> (0 < dq)%R -> (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. intros L1 L2. unfold delta, FtoRradix; apply discri3 with p q t dp dq s; auto. assert (H0: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. cut (exists dp'':float, (Fexp dp''=Fexp dq' /\ (FtoRradix dp''=dp')%R /\ (Rabs (Fnum dp'') <= powerRZ radix (Z.pred precision))%R)). intros T; elim T; intros dp'' T1; elim T1; intros H4'' T2; elim T2; intros H5'' H6''; clear T T1 T2. assert ((Rabs (Fnum dp''-Fnum dq') < (powerRZ radix precision))%R \/ (((Rabs dp'')= (powerRZ radix (Z.pred (Fexp q))))%R /\ ((Rabs dq')= (powerRZ radix (Z.pred (Fexp q))))%R)). case H6''; intros. left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp'') (-(Fnum dq'))%R). rewrite Rabs_Ropp. apply Rlt_le_trans with ((powerRZ radix (Z.pred precision)) +(Rabs (Fnum dq')))%R; auto with real zarith. apply Rle_trans with ((powerRZ radix (Z.pred precision))+ (powerRZ radix (Z.pred precision)))%R; auto with real zarith. right; unfold Z.pred; repeat rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2 4; simpl; unfold radix; field. case H5'; intros. left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp'') (-(Fnum dq'))%R); rewrite Rabs_Ropp. apply Rle_lt_trans with ((powerRZ radix (Z.pred precision)) +(Rabs (Fnum dq')))%R ; auto with real zarith. apply Rlt_le_trans with ((powerRZ radix (Z.pred precision))+ (powerRZ radix (Z.pred precision)))%R; auto with real zarith. right; unfold Z.pred; repeat rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2 4; simpl; unfold radix; field. right; unfold FtoRradix, FtoR;repeat rewrite Rabs_mult. rewrite (Rabs_right (powerRZ radix (Fexp dp''))); try apply Rle_ge; auto with real zarith. 2: apply powerRZ_le, IZR_lt; auto with zarith. rewrite (Rabs_right (powerRZ radix (Fexp dq'))); try apply Rle_ge; auto with real zarith. 2: apply powerRZ_le, IZR_lt; auto with zarith. rewrite H; rewrite H0. repeat rewrite <- powerRZ_add; auto with real zarith. rewrite H4''; rewrite H4'; unfold Z.pred. ring_simplify (precision + -1 + (Fexp q - precision))%Z; ring_simplify (precision + -1 + (Fexp q - precision))%Z; ring_simplify (Fexp q+-1)%Z; auto with zarith real. case H; intros V; clear H. exists (Float (Fnum dp''-Fnum dq') (Fexp dq')). split;[split; auto with zarith|idtac]. simpl; apply lt_IZR. rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto. rewrite <- Rabs_Zabs; unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith. simpl; auto with zarith; apply H2'. fold radix; fold FtoRradix; rewrite dpEq; rewrite dqEq. rewrite <- H3'; rewrite <- H3;rewrite <- H5''. unfold FtoRradix, FtoR; simpl. unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR. rewrite H4''; ring. exists (Float (-1)%Z (Fexp q)). split;[split; simpl; auto with zarith|idtac]. rewrite pGivesBound; apply Z.le_lt_trans with (Zpower_nat radix 0); auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. apply Roundq. fold radix; fold FtoRradix; elim V; intros. replace (FtoRradix dp) with (-(-dp))%R;[idtac|ring]. rewrite <- (Rabs_left dp); auto with real. rewrite <- (Rabs_right dq); auto with real. 2: apply Rle_ge; auto with real. rewrite dpEq; rewrite <- H3; rewrite <- H5''; rewrite H. rewrite dqEq; rewrite <- H3'; rewrite H0. unfold FtoRradix, FtoR, Z.pred; simpl. repeat rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 3 5; simpl; unfold radix; field. assert (FtoRradix dp'=(Float (2*Fnum dp') (Z.pred (Fexp dp'))))%R. unfold FtoRradix, FtoR, Z.pred. apply trans_eq with ((2 * Fnum dp')%Z*(powerRZ radix (Fexp dp'+-1)))%R;[auto|idtac]. rewrite mult_IZR;rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 3; simpl; unfold radix; field. simpl; auto with real. exists (Float (2*Fnum dp') (Z.pred (Fexp dp'))); split. simpl; rewrite H4'; rewrite H4. rewrite q_eqExp; rewrite p_eqF; unfold Z.pred, Z.succ;simpl; auto with zarith. split; auto with real. apply Rmult_le_reg_l with (powerRZ radix (Z.pred (Fexp dp'))); auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. rewrite <- powerRZ_add; auto with real zarith. rewrite <- (Rabs_right (powerRZ radix (Z.pred (Fexp dp'))));auto with real. 2: apply Rle_ge; auto with real zarith. rewrite <- Rabs_mult. replace (powerRZ radix (Z.pred (Fexp dp')) * Fnum (Float (2 * Fnum dp') (Z.pred (Fexp dp'))))%R with (FtoRradix dp'); auto with real. 2: rewrite H; unfold FtoRradix, FtoR; simpl; auto with real. rewrite H3; rewrite <- dpEq. rewrite H4; unfold Z.pred;ring_simplify (Fexp p - precision + -1 + (precision + -1))%Z. rewrite Rabs_left; auto with real. apply Rmult_le_reg_l with 2%R; auto with real. apply Rplus_le_reg_l with (FtoRradix dp). ring_simplify (dp+2*(-dp))%R. rewrite <- Rabs_left; auto with real. assert (Fbounded bo (Float (Z.pred (Zpower_nat radix precision)) e)). split; auto with zarith. simpl; rewrite pGivesBound; lia. simpl; rewrite <- q_eqExp; apply Roundq; auto with zarith. rewrite <- Rabs_Ropp. replace (-dp)%R with (p-b*b')%R; [idtac|rewrite dpEq;ring]. elim Roundp; intros K1 K2; elim K1; intros K3 K4. apply Rle_trans with (Rabs ((Float (Z.pred (Zpower_nat radix precision)) e)-b*b')). unfold FtoRradix; apply K4; auto. clear K1 K2 K3 K4; rewrite Rabs_left1. rewrite dpEq; rewrite p_eqR. apply Rle_trans with (b*b'-(powerRZ radix precision -1)*(powerRZ radix e))%R. unfold FtoRradix, FtoR, Z.pred, radix; simpl. rewrite plus_IZR; simpl; right; ring_simplify. rewrite Zpower_nat_Z_powerRZ; auto with real zarith; simpl; ring. unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l. replace (Fexp p) with (Z.succ e);[unfold Z.succ|rewrite p_eqF; simpl; auto with zarith]. ring_simplify (e+1-2)%Z; unfold Zminus. repeat rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 6; simpl; unfold radix; right; field. apply Rplus_le_reg_l with (p-(Float (Z.pred (Zpower_nat radix precision)) e))%R. apply Rle_trans with (-(b*b'-p))%R;[right;ring|idtac]. rewrite <- dpEq; rewrite <- Rabs_left; auto with real. rewrite dpEq; apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix precision p). unfold FtoRradix; apply ClosestUlp; auto. elim Roundp; auto. rewrite CanonicFulp; auto;[idtac|left; auto]. replace (Fexp p) with (Z.succ e);[unfold Z.succ|rewrite p_eqF; simpl; auto with zarith]. rewrite p_eqR; unfold FtoRradix, FtoR, Z.pred; simpl. rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. repeat rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix;right; ring. apply powerRZ_le, IZR_lt; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz