proposition: Theorem root_correct : forall prec prog bounds vars, contains_all bounds vars -> forall xi x, contains (I.convert xi) (Xreal x) -> nth 0 (eval_real prog (x :: vars)) 0%R = 0%R -> contains (I.convert (root prec prog bounds xi)) (Xreal x).
proof: Proof. intros prec prog bounds vars Hv xi x Hx Zx. generalize (root_correct_ext prec prog bounds vars Hv _ _ Hx). destruct (nth 0 (eval_ext _ _) Xnan) as [|y] eqn:Hy. - intros _. unfold root. assert (H1 := eval_diff_bnd_correct prec prog bounds vars Hv 0 xi). simpl in H1. destruct (nth 0 (eval_generic _ _ _) _) as [yi zi]. generalize (BndValuator.eval_correct_ext prec prog bounds vars Hv 0 _ _ Hx). rewrite (proj1 H1) Hy. intros H2. generalize (I.sign_strict_correct yi). destruct I.sign_strict ; try now intros H3 ; specialize (H3 _ H2). intros _. apply I.meet_correct with (1 := Hx). apply contains_Inan. apply I.sub_propagate_r. apply I.div_propagate_r. destruct H1 as [_ H1]. specialize (H1 _ Hx). assert (H3 := eval_diff_correct prog vars 0 (Xreal x)). destruct (nth 0 (eval_generic _ _ _) _) as [y y']. apply contains_Xnan. destruct H3 as [_ H3]. unfold Xderive_pt in H3. destruct y' as [|y']. easy. now rewrite Hy in H3. - apply. apply f_equal, sym_eq. rewrite <- Zx. apply (xreal_to_real (fun z => z = Xreal y)). easy. intros r H. now injection H. easy. 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