proposition: Theorem binary_normalize_correct : forall m mx ex szero, if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (F2R (Float radix2 mx ex)))) (bpow radix2 emax) then B2R (binary_normalize m mx ex szero) = round radix2 fexp (round_mode m) (F2R (Float radix2 mx ex)) /\ is_finite (binary_normalize m mx ex szero) = true /\ Bsign (binary_normalize m mx ex szero) = match Rcompare (F2R (Float radix2 mx ex)) 0 with | Eq => szero | Lt => true | Gt => false end else B2FF (binary_normalize m mx ex szero) = binary_overflow m (Rlt_bool (F2R (Float radix2 mx ex)) 0).
proof: Proof. intros mode mx ex szero. generalize (binary_normalize_correct prec emax _ _ mode mx ex szero). replace (BinarySingleNaN.binary_normalize _ _ _ _ _ _ _ _) with (B2BSN (binary_normalize mode mx ex szero)) by apply B2BSN_BSN2B'. simpl. destruct Rlt_bool. - now destruct binary_normalize. - intros H. apply eq_binary_overflow_FF2SF. now rewrite FF2SF_B2FF, <- B2SF_B2BSN. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN