proposition: Theorem eval_correct u (Y : I.type) tf f : approximates Y tf f -> I.extension (Xbind f) (eval u tf Y).
proof: Proof. move=> Hf X x Hx. rewrite /eval. case HXY: I.subset; last by rewrite I.nai_correct. move/I.subset_correct: (HXY) => Hsubset. specialize (Hsubset _ Hx). have HneY: not_empty (I.convert Y). { apply (not_empty_contains _ x). exact: Hsubset. } case: tf Hf => [c| |tm]. case. { easy. } { move=> Hne. now rewrite I.mask_propagate_l. } { move=> H. destruct x as [|x]. now apply contains_Xnan, I.mask_propagate_r, contains_Xnan. apply I.mask_correct'. rewrite /is_const in H. case: H => y H1 H2. now rewrite /= (H2 x). } by case: x Hx Hsubset => [|x] Hx Hsubset //= ->. move=> Hf. have /= {Hf} := get_tm_correct u Hf=> Htm. move/(_ HneY): Htm. case => [Hdef Hnai Hzero _ Hmain]. set c0 := proj_val (I.F.convert (I.midpoint Y)). have [qx Hcont Hdelta] := Hmain. destruct x as [|x] ; simpl. { rewrite I.add_propagate_l //. apply: Bnd.ComputeBound_propagate. rewrite I.sub_propagate_l //. now apply contains_Xnan. } move/(_ x) in Hdelta. have->: f x = Xadd (Xreal (PolR.horner tt qx (Rminus x c0))) (Xsub (f x) (Xreal (PolR.horner tt qx (Rminus x c0)))). case Efx : (f x) => [|r]; first by rewrite Xadd_comm. simpl. by congr Xreal; ring. apply I.add_correct =>//. apply: Bnd.ComputeBound_correct =>//. apply: J.sub_correct Hx _. exact: J.contains_midpoint. case Efx: (f x) => [|fx]. apply/contains_Xnan. apply: Hdef Efx. exact: Hsubset. rewrite Efx in Hdelta. apply: Hdelta. exact: Hsubset. Qed.
imports: Coq(Reals ZArith Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq bigop) Interval Xreal Basic Interval_compl Datatypes Taylor_model_sharp Bound Bound_quad Univariate_sig