proposition: Lemma TM_invsqrt_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_invsqrt X0 X n) (fun x => Xinv (Xsqrt (Xreal x))).
proof: Proof. move=> Hsubset Hex. rewrite /TM_invsqrt. case E1: gt0. apply i_validTM_Ztech with (TR.T_invsqrt tt); last 2 first =>//. move=> Y y Hy. replace (Xbind _ y) with (Xinv (Xsqrt y)) by now case y. apply: I.inv_correct; 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 _ (fun t => / sqrt t)); last first. apply: (locally_open (fun t => 0 < t)%R); [exact: open_gt| |exact: gt0_correct E1]. move=> y Hy. rewrite /Xinv' /Xsqrt' /= ?is_zero_false //. now apply Rgt_not_eq, sqrt_lt_R0. 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.invsqrt_rec. have gt0_x : (0 < x)%R by move/(gt0_correct Hx) in E1. rewrite !(is_derive_n_unique _ _ _ _ (is_derive_n_invsqrt _ _ 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/eqNaiPy: R_from_nat_correct |apply: J.add_correct |apply: J.neg_correct |Inc ]. apply: J.inv_correct; exact: J.sqrt_correct. } - move=> I r Ir {X0 X n Hsubset Hex E1} Dx n k Hkn. apply: Pol.rec1_propagate. - move=> q m Hq; rewrite /invsqrt_rec. rewrite I.div_propagate_l //. rewrite I.mul_propagate_r //; exact:eqNaiP. - apply/contains_Xnan; rewrite -Dx. exact/I.inv_correct/I.sqrt_correct. by rewrite Pol.size_rec1. - { clear - E1. move=> n x Hx. move/(gt0_correct Hx) in E1. apply: (ex_derive_n_ext_loc (fun t => / sqrt t)). apply: locally_open E1; first exact: open_gt. simpl=> y Hy; rewrite /Xsqrt' /Xinv' /Xbind ?is_zero_false //. apply: Rgt_not_eq; exact: sqrt_lt_R0. exact: ex_derive_n_is_derive_n (is_derive_n_invsqrt n x E1). } constructor =>//. by move=> *; rewrite I.nai_correct. by move=> Hx; rewrite /= I.nai_correct. by rewrite I.nai_correct. exact: Hsubset. exists (TR.T_invsqrt 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/eqNaiPy: R_from_nat_correct |apply: J.add_correct |apply: J.neg_correct |Inc ]. by apply: J.inv_correct; apply: 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