proposition: Theorem sqr_correct : forall prec, extension Xsqr (sqr prec).
proof: Proof. intros prec [ | xl xu] [ | x] ; try ( intros ; exact I ) ; [now unfold convert; case (_ && _)|]. intros Hxlu. generalize Hxlu. unfold convert at 1. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; exfalso; lra]. intros Vxu Vxl [Hxl Hxu]. simpl. unfold bnd, contains, convert. generalize (sign_large_correct_ xl xu x Hxlu). unfold Rsqr. case (sign_large_ xl xu) ; intros [Hx0 Hx0'] ; [|revert Hx0'; intros [Hxl0 [rxu [Hrxu Hrxu0]]]..|] ; try ( rewrite F'.valid_lb_real, ?F'.valid_ub_real; [|now rewrite F.real_correct, F.zero_correct..] ; simpl ; try ( rewrite Hx0 ; rewrite Rmult_0_l ) ; split ; rewrite F.zero_correct ; apply Rle_refl ) ; rewrite ?F.cmp_correct, ?F.zero_correct ; rewrite ?F'.classify_zero, ?F'.valid_lb_zero ; try match goal with | |- context [F.mul_DN ?prec ?x ?y] => elim (F.mul_DN_correct prec x x); [intros Vmdn Hmdn| unfold F.is_non_neg_real, F.is_non_neg, F.is_non_pos_real, F.is_non_pos ; rewrite Hrxu ; try ( now left ) ; now right ; left] ; generalize Vmdn ; rewrite ?F.valid_lb_correct, ?F.valid_ub_correct ; case_eq (F.classify (F.mul_DN prec x x)) ; intros Cmdn; try easy; intros _ ; generalize (F.classify_correct (F.mul_DN prec x x)) ; rewrite F.real_correct, Cmdn ; [xreal_tac2; [easy|]; intros _|xreal_tac2; [|easy]; intros _..] ; unfold Xcmp ; try ( case Rcompare_spec ; intros Hr ) ; rewrite ?F'.valid_lb_zero, ?F.valid_lb_correct, ?Cmdn ; rewrite ?F.zero_correct end ; try match goal with | |- context [ F.mul_UP prec ?x ?y ] => elim (F'.mul_UP_correct prec x x) ; [intros Vmdu Hmdu| now rewrite ?Vxl, ?Vxu ; try ( now left ) ; now right ; left] ; rewrite Vmdu ; split end ; try apply Rle_0_sqr ; try ( generalize Hmdu ; unfold le_upper ; xreal_tac2; [easy|] ; xreal_tac2; [easy|] ; simpl ; clear_complex ; eauto with mulauto ; fail ) ; try ( generalize Hmdn ; unfold le_lower, le_upper ; simpl ; xreal_tac2 ; simpl; xreal_tac2 ; intro H; apply Ropp_le_cancel in H; revert H ; try ( revert Hxu; rewrite Hrxu ) ; try ( revert Hxl; rewrite Hrxu ) ; clear_complex ; eauto with mulauto ; fail ). simpl. destruct (F.abs_correct xl) as [Haxl Vaxl]. destruct (F'.max_valid_ub _ _ Vaxl Vxu) as [Vmax Hmax]. elim (F'.mul_UP_correct prec (F.max (F.abs xl) xu) (F.max (F.abs xl) xu)). 2:{ unfold F.is_non_neg, F.is_non_pos, F.is_non_neg_real, F.is_non_pos_real. rewrite Vmax, Hmax, Haxl. left. split; (split; [exact eq_refl|]); revert Hx0'; (xreal_tac xu; case (Xabs (F.toX xl)); [now simpl..|]); intros r' Hr; apply (Rle_trans _ _ _ Hr), Rmax_r. } intros Vu Hu. rewrite Vu. split; [apply Rle_0_sqr|]. revert Hu. unfold le_upper. xreal_tac2; [easy|]. rewrite Hmax, Haxl. do 2 ( xreal_tac2; [easy|] ) ; simpl. apply Rle_trans. rewrite (Rabs_left1 _ Hx0). case (Rle_lt_dec 0 x); intro Hx. { now apply (Rmult_le_compat _ _ _ _ Hx Hx); rewrite Rmax_Rle; right. } rewrite <-(Ropp_involutive (x * x)). rewrite Ropp_mult_distr_l, Ropp_mult_distr_r. now apply Rmult_le_compat; try (now rewrite <-Ropp_0; apply Ropp_le_contravar, Rlt_le); rewrite Rmax_Rle; left; apply Ropp_le_contravar. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval