proposition: Theorem Bsqrt_correct : forall m x, B2R (Bsqrt m x) = round radix2 fexp (round_mode m) (sqrt (B2R x)) /\ is_finite (Bsqrt m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end /\ (is_nan (Bsqrt m x) = false -> Bsign (Bsqrt m x) = Bsign x).
proof: Proof. intros m [sx|[|]| |sx mx ex Hx] ; try ( simpl ; rewrite sqrt_0, round_0, ?B2R_build_nan, ?is_finite_build_nan, ?is_nan_build_nan ; intuition auto with typeclass_instances ; easy). simpl. case Bsqrt_correct_aux. intros H1 (H2, (H3, H4)). case sx. refine (conj _ (conj (refl_equal false) _)). apply sym_eq. unfold sqrt. case Rcase_abs. intros _. apply round_0. auto with typeclass_instances. intros H. elim Rge_not_lt with (1 := H). now apply F2R_lt_0. easy. split. now rewrite B2R_SF2B. split. now rewrite is_finite_SF2B. intros _. now rewrite Bsign_SF2B. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative