proposition: Theorem Closestbbext: forall bext:Fbound, forall fext f:float, (vNum bext=vNum b) -> (dExp b < dExp bext)%Z -> (-dExp b <= Fexp fext)%Z -> (Closest b radix fext f) -> (Closest bext radix fext f).
proof: Proof. intros bext fext f K1 K2; intros. elim H0; intros. split. elim H1; intros; split; try lia. intros g Hg. case (Zle_or_lt (-(dExp b)) (Fexp g)); intros. apply H2. elim Hg; split; try lia. case (Zle_lt_or_eq (-(dExp b)) (Fexp (Fnormalize radix b p f))). cut (Fbounded b (Fnormalize radix b p f));[intros T; elim T; auto|idtac]. apply FnormalizeBounded; auto with zarith. intros; apply Rle_trans with ((Fulp b radix p f)/2)%R. apply Rmult_le_reg_l with 2%R; auto with zarith real. apply Rle_trans with (Fulp b radix p f);[idtac|simpl; right; field; auto with real]. rewrite <- Rabs_Ropp. replace (- (FtoR radix f - fext))%R with (fext - FtoR radix f)%R;[idtac|ring]. apply ClosestUlp; auto with zarith. rewrite <- Rabs_Ropp. replace (- (FtoR radix g - fext))%R with (fext - FtoR radix g)%R;[idtac|ring]. apply Rle_trans with (Rabs fext -Rabs (FtoR radix g))%R;[idtac|apply Rabs_triang_inv]. apply Rle_trans with ((powerRZ radix (p-1+Fexp (Fnormalize radix b p f)) - powerRZ radix (-1+ Fexp (Fnormalize radix b p f))) - powerRZ radix (p-1-dExp b))%R; [idtac|unfold Rminus; apply Rplus_le_compat]. apply Rplus_le_reg_l with (powerRZ radix (-1 + Fexp (Fnormalize radix b p f))). ring_simplify ( powerRZ radix (-1 + Fexp (Fnormalize radix b p f)) + (powerRZ radix (p - 1 + Fexp (Fnormalize radix b p f)) - powerRZ radix (-1 + Fexp (Fnormalize radix b p f)) - powerRZ radix (p - 1 - dExp b)))%R. apply Rle_trans with (powerRZ radix (Fexp (Fnormalize radix b p f))). unfold Fulp, Rdiv; apply Rle_trans with ((/2+/radix)* powerRZ radix (Fexp (Fnormalize radix b p f)))%R. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; right; field. apply IZR_neq; auto with real zarith. apply Rle_trans with (1 * powerRZ radix (Fexp (Fnormalize radix b p f)))%R; [apply Rmult_le_compat_r; auto with real zarith|right; ring]. apply powerRZ_le, IZR_lt; lia. apply Rmult_le_reg_l with (2*radix)%R; [apply Rmult_lt_0_compat; auto with real zarith|idtac]. apply IZR_lt; lia. apply Rle_trans with (2+radix)%R; [right; field; auto with real zarith| ring_simplify (2*radix*1)%R]. apply IZR_neq; lia. apply Rle_trans with (radix+radix)%R;[idtac|right; ring]. apply Rplus_le_compat_r, IZR_le; lia. apply Rle_trans with (powerRZ radix (p-2+Fexp (Fnormalize radix b p f))); [apply Rle_powerRZ; try apply IZR_le; auto with real zarith|idtac]. apply Rle_trans with (1*(powerRZ radix (p - 2 + Fexp (Fnormalize radix b p f))))%R; auto with real. apply Rle_trans with ((radix -1)*(powerRZ radix (p - 2 + Fexp (Fnormalize radix b p f))))%R;[apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; lia. apply Rplus_le_reg_l with 1%R. ring_simplify (1+(radix-1))%R; try rewrite <- plus_IZR; try apply IZR_le; auto with real zarith. apply Rle_trans with ( - powerRZ radix (p - 2+ Fexp (Fnormalize radix b p f)) + powerRZ radix (p - 1 + Fexp (Fnormalize radix b p f)))%R. right; unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. simpl; field. apply IZR_neq; lia. unfold Rminus; rewrite Rplus_comm; apply Rplus_le_compat_l; apply Ropp_le_contravar; apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. cut (powerRZ radix (p - 1 + Fexp (Fnormalize radix b p f)) + - powerRZ radix (-1 + Fexp (Fnormalize radix b p f))= (Float (pPred (vNum b)) (-1+Fexp (Fnormalize radix b p f))))%R. intros W; rewrite W. 2: unfold FtoRradix, FtoR, pPred. 2: apply trans_eq with (Z.pred (Zpos (vNum b))*powerRZ radix (-1+Fexp (Fnormalize radix b p f)))%R;[idtac|simpl; auto with real]. 2: unfold Z.pred, Zminus; rewrite plus_IZR. 2: rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ. 2: repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; field. 2: apply IZR_neq; lia. case (Rle_or_lt (Float (pPred (vNum b)) (-1 + Fexp (Fnormalize radix b p f))) (Rabs fext)); auto with real; intros V. absurd ( Rabs f <= Float (pPred (vNum b)) (-1 + Fexp (Fnormalize radix b p f)))%R. apply Rlt_not_le. apply Rlt_le_trans with (powerRZ radix (p-1+Fexp (Fnormalize radix b p f))). rewrite <- W; apply Rlt_le_trans with (powerRZ radix (p - 1 + Fexp (Fnormalize radix b p f))+-0)%R; auto with real zarith. apply Rplus_lt_compat_l, Ropp_lt_contravar. apply powerRZ_lt, IZR_lt; lia. right; ring. unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b p f; auto with zarith. rewrite <- Fabs_correct; auto. rewrite powerRZ_add; unfold FtoRradix, FtoR, Fabs; simpl. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rmult_le_reg_l with radix; auto with real zarith. now apply IZR_lt. apply Rle_trans with (powerRZ radix p). unfold Zminus; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; right; field ; auto with real. apply IZR_neq; lia. cut (Fnormal radix b (Fnormalize radix b p f));[intros Nf|idtac]. rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; rewrite <- mult_IZR; elim Nf; intros. rewrite Zabs_Zmult in H6; rewrite Z.abs_eq in H6; auto with zarith real. apply IZR_le; lia. cut (Fcanonic radix b (Fnormalize radix b p f));[intros X|apply FnormalizeCanonic; auto with zarith]. case X; auto; intros X'. elim X'; intros H5 H6; elim H6; intros. absurd (-dExp b < dExp b)%Z; auto with zarith. apply IZR_neq; lia. unfold FtoRradix; apply RoundAbsMonotoner with b p (Closest b radix) fext; auto with real zarith. apply ClosestRoundedModeP with p; auto with zarith. split. apply Z.le_lt_trans with (pPred (vNum b)); auto with zarith. simpl; rewrite Z.abs_eq; auto with zarith. apply Zlt_le_weak; apply pPredMoreThanOne with radix p; auto with zarith. unfold pPred; auto with zarith. apply Z.le_trans with (Z.pred (Fexp (Fnormalize radix b p f))); auto with zarith. unfold Z.pred; apply Z.le_trans with (-1+Fexp (Fnormalize radix b p f))%Z;auto with zarith. apply Ropp_le_contravar; rewrite <- Fabs_correct; auto. unfold FtoR, Fabs; simpl. apply Rle_trans with ((powerRZ radix p)*(powerRZ radix (-1-dExp b)))%R. apply Rmult_le_compat; auto with real zarith. apply IZR_le; auto with zarith. apply powerRZ_le, IZR_lt; lia. elim Hg; intros; rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound;rewrite <- K1; auto with real zarith. apply IZR_le; lia. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; right; ring. intros H4. apply Rle_trans with 0%R; try apply Rabs_pos; right. rewrite <- FnormalizeCorrect with radix b p f; auto with zarith. unfold FtoRradix; rewrite <- Fminus_correct; auto. rewrite <- Fabs_correct; auto. unfold FtoR. replace (Fnum (Fabs (Fminus radix (Fnormalize radix b p f) fext))) with 0%Z; [simpl; ring|idtac]. apply sym_eq; apply trans_eq with (Z.abs (Fnum (Fminus radix (Fnormalize radix b p f) fext)));[simpl; auto with zarith|idtac]. cut ( 0 <= Z.abs (Fnum (Fminus radix (Fnormalize radix b p f) fext)))%Z; auto with real zarith. cut (Z.abs (Fnum (Fminus radix (Fnormalize radix b p f) fext)) < 1)%Z; auto with real zarith. apply lt_IZR. apply Rmult_lt_reg_l with (powerRZ radix (-(dExp b))); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rle_lt_trans with (Rabs (f-fext))%R. unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b p f; auto with zarith. rewrite <- Fminus_correct; auto; rewrite <- Fabs_correct; auto. unfold FtoR; simpl. replace (Z.min (Fexp (Fnormalize radix b p f)) (Fexp fext)) with (-(dExp b))%Z; [right; ring|idtac]. rewrite Z.min_l; auto with zarith. apply Rlt_le_trans with (Fulp b radix p f); [idtac|unfold Fulp; simpl; rewrite H4; auto with real zarith]. rewrite <- Rabs_Ropp. replace (- (f - fext))%R with (fext -f)%R;[idtac|ring]. unfold FtoRradix; apply RoundedModeUlp with (Closest b radix); auto with zarith real. apply ClosestRoundedModeP with p; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz