proposition: Lemma atan_correct : forall prec, extension Xatan (atan prec).
proof: Proof. intros prec [|xl xu]; [easy|]. intros [|x]. { now simpl; case (_ && _)%bool. } intro Hx; generalize Hx. 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]. assert (Hpi := T.pi4_correct prec). simpl. unfold c2. unfold convert in Hx; rewrite Vxl, Vxu in Hx; simpl in Hx. destruct (pi4_mul2 prec) as [Vmpi2 Hmpi2]. set (l := if F.real xl then _ else _). set (u := if F.real xu then _ else _). assert (Vl : F.valid_lb l = true). { unfold l; rewrite F.real_correct. generalize (T.atan_fast_correct prec xl). case F.toX. { now intros _; rewrite F'.valid_lb_neg. } intro r. unfold T.I.convert. case T.atan_fast; [now simpl; rewrite F'.valid_lb_nan|]. intros l' u'. simpl. now case F.valid_lb; [|intros [H0 H1]; lra]. } assert (Vu : F.valid_ub u = true). { unfold u; rewrite F.real_correct. generalize (T.atan_fast_correct prec xu). case F.toX; [easy|]. intro r. unfold T.I.convert. case T.atan_fast; [now simpl; rewrite F'.valid_ub_nan|]. intros l' u'. simpl. now rewrite Bool.andb_comm; case F.valid_ub; [|intros [H0 H1]; lra]. } rewrite Vl, Vu; simpl. unfold l, u. rewrite 2!F.real_correct. split. - generalize (proj1 Hx). clear Hx. case_eq (F.toX xl). intros _ _. rewrite F'.neg_correct. revert Hmpi2; unfold le_upper. case F.toX; [easy|]; intro rmpi2. intro H. apply (Rle_trans _ _ _ (Ropp_le_contravar _ _ H)). apply Rlt_le. apply Rle_lt_trans with (2 := proj1 (atan_bound x)). lra. intros rl Hl Hx. generalize (T.atan_correct prec xl). destruct (T.atan_fast prec xl) as [|al au]. intros _. simpl. now rewrite F'.nan_correct. simpl. rewrite Hl. case (_ && _)%bool; [|intros [H0 H1]; lra]. destruct (F.toX al) as [|ral] ; try easy. intros [H _]. apply Rle_trans with (1 := H). destruct Hx as [Hx|Hx]. now apply Rlt_le, atan_increasing. rewrite Hx. apply Rle_refl. - generalize (proj2 Hx). clear Hx. case_eq (F.toX xu). intros _ _. revert Hmpi2. unfold le_upper. case F.toX; [easy|]; intro rmpi2. apply Rle_trans. apply Rlt_le, atan_bound. intros rl Hl Hx. generalize (T.atan_correct prec xu). destruct (T.atan_fast prec xu) as [|al au]. intros _. simpl. now rewrite F'.nan_correct. simpl. rewrite Hl. case (_ && _)%bool; [|intros [H0 H1]; lra]. destruct (F.toX au) as [|rau] ; try easy. intros [_ H]. apply Rle_trans with (2 := H). destruct Hx as [Hx|Hx]. now apply Rlt_le, atan_increasing. rewrite Hx. apply Rle_refl. Qed.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend