proposition: Lemma TM_sqrt_correct (x0 : R) (X0 X : I.type) n : subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (TM_sqrt X0 X n) Xsqrt'.
proof: Proof. move=> Hsubset Hex. rewrite /TM_sqrt. case E1: gt0. apply i_validTM_Ztech with (TR.T_sqrt tt); last 2 first =>//. exact: I.sqrt_correct. constructor. - by move=> *; rewrite PolR.size_rec1. - { move=> {X0 n Hsubset Hex} x n k Hx Hkn. rewrite (Derive_n_ext_loc _ sqrt); last first. apply: (locally_open (fun t => 0 < t)%R); [exact: open_gt| |exact: gt0_correct E1]. by move=> y Hy; rewrite /Xsqrt' //; apply: Rlt_le. rewrite /PolR.nth; elim: k Hkn => [|k IHk] Hkn. by rewrite rec1up_co0 /= Rdiv_1. rewrite nth_rec1up ifF; last by apply: negbTE; rewrite ltnNge Hkn. move/(_ (ltnW Hkn)) in IHk. rewrite nth_rec1up ifF in IHk; last by apply: negbTE; rewrite ltnNge ltnW. rewrite iteriS IHk /TR.sqrt_rec. have gt0_x : (0 < x)%R by move/(gt0_correct Hx) in E1. rewrite !(is_derive_n_unique _ _ _ _ (is_derive_n_sqrt _ _ gt0_x)). rewrite big_ord_recr. set big := \big[Rmult/1%R]_(i < k) _. simpl ([the Monoid.law _ of Rmult] _ _). rewrite fact_simpl mult_INR !addn1. have->: (/2 - INR k.+1 = /2 - INR k + (- 1))%R by rewrite -addn1 plus_INR /=; ring. rewrite Rpower_plus Rpower_Ropp Rpower_1 // /Rdiv. have->: ((/ 2 - INR k) = (INR 1 - INR 2 * INR k.+1.-1) / INR 2)%R by simpl; field. move/(gt0_correct Hx)/Rgt_not_eq in E1. simpl (INR 1). simpl (INR 2). rewrite /=; field. split; [exact: INR_fact_neq_0|split; [|exact: E1]]. change (INR k.+1 <> 0%R); exact: not_0_INR. } constructor. - by move=> *; rewrite PolR.size_rec1 Pol.size_rec1. - { move => {X0 X n Hsubset Hex E1} X0 xi0 n Hx. apply: Pol.rec1_correct =>//. by move=> *; repeat first [apply: J.div_correct |apply: J.mul_correct |apply: J.sub_correct |apply: I.fromZ_correct |apply: J.mul_correct |apply: I.fromZ_correct |exact: I.fromZ_small_correct |apply: R_from_nat_correct ]. exact: J.sqrt_correct. } - move=> I r Ir /= {E1 Hex Hsubset X X0 n} //. - { clear - E1. move=> n x Hx. move/(gt0_correct Hx) in E1. apply: (ex_derive_n_ext_loc sqrt). apply: locally_open E1; first exact: open_gt. simpl=> y Hy; rewrite /Xsqrt' //. exact: ex_derive_n_is_derive_n (is_derive_n_sqrt n x E1). } simpl. split =>//. by move=> *; rewrite I.nai_correct. by rewrite I.nai_correct. exact: Hsubset. exists (TR.T_sqrt tt x0 n). apply: Pol.rec1_correct. by move=> *; repeat first [apply: J.div_correct |apply: J.mul_correct |apply: J.sub_correct |apply: I.fromZ_correct |apply: J.mul_correct |apply: I.fromZ_correct |exact: I.fromZ_small_correct |apply: R_from_nat_correct ]. exact: J.sqrt_correct. by rewrite I.nai_correct. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound