proposition: Lemma equivFloat_Sqrt_BinFloat {Tl} : forall (t : ArithExpr Tl BinFloat) (lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) -> 0 <= evalRounded t lM md -> eqExprTypeFloat (evalFloat (Sqrt t) lC md) (evalRounded (Sqrt t) lM md).
proof: Proof. intros t lC md lM [fint B2Rt] H. simpl. generalize (Bsqrt_correct _ _ HPrec_gt_0 HPrec_lt_emax md (evalFloat t lC md)). intros [H1 [H2' H3]]. assert (H2 : is_finite (@Bsqrt Rrnd.prec Rrnd.emax HPrec_gt_0 HPrec_lt_emax md (evalFloat t lC md)) = true). { destruct evalFloat; [easy.. | destruct s; [| easy]]. rewrite <-B2Rt in H. simpl in H. unfold F2R in H. simpl in H. generalize (bpow_gt_0 radix2 e). intros H'. assert (H'' : 0 <= IZR (Z.neg m)) by nra. now apply le_IZR in H''. } clear H2'. unfold eqExprTypeFloat. simpl. unfold FPsqrt. split; [assumption |]. rewrite H1. unfold Rrnd.sqrt, Rrnd.Rnd, SpecFloat.fexp, FLT_exp, SpecFloat.emin, Rrnd.emin. now rewrite B2Rt. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)