proposition: Lemma EvenClosestbplusb: forall b0:Fbound, forall n:nat, forall fext f:float, Zpos (vNum b0)=(Zpower_nat radix n) -> (1 < n) -> (-dExp b0 <= Fexp fext)%Z -> (EvenClosest (plusExp b0) radix n fext f) -> (Fbounded b0 f) -> (EvenClosest b0 radix n fext f).
proof: Proof. intros b0 n fext f nGivesB nGe H H0 H1. elim H0; intros. cut (Closest b0 radix fext f);[intros|apply Closestbplusb; auto]. split; auto. cut (Fcanonic radix b0 (Fnormalize radix b0 n f)); [idtac|apply FnormalizeCanonic; auto with zarith]. intros V; case V; clear V; intros H5. case H3; intros H6. left; generalize H6; unfold FNeven. replace (Fnormalize radix (plusExp b0) n f) with (Fnormalize radix b0 n f); auto. apply FcanonicUnique with radix (plusExp b0) n; auto with zarith. elim H5; intros J1 J2; elim J1; intros J3 J4. unfold plusExp; left; split;[split|idtac];simpl; lia. apply FnormalizeCanonic; auto with zarith. elim H0; intros J1 J2; elim J1; auto. repeat rewrite FnormalizeCorrect; auto with real. right; intros; apply H6. apply Closestbbplus with n; auto. right; intros;apply sym_eq. apply RoundedModeProjectorIdemEq with b0 n (Closest b0 radix); auto with zarith. apply ClosestRoundedModeP with n; auto with zarith. replace (FtoR radix f) with (FtoR radix fext); auto with real. apply Rplus_eq_reg_l with (-(FtoR radix f))%R. ring_simplify (- FtoR radix f + FtoR radix f)%R. rewrite <- FnormalizeCorrect with radix b0 n f; auto. apply trans_eq with ((-Fnum (Fnormalize radix b0 n f) + (Fnum fext)*Zpower_nat radix (Z.abs_nat (Fexp fext+dExp b0)))%Z * (powerRZ radix (-(dExp b0))))%R. rewrite plus_IZR; rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ. rewrite Ropp_Ropp_IZR; unfold FtoR. replace (Fexp (Fnormalize radix b0 n f)) with (-(dExp b0))%Z. rewrite Rmult_plus_distr_r; rewrite Rmult_assoc. rewrite <- powerRZ_add. replace (Z.abs_nat (Fexp fext + dExp b0)+-dExp b0)%Z with (Fexp fext);[ring|idtac]. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply IZR_neq; lia. elim H5; intros J1 J2; elim J2; auto. replace (- Fnum (Fnormalize radix b0 n f) + Fnum fext * Zpower_nat radix (Z.abs_nat (Fexp fext + dExp b0)))%Z with 0%Z; [simpl; ring|idtac]. cut ((Z.abs (- Fnum (Fnormalize radix b0 n f) + Fnum fext * Zpower_nat radix (Z.abs_nat (Fexp fext + dExp b0)))) < 1)%Z; try lia. apply lt_IZR. rewrite <- Rabs_Zabs; rewrite plus_IZR; rewrite Ropp_Ropp_IZR. rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ. apply Rmult_lt_reg_l with (Fulp b0 radix n f); [unfold Fulp; auto with real zarith|idtac]. apply powerRZ_lt, IZR_lt; lia. pattern (Fulp b0 radix n f) at 1; rewrite <- (Rabs_right (Fulp b0 radix n f)). 2: apply Rle_ge; unfold Fulp; apply powerRZ_le, IZR_lt; lia. rewrite <- Rabs_mult. replace (Fulp b0 radix n f * (- Fnum (Fnormalize radix b0 n f) + Fnum fext * powerRZ radix (Z.abs_nat (Fexp fext + dExp b0))))%R with (fext -FtoR radix f)%R. apply Rlt_le_trans with ( Fulp b0 radix n f);[idtac|simpl; right; ring]. apply RoundedModeUlp with (Closest b0 radix); auto with zarith. apply ClosestRoundedModeP with n; auto with zarith. rewrite <- FnormalizeCorrect with radix b0 n f; auto. apply Rplus_eq_reg_l with (FtoR radix (Fnormalize radix b0 n f)). unfold Fulp, FtoRradix, FtoR;ring_simplify. apply trans_eq with (Fnum fext * (powerRZ radix (Fexp (Fnormalize radix b0 n f))* powerRZ radix (Z.abs_nat (Fexp fext + dExp b0))))%R;[idtac|ring]. rewrite <- powerRZ_add. replace (Fexp (Fnormalize radix b0 n f) + Z.abs_nat (Fexp fext + dExp b0))%Z with (Fexp fext); auto. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. elim H5; intros J1 J2; elim J2; intros; auto with zarith. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz