proposition: Lemma Veltkamp_aux: (Rabs (x-hx) <= (powerRZ radix (s+Fexp x)) /2)%R /\ (exists hx':float, (FtoRradix hx'=hx) /\ (Closest b' radix x hx') /\ (s+Fexp x <= Fexp hx')%Z).
proof: Proof. generalize p'GivesBound;intros J. cut (powerRZ radix ((t - 1) + Fexp x) <= x)%R;[intros xGe|idtac]. 2:rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; unfold FtoRradix, FtoR. 2:apply Rmult_le_compat_r; auto with real zarith. 2: apply powerRZ_le, IZR_lt; lia. 2:apply Rmult_le_reg_l with radix; try apply IZR_lt; auto with real zarith. 2:apply Rle_trans with (powerRZ radix t). 2:unfold Zminus; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; right; field; auto with real. 2: apply IZR_neq; lia. 2:rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; rewrite <- mult_IZR; elim Nx; intros H H0. 2:rewrite Zabs_Zmult in H0; rewrite Z.abs_eq in H0; auto with zarith. 2:apply IZR_le; rewrite Z.abs_eq in H0; auto with zarith real. 2:apply LeR0Fnum with radix; auto with real. cut (Rabs (x - hx) <= (powerRZ radix (s + Fexp x))/2)%R;[intros|idtac]. 2:case eqEqual; intros L. 2:fold FtoRradix; rewrite hxExact. 2:replace (x-(p+q))%R with ((x-p)-q)%R;[apply Rmult_le_reg_l with 2%R; auto with real zarith|ring]. 2:apply Rle_trans with (powerRZ radix (Fexp q)). 2:unfold FtoRradix; apply ClosestExp with b t; auto with zarith. 2:rewrite L; simpl; right; field; auto with real. 2:elim L; auto. cut (exists v:float, (FtoRradix v=hx)/\(Fcanonic radix b' v)). intros T; elim T; intros v T'; elim T'; intros; clear T T'. split; auto. exists v; split; auto. cut (Fbounded b' v);[intros Fv|apply FcanonicBound with radix; auto]. cut (Rabs (x - FtoR radix v) <= (powerRZ radix (s + Fexp x))/2)%R;[intros|idtac]. 2: fold FtoRradix; rewrite H0; auto with real. split. apply ImplyClosest with (minus t s) (s+Fexp x)%Z; auto with zarith real. replace (s + Fexp x + (t - s)%nat - 1)%Z with ((t-1)+(Fexp x))%Z;[auto with real|rewrite inj_minus1; auto with zarith]. 2:elim Fx; unfold b'; simpl; auto with zarith. replace (s + Fexp x + (t - s)%nat - 1)%Z with ((t-1)+(Fexp x))%Z;[idtac|rewrite inj_minus1; auto with zarith]. fold FtoRradix; apply Veltkamp_aux_aux; auto. assert (s+Fexp x-1 < Fexp v)%Z; auto with zarith. assert (t-1+Fexp x < t-s+Fexp v)%Z; auto with zarith. apply Zlt_powerRZ with radix; try apply IZR_le; auto with real zarith. apply Rle_lt_trans with (FtoRradix v). apply Veltkamp_aux_aux; auto. apply Rle_lt_trans with (1:=RRle_abs v). unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith. unfold FtoR, Fabs; simpl. rewrite powerRZ_add. 2: apply IZR_neq; lia. apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. elim Fv; intros. apply Rlt_le_trans with (IZR (Zpos (vNum b'))); try apply IZR_lt; auto with real zarith. rewrite J; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. rewrite inj_minus1; auto with real zarith. cut (exists c:float, (FtoRradix c=hx) /\ (Fbounded b' c)). intros T; elim T; intros c H'; elim H'; intros. exists (Fnormalize radix b' (t-s) c); split. unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith. apply FnormalizeCanonic; auto with zarith. case eqEqual; intros L. generalize FboundedMbound; intros P. elim P with radix b' (t-s) (s+Fexp x)%Z (Fnum (Fplus radix p q)); auto with zarith; clear P. intros v H'; elim H'; intros ; clear H'. exists v; split; auto. rewrite hxExact; unfold FtoRradix; rewrite <- Fplus_correct; auto. rewrite H1; unfold FtoR; replace (s+ Fexp x)%Z with (Fexp (Fplus radix p q)); auto with real. unfold Fplus; simpl. rewrite Z.min_r;[auto|apply eqLeep]. 2: elim Fx; unfold b'; simpl; auto with zarith. cut ( (Z.abs (Fnum (Fplus radix p q)) < ((Zpower_nat radix (t - s))+1)))%Z; auto with zarith. apply lt_IZR. apply Rmult_lt_reg_l with (powerRZ radix (Fexp (Fplus radix p q))); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rle_lt_trans with (Rabs (Fplus radix p q)). unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold Fabs, FtoR; simpl; auto with real. unfold FtoRradix; rewrite Fplus_correct; auto. fold FtoRradix; rewrite <- hxExact. replace (FtoRradix hx) with (-(x-hx)+x)%R;[idtac|ring]. apply Rle_lt_trans with (Rabs (-(x-hx))+ Rabs(x))%R;[apply Rabs_triang|idtac]. rewrite Rabs_Ropp. apply Rle_lt_trans with ((powerRZ radix (s + Fexp x))/2 + Rabs x)%R; auto with real. apply Rlt_le_trans with ((powerRZ radix (s + Fexp x))/2 + (powerRZ radix (t+Fexp x)))%R. apply Rplus_lt_compat_l. unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. elim Fx; intros; rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; try apply IZR_lt; auto with real zarith. replace (Fexp (Fplus radix p q)) with (s+ Fexp x)%Z. 2:unfold Fplus; simpl. 2:rewrite Z.min_r;[auto|apply eqLeep]. rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl. rewrite Rmult_plus_distr_l; rewrite <- powerRZ_add. rewrite Rplus_comm; apply Rplus_le_compat. rewrite inj_minus1; auto with real zarith. ring_simplify ((s + Fexp x + (t - s)))%Z. rewrite Zplus_comm; auto with real. unfold Rdiv; apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (/1)%R; auto with real. apply IZR_neq; lia. elim L; clear L; intros L1 L2. cut (Fexp q=s+1+Fexp x)%Z;[intros L3|idtac]. 2:cut (q=Float (-(nNormMin radix t)) (s+1+Fexp x));[intros I; rewrite I; simpl; auto|idtac]. 2:apply FnormalUnique with radix b t; auto with zarith. 2:replace (Float (- nNormMin radix t) (s + 1 + Fexp x)) with (Fopp (Float (nNormMin radix t) (s + 1 + Fexp x))); [idtac|unfold Fopp; auto with zarith]. 2:apply FnormalFop; auto. 2:apply FnormalNnormMin; auto with zarith; elim Fx; auto with zarith. 2:fold FtoRradix; rewrite L1; unfold FtoRradix, FtoR, nNormMin; simpl. 2:rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ. 2:apply trans_eq with (-(powerRZ radix (pred t) * powerRZ radix (s + 1 + Fexp x)))%R; auto with real. 2:rewrite <- powerRZ_add. 2:replace ((pred t + (s + 1 + Fexp x)))%Z with (t + s + Fexp x)%Z; auto with real. 2:rewrite inj_pred; auto with zarith; unfold Z.pred; ring. 2: apply IZR_neq; lia. generalize FboundedMbound; intros P. elim P with radix b' (t-s) (Fexp (Fplus radix p q))%Z (Fnum (Fplus radix p q)); auto with zarith; clear P. intros v H'; elim H'; intros ; clear H'. exists v; split; auto. rewrite hxExact; unfold FtoRradix; rewrite <- Fplus_correct; auto. cut ( (Z.abs (Fnum (Fplus radix p q)) < ((Zpower_nat radix (t - s))+1)))%Z; auto with zarith. apply lt_IZR. apply Rmult_lt_reg_l with (powerRZ radix (Fexp (Fplus radix p q))); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rle_lt_trans with (Rabs (Fplus radix p q)). unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold Fabs, FtoR; simpl; auto with real. unfold FtoRradix; rewrite Fplus_correct; auto. fold FtoRradix; rewrite <- hxExact. replace (FtoRradix hx) with (-(x-hx)+x)%R;[idtac|ring]. apply Rle_lt_trans with (Rabs (-(x-hx))+ Rabs(x))%R;[apply Rabs_triang|idtac]. rewrite Rabs_Ropp. apply Rle_lt_trans with ((powerRZ radix (s + Fexp x))/2 + Rabs x)%R; auto with real. apply Rlt_le_trans with ((powerRZ radix (s + Fexp x))/2 + (powerRZ radix (t+Fexp x)))%R. apply Rplus_lt_compat_l. unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. elim Fx; intros; rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; try apply IZR_lt; auto with real zarith. replace (Fexp (Fplus radix p q)) with (s+ 1+Fexp x)%Z. 2:unfold Fplus; simpl. 2:rewrite Z.min_r;[auto|apply eqLeep]. rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl. rewrite Rmult_plus_distr_l; rewrite <- powerRZ_add. 2: apply IZR_neq; lia. rewrite Rplus_comm; apply Rplus_le_compat. rewrite inj_minus1; auto with real zarith. apply Rle_powerRZ; try apply IZR_le; lia. unfold Rdiv; apply Rmult_le_compat; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_powerRZ; try apply IZR_le; lia. apply Rle_trans with (/1)%R; auto with real. unfold b', Fplus; simpl. rewrite Z.min_r;[elim Nq; intros Fq T; elim Fq; auto|apply eqLeep]. Qed.
imports: Reals ZArith List PeanoNat Psatz