proposition: Theorem binary_normalize_correct : forall m mx ex szero, let x := F2R (Float radix2 mx ex) in let z := binary_normalize m mx ex szero in if Rlt_bool (Rabs (round radix2 fexp (round_mode m) x)) (bpow radix2 emax) then B2R z = round radix2 fexp (round_mode m) x /\ is_finite z = true /\ Bsign z = match Rcompare x 0 with | Eq => szero | Lt => true | Gt => false end else B2SF z = binary_overflow m (Rlt_bool x 0).
proof: Proof. Proof with auto with typeclass_instances. intros m mx ez szero. destruct mx as [|mz|mz] ; simpl. rewrite F2R_0, round_0, Rabs_R0, Rlt_bool_true... split... split... rewrite Rcompare_Eq... apply bpow_gt_0. generalize (binary_round_correct m false mz ez). simpl. case Rlt_bool_spec. intros _ (Vz, (Rz, (Rz', Rz''))). split. now rewrite B2R_SF2B. split. now rewrite is_finite_SF2B. rewrite Bsign_SF2B, Rz''. rewrite Rcompare_Gt... now apply F2R_gt_0. intros Hz' (Vz, Rz). rewrite B2SF_SF2B, Rz. apply f_equal. apply sym_eq. apply Rlt_bool_false. now apply F2R_ge_0. generalize (binary_round_correct m true mz ez). simpl. case Rlt_bool_spec. intros _ (Vz, (Rz, (Rz', Rz''))). split. now rewrite B2R_SF2B. split. now rewrite is_finite_SF2B. rewrite Bsign_SF2B, Rz''. rewrite Rcompare_Lt... now apply F2R_lt_0. intros Hz' (Vz, Rz). rewrite B2SF_SF2B, Rz. apply f_equal. apply sym_eq. apply Rlt_bool_true. now apply F2R_lt_0. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative