proposition: Lemma Veltkamp_aux_aux: forall v:float, (FtoRradix v=hx) -> Fcanonic radix b' v -> (Rabs (x-v) <= (powerRZ radix (s+Fexp x)) /2)%R -> (powerRZ radix (t-1+Fexp x) <= v)%R.
proof: Proof. intros. case (Rle_or_lt (powerRZ radix (t-1)+(powerRZ radix s)/2)%R (Fnum x)); intros W. fold FtoRradix; apply Rplus_le_reg_l with (-v+x-powerRZ radix (t-1+Fexp x))%R. ring_simplify. apply Rle_trans with (x-v)%R; [right; ring|idtac]. apply Rle_trans with (Rabs (x-v))%R;[apply RRle_abs|idtac]. unfold FtoRradix; apply Rle_trans with (1:=H1). unfold FtoR; rewrite powerRZ_add; unfold Rdiv. 2: apply IZR_neq; lia. rewrite powerRZ_add. 2: apply IZR_neq; lia. apply Rle_trans with (powerRZ radix (Fexp x) * (powerRZ radix s * / 2))%R;[right;ring|idtac]. apply Rle_trans with (powerRZ radix (Fexp x) * (- powerRZ radix (t - 1) + Fnum x))%R;[idtac|right;ring]. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with ( - powerRZ radix (t - 1) + (powerRZ radix (t - 1) + powerRZ radix s / 2))%R; auto with real zarith. right; unfold Rdiv; ring. cut (exists eps:Z, (FtoRradix x=powerRZ radix (Fexp x)*(powerRZ radix (t-1) + eps))%R /\ (0 <= eps)%Z /\ (eps < (powerRZ radix s)/2)%R). intros T; elim T; intros eps T'; elim T'; intros H3 T''; elim T''; intros H4 H5; clear T T' T''. fold FtoRradix; rewrite H; rewrite hxExact. cut (Fbounded b (Float (Zpower_nat radix (pred t)+Zpower_nat radix (Z.abs_nat (t-s-1))+eps) (s+Fexp x))); [intros Yp|idtac]. cut (FtoRradix (Float (Zpower_nat radix (pred t)+Zpower_nat radix (Z.abs_nat (t-s-1))+eps) (s+Fexp x)) = powerRZ radix (Fexp x)*(powerRZ radix (t+s-1)+ powerRZ radix (t-1)+eps*powerRZ radix s))%R; [intros Yp'|idtac]. cut (Fbounded b (Float ((Zpower_nat radix (pred t)+eps)) (s+Fexp x))); [intros Yq|idtac]. cut (FtoRradix (Float ((Zpower_nat radix (pred t)+eps)) (s+Fexp x)) = powerRZ radix (Fexp x)*(powerRZ radix (t+s-1)+ eps*powerRZ radix s))%R; [intros Yq'|idtac]. cut (FtoRradix p=(powerRZ radix (Fexp x) * (powerRZ radix (t + s - 1) + powerRZ radix (t - 1) + eps * powerRZ radix s)))%R;[intros YYp|idtac]. cut (FtoRradix (Fopp q)=(powerRZ radix (Fexp x) * (powerRZ radix (t + s - 1) + eps * powerRZ radix s)))%R;[intros YYq|idtac]. replace (FtoRradix q) with (-(-q))%R; [idtac|ring]; unfold FtoRradix; rewrite <- Fopp_correct. fold FtoRradix; rewrite YYp; rewrite YYq; right. repeat rewrite powerRZ_add; try ring. apply IZR_neq; lia. rewrite <- Yq'. unfold FtoRradix; apply sym_eq. apply ImplyClosestStrict with b t (-(x-p))%R (s+Fexp x)%Z; auto with zarith. left; split; auto. rewrite pGivesBound; rewrite Zabs_Zmult; rewrite Z.abs_eq; auto with zarith. simpl; rewrite Z.abs_eq; auto with zarith. apply Z.le_trans with (radix*((Zpower_nat radix (pred t) + 0)))%Z; auto with zarith. pattern t at 1; replace t with (1+(pred t)); auto with zarith. rewrite Zpower_nat_is_exp. replace (Zpower_nat radix 1) with radix; auto with zarith. unfold Zpower_nat; simpl; auto with zarith. apply Z.add_nonneg_nonneg; try apply Zpower_NR0; lia. rewrite YYp; rewrite H3. ring_simplify. rewrite <- powerRZ_add. 2: apply IZR_neq; lia. replace (Fexp x+(t+s-1))%Z with (s+Fexp x+t-1)%Z;[idtac|ring]. apply Rplus_le_reg_l with ( -(powerRZ radix (s + Fexp x + t - 1))+eps * powerRZ radix (Fexp x))%R. ring_simplify. rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real zarith. apply IZR_le; easy. apply Rle_trans with (powerRZ radix (Fexp x)*1)%R; auto with real; apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (powerRZ radix 0); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; lia. fold FtoRradix; rewrite Yq'. apply Rle_trans with (powerRZ radix (Fexp x) *(powerRZ radix (t + s - 1) + 0))%R. ring_simplify (powerRZ radix (t + s - 1) + 0)%R. rewrite <- powerRZ_add. replace (s + Fexp x + t - 1)%Z with (Fexp x+(t + s - 1))%Z; auto with real zarith. apply IZR_neq; lia. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rplus_le_compat_l; apply Rmult_le_pos; auto with real zarith. now apply IZR_le. apply powerRZ_le, IZR_lt; lia. elim Fx; auto with zarith. fold FtoRradix; rewrite Yq'; rewrite YYp; rewrite H3. ring_simplify ( (- (powerRZ radix (Fexp x) * (powerRZ radix (t - 1) + eps) - powerRZ radix (Fexp x) * (powerRZ radix (t + s - 1) + powerRZ radix (t - 1) + eps * powerRZ radix s)) - powerRZ radix (Fexp x) * (powerRZ radix (t + s - 1) + eps * powerRZ radix s)))%R. rewrite Ropp_mult_distr_l_reverse; rewrite Rabs_Ropp; rewrite Rabs_mult. rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith]. rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith]. unfold Rdiv; rewrite powerRZ_add. apply Rlt_le_trans with ((powerRZ radix s*/2) * powerRZ radix (Fexp x))%R;[idtac|right;ring]. rewrite Rmult_comm; apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply IZR_neq; lia. apply IZR_le; easy. apply powerRZ_le, IZR_lt; lia. apply ClosestOpp; auto. rewrite <- Yp'. unfold FtoRradix; apply sym_eq. apply ImplyClosestStrict with b t (x * (powerRZ radix s + 1))%R (s+Fexp x)%Z; auto with zarith. left; split; auto. rewrite pGivesBound; rewrite Zabs_Zmult; rewrite Z.abs_eq; auto with zarith. simpl; rewrite Z.abs_eq; auto with zarith. apply Z.le_trans with (radix*((Zpower_nat radix (pred t) + 0+0)))%Z; auto with zarith. pattern t at 1; replace t with (1+(pred t)); auto with zarith. rewrite Zpower_nat_is_exp. rewrite Zpower_nat_1; auto with zarith. apply Zmult_le_compat_l; auto with zarith. apply Zplus_le_compat; auto with zarith. apply Zplus_le_compat_l. apply Zpower_NR0; lia. apply Z.add_nonneg_nonneg; auto. apply Z.add_nonneg_nonneg; apply Zpower_NR0; lia. rewrite H3. apply Rle_trans with (powerRZ radix (Fexp x) * (powerRZ radix (t - 1) + 0) * (powerRZ radix s + 0))%R; auto with real zarith. right; ring_simplify. unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; ring. apply Rmult_le_compat; auto with real zarith. ring_simplify (powerRZ radix (t - 1) + 0)%R; apply Rmult_le_pos; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply powerRZ_le, IZR_lt; lia. ring_simplify; apply powerRZ_le, IZR_lt; lia. apply Rmult_le_compat_l. apply powerRZ_le, IZR_lt; lia. apply Rplus_le_compat_l, IZR_le; lia. fold FtoRradix; rewrite Yp'. apply Rle_trans with (powerRZ radix (Fexp x) *(powerRZ radix (t + s - 1) + 0+0))%R. right; ring_simplify. rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. replace (s + Fexp x + t - 1)%Z with (Fexp x+(t + s - 1))%Z; auto with real zarith. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rplus_le_compat. apply Rplus_le_compat_l. apply powerRZ_le, IZR_lt; lia. apply Rmult_le_pos; try apply IZR_le; auto with real zarith. apply powerRZ_le, IZR_lt; lia. elim Fx; auto with zarith. fold FtoRradix; rewrite Yp';rewrite H3. ring_simplify (powerRZ radix (Fexp x) * (powerRZ radix (t - 1) + eps) * (powerRZ radix s + 1) - powerRZ radix (Fexp x) * (powerRZ radix (t + s - 1) + powerRZ radix (t - 1) + eps * powerRZ radix s))%R. replace (t+s-1)%Z with (s+(t-1))%Z; [rewrite powerRZ_add; try apply IZR_neq|idtac]; auto with real zarith. ring_simplify (powerRZ radix (Fexp x) * powerRZ radix (t - 1) * powerRZ radix s + powerRZ radix (Fexp x) * eps - powerRZ radix (Fexp x) * (powerRZ radix s * powerRZ radix (t - 1)))%R. rewrite Rabs_mult. rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith]. 2: apply powerRZ_le, IZR_lt; lia. rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith]. 2: now apply IZR_le. unfold Rdiv; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. apply Rlt_le_trans with (powerRZ radix (Fexp x)* (powerRZ radix s*/2))%R;[idtac|right;ring]. apply Rmult_lt_compat_l; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. unfold FtoRradix, FtoR; simpl. rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith. unfold Z.pred, Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. simpl; ring. split; simpl. clear Yp'; elim Yp; simpl; intros. rewrite Z.abs_eq; auto with zarith. rewrite Z.abs_eq in H2; auto with zarith. apply Z.le_lt_trans with (2:=H2). rewrite <- Zplus_assoc; apply Zplus_le_compat_l; auto with zarith. apply Z.le_trans with (0+eps)%Z; auto with zarith; apply Zplus_le_compat_r; auto with zarith. apply Zpower_NR0; lia. apply Z.add_nonneg_nonneg; auto with zarith. apply Z.add_nonneg_nonneg; apply Zpower_NR0; lia. apply Z.add_nonneg_nonneg; try apply Zpower_NR0; lia. elim Fx; auto with zarith. unfold FtoRradix, FtoR; simpl. rewrite plus_IZR; rewrite plus_IZR. repeat rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. unfold Z.pred, Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. rewrite powerRZ_Zopp. 2: apply IZR_neq; lia. simpl; field; auto with real zarith. split; apply Rgt_not_eq. apply IZR_lt; lia. apply powerRZ_lt, IZR_lt; lia. split; simpl. 2: elim Fx; auto with zarith. rewrite Z.abs_eq; auto with zarith. rewrite pGivesBound; apply lt_IZR. rewrite plus_IZR;rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ. rewrite inj_pred; auto with zarith. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply Rlt_le_trans with (powerRZ radix (Z.pred t) + powerRZ radix (t - s - 1) + powerRZ radix s / 2)%R; auto with real. apply Rle_trans with (powerRZ radix (Z.pred t)+powerRZ radix (t-2)+powerRZ radix (t-2))%R. apply Rplus_le_compat. apply Rplus_le_compat_l; auto with real zarith. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply Rle_trans with (powerRZ radix s). apply Rmult_le_reg_l with (2%R); auto with real. apply Rle_trans with (powerRZ radix s);[right; field; auto with real|auto with real zarith]. rewrite <- (Rmult_1_l (powerRZ _ _)) at 1; apply Rmult_le_compat_r. apply powerRZ_le, IZR_lt; lia. auto with real. apply Rle_powerRZ; try apply IZR_le; auto with zarith real. replace (Z.pred t) with (t-1)%Z;[idtac|unfold Z.pred; ring]. apply Rle_trans with (powerRZ radix (t-1)+powerRZ radix (t-1))%R. rewrite Rplus_assoc; apply Rplus_le_compat_l. apply Rle_trans with (2*powerRZ radix (t - 2))%R; [right;ring|idtac]. apply Rle_trans with (radix*powerRZ radix (t - 2))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; lia. apply IZR_le; lia. replace (t-1)%Z with (1+(t-2))%Z;[rewrite powerRZ_add; try apply IZR_neq; simpl|idtac]; auto with real zarith. right; ring. apply Rle_trans with (2*powerRZ radix (t - 1))%R; [right;ring|idtac]. apply Rle_trans with (radix*powerRZ radix (t - 1))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; lia. apply IZR_le; lia. pattern (Z_of_nat t)%Z at 2 in |-*; replace (Z_of_nat t)%Z with (1+(t-1))%Z; [rewrite powerRZ_add; simpl|ring]. right; ring. apply IZR_neq; lia. apply Z.add_nonneg_nonneg; auto with zarith. apply Z.add_nonneg_nonneg; apply Zpower_NR0; lia. exists (Fnum x- Zpower_nat radix (pred t))%Z; split. unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ. replace (Z_of_nat (pred t)) with (t+-(1))%Z; [idtac|rewrite inj_pred; auto with zarith]. unfold FtoRradix, FtoR; ring. split. apply Zplus_le_reg_l with (Zpower_nat radix (pred t)). ring_simplify. apply Zmult_le_reg_r with radix; auto with zarith. elim Nx; intros. rewrite Zabs_Zmult in H3. rewrite Z.abs_eq in H3; auto with zarith. rewrite Z.abs_eq in H3; [idtac|apply LeR0Fnum with radix; auto with zarith real]. rewrite Zmult_comm with (Fnum x) radix. apply Z.le_trans with (2:=H3); rewrite pGivesBound. pattern t at 2; replace t with (1+(pred t)) by auto with zarith. rewrite Zpower_nat_is_exp. replace ( Zpower_nat radix 1) with radix;[idtac|unfold Zpower_nat; simpl]; auto with zarith. unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ. replace (Z_of_nat (pred t)) with (t-1)%Z; [idtac|rewrite inj_pred; auto with zarith]. apply Rplus_lt_reg_l with (powerRZ radix (t - 1)). apply Rle_lt_trans with (2:=W); right;ring. Qed.
imports: Reals ZArith List PeanoNat Psatz