proposition: Theorem Bfrexp_correct : forall f, is_finite_strict f = true -> let (z, e) := Bfrexp f in (B2R f = B2R z * bpow radix2 e)%R /\ ( (2 < emax)%Z -> (/2 <= Rabs (B2R z) < 1)%R /\ e = mag radix2 (B2R f) ).
proof: Proof. intro f; case f; intro s; try discriminate; intros m e Hf _. generalize (Bfrexp_correct_aux s m e Hf). intros (_, (Hb, Heq)); simpl; rewrite B2R_SF2B. split. easy. intros Hp. specialize (Hb Hp). split. easy. rewrite Heq, mag_mult_bpow. - apply (Z.add_reg_l (- (snd (Ffrexp_core_binary s m e)))). now ring_simplify; symmetry; apply mag_unique. - intro H; destruct Hb as (Hb, _); revert Hb; rewrite H, Rabs_R0; lra. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative