proposition: Theorem NormalbPrim: forall (f:float), Fcanonic radix b f -> (FtoRradix f <>0) -> (exists f':float, (Fnormal radix b' f') /\ FtoRradix f'=f /\ (-t-dExp b <= Fexp f')%Z).
proof: Proof. intros. exists (Fnormalize radix b' t f). assert (powerRZ radix (-(dExp b)) <= (Fabs (Fnormalize radix b' t f)))%R. unfold FtoRradix; rewrite Fabs_correct; auto. rewrite FnormalizeCorrect; auto with zarith; rewrite <- Fabs_correct; auto. unfold FtoRradix, FtoR, Fabs; simpl. apply Rle_trans with ((IZR 1)*powerRZ radix (- dExp b))%R;[right; simpl; ring|idtac]. apply Rmult_le_compat; auto with real zarith. apply powerRZ_le, IZR_lt; lia. case (Zle_lt_or_eq 0 (Z.abs (Fnum f))); auto with zarith real. intros H1; apply IZR_le; lia. intros; absurd (Rabs f =0)%R. apply Rabs_no_R0; auto. unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl; rewrite <- H1; simpl; ring. assert (Fbounded b f);[apply FcanonicBound with radix; auto with zarith|idtac]. elim H1; intros; apply Rle_powerRZ; auto with zarith real. apply IZR_le; lia. assert (Fcanonic radix b' (Fnormalize radix b' t f)). apply FnormalizeCanonic; auto with zarith. assert (Fbounded b f);[apply FcanonicBound with radix; auto with zarith|idtac]. elim H2; generalize dExpPrim; intros; split; auto with zarith. split. case H2; auto. intros; absurd (Fabs f < (firstNormalPos radix b' t))%R. apply Rle_not_lt. apply Rle_trans with (powerRZ radix (-(dExp b))). unfold firstNormalPos, FtoRradix, FtoR; simpl. unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add. apply Rle_powerRZ. apply IZR_le; lia. rewrite dExpPrimEq. rewrite inj_pred; lia. apply IZR_neq; lia. apply Rle_trans with (1:=H1); unfold FtoRradix; repeat rewrite Fabs_correct; auto. rewrite FnormalizeCorrect; auto with zarith real. apply Rle_lt_trans with (Fabs (Fnormalize radix b' t f)). unfold FtoRradix; repeat rewrite Fabs_correct; auto. rewrite FnormalizeCorrect; auto with zarith real. unfold FtoRradix; apply FsubnormalLtFirstNormalPos; auto with zarith. apply FsubnormFabs; auto. rewrite Fabs_correct; auto with real zarith; apply Rabs_pos. split;[unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith|idtac]. apply Z.le_trans with (Fexp (Float (nNormMin radix t) (-t-dExp b))); auto with zarith. apply Fcanonic_Rle_Zle with radix b' t; auto with zarith. apply FcanonicNnormMin; auto with zarith. unfold b'; simpl; rewrite dExpPrimEq; lia. rewrite Rabs_right. rewrite <- Fabs_correct; auto; fold FtoRradix; apply Rle_trans with (2:=H1). unfold FtoRradix, FtoR, nNormMin; simpl; rewrite Zpower_nat_Z_powerRZ. rewrite <- powerRZ_add by (apply IZR_neq; lia). apply Rle_powerRZ; try lia. apply IZR_le; lia. apply Rle_ge; apply LeFnumZERO; auto with zarith. unfold nNormMin; simpl; auto with zarith. apply Zpower_NR0; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz