proposition: Theorem FnormalizeCanonic : forall p : float, Fbounded b p -> Fcanonic (Fnormalize p).
proof: Proof. intros p H'. generalize (FnormalizeBounded p H'). unfold Fnormalize in |- *; case (Z_zerop (Fnum p)); auto. intros H'0; right; repeat split; simpl in |- *; lia. intros H'1. case (min_or (precision - Fdigit radix p) (Z.abs_nat (dExp b + Fexp p))); intros Min; case Min; clear Min; intros MinR MinL. intros H'2; left; split; auto. rewrite MinR; unfold Fshift in |- *; simpl in |- *. apply Z.le_trans with (Z.abs (radix * (Zpower_nat radix (pred (Fdigit radix p)) * Zpower_nat radix (precision - Fdigit radix p)))). pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix). repeat rewrite <- Zpower_nat_is_exp; auto with zarith. replace (1 + (pred (Fdigit radix p) + (precision - Fdigit radix p))) with precision; auto. rewrite pGivesBound; lia. cut (Fdigit radix p <= precision). 2: now apply pGivesDigit. unfold Fdigit in |- *. generalize (digitNotZero _ radixMoreThanOne _ H'1); case (digit radix (Fnum p)); simpl in |- *; auto. intros tmp; contradict tmp; auto with arith. intros n H H0; change (precision = S n + (precision - S n)) in |- *. rewrite Nat.add_comm, Nat.sub_add; auto. repeat rewrite Zabs_Zmult. apply Zle_Zmult_comp_l. apply Z.abs_nonneg. apply Zle_Zmult_comp_r. apply Z.abs_nonneg. rewrite (fun x => Z.abs_eq (Zpower_nat radix x)); auto with zarith. unfold Fdigit in |- *; apply digitLess; auto. apply Zpower_NR0; lia. intros H'0; right; split; auto; split. rewrite MinR; clear MinR; auto. cut (- dExp b <= Fexp p)%Z; [ idtac | apply H' ]. case p; simpl in |- *. intros Fnum1 Fexp1 H'2; rewrite inj_abs; auto with zarith. rewrite MinR. rewrite <- (fun x => Z.abs_eq (Zpos x)). unfold Fshift in |- *; simpl in |- *. apply Z.lt_le_trans with (Z.abs (radix * (Zpower_nat radix (Fdigit radix p) * Zpower_nat radix (Z.abs_nat (dExp b + Fexp p))))). repeat rewrite Zabs_Zmult. apply Zmult_gt_0_lt_compat_l. apply Z.lt_gt; rewrite Z.abs_eq; auto with zarith. apply Zmult_gt_0_lt_compat_r. apply Z.lt_gt; rewrite Z.abs_eq; auto with zarith. now apply Zpower_nat_less. apply Zpower_NR0; lia. rewrite (fun x => Z.abs_eq (Zpower_nat radix x)); auto with zarith. unfold Fdigit in |- *; apply digitMore; auto. apply Zpower_NR0; lia. pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix). repeat rewrite <- Zpower_nat_is_exp; auto with zarith. rewrite Z.abs_eq, pGivesBound. apply Zpower_nat_monotone_le; lia. apply Zpower_NR0; lia. auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz