proposition: Theorem subset_correct : forall xi yi v, contains (convert xi) v -> subset xi yi = true -> contains (convert yi) v.
proof: Proof. intros xi yi. case xi ; case yi ; try (simpl ; intros ; try exact I ; discriminate). unfold subset. intros yl yu xl xu v Hv. generalize (is_empty_correct (Ibnd xl xu) v Hv). destruct is_empty. { intros H H'. now elim H. } intros _. revert Hv. simpl. rewrite !F.cmp_correct, !F.valid_lb_correct, !F.valid_ub_correct. generalize (F.classify_correct xl); rewrite F.real_correct. generalize (F.classify_correct xu); rewrite F.real_correct. generalize (F.classify_correct yl); rewrite F.real_correct. generalize (F.classify_correct yu); rewrite F.real_correct. intros Hyu Hyl Hxu Hxl Hv. assert (Hc : match F.classify xl with Fpinfty => false | _ => true end && match F.classify xu with Fminfty => false | _ => true end = true). { clear -Hv. destruct andb. easy. destruct v as [|v]. easy. elim (Rlt_irrefl v). apply Rle_lt_trans with (1 := proj2 Hv). apply Rlt_le_trans with (2 := proj1 Hv). exact Rlt_0_1. } rewrite Hc in Hv. destruct v as [|v]. easy. revert Hxl Hyl Hxu Hyu Hc. case (F.classify xl) ; destruct (F.toX xl) as [|xlr] ; try easy ; intros _ ; case (F.classify yl) ; destruct (F.toX yl) as [|ylr] ; try easy ; intros _ ; case (F.classify xu) ; destruct (F.toX xu) as [|xur] ; try easy ; intros _ ; case (F.classify yu) ; destruct (F.toX yu) as [|yur] ; try easy ; intros _ ; intros _ ; simpl ; (try now rewrite andb_false_r) ; simpl in Hv ; case Rcompare_spec ; try easy ; try lra ; case Rcompare_spec ; try easy ; try lra. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval