proposition: Theorem eval_correct_aux' : forall prec deg prog bounds vars, contains_all bounds vars -> forall n xi, TM.approximates xi (nth n (eval prec deg xi prog (TM.var :: map TM.const bounds)) TM.dummy) (fun x => Xreal (nth n (eval_real prog (x :: vars)) 0)).
proof: Proof. intros prec deg prog bounds vars Hv n xi. generalize (eval_correct_aux prec deg prog bounds vars Hv n xi). intros H Ex. specialize (H Ex). destruct (nth n _ _) as [c| |]. - destruct H as [->|[[|y] H1 H2]]. now left. left. now destruct (I.convert c). right. exists (Xreal y). exact H1. intros x Hx. apply (xreal_to_real (fun x => x = Xreal y) (fun x => Xreal x = Xreal y)) ; try easy. now apply H2. - intros y Hy. apply (xreal_to_real (fun x => x = Xreal y) (fun x => Xreal x = Xreal y)) ; try easy. now apply H. - destruct H as [H1 H2 H3 H4 H5]. split ; try easy. destruct H5 as [Q H6 H7]. exists Q. exact H6. intros x Hx. simpl. set (x0 := proj_val (I.F.convert (I.midpoint xi))). apply (xreal_to_real (fun v => (v = Xnan -> I.convert (Taylor_model_sharp.error r) = Inan) /\ contains (I.convert (Taylor_model_sharp.error r)) (Xreal (proj_val v - Datatypes.PolR.horner tt Q (x - x0)))) (fun v => contains (I.convert (Taylor_model_sharp.error r)) (Xreal (v - Datatypes.PolR.horner tt Q (x - x0))))). + intros [Ha _]. now rewrite Ha. + intros a Ha. apply Ha. + simpl. split. now apply H1. now apply H7. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog