proposition: Theorem eval_correct_ext : forall prec prog bounds vars, contains_all bounds vars -> forall n, I.extension (fun x => nth n (eval_ext prog (x :: map Xreal vars)) Xnan) (fun b => eval prec prog bounds n b).
proof: Proof. intros prec prog bounds vars Hv n xi x Hx. unfold eval. pose (f := fun x => nth n (eval_ext prog (x :: map Xreal vars)) Xnan). fold (f x). pose (ff' := fun x => nth n (eval_generic (diff_operations _ ext_operations) prog ((x, Xmask (Xreal 1) x) :: map (fun v => (Xreal v, Xmask (Xreal 0) x)) vars)) (Xnan, Xnan)). set (fi := fun xi => nth n (BndValuator.eval prec prog (xi :: bounds)) I.nai). pose (ffi' := fun xi => nth n (eval_generic (diff_operations _ (BndValuator.operations prec)) prog ((xi, I.mask (I.fromZ_small 1) xi) :: map (fun b => (b, I.mask I.zero xi)) bounds)) (I.nai, I.nai)). fold (ffi' xi). rewrite (surjective_pairing (ffi' xi)). assert (H := eval_diff_bnd_correct prec prog bounds vars Hv n). replace (fst (ffi' xi)) with (fi xi) by apply H. pose (fi' := fun xi => snd (ffi' xi)). fold (fi' xi). pose (f' x := snd (ff' x)). refine (diff_refining_correct prec f f' _ _ _ _ _ xi x Hx) ; clear Hx xi x. - now apply BndValuator.eval_correct_ext. - intros xi x Hx. now apply H. - intros x. apply eval_diff_correct. 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