proposition: Lemma eqLe: (Fexp q <= s+ Fexp x)%Z \/ ((FtoRradix q= - powerRZ radix (t+s+Fexp x))%R /\(Rabs (x - hx) <= (powerRZ radix (s + Fexp x))/2)%R).
proof: Proof. cut (0 < Fnum x)%Z; [intros L|apply LtR0Fnum with radix; auto with real zarith]. cut ( (Fnum x <= Zpower_nat radix t -radix-1)%Z \/ (Zpower_nat radix t -radix <=Fnum x ))%Z. 2:case (Zle_or_lt (Zpower_nat radix t -radix)%Z (Fnum x));auto with zarith. intros H; case H; clear H; intros H. cut (exists g:float, (Fnormal radix b g)/\(FtoRradix g=(Fnum x+radix)*(powerRZ radix (Fexp x+s)))%R/\ (Fexp g=Fexp x +s)%Z). intros T; elim T; intros g T'; elim T'; intros H1 T''; elim T''; intros H2 H3; clear T T' T''. left. apply Z.le_trans with (Fexp g); auto with zarith. apply Fcanonic_Rle_Zle with radix b t; auto with zarith. left; auto. left; auto. fold FtoRradix; rewrite <- Rabs_Ropp. replace (Rabs (-q))%R with (Rabs ((p-x)+((x-p)-q)))%R;[idtac|ring_simplify ((p-x)+((x-p)-q))%R; auto with real]. apply Rle_trans with (Rabs (p-x)+ Rabs((x-p)-q))%R;[apply Rabs_triang|idtac]. apply Rle_trans with ((p - x)+ /2* (powerRZ radix (Fexp q)))%R;[apply Rplus_le_compat|idtac]. rewrite Rabs_right; auto with real. apply Rle_ge; apply Rplus_le_reg_l with (x)%R; ring_simplify. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H0 with b x (x * (powerRZ radix s + 1))%R; auto with zarith real. apply Rplus_lt_reg_r with (-x)%R; ring_simplify. apply Rle_lt_trans with (x*0)%R;[right;ring|apply Rmult_lt_compat_l;auto with real zarith]. apply powerRZ_lt;apply IZR_lt; lia. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto. apply ClosestRoundedModeP with t; auto with zarith. apply Rmult_le_reg_l with (2); auto with real arith. apply Rle_trans with (powerRZ radix (Fexp q)). unfold FtoRradix; apply ClosestExp with b t; auto with zarith. right; simpl; field; auto with real. apply Rle_trans with ((x * (powerRZ radix s + 1)+/ 2 * powerRZ radix (Fexp p)) - x + / 2 * powerRZ radix (Fexp q))%R. apply Rplus_le_compat_r; unfold Rminus; apply Rplus_le_compat_r. apply Rplus_le_reg_l with (-( x * (powerRZ radix s + 1)))%R. apply Rle_trans with (Rabs ((- (x * (powerRZ radix s + 1)) + p)))%R; [apply RRle_abs|idtac]. rewrite <- Rabs_Ropp. replace (- (- (x * (powerRZ radix s + 1)) + p))%R with ((x * (powerRZ radix s + 1)-p))%R;[idtac|ring]. apply Rle_trans with (/ 2 * powerRZ radix (Fexp p))%R;[idtac|right;ring]. apply Rmult_le_reg_l with (2); auto with real arith. apply Rle_trans with (powerRZ radix (Fexp p)). unfold FtoRradix; apply ClosestExp with b t; auto with zarith. right; simpl; field; auto with real. apply Rle_trans with (x * (powerRZ radix s)+(/ 2 * powerRZ radix (Fexp p)+/ 2 * powerRZ radix (Fexp q)))%R; [right;ring|idtac]. apply Rle_trans with (x * powerRZ radix s + powerRZ radix (Fexp p))%R;[apply Rplus_le_compat_l|idtac]. apply Rle_trans with (/ 2 * powerRZ radix (Fexp p) + / 2 * powerRZ radix (Fexp p))%R; [apply Rplus_le_compat_l|right; field; auto with real]. apply Rmult_le_compat_l; auto with real; apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. apply eqLeep. apply Rle_trans with (x * powerRZ radix s + radix * powerRZ radix (s+Fexp x))%R;[apply Rplus_le_compat_l|idtac]. apply Rle_trans with (powerRZ radix (s+1+Fexp x))%R;[apply Rle_powerRZ; auto with real zarith; try apply epLe|idtac]. apply IZR_le; lia. right; repeat rewrite powerRZ_add; try apply IZR_neq; try lia. simpl; ring. right; rewrite H2; 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]. 2: apply powerRZ_le; apply IZR_lt; lia. unfold FtoRradix, FtoR; repeat rewrite powerRZ_add; try apply IZR_neq; try lia. simpl; ring. apply Rle_trans with ((Fnum x)+0)%R. ring_simplify. apply IZR_le, LeR0Fnum with radix; auto with real zarith. apply Rplus_le_compat_l; apply IZR_le; lia. exists (Float (Fnum x +radix) (Fexp x + s)). elim Nx; elim Fx; intros. repeat split; simpl. 1,2 : lia. rewrite Z.abs_eq by auto with zarith. rewrite Z.abs_eq in H3 by auto with zarith. apply Z.le_trans with (1:=H3); auto with zarith. unfold FtoRradix, FtoR; simpl; rewrite plus_IZR; simpl; ring. cut (FtoRradix p <= powerRZ radix (Fexp x+t+s) + powerRZ radix (Fexp x+t))%R;[intros J1|idtac]. cut (- (x - p) < powerRZ radix (Fexp x) * (powerRZ radix (t + s) + radix + 1))%R;[intros J2|idtac]. cut (FtoRradix (Fopp q) <= powerRZ radix (t + s + Fexp x))%R;[intros V|idtac]. case V; auto; intros V'. left; replace (Fexp q) with (Fexp (Fopp q)); [idtac|simpl; auto]. replace (s+Fexp x)%Z with (Fexp (FPred b radix t (Float (nNormMin radix t) (s+1+Fexp x)))). apply Fcanonic_Rle_Zle with radix b t; auto with zarith. apply FcanonicFopp; left; auto. apply FPredCanonic; auto with zarith. apply FcanonicNnormMin; elim Fx; auto with zarith. rewrite Rabs_right. rewrite Rabs_right. apply FPredProp; auto with zarith. apply FcanonicFopp; left; auto. apply FcanonicNnormMin; elim Fx; auto with zarith. fold FtoRradix; apply Rlt_le_trans with (1:=V'). unfold FtoRradix, FtoR, nNormMin; simpl. rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add. replace (pred t +(s+1+Fexp x))%Z with (t+s+Fexp x)%Z; auto with real. rewrite inj_pred; unfold Z.pred; auto with zarith. apply IZR_neq; lia. apply Rle_ge; apply R0RltRlePred; auto with zarith. apply LtFnumZERO; auto. simpl; unfold nNormMin; auto with zarith. apply Zpower_nat_less; lia. apply Rle_ge; rewrite Fopp_correct; auto; generalize qNeg; auto with real. rewrite FPredSimpl2; simpl; auto with zarith. elim Fx; auto with zarith. right; split. unfold FtoRradix in V'; rewrite Fopp_correct in V'; auto with real. fold FtoRradix; rewrite <- V'; ring_simplify; auto with real. rewrite hxExact. replace (x-(p+q))%R with ((x-p)- q)%R;[idtac|ring]. case (Rle_or_lt (x-p)%R q). intros. rewrite Rabs_left1. 2: apply Rplus_le_reg_l with (FtoRradix q); ring_simplify (q+0)%R. 2: apply Rle_trans with (2:=H0); right; ring. apply Rle_trans with (q+(p+-x))%R;[right; ring|idtac]. apply Rle_trans with (-(powerRZ radix (t + s + Fexp x)) + ((powerRZ radix (Fexp x + t + s) + powerRZ radix (Fexp x + t))+ -((powerRZ radix t -radix)*powerRZ radix (Fexp x))))%R. apply Rplus_le_compat. rewrite <- V'; unfold FtoRradix; rewrite Fopp_correct; auto with real. apply Rplus_le_compat; auto with real. apply Ropp_le_contravar. unfold FtoRradix, FtoR; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (IZR (Zpower_nat radix t - radix)). unfold Zminus; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite Ropp_Ropp_IZR; auto with real zarith. now apply IZR_le. replace (t+s+Fexp x)%Z with (Fexp x+t+s)%Z; auto with zarith. ring_simplify. pattern (IZR radix) at 4 in |-*; replace (IZR radix) with (powerRZ radix 1). repeat rewrite <- powerRZ_add. rewrite Zplus_comm. ring_simplify. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (radix*powerRZ radix (1+Fexp x))%R. apply Rmult_le_compat_r; replace 2%R with (IZR 2); auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply IZR_le; lia. apply Rle_trans with (powerRZ radix (2+Fexp x)). right; repeat rewrite powerRZ_add; try apply IZR_neq; try lia. simpl; ring. apply Rle_trans with (powerRZ radix (s+Fexp x)). apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. right; field; auto with real. apply IZR_neq; lia. apply IZR_neq; lia. simpl; ring. intros. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (powerRZ radix (s + Fexp x));[idtac|right; field; auto with real]. apply Rplus_le_reg_l with (-( Rabs (x - p - q)))%R. ring_simplify (- Rabs (x - p - q) + 2 * Rabs (x - p - q))%R. cut (exists qplus:float, (Fbounded b qplus)/\ (qplus-q=powerRZ radix (s+Fexp x))%R /\ qplus=FNSucc b radix t q). intros T; elim T; intros qplus T'; elim T'; intros H1 T''; elim T''; intros; clear T T' T''. apply Rle_trans with (Rabs (x-p-qplus))%R. elim qDef; fold FtoRradix; intros. replace (x-p-q)%R with (-(q-(x-p)))%R;[rewrite Rabs_Ropp|ring]. replace (x-p-qplus)%R with (-(qplus-(x-p)))%R;[rewrite Rabs_Ropp|ring]. apply H5; auto. rewrite Rabs_left1. rewrite Rabs_right. rewrite <- H2; right; ring. apply Rle_ge; apply Rplus_le_reg_l with (FtoRradix q); ring_simplify (q+0)%R. apply Rlt_le; apply Rlt_le_trans with (1:=H0); right; ring. apply Rplus_le_reg_l with (FtoRradix qplus). ring_simplify. cut (isMax b radix (x-p)%R qplus). intros H4; elim H4; intros H5 H6; elim H6; intros H7 H8; auto with real. rewrite H3; apply MinMax; auto with zarith real. generalize ClosestMinOrMax; unfold MinOrMaxP; intros T. case (T b radix (x-p)%R q); auto. clear T; intros W; elim W; intros T1 T2; elim T2; intros H4 H5; clear T1 T2 H5. fold FtoRradix in H4; contradict H4; auto with real. exists (FNSucc b radix t q); split. apply FcanonicBound with radix; auto. apply FNSuccCanonic; auto with zarith; elim Nq; auto. split; auto. unfold FNSucc; rewrite FcanonicFnormalizeEq; auto with zarith. 2: left; auto. unfold FtoRradix; rewrite <- Fminus_correct; auto. replace q with (Float (-(nNormMin radix t)) (s+1+Fexp x)). rewrite FSuccDiff3; auto with zarith real. unfold FtoR; simpl. replace (Z.pred (s+1+Fexp x))%Z with (s+Fexp x)%Z; unfold Z.pred; auto with real zarith. simpl; elim Fx; auto with zarith. apply FnormalUnique with radix b t; auto with zarith. 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]. apply FnormalFop; auto. apply FnormalNnormMin; auto with zarith; elim Fx; auto with zarith. apply trans_eq with (-(-FtoR radix q))%R; auto with real. rewrite <- Fopp_correct; fold FtoRradix. rewrite V'; unfold FtoRradix, FtoR, nNormMin; simpl. rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ. apply trans_eq with (-(powerRZ radix (pred t) * powerRZ radix (s + 1 + Fexp x)))%R; auto with real. rewrite <- powerRZ_add. replace ((pred t + (s + 1 + Fexp x)))%Z with (t + s + Fexp x)%Z; auto with real. rewrite inj_pred; auto with zarith; unfold Z.pred; ring. apply IZR_neq; lia. apply Rle_trans with (FtoRradix (Float 1%Z (t+s+Fexp x)));[idtac|right; unfold FtoRradix, FtoR; simpl; ring]. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H0 with b (-(x-p))%R ((powerRZ radix (Fexp x))*(powerRZ radix (t+s)+radix+1))%R; auto with zarith real. apply ClosestOpp; auto. clear H0; generalize ClosestCompatible; unfold CompatibleP; intros T. cut (Fbounded b (Float 1 (t + s + Fexp x)));[intros H1|idtac]. 2: split; simpl; elim Fx; intros; lia. apply T with (powerRZ radix (Fexp x) * (powerRZ radix (t + s) + radix + 1))%R (Fnormalize radix b t (Float 1 (t + s + Fexp x))); auto with real. 2: rewrite FnormalizeCorrect; auto with zarith. apply ImplyClosest with t (Fexp x+s+1)%Z; auto with zarith. apply FnormalizeBounded; auto with zarith. apply FnormalizeCanonic; auto with zarith. apply Rle_trans with (powerRZ radix (Fexp x) * powerRZ radix (t + s))%R. rewrite <- powerRZ_add. replace (Fexp x + s + 1 + t - 1)%Z with (Fexp x + (t + s))%Z; auto with real zarith. apply IZR_neq; lia. apply Rmult_le_compat_l. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (powerRZ radix (t + s) +0)%R; auto with real zarith. rewrite Rplus_assoc; apply Rplus_le_compat_l; auto with real zarith. rewrite <- plus_IZR; apply IZR_le; lia. rewrite FnormalizeCorrect; auto with zarith; unfold FtoR; simpl; right. replace (Fexp x + s + 1 + t - 1)%Z with (t + s + Fexp x)%Z; ring. elim Fx; auto with zarith. rewrite FnormalizeCorrect; auto with zarith; unfold FtoR; simpl. replace (powerRZ radix (Fexp x) * (powerRZ radix (t + s) + radix + 1) - 1 * powerRZ radix (t + s + Fexp x))%R with (powerRZ radix (Fexp x) *(radix+1))%R. rewrite Rabs_right. replace (Fexp x+s+1)%Z with (Fexp x+(1+s))%Z;[idtac|ring]. rewrite powerRZ_add. apply Rle_trans with (powerRZ radix (Fexp x) * (powerRZ radix (1+s) */ 2))%R;[idtac|right;unfold Rdiv; ring]. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (powerRZ radix (1+s));[idtac|right; field; auto with real]. rewrite powerRZ_add. apply Rmult_le_compat; auto with real zarith. rewrite <- plus_IZR; apply IZR_le; lia. simpl; ring_simplify (radix*1)%R; apply IZR_le; auto with real zarith. 2: apply IZR_neq; lia. 2: apply IZR_neq; lia. apply Rle_trans with (powerRZ radix 2); [idtac|apply Rle_powerRZ; try apply IZR_le; auto with real zarith]. simpl; ring_simplify (radix*1)%R. apply Rle_trans with (radix+radix)%R. apply Rplus_le_compat_l, IZR_le; lia. apply Rle_trans with (2*radix)%R; [right;ring|idtac]. apply Rmult_le_compat_r; apply IZR_le; auto with real zarith. apply Rle_ge; apply Rmult_le_pos; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rplus_le_le_0_compat; apply IZR_le; lia. repeat rewrite powerRZ_add; try apply IZR_neq; try lia. ring. replace (-(x-p))%R with (p+-x)%R by ring. apply Rle_lt_trans with ((powerRZ radix (Fexp x + t + s) + powerRZ radix (Fexp x + t))+ -(powerRZ radix (Fexp x + t) - radix*powerRZ radix (Fexp x)))%R. apply Rplus_le_compat; auto with real. apply Ropp_le_contravar; unfold FtoRradix, FtoR; rewrite powerRZ_add. apply Rle_trans with ((powerRZ radix t - radix)*powerRZ radix (Fexp x))%R;[right;ring|idtac]. apply Rmult_le_compat_r. apply powerRZ_le, IZR_lt; lia. rewrite <- Zpower_nat_Z_powerRZ. apply Rle_trans with (IZR ((Zpower_nat radix t - radix))); auto with real zarith. unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; simpl; auto with real. now apply IZR_le. apply IZR_neq; lia. apply Rplus_lt_reg_r with (radix * powerRZ radix (Fexp x))%R. ring_simplify. rewrite Rplus_comm, Rplus_assoc; apply Rplus_lt_compat_l. rewrite <- powerRZ_add. replace (Fexp x+(t+s))%Z with (Fexp x +t+s)%Z; auto with zarith real. apply Rle_lt_trans with (powerRZ radix (Fexp x + t + s)+0)%R; auto with real zarith. apply Rplus_lt_compat_l. apply powerRZ_lt, IZR_lt; lia. apply IZR_neq; lia. cut ( powerRZ radix (Fexp x + t + s) + powerRZ radix (Fexp x + t)= Float (Zpower_nat radix (pred t)+Zpower_nat radix (Z.abs_nat (t-s-1))) (Fexp x+s+1))%R. cut (Fbounded b (Float (Zpower_nat radix (pred t)+Zpower_nat radix (Z.abs_nat (t-s-1))) (Fexp x+s+1))). intros. rewrite H1. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H2 with b (x * (powerRZ radix s + 1))%R (powerRZ radix (Fexp x + t + s) + powerRZ radix (Fexp x + t))%R; auto with zarith real. unfold FtoRradix, FtoR. apply Rlt_le_trans with ((powerRZ radix t * powerRZ radix (Fexp x) * (powerRZ radix s + 1)))%R. apply Rmult_lt_compat_r; auto with real zarith. apply Rplus_lt_0_compat; auto with real. apply powerRZ_lt, IZR_lt; lia. apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; elim Fx; intros. rewrite Z.abs_eq in H3; auto with zarith real. now apply IZR_lt. right;repeat rewrite powerRZ_add; try apply IZR_neq; try lia. ring. rewrite H1; unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto. apply ClosestRoundedModeP with t; auto with zarith. split; simpl. rewrite pGivesBound; rewrite Z.abs_eq ; auto with zarith. apply Z.lt_le_trans with (Zpower_nat radix (pred t) + Zpower_nat radix (pred t))%Z. apply Zplus_lt_compat_l. apply Zpower_nat_monotone_lt; lia. pattern t at 3 in |-*; replace t with (1+(pred t)); auto with zarith. rewrite Zpower_nat_is_exp; replace (Zpower_nat radix 1) with radix; auto with zarith. apply Z.le_trans with (2*Zpower_nat radix (pred t))%Z; auto with zarith. apply Zmult_le_compat_r; try lia. apply Zpower_NR0; lia. unfold Zpower_nat; simpl; auto with zarith. apply Z.add_nonneg_nonneg; apply Zpower_NR0; lia. elim Fx; auto with zarith. unfold FtoRradix, FtoR; simpl; rewrite plus_IZR. repeat rewrite Zpower_nat_Z_powerRZ. rewrite Rmult_plus_distr_r. repeat rewrite <- powerRZ_add. replace (Z.abs_nat (t - s - 1) + (Fexp x + s + 1))%Z with (Fexp x + t)%Z. replace (pred t + (Fexp x + s + 1))%Z with (Fexp x + t + s)%Z; auto with real. rewrite inj_pred; unfold Z.pred; auto with zarith. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply IZR_neq; lia. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz