proposition: Theorem Bdiv_correct : forall div_nan m x y, B2R y <> 0%R -> if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x / B2R y))) (bpow radix2 emax) then B2R (Bdiv div_nan m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\ is_finite (Bdiv div_nan m x y) = is_finite x /\ (is_nan (Bdiv div_nan m x y) = false -> Bsign (Bdiv div_nan m x y) = xorb (Bsign x) (Bsign y)) else B2FF (Bdiv div_nan m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
proof: Proof. intros div_nan mode x y Zy. rewrite <- B2R_B2BSN in Zy. generalize (Bdiv_correct prec emax _ _ mode (B2BSN x) _ Zy). replace (BinarySingleNaN.Bdiv _ _ _) with (B2BSN (Bdiv div_nan mode x y)) by apply B2BSN_BSN2B. unfold Rdiv. destruct y as [sy|sy|sy ply|sy my ey Hy] ; try now elim Zy. destruct x as [sx|sx|sx plx Hx|sx mx ex Hx] ; try ( simpl ; rewrite Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ simpl ; try easy ; now rewrite B2R_build_nan, is_finite_build_nan, is_nan_build_nan | apply bpow_gt_0 | auto with typeclass_instances ] ). destruct Rlt_bool. - now destruct Bdiv. - intros H. apply eq_binary_overflow_FF2SF. now rewrite FF2SF_B2FF, <- B2SF_B2BSN. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN