proposition: Lemma eqGe: (s+ Fexp x <= Fexp q)%Z.
proof: Proof. case (Rle_or_lt ((powerRZ radix (Fexp x))*((powerRZ radix (t-1))+radix))%R x);intros H. apply Z.le_trans with (Fexp (Float (nNormMin radix t) (s+Fexp x)));[simpl; auto with zarith|idtac]. apply Z.le_trans with (Fexp (Fopp q));[idtac|simpl; auto with zarith]. apply Fcanonic_Rle_Zle with radix b t; try lia. apply FcanonicNnormMin; auto with zarith. elim Fx; auto with zarith. apply FcanonicFopp; left; auto. rewrite Fopp_correct; fold FtoRradix; rewrite Rabs_Ropp. replace (FtoRradix q) with ((-(p-x))-((x-p)-q))%R;[idtac|ring]. apply Rle_trans with (2:=Rabs_triang_inv (-(p-x))%R ((x-p)-q)%R). apply Rle_trans with ((x*(powerRZ radix s)-(powerRZ radix (Fexp p))/2)-(powerRZ radix (Fexp q))/2)%R. apply Rle_trans with (((powerRZ radix (Fexp x) * (powerRZ radix (t - 1) + radix))) * powerRZ radix s - powerRZ radix (s+1+Fexp x) / 2 - powerRZ radix (s+1+Fexp x) / 2)%R. unfold nNormMin, FtoRradix, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ. rewrite <- powerRZ_add. 2: apply IZR_neq; lia. rewrite Rabs_right. 2: apply Rle_ge, powerRZ_le, IZR_lt; lia. replace (pred t+(s+Fexp x))%Z with (t-1+(s+Fexp x))%Z by lia. apply Rle_trans with (powerRZ radix (Fexp x) * (powerRZ radix (t - 1) + radix) * powerRZ radix s - powerRZ radix (s + 1 + Fexp x))%R;[idtac|right;field; auto with real]. rewrite Rmult_plus_distr_l. rewrite Rmult_plus_distr_r. pattern (IZR radix) at 6 in |-*; replace (IZR radix) with (powerRZ radix 1)%R; [idtac|simpl; ring]. repeat rewrite <- powerRZ_add; try apply IZR_neq; try lia. replace (Fexp x + (t - 1) + s)%Z with (t - 1 + (s + Fexp x))%Z;[idtac|ring]. replace (s + 1+ Fexp x)%Z with (Fexp x+1+s)%Z;[right|idtac];ring. unfold Rminus; apply Rplus_le_compat. apply Rplus_le_compat. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Ropp_le_contravar; unfold Rdiv; apply Rmult_le_compat_r; auto with real. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. apply epLe. apply Ropp_le_contravar; unfold Rdiv; apply Rmult_le_compat_r; auto with real. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. apply Z.le_trans with (Fexp p);[apply eqLeep|apply epLe]. unfold Rminus; apply Rplus_le_compat. rewrite Rabs_left1. apply Rplus_le_reg_l with ((powerRZ radix (Fexp p) / 2)+x-p)%R. ring_simplify. apply Rle_trans with ((x * (powerRZ radix s + 1))-p)%R;[right;ring|idtac]. apply Rle_trans with (Rabs ((x * (powerRZ radix s + 1))-p))%R;[apply RRle_abs|idtac]. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (powerRZ radix (Fexp p)). unfold FtoRradix; apply ClosestExp with b t; auto with zarith. simpl; right; field; auto with real. apply Rplus_le_reg_l with p; 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, IZR_lt; lia. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto. apply ClosestRoundedModeP with t; auto with zarith. apply Ropp_le_contravar. replace (x + - p + - q)%R with ((x-p)-q)%R;[idtac|ring]. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (powerRZ radix (Fexp q)). unfold FtoRradix; apply ClosestExp with b t; auto with zarith. simpl; right; field; auto with real. case (Rle_or_lt (powerRZ radix (Fexp x) * (powerRZ radix (t - 1) + 1))%R x); intros H'. cut ((powerRZ radix (Fexp x) * ((powerRZ radix (s+t-1))+(powerRZ radix (t-1))+(powerRZ radix s))) <= p)%R;[intros|idtac]. apply Z.le_trans with (Fexp (Float (nNormMin radix t) (Fexp x+s)));[simpl;auto with zarith|idtac]. apply Fcanonic_Rle_Zle with radix b t; auto with real zarith. apply FcanonicNnormMin; auto with zarith; elim Fx; auto with zarith. left; auto. rewrite Rabs_right. rewrite Rabs_left1. rewrite <- Fopp_correct. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H1 with b (Float (nNormMin radix t) (Fexp x + s)) (-(x-p))%R. 2: unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto. 2:apply ClosestRoundedModeP with t; auto with zarith. 2: apply FcanonicBound with radix; apply FcanonicNnormMin; auto with zarith; elim Fx; auto with zarith. 2: apply ClosestOpp; auto. clear H1; replace (-(x-p))%R with (p+-x)%R by ring. apply Rlt_le_trans with (((powerRZ radix (Fexp x) * (powerRZ radix (s + t - 1) + powerRZ radix (t - 1) + powerRZ radix s)))+ -(powerRZ radix (Fexp x) * (powerRZ radix (t - 1) + radix)))%R; auto with real. 2: apply Rplus_le_compat; auto with real. unfold FtoRradix, FtoR,nNormMin; simpl; rewrite Zpower_nat_Z_powerRZ. repeat rewrite Rmult_plus_distr_l. repeat rewrite <- powerRZ_add; try apply IZR_neq; try lia. replace (pred t + (Fexp x + s))%Z with (Fexp x+(s + t - 1))%Z;[idtac|rewrite inj_pred; unfold Z.pred; auto with zarith]. apply Rplus_lt_reg_r with ((radix * powerRZ radix (Fexp x))- (powerRZ radix (Fexp x+(s + t - 1))))%R. ring_simplify. apply Rle_lt_trans with (powerRZ radix (1+Fexp x)); auto with real zarith. rewrite powerRZ_add; try apply IZR_neq; try lia. simpl; right;ring. apply Rlt_powerRZ; auto with zarith; apply IZR_lt; lia. apply qNeg. apply Rle_ge; apply LeFnumZERO; simpl; auto with zarith. unfold nNormMin; auto with zarith. apply Zpower_NR0; lia. cut ( (powerRZ radix (Fexp x) * (powerRZ radix (s + t - 1) + powerRZ radix (t - 1) + powerRZ radix s))= (Float ((Zpower_nat radix (pred t) + Zpower_nat radix (Z.abs_nat (t -s-1)) + 1)) ((Fexp x)+s)))%R;[intros V1|idtac]. cut (Fbounded b ( Float ((Zpower_nat radix (pred t) + Zpower_nat radix (Z.abs_nat (t -s-1)) + 1))%Z ((Fexp x)+s)));[intros V2|idtac]. rewrite V1. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H0 with b ( (Float (Zpower_nat radix (pred t) + Zpower_nat radix (Z.abs_nat (t - s - 1)) + 1) (Fexp x + s))%R) (x * (powerRZ radix s + 1))%R; auto with zarith real. 2: unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto. 2:apply ClosestRoundedModeP with t; auto with zarith. rewrite <- V1; clear H0 V2 V1. apply Rlt_le_trans with ( (powerRZ radix (Fexp x) * (powerRZ radix (t - 1) + 1) *(powerRZ radix s + 1)))%R. 2: apply Rmult_le_compat_r; auto with real zarith. 2: apply Rplus_le_le_0_compat; auto with real; apply powerRZ_le, IZR_lt; lia. rewrite Rmult_assoc; apply Rmult_lt_compat_l; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. rewrite Rmult_plus_distr_l; rewrite Rmult_plus_distr_r. rewrite <- powerRZ_add. 2: apply IZR_neq; lia. apply Rlt_le_trans with ((powerRZ radix (s + t - 1))+ powerRZ radix (t - 1)+ powerRZ radix s+1)%R . repeat rewrite Rplus_assoc; repeat apply Rplus_lt_compat_l; auto with real zarith. replace (s+t-1)%Z with (t-1+s)%Z; [right; ring|ring]. 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 (pred t)) + Zpower_nat radix (pred (pred t))))%Z. repeat rewrite <- Zplus_assoc;apply Zplus_lt_compat_l. cut (Zpower_nat radix (Z.abs_nat (t - s - 1)) <= Zpower_nat radix (pred (pred t)))%Z;[intros|idtac]. cut (1 <Zpower_nat radix (pred (pred t)))%Z;auto with zarith. apply Z.le_lt_trans with (Zpower_nat radix 0)%Z; auto with zarith. apply Zpower_nat_monotone_lt; lia. apply Zpower_nat_monotone_le; lia. pattern t at 4 in |-*; replace t with ((pred t)+1); auto with zarith. cut ((Zpower_nat radix 1)=radix)%Z;[intros K|unfold Zpower_nat; simpl; auto with zarith]. rewrite Zpower_nat_is_exp; rewrite K. apply Z.le_trans with (Zpower_nat radix (pred t)+ (Zpower_nat radix (pred t)))%Z. rewrite <- Zplus_assoc; apply Zplus_le_compat_l. pattern (pred t) at 3 in |-*; replace (pred t) with ((pred (pred t))+1); auto with zarith. rewrite Zpower_nat_is_exp; rewrite K. apply Z.le_trans with (Zpower_nat radix (pred (pred t)) * 2)%Z; auto with zarith. apply Zmult_le_compat_l; try lia. apply Zpower_NR0; lia. apply Z.le_trans with (Zpower_nat radix ((pred t)) * 2)%Z; auto with zarith. apply Zmult_le_compat_l; try lia. apply Zpower_NR0; lia. apply Z.add_nonneg_nonneg; try apply Z.add_nonneg_nonneg; try apply Zpower_NR0; lia. elim Fx; auto with zarith. unfold FtoRradix, FtoR; simpl. repeat rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ. rewrite inj_pred; auto with zarith; unfold Z.pred. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. simpl; unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; try lia. repeat rewrite Rmult_plus_distr_l; repeat rewrite Rmult_plus_distr_r. repeat rewrite <- powerRZ_add; try apply IZR_neq; try lia. replace (Fexp x + (s + t + - (1)))%Z with (t + -1 + (Fexp x + s))%Z by ring. replace (Fexp x + (t + - (1)))%Z with (t + - s + - (1) + (Fexp x + s))%Z; ring. cut (FtoRradix x= powerRZ radix (Fexp x+t-1))%R;[intros K|idtac]. cut (FtoRradix p= powerRZ radix (Fexp x+t-1)*((powerRZ radix s + 1)))%R;[intros K'|idtac]. replace q with (Fopp (Float ((nNormMin radix t)) (s+Fexp x)%Z)); simpl; auto with zarith. apply FcanonicUnique with radix b t; auto with zarith. apply FcanonicFopp; apply FcanonicNnormMin; auto with zarith. elim Fx; auto with zarith. left; auto. apply ClosestIdem with b; auto. apply FcanonicBound with radix; apply FcanonicFopp; apply FcanonicNnormMin; auto with zarith;elim Fx; auto with zarith. replace (FtoR radix (Fopp (Float (nNormMin radix t) (s + Fexp x)))) with (x-p)%R; auto. rewrite K'; rewrite K; rewrite Fopp_correct; unfold FtoR; simpl. unfold nNormMin; rewrite Zpower_nat_Z_powerRZ. rewrite inj_pred; auto with zarith. unfold Z.pred, Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; try lia. simpl; ring. cut ((powerRZ radix (Fexp x + t - 1) * (powerRZ radix s + 1))= (FtoRradix (Float (Zpower_nat radix s +1) (Fexp x+t-1))))%R;[intros L; rewrite L|idtac]. unfold FtoRradix; apply sym_eq; apply ClosestIdem with b; auto. split;simpl;[idtac|elim Fx; auto with zarith]. rewrite pGivesBound; rewrite Z.abs_eq; auto with zarith. replace t with ((pred t)+1); auto with zarith; rewrite Zpower_nat_is_exp. apply Z.lt_le_trans with (Zpower_nat radix (pred t)+ Zpower_nat radix (pred t))%Z; auto with zarith. apply Zplus_lt_compat. apply Zpower_nat_monotone_lt; auto with zarith. replace 1%Z with (Zpower_nat radix 0)%Z; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. apply Z.le_trans with (Zpower_nat radix (pred t) * 2)%Z; auto with zarith. apply Zmult_le_compat_l; auto with zarith. unfold Zpower_nat; simpl; auto with zarith. apply Zpower_NR0; auto with zarith. apply Z.add_nonneg_nonneg; try apply Zpower_NR0; auto with zarith. fold FtoRradix; rewrite <- L; rewrite <- K; auto. unfold FtoRradix, FtoR; simpl; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl; ring. cut (Fnum x=Zpower_nat radix (pred t));[intros|idtac]. unfold FtoRradix, FtoR; rewrite H0; rewrite Zpower_nat_Z_powerRZ. rewrite <- powerRZ_add. replace (pred t + Fexp x)%Z with (Fexp x + t - 1)%Z; try easy. lia. apply IZR_neq; lia. cut ( Zpower_nat radix (pred t) <= Fnum x)%Z;[intros P1|idtac]. cut ( Fnum x < Zpower_nat radix (pred t) +1)%Z;[intros P2; auto with zarith|idtac]. apply lt_IZR; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ. apply Rmult_lt_reg_l with (powerRZ radix (Fexp x)); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rle_lt_trans with (FtoRradix x);[right; unfold FtoRradix, FtoR;ring|idtac]. apply Rlt_le_trans with (1:=H'); right; simpl. replace (t-1)%Z with (Z_of_nat (pred t));[ring|rewrite inj_pred; auto with zarith]. apply Zmult_le_reg_r with radix; auto with zarith. apply Z.le_trans with (Zpos (vNum b)); [rewrite pGivesBound|rewrite Zmult_comm]. pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1). rewrite <- Zpower_nat_is_exp. replace (pred t + 1) with t; auto with zarith. unfold Zpower_nat; simpl; auto with zarith. elim Nx; intros. rewrite Zabs_Zmult in H1. rewrite Z.abs_eq in H1; auto with zarith. rewrite Z.abs_eq in H1; auto with zarith. apply LeR0Fnum with radix; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz