proposition: Lemma sign_strict_correct_ : forall xl xu x, contains (convert (Ibnd xl xu)) (Xreal x) -> match sign_strict_ xl xu with | Xeq => x = 0%R /\ F.toX xl = Xreal 0 /\ F.toX xu = Xreal 0 | Xlt => (x < 0)%R /\ (match F.toX xl with Xreal rl => (rl < 0)%R | _=> True end) /\ (exists ru, F.toX xu = Xreal ru /\ (ru < 0)%R) | Xgt => (0 < x)%R /\ (match F.toX xu with Xreal ru => (0 < ru)%R | _=> True end) /\ (exists rl, F.toX xl = Xreal rl /\ (0 < rl)%R) | Xund => match F.toX xl with Xreal rl => (rl <= 0)%R | _=> True end /\ match F.toX xu with Xreal ru => (0 <= ru)%R | _=> True end end.
proof: Proof. assert (H1v0 : forall v, ~(1 <= v <= 0)%R). { intros v Hf. apply (Rlt_irrefl 0), (Rlt_le_trans _ 1); [apply Rlt_0_1|]. elim Hf; apply Rle_trans. } intros xl xu x; simpl. case_eq (F.valid_lb xl); intro Vxl; [|now intro H; destruct (H1v0 x)]. case_eq (F.valid_ub xu); intro Vxu; [|now intro H; destruct (H1v0 x)]. unfold sign_strict_. rewrite 2!F.cmp_correct, F.zero_correct, F'.classify_zero. generalize Vxl ; rewrite F.valid_lb_correct ; generalize (F.classify_correct xl) ; rewrite F.real_correct ; case_eq (F.classify xl); [..|easy]; intro Cxl ; [case_eq (F.toX xl); [easy|]; intros rxl|case_eq (F.toX xl); [|easy]..] ; intros Hrxl _ _ ; ( generalize Vxu ; rewrite F.valid_ub_correct ; generalize (F.classify_correct xu) ; rewrite F.real_correct ; case_eq (F.classify xu); [..|easy|]; intro Cxu ; [case_eq (F.toX xu); [easy|]; intros rxu|case_eq (F.toX xu); [|easy]..] ; intros Hrxu _ _ ) ; intros [Hxl Hxu] ; unfold Xcmp ; try ( case Rcompare_spec; intros H1 ; try easy ) ; try ( case Rcompare_spec; intros H2 ; try easy ) ; try lra ; ( split ; [try lra|] ) ; ( split ; [try lra|] ) ; rewrite ?H1, ?H2 ; try easy ; try ( now exists rxu ) ; try ( now exists rxl ). Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval