proposition: Lemma Bnormfr_mantissa_correct : forall f : binary_float FloatOps.prec emax, (/ 2 <= Rabs (B2R f) < 1)%R -> match f with | B754_finite _ m e _ => Bnormfr_mantissa f = N.pos m /\ Z.pos (digits2_pos m) = FloatOps.prec /\ (e = - FloatOps.prec)%Z | _ => False end.
proof: Proof. intro f. destruct f as [s|s| |s m e B]; [now simpl; rewrite Rabs_R0; lra..| ]. unfold Bnormfr_mantissa, SFnormfr_mantissa; simpl. intro Hf. cut (e = -53 /\ Z.pos (digits2_pos m) = FloatOps.prec)%Z. { now intros [-> ->]; rewrite Z.eqb_refl. } revert Hf. change (/ 2)%R with (bpow radix2 (0 - 1)); change 1%R with (bpow radix2 0). intro H; generalize (mag_unique _ _ _ H); clear H. rewrite Float_prop.mag_F2R_Zdigits; [ |now case s]. replace (Digits.Zdigits _ _) with (Digits.Zdigits radix2 (Z.pos m)); [ |now case s]. clear s. rewrite <-Digits.Zpos_digits2_pos. intro He; replace e with (e - 0)%Z by ring; rewrite <-He. cut (Z.pos (digits2_pos m) = 53)%Z. { intro H; split; [ |exact H]; ring_simplify. now rewrite <-Pos2Z.opp_pos; apply f_equal. } revert B; unfold SpecFloat.bounded, canonical_mantissa. intro H; generalize (andb_prop _ _ H); clear H; intros [H _]; revert H. intro H; generalize (Zeq_bool_eq _ _ H); clear H. unfold fexp, emin; fold FloatOps.prec. apply Z.max_case_strong; [ |unfold emax]; lia. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig