proposition: Lemma sign_large_correct_ : forall xl xu x, contains (convert (Ibnd xl xu)) (Xreal x) -> match sign_large_ 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)]. simpl. unfold sign_large_. rewrite 2!F.cmp_correct. rewrite 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); intro Cxl ; [..|easy] ; [case_eq (F.toX xl); [easy|] ; intros rxl Hrxl _ |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); intro Cxu ; [..|easy|] ; [case_eq (F.toX xu); [easy|] ; intros rxu Hrxu _ |case_eq (F.toX xu); [|easy] ; intros Hrxu _..] ) ; intros _ _ [Hxl Hxu] ; unfold Xcmp ; try ( case (Rcompare_spec rxl 0) ; intros Hrxl0 ) ; try ( case (Rcompare_spec rxu 0) ; intros Hrxu0 ) ; rewrite ?Hrxl0, ?Hrxu0 ; ( split; [lra|] ) ; try ( easy || lra ) ; ( split ; [try ( exact I || lra )|] ) ; try ( now exists 0%R; split; [|lra] ) ; try ( now exists rxu; split; [|lra] ) ; try ( now exists rxl; split; [|lra] ). Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval