proposition: Theorem binary_round_aux_correct : forall mode x mx ex lx, inbetween_float radix2 (Zpos mx) ex (Rabs x) lx -> (ex <= fexp (Zdigits radix2 (Zpos mx) + ex))%Z -> let z := binary_round_aux mode (Rlt_bool x 0) (Zpos mx) ex lx in valid_binary z = true /\ if Rlt_bool (Rabs (round radix2 fexp (round_mode mode) x)) (bpow radix2 emax) then FF2R radix2 z = round radix2 fexp (round_mode mode) x /\ is_finite_FF z = true /\ sign_FF z = Rlt_bool x 0 else z = binary_overflow mode (Rlt_bool x 0).
proof: Proof. intros mode x mx ex lx Bx Ex. generalize (binary_round_aux_correct prec emax _ _ mode x mx ex lx Bx Ex). unfold binary_round_aux. destruct (Rlt_bool (Rabs _) _). - now destruct BinarySingleNaN.binary_round_aux as [sz|sz| |sz mz ez]. - intros [_ ->]. split. rewrite valid_binary_SF2FF by apply is_nan_binary_overflow. now apply binary_overflow_correct. easy. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN