proposition: Theorem RND_Min_Pos_projector : forall f : float, (0 <= f)%R -> Fcanonic radix b f -> FtoRradix (RND_Min_Pos f) = f.
proof: Proof. intros f H1 H2. unfold RND_Min_Pos in |- *; case (Rle_dec (firstNormalPos radix b p) f); intros H3. replace (IRNDD (ln f / ln radix + (- Z.pred p)%Z)) with (Fexp f). replace (f * powerRZ radix (- Fexp f))%R with (IZR (Fnum f)). rewrite IRNDD_projector; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite Rmult_assoc; rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. ring_simplify (Fexp f + - Fexp f)%Z; simpl in |- *; ring. generalize ln_radix_pos; intros V1. cut (0 < Fnum f)%R; [ intros V2 | idtac ]. apply sym_eq; apply IRNDD_eq. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite ln_mult; auto with real zarith. unfold Rdiv in |- *; rewrite Rmult_plus_distr_r. apply Rle_trans with (Z.pred p + Fexp f + (- Z.pred p)%Z)%R; [ rewrite Ropp_Ropp_IZR; right; ring | idtac ]. apply Rplus_le_compat_r; apply Rplus_le_compat. apply Rmult_le_reg_l with (ln radix); [ auto with real | idtac ]. apply Rle_trans with (ln (Fnum f)); [ idtac | right; field; auto with real ]. apply exp_le_inv. rewrite exp_ln; auto. rewrite exp_ln_powerRZ; auto with zarith. case H2; intros T; elim T; intros C1 C2. apply Rmult_le_reg_l with radix; auto with real zarith. apply IZR_lt; lia. apply Rle_trans with (IZR (Zpos (vNum b))); [ right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ | idtac ]. pattern (Z_of_nat p) at 2 in |- *; replace (Z_of_nat p) with (1 + Z.pred p)%Z; [ rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl in |- *; ring | unfold Z.pred in |- *; ring ]. rewrite <- (Rabs_right (radix * Fnum f)); auto with real zarith. rewrite <- mult_IZR; rewrite Rabs_Zabs; auto with real zarith. apply IZR_le; auto. apply Rle_ge; apply Rmult_le_pos; auto with real. apply IZR_le; auto with real zarith. contradict H3; apply Rlt_not_le; unfold FtoRradix in |- *; apply FsubnormalLtFirstNormalPos; auto with zarith. apply Rmult_le_reg_l with (ln radix); [ auto with real | idtac ]. apply Rle_trans with (ln (powerRZ radix (Fexp f))); [ idtac | right; field; auto with real ]. rewrite <- exp_ln_powerRZ; auto with zarith. rewrite ln_exp; auto with real. apply powerRZ_lt, IZR_lt; lia. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite ln_mult; auto with real zarith. rewrite <- exp_ln_powerRZ; auto with zarith. rewrite ln_exp; auto with real. unfold Rdiv in |- *; rewrite Rmult_plus_distr_r. apply Rlt_le_trans with (p + Fexp f + (- Z.pred p)%Z)%R. 2: rewrite Ropp_Ropp_IZR; unfold Z.succ, Z.pred in |- *; repeat rewrite plus_IZR; simpl in |- *; right; ring. replace (ln radix * Fexp f * / ln radix)%R with (IZR (Fexp f)); [ idtac | field; auto with real ]. apply Rplus_lt_compat_r; apply Rplus_lt_compat_r. apply Rmult_lt_reg_l with (ln radix); [ auto with real | idtac ]. apply Rle_lt_trans with (ln (Fnum f)); [ right; field; auto with real | idtac ]. apply exp_lt_inv. rewrite exp_ln; auto. rewrite exp_ln_powerRZ; auto with zarith. apply Rlt_le_trans with (IZR (Zpos (vNum b))). rewrite <- (Rabs_right (IZR (Fnum f))); auto with real. rewrite Rabs_Zabs; apply IZR_lt; cut (Fbounded b f); auto with real zarith. intros T; apply T. apply FcanonicBound with radix; auto. apply Rle_ge; auto with real. right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply IZR_lt. apply LtR0Fnum with radix; auto with zarith; fold FtoRradix in |- *. apply Rlt_le_trans with (2 := H3); rewrite firstNormalPos_eq; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. case H2; intros T; elim T; intros C1 C2. absurd (firstNormalPos radix b p <= f)%R; auto with real. unfold FtoRradix in |- *; apply FnormalLtFirstNormalPos; auto with zarith. elim C2; intros C3 C4. replace (f * powerRZ radix (dExp b))%R with (IZR (Fnum f)). rewrite IRNDD_projector; rewrite <- C3; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring. unfold FtoRradix, FtoR in |- *; rewrite C3. rewrite Rmult_assoc; rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. ring_simplify (- dExp b + dExp b)%Z; simpl in |- *; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz