proposition: Lemma abs_correct_aux : forall xl xu x, contains (convert (Ibnd xl xu)) (Xreal x) -> let xm := F.max (F.neg xl) xu in le_upper (Xreal (Rabs x)) (F.toX xm).
proof: Proof. intros xl xu x Hx xm. generalize (F.neg_correct xl). intros Hxl. generalize (F.max_correct (F.neg xl) xu). intros Hxm. destruct (F.classify xl) eqn:Hxl_eq. - generalize (F.classify_correct (F.neg xl)). rewrite F'.real_neg. rewrite (F.classify_correct xl). rewrite Hxl_eq. destruct (F.classify (F.neg xl)); [| easy..]. intros _. destruct (F.classify xu) eqn:Hxu_eq. + unfold xm. rewrite Hxm, Hxl. simpl in Hx. rewrite F.valid_lb_correct, F.valid_ub_correct in Hx. rewrite Hxl_eq, Hxu_eq in Hx. simpl in Hx. generalize (F.classify_correct xu). rewrite (F.real_correct xu). rewrite Hxu_eq. generalize (F.classify_correct xl). rewrite (F.real_correct xl). rewrite Hxl_eq. intros Hxl' Hxu'. destruct (F.toX xl), (F.toX xu); try easy. simpl. apply Rmax_Rle. destruct (Rle_or_lt 0 x). * apply Rabs_pos_eq in H. rewrite H. now right. * apply Rabs_left in H. rewrite H. lra. + unfold xm. rewrite F'.real_correct_false; [easy |]. rewrite F.classify_correct. now rewrite Hxm. + specialize (F.real_correct xm) as Hxm'. unfold xm in *. rewrite Hxm in *. rewrite F'.real_neg, F.classify_correct, Hxl_eq in Hxm'. destruct (F.toX (F.neg xl)); [easy | clear Hxm']. rewrite Hxl. simpl in Hx. rewrite F.valid_lb_correct, F.valid_ub_correct in Hx. rewrite Hxl_eq, Hxu_eq in Hx. simpl in Hx. lra. + unfold xm. rewrite F'.real_correct_false; [easy |]. rewrite F.classify_correct. now rewrite Hxm. - rewrite Hxl in Hxm. rewrite F'.real_correct_false; [easy |]. rewrite F.classify_correct. unfold xm. now rewrite Hxm. - rewrite Hxl in Hxm. now destruct (F.classify xu); rewrite F'.real_correct_false; try (rewrite F.classify_correct; unfold xm; rewrite Hxm). - rewrite Hxl in Hxm. destruct (F.classify xu) eqn:Hxu_eq. + unfold xm. rewrite Hxm. simpl in Hx. rewrite F.valid_lb_correct, F.valid_ub_correct in Hx. rewrite Hxl_eq, Hxu_eq in Hx. simpl in Hx. lra. + rewrite F'.real_correct_false; [easy |]. rewrite F.classify_correct. unfold xm. now rewrite Hxm. + unfold xm. rewrite Hxm. simpl in Hx. rewrite F.valid_lb_correct, F.valid_ub_correct in Hx. rewrite Hxl_eq, Hxu_eq in Hx. simpl in Hx. lra. + rewrite F'.real_correct_false; [easy |]. rewrite F.classify_correct. unfold xm. now rewrite Hxm. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval