proposition: Lemma tan_correct : forall prec, extension Xtan (tan 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]. unfold tan, c2. case_eq (F'.le' xu xl). intros Hl. apply F'.le'_correct in Hl. assert (Htxl := T.tan_fast_correct prec xl). unfold convert in Hx; rewrite Vxl, Vxu in Hx; simpl in Hx. destruct (F.toX xu) as [|xur] ; try easy. destruct (F.toX xl) as [|xlr] ; try easy. replace x with xlr. exact Htxl. apply Rle_antisym with (1 := proj1 Hx). apply Rle_trans with (2 := Hl). apply Hx. intros _. case_eq (F'.lt' (F.neg (F.mul_DN prec (lower (T.pi4 prec)) (F.fromZ 2))) xl) ; try easy. intros Hlt1. apply F'.lt'_correct in Hlt1. case_eq (F'.lt' xu (F.mul_DN prec (lower (T.pi4 prec)) (F.fromZ 2))) ; try easy. intros Hlt2. apply F'.lt'_correct in Hlt2. generalize (T.tan_correct prec xl) (T.tan_correct prec xu). unfold convert in Hx; rewrite Vxl, Vxu in Hx; simpl in Hx. destruct (F.toX xl) as [|rl]. { now destruct (F.toX (F.neg (F.mul_DN prec (lower (T.pi4 prec)) (F.fromZ 2)))). } destruct (F.toX xu) as [|ru] ; try easy. intros Hl Hu. rewrite bnd_correct. 2: { generalize (T.tan_fast_correct prec xl). unfold T.I.convert. case T.tan_fast; [now simpl; unfold valid_lb; rewrite F'.valid_lb_nan|]. intros l u; simpl; unfold valid_lb; case F.valid_lb; [easy|]. now case Xtan; [|intros r [H0 H1]; lra]. } 2: { generalize (T.tan_fast_correct prec xu). unfold T.I.convert. case T.tan_fast; [now simpl; unfold valid_ub; rewrite F'.valid_ub_nan|]. intros l u; rewrite Bool.andb_comm. simpl; unfold valid_ub; case F.valid_ub; [easy|]. now case Xtan; [|intros r [H0 H1]; lra]. } rewrite F'.neg_correct in Hlt1. elim (F.mul_DN_correct prec (lower (T.pi4 prec)) (F.fromZ 2)). 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. { intros _; do 3 right; simpl. rewrite F'.valid_lb_nan, F'.nan_correct; repeat split; lra. } intros pl pu; simpl. case (F.valid_lb pl); [|intros [H0 H1]; lra]; intros _. case F.toX; [do 3 right; repeat split; lra|]. intro r'. case (Rle_or_lt 0 r'); intro Hr'; [left; split; lra|]. do 3 right; repeat split; lra. } intro Vmpi2. unfold le_lower, le_upper. rewrite F.fromZ_correct by easy. revert Hlt1 Hlt2. case F.toX; [easy|]; intro rpi2. simpl. intros Hlt1 Hlt2. generalize (T.pi4_correct prec). destruct (T.pi4 prec) as [|pi4l pi4u]. { now simpl; rewrite F'.nan_correct. } unfold T.I.convert. case (_ && _)%bool; [|intros [H0 H1]; lra]. intros [Hpil _]. simpl. destruct (F.toX pi4l) as [|pi4r] ; [easy|]. simpl. intro Hmpi2. apply (Rmult_le_compat_r 2) in Hpil; [|now apply IZR_le]. unfold Rdiv in Hpil. replace (PI * /4 * 2)%R with (PI / 2)%R in Hpil by field. assert (H1: (- PI / 2 < rl)%R) by lra. assert (H2: (ru < PI / 2)%R) by lra. unfold Xtan'. simpl. case is_zero_spec. simpl in Hx. apply Rgt_not_eq, cos_gt_0. apply Rlt_le_trans with (2 := proj1 Hx). unfold Rdiv. now rewrite <- Ropp_mult_distr_l_reverse. now apply Rle_lt_trans with ru. unfold Xtan' in Hl, Hu. intros _. split. - destruct (T.tan_fast prec xl) as [|tl tu]. simpl. now rewrite F'.nan_correct. revert Hl. simpl. case (_ && _)%bool; [|now case is_zero; [|intros [H0' H1']; lra]]. simpl. case is_zero_spec ; try easy. intros _ [H _]. destruct (F.toX tl) as [|rtl] ; try easy. apply Rle_trans with (1 := H). destruct (proj1 Hx) as [Hx'|Hx']. apply Rlt_le. apply tan_increasing ; try easy. now apply Rle_lt_trans with ru. rewrite Hx'. apply Rle_refl. - destruct (T.tan_fast prec xu) as [|tl tu]. simpl. now rewrite F'.nan_correct. revert Hu. simpl. case (_ && _)%bool; [|now case is_zero; [|intros [H0' H1']; lra]]. simpl. case is_zero_spec ; [easy|]. intros _ [_ H]. destruct (F.toX tu) as [|rtu] ; try easy. apply Rle_trans with (2 := H). destruct (proj2 Hx) as [Hx'|Hx']. apply Rlt_le. apply tan_increasing ; try easy. now apply Rlt_le_trans with rl. rewrite Hx'. apply Rle_refl. Qed.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend