proposition: Theorem binary_round_correct : forall m sx mx ex, let z := binary_round m sx mx ex in valid_binary z = true /\ let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in if Rlt_bool (Rabs (round radix2 fexp (round_mode m) x)) (bpow radix2 emax) then SF2R radix2 z = round radix2 fexp (round_mode m) x /\ is_finite_SF z = true /\ sign_SF z = sx else z = binary_overflow m sx.
proof: Proof. intros m sx mx ex. unfold binary_round. generalize (shl_align_fexp_correct mx ex). destruct (shl_align_fexp mx ex) as (mz, ez). intros (H1, H2). set (x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex)). replace sx with (Rlt_bool x 0). apply binary_round_aux_correct. constructor. unfold x. now rewrite <- F2R_Zabs, abs_cond_Zopp. exact H2. unfold x. case sx. apply Rlt_bool_true. now apply F2R_lt_0. apply Rlt_bool_false. now apply F2R_ge_0. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative