proposition: Lemma contains_RInt_gen_zero : forall prec deg limit check vars hyps mi mp mr pf pv cf cv, R.eval_hyps_bnd (R.merge_hyps prec hyps) vars -> (forall yi vi f v, contains (I.convert vi) (Xreal v) -> (forall t, (0 <= t <= v)%R -> continuous f t) -> (forall t, (0 <= t <= v)%R -> contains (I.convert yi) (Xreal (f t))) -> I.bounded yi = true -> I.convert (mi prec vi) <> Inan -> exists I : R, is_RInt_gen (fun t : R => f t * mr t) (at_right 0) (at_point v) I /\ contains (I.convert (I.mul prec yi (mi prec vi))) (Xreal I)) -> (forall c t, nth 0 (Prog.eval_real mp (t :: c)) 0 = nth 0 (Prog.eval_real pf (t :: c)) 0 * mr t)%R -> no_floor_prog mp = true -> no_floor_prog pf = true -> let hyps := R.merge_hyps prec hyps in let (mid, Fi) := eval_RInt_gen_zero_init prec deg hyps mi pf mp pv cf cf cv in contains (I.convert (IR.bisect prec limit mid Fi check)) (Xreal (RInt_gen (fun t => Prog.eval_real' pf (t :: vars) cf * mr t) (at_right 0) (at_point (Prog.eval_real' pv vars cv)))).
proof: Proof. intros prec deg limit check vars hyps mi mp mr pf pv cf cv H' Hf Hm1 Hm2 Hp. unfold Prog.eval_real'. simpl. fold (compute_inputs prec hyps cv). assert (Hcv := app_merge_hyps_eval_bnd prec _ _ cv H'). generalize (A.BndValuator.eval_correct' prec pv _ _ Hcv 0). generalize (nth 0 (A.BndValuator.eval prec pv (compute_inputs prec hyps cv)) I.nai). generalize (nth 0 (Prog.eval_real pv (vars ++ map (fun c => eval c nil) cv)) 0%R). clear -H' Hf Hm1 Hm2 Hp. intros v vi Hv. apply IR.bisect_correct with (uf := at_right 0) (vf := at_point v) ; [ typeclasses eauto .. | idtac ]. intros u' v'. fold (compute_inputs prec hyps cf). apply (app_merge_hyps_eval_bnd prec _ _ cf) in H'. set (bounds := compute_inputs prec hyps cf). set (fi := fun b => nth 0 (A.BndValuator.eval prec pf (b :: bounds)) I.nai). set (fmi := fun b => nth 0 (A.BndValuator.eval prec mp (b :: bounds)) I.nai). set (Fi1 := let bounds := map A.TaylorValuator.TM.const bounds in fun ui vi => let xi := I.join ui vi in let gi := A.TaylorValuator.TM.get_tm (prec, deg) xi (nth 0 (A.TaylorValuator.eval prec deg xi mp (A.TaylorValuator.TM.var :: bounds)) A.TaylorValuator.TM.dummy) in IT.taylor_integral_naive_intersection prec fmi gi xi ui vi). set (Fi2 := let bounds := map A.TaylorValuator.TM.const bounds in fun vi => let yi := fi (I.join I.zero vi) in if I.bounded yi then I.mul prec yi (mi prec vi) else I.nai). apply IR.valid_at_mixed' with (u := at_right 0) (v := v) (fi1 := Fi1) (fi2 := Fi2) (vi := vi) (u' := u') (v' := v'). - typeclasses eauto. - exact Hv. - clear -H' Hf Hm1 Hm2 Hp. intros ui vi u v Hu Hv. 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 * mr t) u v) as [I HI]. eapply ex_RInt_ext. intros x _. apply Hm1. apply (A.BndValuator.ex_RInt_eval prec) with (xi := I.join ui vi) (1 := H'). apply Hm2. 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 Fi1, IT.taylor_integral_naive_intersection, fmi. clear -Hi. rewrite I.real_correct. destruct (I.convert (I.mul _ _ _)) as [|il iu] eqn:Hm. easy. exfalso. eapply I.mul_propagate_r in Hi. fold bounds in Hi. now rewrite Hm in Hi. 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 Hx. rewrite <- Hm1. now apply A.BndValuator.eval_correct_ext'. apply A.TaylorValuator.TM.get_tm_correct ; cycle 1. exists u. apply I.join_correct. now left. eapply A.TaylorValuator.TM.approximates_ext. intros x. rewrite <- Hm1. easy. now apply A.TaylorValuator.eval_correct_aux'. - clear -H' Hp Hf. intros vi v Hv. apply RInt_gen_helper ; [typeclasses eauto .. | idtac]. unfold Fi2. destruct I.bounded eqn:Hb ; cycle 1. now rewrite I.nai_correct. assert (Ht': forall t, (0 <= t <= v)%R -> contains (I.convert (I.join I.zero vi)) (Xreal t)). apply contains_connected. apply I.join_correct. left. rewrite I.zero_correct. split ; apply Rle_refl. apply I.join_correct. now right. intros Hi. apply Hf with (1 := Hv) (4 := Hb). + intros t Ht. apply A.BndValuator.continuous_eval with (prec := prec) (xi := I.join I.zero vi) (1 := H') (2 := Hp). now apply Ht'. change (I.convert (fi (I.join I.zero vi)) <> Inan). contradict Hi. now apply I.mul_propagate_l. + intros t Ht. apply A.BndValuator.eval_correct_ext' with (1 := H'). now apply Ht'. + contradict Hi. now apply I.mul_propagate_r. 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