proposition: Lemma VeltkampEven2: (Odd 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; 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 Rgt_not_eq, IZR_lt; 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)). intros T; elim T; intros v T'; elim T'; intros; clear 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 L. 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. absurd (Even (Zpower_nat radix s)). apply OddNEven. elim s. unfold Zpower_nat; simpl; unfold Odd. exists 0%Z; ring. intros n Hrecn. replace (S n)with (1+n); auto with zarith. rewrite Zpower_nat_is_exp. apply OddMult; auto. unfold Zpower_nat; simpl; ring_simplify (radix*1)%Z; auto. replace (Zpower_nat radix s) with (2*(Z.abs (Fnum x- Fnum v*Zpower_nat radix (Z.abs_nat (Fexp v-Fexp x)))))%Z. apply EvenMult1; unfold Even; exists 1%Z; auto with zarith. apply eq_IZR. rewrite mult_IZR; rewrite <- Rabs_Zabs. unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR. rewrite mult_IZR; repeat rewrite Zpower_nat_Z_powerRZ; simpl. apply Rmult_eq_reg_l with (powerRZ radix (Fexp x)); auto with zarith real. rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. apply Rmult_eq_reg_l with (/2)%R; auto with real. apply trans_eq with (powerRZ radix (s + Fexp x) / 2)%R. 2: unfold Rdiv; rewrite Zplus_comm; ring. 2: apply Rgt_not_eq; apply powerRZ_lt, IZR_lt; lia. rewrite <- L. apply trans_eq with ((powerRZ radix (Fexp x) * (Rabs (Fnum x +- (Fnum v * powerRZ radix (Z.abs_nat (Fexp v +- Fexp x)))))))%R. field; auto with real. rewrite <- (Rabs_right (powerRZ radix (Fexp x)));[idtac|apply Rle_ge; auto with real zarith]. rewrite <- Rabs_mult. replace (x - FtoR radix v)%R with (powerRZ radix (Fexp x) * (Fnum x + -(Fnum v * powerRZ radix (Z.abs_nat (Fexp v +- Fexp x)))))%R; auto with real. unfold FtoRradix, FtoR; rewrite Rmult_plus_distr_l. rewrite <- Zabs_absolu; rewrite Z.abs_eq. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. rewrite powerRZ_Zopp; try apply IZR_neq; auto with real zarith. field. apply Rgt_not_eq; apply powerRZ_lt, IZR_lt; lia. apply Zplus_le_reg_l with (Fexp x). ring_simplify. apply Z.le_trans with (Fexp (Float (nNormMin radix (t-s)) (Fexp x))); [simpl; auto with zarith|idtac]. apply Fcanonic_Rle_Zle with radix b' (t-s); auto with zarith. apply FcanonicNnormMin; auto with zarith. unfold b'; simpl; elim Fx; auto. cut (powerRZ radix (t - 1 + Fexp x) <= v)%R;[intros H3|idtac]. 2: apply Veltkamp_aux_aux; auto. fold (FtoRradix v);unfold FtoR, nNormMin; simpl. rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add. rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith]. rewrite Rabs_right;[idtac|apply Rle_ge; apply Rle_trans with (2:=H3); auto with real zarith]. apply Rle_trans with (2:=H3); apply Rle_powerRZ; try apply IZR_le; try lia. apply powerRZ_le, IZR_lt; lia. apply powerRZ_le, IZR_lt; lia. apply IZR_neq; lia. apply powerRZ_le, IZR_lt; lia. 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; auto with real zarith. apply IZR_lt; easy. 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. replace ((s + Fexp x + (t - s)))%Z with (t+Fexp x)%Z; auto with real; ring. 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; auto with real zarith. now apply IZR_lt. 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; try apply IZR_neq; auto with real zarith. rewrite Rplus_comm; apply Rplus_le_compat. 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; auto with zarith. 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