proposition: Lemma contains_RInt : forall prec deg limit check vars hyps pf pu pv cf cu cv, R.eval_hyps_bnd (R.merge_hyps prec hyps) vars -> no_floor_prog pf = true -> let hyps := R.merge_hyps prec hyps in let (mid, Fi) := eval_RInt_init prec deg hyps pf pu pv cf cu cv in contains (I.convert (IR.bisect prec limit mid Fi check)) (Xreal (RInt (fun t => Prog.eval_real' pf (t :: vars) cf) (Prog.eval_real' pu vars cu) (Prog.eval_real' pv vars cv))).
proof: Proof. intros prec deg limit check vars hyps pf pu pv cf cu cv H' Hp. unfold eval_RInt_init, Prog.eval_real'. simpl. fold (compute_inputs prec hyps cu). fold (compute_inputs prec hyps cv). assert (Hcu := app_merge_hyps_eval_bnd prec _ _ cu H'). assert (Hcv := app_merge_hyps_eval_bnd prec _ _ cv H'). generalize (A.BndValuator.eval_correct' prec pv _ _ Hcv 0). generalize (A.BndValuator.eval_correct' prec pu _ _ Hcu 0). generalize (nth 0 (A.BndValuator.eval prec pv (compute_inputs prec hyps cv)) I.nai). generalize (nth 0 (A.BndValuator.eval prec pu (compute_inputs prec hyps cu)) I.nai). generalize (nth 0 (Prog.eval_real pv (vars ++ map (fun c => eval c nil) cv)) 0%R). generalize (nth 0 (Prog.eval_real pu (vars ++ map (fun c => eval c nil) cu)) 0%R). clear -H' Hp. intros u v ui vi Hu Hv. apply IR.contains_RInt_valid. apply IR.bisect_correct ; [ typeclasses eauto .. | idtac ]. intros u' v'. set (cbu := match u' with IR.IBu => ui | IR.IBv => vi | IR.IBp x => I.singleton x end). set (cbv := match v' with IR.IBu => ui | IR.IBv => vi | IR.IBp x => I.singleton x end). fold (compute_inputs prec hyps cf). match goal with | |- IR.valid _ _ _ _ _ ?fi => let fi' := eval pattern cbu, cbv in fi in change fi with fi' end. apply IR.valid_at_point ; try easy. apply (app_merge_hyps_eval_bnd prec _ _ cf) in H'. clear -H' Hp. intros ui vi u v Hu Hv. set (i := IT.taylor_integral_naive_intersection _ _ _ _ _ _). apply RInt_helper. intros Hi. assert (ex_RInt (fun t => nth 0 (Prog.eval_real pf (t :: vars ++ map (fun c => eval c nil) cf)) 0%R) u v) as [I HI]. apply (A.BndValuator.ex_RInt_eval prec) with (xi := I.join ui vi) (1 := H') (2 := Hp). apply contains_connected. apply Rmin_case ; apply I.join_correct. now left. now right. apply Rmax_case ; apply I.join_correct. now left. now right. contradict Hi. unfold i, IT.taylor_integral_naive_intersection. clear i. rewrite I.real_correct. destruct (I.convert (I.mul _ _ _)) as [|il iu] eqn:Hm. easy. exfalso. now rewrite I.mul_propagate_r in Hm. exists I. apply (conj HI). rewrite <- is_RInt_unique with (1 := HI). apply IT.taylor_integral_naive_intersection_correct ; cycle 2. now exists I. exact Hu. exact Hv. apply I.join_correct. now left. apply I.join_correct. now right. intros xi x Ix. now apply A.BndValuator.eval_correct_ext'. apply A.TaylorValuator.TM.get_tm_correct ; cycle 1. exists u. apply I.join_correct. now left. now apply A.TaylorValuator.eval_correct_aux'. Qed.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Coquelicot(Coquelicot) Stdlib Coquelicot Xreal Basic Sig Interval Integral Eval Bertrand Tree Prog Reify Refine Interval_helper