proposition: Lemma cos_correct : forall prec, extension Xcos (cos prec).
proof: Proof. intros prec xi x Hx. unfold cos. generalize (abs_correct xi x Hx) (abs_ge_0' xi). destruct (abs xi) as [|xl xu]; [easy|]. destruct x as [|x]. { now simpl; case (_ && _)%bool. } unfold convert at 1. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; lra]. intros Vxu Vxl [Hxl Hxu]. intros Hal. simpl in Hal. assert (H : not_empty (convert xi)). { now exists x. } specialize (Hal H); clear H. unfold Xbind. replace (Rtrigo_def.cos x) with (Rtrigo_def.cos (Rabs x)). 2: now unfold Rabs ; case Rcase_abs ; intros _ ; try easy ; apply cos_neg. clear Hx. assert (Hcxl := T.cos_fast_correct prec xl). assert (Hcxu := T.cos_fast_correct prec xu). case_eq (F'.le' xu xl). { intros Hl. apply F'.le'_correct in Hl. destruct (F.toX xu) as [|xur] ; [easy|]. destruct (F.toX xl) as [|xlr] ; [easy|]. replace (Rabs x) with xlr. { exact Hcxl. } apply Rle_antisym. { easy. } now apply Rle_trans with (2 := Hl). } intros _. unfold cm1, c1, c3, c4, c8. assert (Hlb'_cos : F.valid_lb (lower (T.cos_fast prec xl)) = true). { generalize Hcxl. unfold T.I.convert. case (T.cos_fast prec xl). { now simpl; rewrite F'.valid_lb_nan. } simpl. intros l u. case (F.valid_lb l); [easy|]. now simpl; case F.toX; [|intros r [H0 H1]; lra]. } assert (Hub'_cos : F.valid_ub (upper (T.cos_fast prec xu)) = true). { generalize Hcxu. unfold T.I.convert. case (T.cos_fast prec xu). { now simpl; rewrite F'.valid_ub_nan. } simpl. intros l u. rewrite Bool.andb_comm. case (F.valid_ub u); [easy|]. now simpl; case F.toX; [|intros r [H0 H1]; lra]. } assert (Hub_cos : F.valid_ub (upper (T.cos_fast prec xl)) = true). { generalize Hcxl. unfold T.I.convert. case (T.cos_fast prec xl). { now simpl; rewrite F'.valid_ub_nan. } simpl. intros l u; rewrite Bool.andb_comm. case (F.valid_ub u); [easy|]. now simpl; case F.toX; [|intros r [H0 H1]; lra]. } assert (Hlb_cos : F.valid_lb (lower (T.cos_fast prec xu)) = true). { generalize Hcxu. unfold T.I.convert. case (T.cos_fast prec xu). { now simpl; rewrite F'.valid_lb_nan. } simpl. intros l u. now case (F.valid_lb l); [|simpl; case Xcos; [|intros r [H0 H1]; lra]]. } case_eq (F'.le' xu (F.mul_DN prec (lower (T.pi4 prec)) (F.fromZ 4))). { intros Hu. apply F'.le'_correct in Hu. destruct (F.toX xu) as [|xur] ; try easy. assert (Hxur: (xur <= PI)%R). { revert Hu. elim (F.mul_DN_correct prec (lower (T.pi4 prec)) (F.fromZ 4)). 2:{ unfold F.is_non_neg_real, F.is_non_pos_real, F.is_non_neg', F.is_non_pos'. rewrite F.fromZ_correct by easy. generalize (T.pi4_correct prec). unfold T.I.convert. case T.pi4. { simpl; intros _; do 3 right; rewrite F'.valid_lb_nan, F'.nan_correct. repeat split; lra. } intros l u; simpl. rewrite F.valid_lb_correct. case F.classify; [..|intros [H0 H1]; lra]; intros _; (case F.toX; [now do 3 right; repeat split; lra|]; intro rl); (case (Rle_or_lt 0 rl); intro Hrl; [now left; repeat split; lra|do 3 right; repeat split; lra]). } intros Vmdn. unfold le_lower, le_upper. case F.toX; [easy|]; intro Rmdn; simpl. rewrite F.fromZ_correct by easy. generalize (T.pi4_correct prec). destruct (T.pi4 prec) as [|pi4l pi4u] ; simpl. { now rewrite F'.nan_correct. } case (_ && _)%bool; [|intros [H0 H1]; lra]. case F.toX; [easy|]; intro pi4r. simpl. intros [H _] Hu. apply Ropp_le_cancel in Hu. intro H'; apply (Rle_trans _ _ _ H'); clear H'. apply Rle_trans with (1 := Hu). lra. } clear Hu. unfold convert; simpl. rewrite Hlb_cos; simpl. rewrite Hub_cos; simpl. split. { destruct (T.cos_fast prec xu) as [|cu cu'] ; simpl. { now rewrite F'.nan_correct. } generalize Hcxu; unfold T.I.convert; case (_ && _)%bool; [|intros [H0 H1]; lra]. intros [Hcu _]. destruct (F.toX cu) as [|cur] ; [easy|]. apply Rle_trans with (1 := Hcu). apply cos_decr_1 with (4 := Hxur). { apply Rabs_pos. } { now apply Rle_trans with xur. } { revert Hxu; apply Rle_trans, Rabs_pos. } exact Hxu. } generalize (T.cos_fast_correct prec xl). unfold T.I.convert. case_eq (T.cos_fast prec xl); [now simpl; rewrite F'.nan_correct|]. intros cl' cl Hcl. generalize Hub_cos; rewrite Hcl; simpl=> ->. generalize Hlb'_cos; rewrite Hcl; simpl=> ->; simpl. destruct (F.toX xl) as [|xlr] ; [easy|]. intros [_ Hl]. destruct (F.toX cl) as [|clr] ; [easy|]. apply Rle_trans with (2 := Hl). apply cos_decr_1 with (1 := Hal). { apply Rle_trans with (2 := Hxur). now apply Rle_trans with (Rabs x). } { apply Rabs_pos. } { now apply Rle_trans with xur. } apply Hxl. } intros _. case_eq (F'.le' xu (F.mul_DN prec (lower (T.pi4 prec)) (F.fromZ 8))). { intros Hu. apply F'.le'_correct in Hu. destruct (F.toX xu) as [|xur] ; [easy|]. assert (Hxur: (xur <= 2 * PI)%R). { revert Hu. elim (F.mul_DN_correct prec (lower (T.pi4 prec)) (F.fromZ 8)). 2:{ unfold F.is_non_neg_real, F.is_non_pos_real, F.is_non_neg', F.is_non_pos'. rewrite F.fromZ_correct by easy. generalize (T.pi4_correct prec). unfold T.I.convert. case T.pi4. { simpl; intros _; do 3 right; rewrite F'.valid_lb_nan, F'.nan_correct. repeat split; lra. } intros l u; simpl. rewrite F.valid_lb_correct. case F.classify; [..|intros [H0 H1]; lra]; intros _; (case F.toX; [now do 3 right; repeat split; lra|]; intro rl); (case (Rle_or_lt 0 rl); intro Hrl; [now left; repeat split; lra|do 3 right; repeat split; lra]). } intros Vmdn. unfold le_lower, le_upper. case F.toX; [easy|]; intro rmdn; simpl. rewrite F.fromZ_correct by easy. generalize (T.pi4_correct prec). unfold T.I.convert. case T.pi4; [now simpl; rewrite F'.nan_correct|]; intros l u. case (_ && _)%bool; [|intros [H0 H1]; lra]. simpl. case F.toX; simpl; [easy|]. intros rlpi4 [Hrlpi4 _]. lra. } clear Hu. case_eq (F'.le' (F.mul_UP prec (upper (T.pi4 prec)) (F.fromZ 4)) xl). { intros Hl. apply F'.le'_correct in Hl. destruct (F.toX xl) as [|xlr]. { now destruct (F.toX (F.mul_UP prec (upper (T.pi4 prec)) (F.fromZ 4))). } assert (Hxlr: (PI <= xlr)%R). { revert Hl. elim (F.mul_UP_correct prec (upper (T.pi4 prec)) (F.fromZ 4)). 2:{ left ; unfold F.is_non_neg' ; split. clear. assert (H := T.pi4_correct prec). rewrite T.I.valid_ub_upper, T.I.upper_correct by (eexists ; exact H). destruct T.I.convert as [|l [|u]] ; try easy. apply Rle_trans with (2 := proj2 H). apply Rlt_le, PI4_RGT_0. rewrite F.fromZ_correct by easy. now apply IZR_le. } intros Vmup. rewrite F.fromZ_correct by easy. unfold le_upper. case F.toX; [easy|]; intro rmup. generalize (T.pi4_correct prec). unfold T.I.convert. case T.pi4; [now simpl; rewrite F'.nan_correct|]; intros l u. case (_ && _)%bool; [|intros [H0 H1]; lra]. simpl. case (F.toX u); simpl; [easy|]. intros rupi4 [_ Hrupi4]. lra. } clear Hl. simpl. rewrite Hlb'_cos, Hub'_cos. split. { destruct (T.cos_fast prec xl) as [|cl cl'] ; simpl. { now rewrite F'.nan_correct. } revert Hcxl. unfold T.I.convert. case (_ && _)%bool; [|intros [H0 H1]; lra]. intros [Hcl _]. destruct (F.toX cl) as [|clr] ; [easy|]. apply Rle_trans with (1 := Hcl). apply cos_incr_1 with (1 := Hxlr) (5 := Hxl). { apply Rle_trans with (2 := Hxur). apply Rle_trans with (1 := Hxl) (2 := Hxu). } { apply Rle_trans with (1 := Hxlr) (2 := Hxl). } apply Rle_trans with (1 := Hxu) (2 := Hxur). } destruct (T.cos_fast prec xu) as [|cu' cu] ; simpl. { now rewrite F'.nan_correct. } revert Hcxu. unfold T.I.convert. case (_ && _)%bool; [|intros [H0 H1]; lra]. intros [_ Hcu]. destruct (F.toX cu) as [|cur] ; [easy|]. apply Rle_trans with (2 := Hcu). apply cos_incr_1 with (4 := Hxur) (5 := Hxu). { apply Rle_trans with (1 := Hxlr) (2 := Hxl). } { apply Rle_trans with (1 := Hxu) (2 := Hxur). } apply Rle_trans with (1 := Hxlr). apply Rle_trans with (1 := Hxl) (2 := Hxu). } intros _. unfold convert. simpl; rewrite F'.valid_lb_real. 2: now rewrite F.real_correct, F.fromZ_correct; [..|lia]. generalize (F'.max_valid_ub _ _ Hub_cos Hub'_cos). intros [Vmax Hmax]. rewrite Vmax, Hmax. split. { rewrite F.fromZ_correct by easy. apply COS_bound. } destruct (T.cos_fast prec xl) as [|cl' cl] ; simpl. { now rewrite F'.nan_correct. } revert Hcxl. unfold T.I.convert; simpl. simpl in Hlb'_cos. rewrite Hlb'_cos. simpl in Hub_cos. rewrite Hub_cos. simpl. destruct (F.toX xl) as [|xlr] ; [easy|]. intros [_ Hcl]. destruct (F.toX cl) as [|clr] ; [easy|]. destruct (T.cos_fast prec xu) as [|cu' cu] ; simpl. { now rewrite F'.nan_correct. } revert Hcxu. unfold T.I.convert. simpl in Hub'_cos. rewrite Hub'_cos. simpl in Hlb_cos. rewrite Hlb_cos. simpl. intros [_ Hcu]. destruct (F.toX cu) as [|cur] ; [easy|]. destruct (Rle_dec (Rabs x) PI) as [Hx|Hx]. { apply Rle_trans with (2 := Rmax_l _ _). apply Rle_trans with (2 := Hcl). apply cos_decr_1 with (1 := Hal) (3 := Rabs_pos _) (4 := Hx) (5 := Hxl). apply Rle_trans with (1 := Hxl) (2 := Hx). } apply Rle_trans with (2 := Rmax_r _ _). apply Rle_trans with (2 := Hcu). apply Rnot_le_lt, Rlt_le in Hx. apply cos_incr_1 with (1 := Hx) (4 := Hxur) (5 := Hxu). { apply Rle_trans with (1 := Hxu) (2 := Hxur). } apply Rle_trans with (1 := Hx) (2 := Hxu). } intros _. case_eq (F'.le' (F.sub_UP prec xu xl) (F.fromZ 3)). { intros Hd. apply F'.le'_correct in Hd. revert Hd. elim (F.sub_UP_correct prec xu xl); [|easy..]. intros Vsup. unfold le_upper. case F.toX; [easy|]; intro rsup. rewrite F.fromZ_correct by easy. case_eq (F.toX xu) ; [easy|] ; intros xur Hur. case_eq (F.toX xl) ; [easy|] ; intros xlr Hlr. rewrite Hur in Hxu. rewrite Hlr in Hxl. intros Hsup Hrsup3. simpl in Hsup. apply meet_correct. { unfold convert, bnd. rewrite F'.valid_ub_real, F'.valid_lb_real by now rewrite F.real_correct, F.fromZ_correct. rewrite 2!F.fromZ_correct by easy. apply COS_bound. } elim (F.midpoint_correct xl xu); [|easy|now rewrite F.real_correct, ?Hlr, ?Hur.. |now unfold F.toR; rewrite Hlr, Hur; apply (Rle_trans _ _ _ Hxl)]. set (m := F.midpoint xl xu). intros Rm [Hlm Hum]. replace (Xreal (Rtrigo_def.cos (Rabs x))) with (Xadd (Xcos (Xreal (F.toR m))) (Xreal (Rtrigo_def.cos (Rabs x) - Rtrigo_def.cos (F.toR m)))) by (apply (f_equal Xreal) ; ring). apply add_correct. { generalize (T.cos_fast_correct prec m). now rewrite (F'.real_correct _ Rm). } simpl. rewrite F'.valid_lb_neg. rewrite F'.neg_correct. elim (F.sub_UP_correct prec xu m); [|easy|now generalize (F.classify_correct m); rewrite Rm, F.valid_lb_correct; case F.classify]. intros Vsxum Hsxum. elim (F.sub_UP_correct prec m xl); [|now generalize (F.classify_correct m); rewrite Rm, F.valid_ub_correct; case F.classify|easy]. intros Vsmxl Hsmxl. elim (F'.max_valid_ub _ _ Vsxum Vsmxl). intros Vm Hm. rewrite Vm, Hm. revert Hsxum Hsmxl. rewrite Hlr, Hur, (F'.real_correct _ Rm). unfold le_upper. case F.toX; [easy|]; simpl. intros rsxum Hrsxum. case F.toX; [easy|]; simpl. intros rsmxl Hrsmxl. apply Raux.Rabs_le_inv. destruct (MVT_abs Rtrigo_def.cos (fun t => Ropp (sin t)) (F.toR m) (Rabs x)) as [v [-> _]]. { intros c _. apply derivable_pt_lim_cos. } apply Rle_trans with (1 * Rabs (Rabs x - (F.toR m)))%R. { apply Rmult_le_compat_r. apply Rabs_pos. rewrite Rabs_Ropp. apply Rabs_le, SIN_bound. } rewrite Rmult_1_l. case (Rle_lt_dec (Rabs x) (F.toR m)); intro Hxm. { refine (Rle_trans _ _ _ _ (Rmax_r _ _)). rewrite Rabs_minus_sym, Rabs_pos_eq; [|lra]. apply (Rle_trans _ ((F.toR m) - xlr)); lra. } refine (Rle_trans _ _ _ _ (Rmax_l _ _)). rewrite Rabs_pos_eq; [|lra]. apply (Rle_trans _ (xur - (F.toR m))); lra. } intros _. unfold convert, bnd. rewrite F'.valid_ub_real, F'.valid_lb_real by now rewrite F.real_correct, F.fromZ_correct. rewrite 2!F.fromZ_correct by easy. apply COS_bound. Qed.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend