proposition: Theorem refine_root_correct : forall prec depth vars hyps px cx pf cf pg cg g, refine_root prec depth hyps px cx pf cf pg cg g = true -> eval_hyps hyps vars (eval_real' pf (eval_real' px vars cx :: vars) cf = 0%R -> eval_goal g (eval_real' pg (eval_real' px vars cx :: vars) cg)).
proof: Proof. intros prec depth vars hyps px cx pf cf pg cg g H. apply (R.eval_hyps_bnd_correct prec). set (x := eval_real' px vars cx). intros H1 H2. unfold refine_root in H. revert H. set (xi := nth 0 _ _). assert (Hx: contains (I.convert xi) (Xreal x)). { apply A.BndValuator.eval_correct'. now apply app_merge_hyps_eval_bnd. } clearbody xi. revert xi Hx. induction depth as [|depth IH]. easy. intros xi Hx. simpl. fold (compute_inputs prec hyps cf). refine (_ (A.DiffValuator.root_correct prec pf (compute_inputs prec hyps cf) _ _ xi x Hx H2)). 2: now apply app_merge_hyps_eval_bnd. set (xi' := A.DiffValuator.root _ _ _ _). intros Hx' H. destruct check_goal eqn:Hg ; [|destruct fast_enough]. - clear H IH. apply (R.eval_goal_bnd_correct prec) with (2 := Hg). unfold eval_real'. fold (compute_inputs prec hyps cg). simpl. apply A.BndValuator.eval_correct_ext' with (2 := Hx'). now apply app_merge_hyps_eval_bnd. - now apply (IH _ Hx'). - generalize (I.bisect_correct _ _ Hx'). destruct (I.bisect xi') as [xi1 xi2]. destruct refine_root_aux eqn:Hb. now intros [K|K] ; apply (IH _ K). easy. Qed.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify Interval_helper