proposition: Theorem binary_fit_aux_correct : forall mode sx mx ex, canonical_mantissa mx ex = true -> let x := SF2R radix2 (S754_finite sx mx ex) in let z := binary_fit_aux mode sx mx ex in valid_binary z = true /\ if Rlt_bool (Rabs x) (bpow radix2 emax) then SF2R radix2 z = x /\ is_finite_SF z = true /\ sign_SF z = sx else z = binary_overflow mode sx.
proof: Proof. intros m sx mx ex Cx. unfold binary_fit_aux. simpl. rewrite F2R_cond_Zopp. rewrite abs_cond_Ropp. rewrite Rabs_pos_eq by now apply F2R_ge_0. destruct Zle_bool eqn:He. - assert (Hb: bounded mx ex = true). { unfold bounded. now rewrite Cx. } apply (conj Hb). rewrite Rlt_bool_true. repeat split. apply F2R_cond_Zopp. now apply bounded_lt_emax. - rewrite Rlt_bool_false. { repeat split. apply binary_overflow_correct. } apply Rnot_lt_le. intros Hx. apply bounded_canonical_lt_emax in Hx. revert Hx. unfold bounded. now rewrite Cx, He. now apply (canonical_canonical_mantissa false). Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative