proposition: Theorem midpoint_correct : forall xi, not_empty (convert xi) -> F.toX (midpoint xi) = Xreal (proj_val (F.toX (midpoint xi))) /\ contains (convert xi) (F.toX (midpoint xi)).
proof: Proof. intros [|xl xu]. { intros _. refine (conj _ I). simpl. now rewrite F.zero_correct. } intros (x, Hx). unfold midpoint, c1, cm1, c2. destruct (F.real xl) eqn:Rl. - destruct (F.real xu) eqn:Ru. + revert Hx. simpl. rewrite F'.valid_lb_real, F'.valid_ub_real by easy. rewrite 2!F'.real_correct by easy. intros [Hxl Hxu]. destruct (F.midpoint_correct _ _ eq_refl Rl Ru (Rle_trans _ _ _ Hxl Hxu)) as [Hm1 Hm2]. simpl. now rewrite F'.real_correct. + assert (Hx': (proj_val (F.toX xl) <= x)%R). { revert Hx. simpl. case andb ; simpl. now rewrite F'.real_correct. lra. } assert (Hz: forall z, (F.toR xl <= z)%R -> contains (convert (Ibnd xl xu)) (Xreal z)). { intros z Hz. revert Hx. simpl. case andb ; simpl. intros _. split. now rewrite F'.real_correct. now rewrite F'.real_correct_false. lra. } rewrite F.cmp_correct. rewrite F'.classify_real by easy. rewrite F'.classify_real by now rewrite F.real_correct, F.zero_correct. rewrite (F'.real_correct xl) by easy. rewrite F.zero_correct. simpl Xcmp. case Rcompare_spec ; intros Hl. * rewrite F.zero_correct. apply (conj eq_refl). apply Hz. now apply Rlt_le. * rewrite F.fromZ_correct by easy. apply (conj eq_refl). apply Hz. rewrite Hl. apply Rle_0_1. * destruct (F.mul_UP_correct p52 xl (F.fromZ 2)) as [Hm1 Hm2]. { left. unfold F.is_non_neg'. split. rewrite F'.real_correct by easy. now apply Rlt_le. rewrite F.fromZ_correct by easy. now apply IZR_le. } destruct (F.real (F.mul_UP p52 xl (F.fromZ 2))) eqn:Rp. split. now apply F'.real_correct. rewrite F'.real_correct by easy. apply Hz. revert Hm2. unfold le_upper, F.toR. rewrite F'.real_correct by easy. rewrite F'.real_correct by easy. rewrite F.fromZ_correct by easy. simpl. lra. split. now apply F'.real_correct. rewrite F'.real_correct by easy. apply Hz. apply Rle_refl. - destruct (F.real xu) eqn:Ru. + assert (Hx': (x <= proj_val (F.toX xu))%R). { revert Hx. simpl. case andb ; simpl. now rewrite (F'.real_correct xu). lra. } assert (Hz: forall z, (z <= F.toR xu)%R -> contains (convert (Ibnd xl xu)) (Xreal z)). { intros z Hz. revert Hx. simpl. case andb ; simpl. intros _. split. now rewrite F'.real_correct_false. now rewrite F'.real_correct. lra. } rewrite F.cmp_correct. rewrite F'.classify_real by easy. rewrite F'.classify_real by now rewrite F.real_correct, F.zero_correct. rewrite (F'.real_correct xu) by easy. rewrite F.zero_correct. simpl Xcmp. case Rcompare_spec ; intros Hu. * destruct (F.mul_DN_correct p52 xu (F.fromZ 2)) as [Hm1 Hm2]. { right. right. right. unfold F.is_non_pos', F.is_non_neg'. split. rewrite F'.real_correct by easy. now apply Rlt_le. rewrite F.fromZ_correct by easy. now apply IZR_le. } destruct (F.real (F.mul_DN p52 xu (F.fromZ 2))) eqn:Rp. split. now apply F'.real_correct. rewrite F'.real_correct by easy. apply Hz. revert Hm2. unfold le_lower, le_upper, F.toR. unfold Xneg. rewrite F'.real_correct by easy. rewrite F'.real_correct by easy. rewrite F.fromZ_correct by easy. simpl. lra. split. now apply F'.real_correct. rewrite F'.real_correct by easy. apply Hz. apply Rle_refl. * rewrite F.fromZ_correct by easy. apply (conj eq_refl). apply Hz. rewrite Hu. now apply IZR_le. * rewrite F.zero_correct. apply (conj eq_refl). apply Hz. now apply Rlt_le. + rewrite F.zero_correct. apply (conj eq_refl). revert Hx. simpl. case andb ; simpl. intros _. now rewrite 2!F'.real_correct_false. lra. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval