proposition: Lemma equivPrim_Sqrt_BinFloat {Tl} : forall (t : ArithExpr Tl BinFloat) (lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) -> 0 <= evalRounded t lM mode_NE -> eqExprTypePrim (evalPrim (Sqrt t) lP) (evalRounded (Sqrt t) lM mode_NE).
proof: Proof. intros t lP lM [fint B2Rt] H. simpl. generalize (Bsqrt_correct _ _ HPrec_gt_0 HPrec_lt_emax mode_NE (P2C (evalPrim t lP))). rewrite <-is_finite_SF_B2SF. intros [H1 [H2' H3]]. simpl in fint, B2Rt. unfold P2C in *. rewrite <-B2SF_Prim2B, SF2R_B2SF in B2Rt. rewrite <-B2SF_Prim2B in fint. assert (H2 : is_finite_SF (B2SF (@Bsqrt Rrnd.prec Rrnd.emax HPrec_gt_0 HPrec_lt_emax mode_NE (Prim2B (evalPrim t lP)))) = true). { destruct Prim2B; [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 eqExprTypePrim. simpl. unfold FPsqrt. rewrite <-B2SF_Prim2B, SF2R_B2SF. rewrite sqrt_equiv. split; [assumption |]. unfold FloatOps.prec, FloatOps.emax, Rrnd.prec, Rrnd.emax, Format64.prec, Format64.emax in *. unfold HPrec_gt_0, HPrec_lt_emax in H1. now rewrite H1, B2Rt. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)