proposition: Theorem eval_bisect_contains_aux : forall prec depth idx vars hyps prog consts b fi, ( forall xi x, A.contains_all xi x -> contains (I.convert (fi xi)) (Xreal (nth 0 (eval_real prog x) 0%R)) ) -> A.bisect (compute_inputs prec hyps consts) idx (fun xi => I.subset (fi xi) b) depth = true -> eval_hyps hyps vars (contains (I.convert b) (Xreal (eval_real' prog vars consts))).
proof: Proof. intros prec depth idx vars hyps prog consts b fi Hfi H. apply (R.eval_hyps_bnd_correct prec). intros H'. apply A.bisect_correct with (P := fun x => contains (I.convert b) (Xreal (nth 0 (eval_real prog x) 0%R))) (2 := H). - intros x xi Ix H''. apply I.subset_correct with (2 := H''). now apply Hfi. - now apply app_merge_hyps_eval_bnd. Qed.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify