proposition: Lemma TM_horner_correct (x0 : R) (X0 X : I.type) Mf f pi pr n : contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) Mf f -> pi >:: pr -> i_validTM x0 (I.convert X) (TM_horner n pi Mf X0 X) (fun x : R => Xreal pr.[proj_val (f x)]).
proof: Proof. move=> Hne [Fdef Fnai Fzero Fsubs Fmain] Hp. wlog Hsize : pi pr Hp / Pol.size pi = PolR.size pr => [Hwlog|]. apply: (@TM_fun_eq (fun x : R => Xreal (pad pi pr).[proj_val (f x)])). by move=> x Hx; rewrite /= [in RHS](@horner_pad pi). apply: Hwlog. exact: pad_correct. exact: size_pad. elim/PolR.poly_ind: pr pi Hp Hsize => [|ar pr IHpr] pi Hp Hsize; elim/Pol.poly_ind: pi Hp Hsize =>[|ai pi _] Hp Hsize. + rewrite /TM_horner Pol.fold_polyNil /=. apply: TM_cst_correct =>//. exact: J.zero_correct. + by rewrite sizes in Hsize. + by rewrite sizes in Hsize. + rewrite /= /TM_horner Pol.fold_polyCons. apply: (@TM_fun_eq (fun x : R => Xreal ar + Xreal pr.[proj_val (f x)] * Xreal (proj_val (f x)))%XR). move=> x Hx /=. congr Xreal; ring. apply: TM_add_correct. apply: TM_cst_correct=>//. by have := Hp 0; rewrite Pol.nth_polyCons PolR.nth_polyCons. apply: TM_mul_correct =>//. apply: IHpr. by move=> k; have := Hp k.+1; rewrite Pol.nth_polyCons PolR.nth_polyCons. by move: Hsize; rewrite !sizes; case. 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