proposition: Lemma VeltkampEven1: (Even radix) ->(exists hx':float, (FtoRradix hx'=hx) /\ (EvenClosest b' radix (t-s) x hx')).
proof: Proof. intros I. 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; auto with real zarith. 2: apply IZR_lt; lia. 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. 2:apply IZR_le; rewrite Zabs_Zmult in H0; rewrite Z.abs_eq in H0; auto with zarith. 2: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) /\ ((FNeven b' radix (t-s) v) \/ (Fexp v <= s+Fexp x)%Z)). intros T;elim T; intros v T'; elim T'; intros H0 T''; elim T''; intros H1 L; clear T T' T''. 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. case H2; intros; clear H2. unfold EvenClosest. cut (Closest b' radix x v /\ (forall g : float, Closest b' radix x g -> FtoR radix v = FtoR radix g)). intros T; elim T; split; auto. right; intros; apply sym_eq; auto. apply ImplyClosestStrict2 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 with real. cut (Closest b' radix x v);[intros|idtac]. 2: apply ImplyClosest with (minus t s) (s+Fexp x)%Z; auto with zarith real. 2: rewrite inj_minus1; auto with zarith real. 2: replace (s + Fexp x + (t - s) - 1)%Z with (t - 1 + Fexp x)%Z; [auto with real|ring]. 2: rewrite inj_minus1; auto with zarith real. 2: replace (s + Fexp x + (t - s) - 1)%Z with (t - 1 + Fexp x)%Z; [auto with real|ring]. 2: fold FtoRradix; apply Veltkamp_aux_aux; auto with real. 2: elim Fx; unfold b'; simpl; auto with zarith. split; auto. left. case L; clear L; intros L; auto. unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith. case (Zle_lt_or_eq _ _ L); intros H4; clear L;unfold Feven. cut (exists m:Z, (Fnum v=radix*m)%Z);[intros T; elim T; intros m H5|idtac]. rewrite H5; apply EvenMult1; auto. exists (Fnum p*Zpower_nat radix ((Z.abs_nat (Fexp p-Fexp v-1)))+ Fnum q*Zpower_nat radix ((Z.abs_nat (Fexp q-Fexp v-1))))%Z. apply eq_IZR. rewrite mult_IZR; rewrite plus_IZR; repeat rewrite mult_IZR. repeat rewrite Zpower_nat_Z_powerRZ. generalize eqGe; generalize eqLeep; intros. repeat rewrite <- Zabs_absolu. repeat rewrite Z.abs_eq; auto with zarith. unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. repeat rewrite powerRZ_Zopp; try apply IZR_neq; auto with real zarith. rewrite powerRZ_1. apply Rmult_eq_reg_l with (powerRZ radix (Fexp v)); auto with real zarith. apply trans_eq with (FtoRradix v);[unfold FtoRradix, FtoR; ring|idtac]. rewrite H0; rewrite hxExact; unfold FtoRradix, FtoR; field. split; apply Rgt_not_eq; try apply IZR_lt; auto with zarith. apply powerRZ_lt, IZR_lt; lia. apply Rgt_not_eq, powerRZ_lt, IZR_lt; lia. replace (Fnum v) with (Fnum p*Zpower_nat radix ((Z.abs_nat (Fexp p-Fexp v)))+ Fnum q*Zpower_nat radix ((Z.abs_nat (Fexp q-Fexp v))))%Z. 2:apply eq_IZR. 2:rewrite plus_IZR; repeat rewrite mult_IZR. 2:repeat rewrite Zpower_nat_Z_powerRZ. 2: generalize eqGe; generalize eqLeep; intros. 2:repeat rewrite <- Zabs_absolu. 2:repeat rewrite Z.abs_eq; auto with zarith. 2:unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. 2:repeat rewrite powerRZ_Zopp; try apply IZR_neq; auto with real zarith. 2:apply Rmult_eq_reg_l with (powerRZ radix (Fexp v)); auto with real zarith. 2:apply trans_eq with (FtoRradix v);[idtac|unfold FtoRradix, FtoR; ring]. 2:rewrite H0; rewrite hxExact; unfold FtoRradix, FtoR; field. 2: apply Rgt_not_eq, powerRZ_lt, IZR_lt; lia. 2: apply Rgt_not_eq, powerRZ_lt, IZR_lt; lia. cut (exists eps:R, ((eps=1)%R \/ (eps=-1)%R) /\ (FtoRradix x=v+ eps*(powerRZ radix (s + Fexp x))/2)%R). intros T; elim T; intros eps T'; elim T'; intros Heps1 Heps2; clear T T'. apply EvenPlus1. rewrite H4. cut ((Fexp p=1+s+Fexp x)%Z \/ (Fexp p=s+Fexp x)%Z);[intros T; case T; clear T; intros|idtac]. rewrite H5; ring_simplify (1 + s + Fexp x - (s + Fexp x))%Z. replace (Zpower_nat radix (Z.abs_nat 1))%Z with radix%Z. apply EvenMult2; auto. unfold Zpower_nat; simpl; auto with zarith. rewrite H5;ring_simplify ( (s + Fexp x - (s + Fexp x)))%Z. unfold Zpower_nat; simpl;ring_simplify (Fnum p * 1)%Z. cut (FNeven b radix t p). unfold FNeven;rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. apply ClosestImplyEven_int with (x * (powerRZ radix s + 1))%R ((Fnum v)*(powerRZ radix s)+(Fnum v)+eps*(powerRZ radix s)/2+(eps-1)/2)%R; auto with zarith. left; auto. apply pPos. rewrite Heps2; unfold FtoRradix, FtoR; rewrite H4; rewrite H5. unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl. field; auto with real. elim I; intros rradix I'. cut ((powerRZ radix s)/2=(rradix*Zpower_nat radix (pred s))%Z)%R;[intros K|idtac]. case Heps1; intros T; rewrite T. exists (Fnum v*(Zpower_nat radix s)+Fnum v+rradix*Zpower_nat radix (pred s))%Z. repeat rewrite plus_IZR; rewrite mult_IZR. rewrite <- K. rewrite Zpower_nat_Z_powerRZ; unfold Rdiv; ring. exists (Fnum v*(Zpower_nat radix s)+Fnum v+-(rradix*Zpower_nat radix (pred s))-1)%Z. unfold Zminus; repeat rewrite plus_IZR; rewrite mult_IZR; rewrite Ropp_Ropp_IZR. rewrite <- K. simpl; rewrite Zpower_nat_Z_powerRZ; unfold Rdiv; field; auto with real. rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith. unfold Z.pred, Zminus; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl. rewrite I'; rewrite mult_IZR; simpl; field. apply IZR_neq; auto with real zarith. generalize eqLeep; generalize epLe; generalize eqLe; generalize eqGe; intros. cut (s+Fexp x <= Fexp p)%Z; auto with zarith. intros T; case (Zle_lt_or_eq _ _ T); auto with zarith. cut ((Fexp q=1+s+Fexp x)%Z \/ (Fexp q=s+Fexp x)%Z);[intros T; case T; clear T; intros|idtac]. rewrite H4; rewrite H5; ring_simplify (1 + s + Fexp x - (s + Fexp x))%Z. replace (Zpower_nat radix (Z.abs_nat 1))%Z with radix%Z. apply EvenMult2; auto. unfold Zpower_nat; simpl; auto with zarith. rewrite H4; rewrite H5;ring_simplify ( (s + Fexp x - (s + Fexp x)))%Z. unfold Zpower_nat; simpl;ring_simplify (Fnum q * 1)%Z. 2: generalize eqLeep; generalize epLe; generalize eqLe; generalize eqGe; intros. 2: case (Zle_lt_or_eq _ _ H5); auto with zarith. cut (FNeven b radix t q). unfold FNeven;rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. replace q with (Fopp (Fopp q)). apply FNevenFop; auto with zarith. apply ClosestImplyEven_int with (-(x-p))%R ((Fnum p)*(powerRZ radix ((Fexp p)-s-(Fexp x)))-(Fnum v)-(eps+1)/2)%R; auto with zarith. generalize EvenClosestSymmetric; unfold SymmetricP; intros; auto with zarith. left; apply FnormalFop; auto. rewrite Fopp_correct; auto; generalize qNeg; auto with real. simpl; rewrite H5. apply trans_eq with ((powerRZ radix (s + Fexp x) * powerRZ radix (Fexp p - s - Fexp x))*Fnum p+ (powerRZ radix (s + Fexp x) * ( - Fnum v - (eps + 1) / 2 + 1 / 2)))%R;[idtac|ring]. rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith; ring_simplify (s + Fexp x + (Fexp p - s - Fexp x))%Z. rewrite Heps2; unfold FtoRradix, FtoR; rewrite H4. unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl. field; auto with real. case Heps1; intros T; rewrite T. exists (Fnum p*(Zpower_nat radix (Z.abs_nat (Fexp p-(s+Fexp x))))-Fnum v-1)%Z. unfold Zminus; repeat rewrite plus_IZR; rewrite mult_IZR; repeat rewrite Ropp_Ropp_IZR; simpl. repeat rewrite Zpower_nat_Z_powerRZ; replace (Z_of_nat (Z.abs_nat (Fexp p + - (s + Fexp x)))) with (Fexp p + - s + - Fexp x)%Z;[unfold Rdiv; field; auto with real|idtac]. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. generalize eqLeep; generalize epLe; generalize eqLe; generalize eqGe; intros; auto with zarith. exists (Fnum p*(Zpower_nat radix (Z.abs_nat (Fexp p-(s+Fexp x))))-Fnum v)%Z. unfold Zminus; repeat rewrite plus_IZR; rewrite mult_IZR; repeat rewrite Ropp_Ropp_IZR; simpl. repeat rewrite Zpower_nat_Z_powerRZ; replace (Z_of_nat (Z.abs_nat (Fexp p + - (s + Fexp x)))) with (Fexp p + - s + - Fexp x)%Z;[unfold Rdiv; field; auto with real|idtac]. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. generalize eqLeep; generalize epLe; generalize eqLe; generalize eqGe; intros; auto with zarith. unfold Fopp; destruct q; simpl; auto with zarith. ring_simplify (-(-Fnum0))%Z; auto. fold FtoRradix in H3; case (Rcase_abs (x-v)%R); intros. rewrite Rabs_left in H3; auto. exists (-1)%R; split; auto with real. apply trans_eq with (v + -1 * (powerRZ radix (s + Fexp x) / 2))%R. rewrite <- H3; ring. unfold Rdiv; ring. rewrite Rabs_right in H3; auto. exists (1)%R; split; auto with real. apply trans_eq with (v + 1 * (powerRZ radix (s + Fexp x) / 2))%R. rewrite <- H3; ring. unfold Rdiv; ring. cut (exists v : float, FtoRradix v = hx /\ Fbounded b' v /\ (FNeven b' radix (t - s) v \/ (Fexp v <= s + Fexp x)%Z)). intros T; elim T; intros v T1; elim T1; intros H1 T2; elim T2; intros H2 H3; clear T T1 T2. exists (Fnormalize radix b' (t-s) v). split. rewrite <- H1; unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith. split. apply FnormalizeCanonic; auto with zarith. case H3; intros. left; unfold FNeven; unfold FNeven in H0. rewrite FcanonicFnormalizeEq; auto with zarith. apply FnormalizeCanonic; auto with zarith. right; apply Z.le_trans with (2:=H0). apply FcanonicLeastExp with radix b' (t-s); auto with zarith. rewrite FnormalizeCorrect; auto with real zarith. apply FnormalizeCanonic; auto with zarith. cut (exists m:Z, (FtoRradix hx=m*powerRZ radix (s+Fexp x))%R /\ ((Z.abs m) <= Zpos (vNum b'))%Z ). intros T; elim T; intros m T'; elim T'; intros; clear T T'. case (Zle_lt_or_eq _ _ H1); intros H2. exists (Float m (s+Fexp x)). split;[rewrite H0; unfold FtoRradix, FtoR; simpl; ring|split]. split; simpl; elim Fx; auto with zarith. right; simpl; auto with zarith. exists (Float (nNormMin radix (t-s)) (s+1+Fexp x)). cut (Fcanonic radix b' (Float (nNormMin radix (t-s)) (s+1+Fexp x))). 2: apply FcanonicNnormMin; elim Fx; unfold b'; simpl; auto with zarith. intros H3; split. rewrite H0; unfold FtoRradix, FtoR, nNormMin; simpl. rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith. rewrite Z.abs_eq in H2. rewrite H2; rewrite J;rewrite Zpower_nat_Z_powerRZ. repeat rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. replace (Z.pred (t - s)%nat + (s + 1 + Fexp x))%Z with ((t - s)%nat + (s + Fexp x))%Z; auto with real zarith; unfold Z.pred; ring. apply le_IZR. apply Rmult_le_reg_l with (powerRZ radix (s + Fexp x)); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rle_trans with 0%R;[simpl; right; ring|rewrite Rmult_comm]. rewrite <- H0; rewrite hxExact. apply Rplus_le_reg_l with (-q)%R. ring_simplify; unfold FtoRradix; rewrite <- Fopp_correct. generalize ClosestMonotone; unfold MonotoneP; intros. apply H4 with b (-(x-p))%R p; auto with zarith real. apply Rplus_lt_reg_r with (x-p)%R. ring_simplify; auto with real. apply ClosestOpp; auto. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b). apply ClosestRoundedModeP with t; auto with zarith. elim pDef; auto. split;[apply FcanonicBound with radix; auto|idtac]. left; unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith. unfold Feven, nNormMin; simpl. replace (pred (t-s)) with (S (pred (pred (t-s)))); auto with zarith. apply EvenExp; auto with zarith. exists (Fnum p*Zpower_nat radix ((Z.abs_nat (Fexp p-s-Fexp x)))+ Fnum q*Zpower_nat radix ((Z.abs_nat (Fexp q-s-Fexp x))))%Z. cut (FtoRradix hx = ((Fnum p * Zpower_nat radix (Z.abs_nat (Fexp p - s - Fexp x)) + Fnum q * Zpower_nat radix (Z.abs_nat (Fexp q - s - Fexp x)))%Z * powerRZ radix (s + Fexp x)))%R;[intros H'; split; auto|idtac]. cut (Z.abs (Fnum p * Zpower_nat radix (Z.abs_nat (Fexp p - s - Fexp x)) + Fnum q * Zpower_nat radix (Z.abs_nat (Fexp q - s - Fexp x))) < Zpos (vNum b')+1)%Z; auto with zarith. apply lt_IZR. rewrite plus_IZR; simpl (IZR 1). rewrite <- Rabs_Zabs. apply Rmult_lt_reg_l with (powerRZ radix (s + Fexp x)); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rle_lt_trans with (Rabs ((powerRZ radix (s + Fexp x))*((Fnum p * Zpower_nat radix (Z.abs_nat (Fexp p - s - Fexp x)) + Fnum q * Zpower_nat radix (Z.abs_nat (Fexp q - s - Fexp x)))%Z)))%R. rewrite Rabs_mult; rewrite (Rabs_right (powerRZ radix (s + Fexp x))); auto with real. apply Rle_ge; apply powerRZ_le, IZR_lt; lia. rewrite Rmult_comm; rewrite <- H'. replace (FtoRradix hx) with (x+(-(x-hx)))%R;[idtac|ring]. apply Rle_lt_trans with (Rabs x+Rabs (-(x-hx)))%R;[apply Rabs_triang|idtac]. rewrite Rabs_Ropp; apply Rlt_le_trans with (powerRZ radix (t+Fexp x)+Rabs (x-hx))%R. apply Rplus_lt_compat_r; unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold FtoR, Fabs; 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. apply Rle_trans with (powerRZ radix (t + Fexp x)+ powerRZ radix (s + Fexp x) / 2)%R; auto with real. rewrite J; rewrite Zpower_nat_Z_powerRZ; rewrite inj_minus1; auto with zarith. rewrite Rmult_plus_distr_l. apply Rplus_le_compat. rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. replace (s + Fexp x + (t - s))%Z with (t + Fexp x)%Z by ring; 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. rewrite plus_IZR; repeat rewrite mult_IZR. repeat rewrite Zpower_nat_Z_powerRZ. generalize eqGe; generalize eqLeep; intros. repeat rewrite <- Zabs_absolu. repeat rewrite Z.abs_eq; auto with zarith. rewrite Rmult_plus_distr_r. repeat rewrite Rmult_assoc. repeat rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. ring_simplify (Fexp p - s - Fexp x + (s + Fexp x))%Z. ring_simplify (Fexp q - s - Fexp x + (s + Fexp x))%Z. rewrite hxExact; unfold FtoRradix, FtoR; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz