proposition: Theorem abs_correct : extension Xabs abs.
proof: Proof. intros [ | xl xu] [ | x] Hx ; trivial; [ | ]. { now revert Hx; unfold convert; case (_ && _). } simpl. generalize (sign_large_correct_ _ _ _ Hx). case (sign_large_ xl xu) ; intros. { rewrite (proj1 H). rewrite Rabs_R0. simpl. rewrite F'.valid_lb_zero, F'.valid_ub_zero. rewrite F.zero_correct. split ; exact (Rle_refl R0). } { rewrite (Rabs_left1 _ (proj1 H)). exact (neg_correct _ _ Hx). } { rewrite (Rabs_right _ (Rle_ge _ _ (proj1 H))). exact Hx. } clear H. simpl. rewrite F.zero_correct. rewrite F'.valid_lb_zero. assert (Vxu : F.valid_ub xu = true). { revert Hx; unfold convert; case (F.valid_ub xu); [easy|]. rewrite andb_comm; intros (H0, H1); lra. } revert Hx; unfold convert; rewrite Vxu. case_eq (F.valid_lb xl); [|now intros _ [H0 H1]; exfalso; lra]. intros Vxl [Hxl Hxu]. generalize (F.max_correct (F.neg xl) xu). generalize (F.real_correct xu) ; generalize (F.classify_correct xu) ; generalize Vxu; rewrite F.valid_ub_correct ; case (F.classify xu); try easy; intros _ H; rewrite H; clear H ; [xreal_tac xu; [easy|intros _]|xreal_tac xu; [intros _|easy]..] ; ( generalize (F.real_correct (F.neg xl)) ; generalize (F.classify_correct (F.neg xl)) ; generalize Vxl ; rewrite F'.neg_correct, <-F'.valid_ub_neg, F.valid_ub_correct ; ( case (F.classify (F.neg xl)); try easy; intros _ H; rewrite H; clear H ) ; [xreal_tac xl; [easy|intros _]|xreal_tac xl; [intros _|easy]..] ) ; simpl ; intro Hmax ; rewrite ?Hmax ; try match type of Hmax with | F.toX _ = Xreal _ => rewrite F'.valid_ub_real; [|now rewrite F.real_correct, Hmax] | F.classify ?m = _ => generalize (F.valid_ub_correct m) ; rewrite Hmax => -> end ; ( split; [now apply Rabs_pos|] ) ; [|now generalize (F.classify_correct (F.max (F.neg xl) xu)) ; rewrite Hmax ; rewrite F.real_correct ; xreal_tac2..]. apply <- Rmax_Rle. unfold Rabs. destruct (Rcase_abs x) as [H|H]. { left. apply Ropp_le_contravar. exact Hxl. } right. exact Hxu. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval