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 => nth n (eval_ext prog (Xreal x :: map Xreal vars)) Xnan).
proof: Proof. intros prec deg prog bounds vars Hv n xi. unfold eval, eval_ext. rewrite rev_formula. apply (@TM.approximates_ext (fun t => nth n (fold_right (fun y l => eval_generic_body ext_operations l y) (Xreal t :: map Xreal vars) (rev prog)) Xnan)). intros t. apply (f_equal (fun v => nth n v _)). apply sym_eq, rev_formula. revert n. induction (rev prog) as [|t l]. - intros [|n]. + now apply TM.var_correct. + simpl. rewrite (nth_map I.nai). destruct le_lt_dec as [H|H]. rewrite nth_overflow. eapply TM.approximates_ext. easy. now apply TM.dummy_correct. rewrite map_length. now rewrite <- (proj1 Hv). rewrite (nth_map_lt 0). eapply TM.approximates_ext. easy. apply TM.const_correct. apply Hv. now rewrite <- (proj1 Hv). - intros [|n]. 2: apply IHl. simpl. destruct t as [|uo n1|bo n1 n2]. + apply IHl. + generalize (IHl n1). destruct uo. apply TM.opp_correct. apply TM.abs_correct. apply TM.inv_correct. apply TM.sqr_correct. apply TM.sqrt_correct. apply TM.cos_correct. apply TM.sin_correct. apply TM.tan_correct. apply TM.atan_correct. apply TM.exp_correct. apply TM.ln_correct. apply TM.power_int_correct. apply TM.nearbyint_correct. apply TM.round_flt_correct. apply TM.error_flt_correct. apply TM.round_fix_correct. apply TM.error_fix_correct. + generalize (IHl n1) (IHl n2). destruct bo. apply TM.add_correct. apply TM.sub_correct. apply TM.mul_correct. apply TM.div_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