proposition: Theorem eval_goal_bnd_correct : forall prec g xi x, contains (I.convert xi) (Xreal x) -> eval_goal_bnd prec g xi = true -> eval_goal g x.
proof: Proof. intros prec g xi x Ix. unfold eval_goal_bnd. destruct (I.is_empty xi) eqn:Ex. { now elim I.is_empty_correct with (1 := Ix). } clear Ex. destruct g as [b v|b u|u v|u v|u v|u v|b v|v|u|b u] ; simpl ; intros H. - cut (x <= eval v nil)%R. now destruct b ; [|apply Rle_ge]. assert (H' := I.subset_correct _ _ _ Ix H). apply I.lower_complement_correct with (2 := H'). apply E.eval_bnd_correct. - cut (eval u nil <= x)%R. now destruct b ; [|apply Rle_ge]. assert (H' := I.subset_correct _ _ _ Ix H). apply I.upper_complement_correct with (2 := H'). apply E.eval_bnd_correct. - assert (H' := I.subset_correct _ _ _ Ix H). apply I.meet_correct' in H'. split. apply I.upper_complement_correct with (2 := proj1 H'). apply E.eval_bnd_correct. apply I.lower_complement_correct with (2 := proj2 H'). apply E.eval_bnd_correct. - generalize (I.sign_strict_correct (I.sub prec xi (E.eval_bnd prec u))). destruct I.sign_strict ; try easy. intros Hd. split. apply Rminus_gt. apply (Hd (Xreal (x - eval u nil))). apply J.sub_correct with (1 := Ix). apply E.eval_bnd_correct. assert (H' := I.subset_correct _ _ _ Ix H). apply I.lower_complement_correct with (2 := H'). apply E.eval_bnd_correct. - generalize (I.sign_strict_correct (I.sub prec xi (E.eval_bnd prec v))). destruct I.sign_strict ; try easy. intros Hd. split. assert (H' := I.subset_correct _ _ _ Ix H). apply I.upper_complement_correct with (2 := H'). apply E.eval_bnd_correct. apply Rminus_lt. apply (Hd (Xreal (x - eval v nil))). apply J.sub_correct with (1 := Ix). apply E.eval_bnd_correct. - generalize (I.sign_strict_correct (I.sub prec xi (E.eval_bnd prec u))). destruct I.sign_strict ; try easy. intros Hd. generalize (I.sign_strict_correct (I.sub prec xi (E.eval_bnd prec v))). destruct I.sign_strict ; try easy. intros He. split. apply Rminus_gt. apply (Hd (Xreal (x - eval u nil))). apply J.sub_correct with (1 := Ix). apply E.eval_bnd_correct. apply Rminus_lt. apply (He (Xreal (x - eval v nil))). apply J.sub_correct with (1 := Ix). apply E.eval_bnd_correct. - cut (Rabs x <= eval v nil)%R. now destruct b ; [|apply Rle_ge]. assert (H' := I.subset_correct _ _ _ Ix H). apply I.meet_correct' in H'. apply Rabs_le. destruct H' as [H1 H2]. split. rewrite <- (Ropp_involutive x) in H1 |- *. apply Ropp_le_contravar. apply (I.neg_correct' _ (Xreal (-x))) in H1. apply I.lower_complement_correct with (2 := H1). apply E.eval_bnd_correct. apply I.lower_complement_correct with (2 := H2). apply E.eval_bnd_correct. - apply Rminus_lt. generalize (I.sign_strict_correct (I.sub prec xi (E.eval_bnd prec v))). destruct I.sign_strict ; try easy. intros Hd. apply (Hd (Xreal (x - eval v nil))). apply J.sub_correct with (1 := Ix). apply E.eval_bnd_correct. - apply Rminus_gt. generalize (I.sign_strict_correct (I.sub prec xi (E.eval_bnd prec u))). destruct I.sign_strict ; try easy. intros Hd. apply (Hd (Xreal (x - eval u nil))). apply J.sub_correct with (1 := Ix). apply E.eval_bnd_correct. - cut (x - eval u nil <> 0)%R. destruct b ; lra. generalize (I.sign_strict_correct (I.sub prec xi (E.eval_bnd prec u))). destruct I.sign_strict ; try easy ; intros Hd. apply Rlt_not_eq. apply (Hd (Xreal (x - eval u nil))). apply J.sub_correct with (1 := Ix). apply E.eval_bnd_correct. apply Rgt_not_eq. apply (Hd (Xreal (x - eval u nil))). apply J.sub_correct with (1 := Ix). apply E.eval_bnd_correct. Qed.
imports: Coq(Reals Psatz) Flocq(Raux) Coq(List) Xreal Interval Tree Prog