proposition: Lemma eval_correct_aux : forall prec prog bounds vars, (forall n, contains (I.convert (nth n bounds I.nai)) (nth n vars Xnan)) -> forall n, contains (I.convert (nth n (eval prec prog bounds) I.nai)) (nth n (eval_ext prog vars) Xnan).
proof: Proof. intros prec prog bounds vars Hinp. unfold eval, eval_ext. apply (eval_inductive_prop _ _ (fun a b => contains (I.convert a) b)). destruct o ; simpl ; [ apply I.neg_correct | apply I.abs_correct | apply I.inv_correct | apply I.sqr_correct | apply I.sqrt_correct | apply I.cos_correct | apply I.sin_correct | apply I.tan_correct | apply I.atan_correct | apply I.exp_correct | apply I.ln_correct | apply I.power_int_correct | apply I.nearbyint_correct | apply J.round_flt_correct' | apply I.error_flt_correct | apply J.round_fix_correct' | apply I.error_fix_correct ]. destruct o ; simpl ; [ apply I.add_correct | apply I.sub_correct | apply I.mul_correct | apply I.div_correct ]. exact Hinp. 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