proposition: Lemma tan_fastP_correct : forall prec x, F.toX x = Xreal (toR x) -> (0 <= toR x)%R -> contains (I.convert (tan_fastP prec x)) (Xtan (Xreal (toR x))).
proof: Proof. intros prec x Rx Bx. unfold tan_fastP. case_eq (F'.le' x c1_2) ; intros Hx. - apply F'.le'_correct in Hx. revert Hx. rewrite c1_2_correct, Rx. intros Bx'. replace (Xtan (Xreal (toR x))) with (Xdiv (Xreal (sin (toR x))) (Xsqrt (Xsub (Xreal 1) (Xsqr (Xreal (sin (toR x))))))). apply I.div_correct. apply sin_fast0_correct with (1 := Rx). now rewrite Rabs_pos_eq. apply I.sqrt_correct. apply I.sub_correct. now apply I.fromZ_small_correct. apply I.sqr_correct. apply sin_fast0_correct with (1 := Rx). now rewrite Rabs_pos_eq. unfold Xsqrt'. simpl. set (e := (1 - _)%R). case (Rlt_or_le e 0); unfold e. { intro H. elim Rlt_not_le with (1 := H). apply Rle_0_minus. rewrite <- (Rmult_1_r 1). apply neg_pos_Rsqr_le ; apply SIN_bound. } change (sin (toR x) * sin (toR x))%R with (Rsqr (sin (toR x))). rewrite <- cos2. intros H'. assert (Hc: (0 < cos (toR x))%R). apply cos_gt_0. apply Rlt_le_trans with (2 := Bx). apply Ropp_lt_gt_0_contravar. apply PI2_RGT_0. apply Rle_lt_trans with (1 := Bx'). apply Rlt_trans with (2 := PI2_1). lra. unfold Xdiv'. case is_zero_spec. intros H. elim Rgt_not_eq with (1 := Hc). apply Rsqr_0_uniq. now apply sqrt_eq_0. intros H''. unfold Xtan'. simpl. case is_zero_spec. intros H. rewrite H in Hc. elim Rlt_irrefl with (1 := Hc). intros _. apply (f_equal (fun v => Xreal (_ / v))). apply sqrt_Rsqr. now apply Rlt_le. - generalize (F.incr_prec prec (Z2P (F.StoZ (F.mag x) + 7))). clear prec. intros prec. generalize (sin_cos_reduce_correct prec (S (Z2nat (F.StoZ (F.mag x)))) x Rx Bx). case sin_cos_reduce. intros s c [Hc Hs]. assert (H: contains (I.convert (I.sqrt prec (I.sub prec (I.inv prec (I.sqr prec c)) i1))) (Xabs (Xdiv (Xreal (sin (toR x))) (Xreal (cos (toR x)))))). replace (Xabs (Xdiv (Xreal (sin (toR x))) (Xreal (cos (toR x))))) with (Xsqrt (Xsub (Xinv (Xsqr (Xreal (cos (toR x))))) (Xreal 1))). apply I.sqrt_correct. apply I.sub_correct. apply I.inv_correct. now apply I.sqr_correct. now apply I.fromZ_small_correct. unfold Xdiv', Xinv'. simpl. case is_zero_spec ; intros Zc. rewrite Rsqr_0_uniq with (1 := Zc). now rewrite is_zero_0. case is_zero_spec ; intros Zc'. rewrite Zc' in Zc. elim Zc. apply Rmult_0_l. unfold Xsqrt'. simpl. replace (/ (Rsqr (cos (toR x))) - 1)%R with (Rsqr (sin (toR x) / cos (toR x))). { set (e := (_²)%R). case (Rlt_or_le e 0); unfold e; intro H. { elim Rlt_not_le with (1 := H). apply Rle_0_sqr. } apply f_equal, sqrt_Rsqr_abs. } rewrite Rsqr_div with (1 := Zc'). rewrite sin2. unfold Rsqr. now field. unfold Xdiv', Xbind2 in H. generalize (I.sign_large_correct c). unfold Xtan', Xbind. destruct s ; try easy ; case I.sign_large ; try easy ; intros Hc'. destruct (is_zero_spec (cos (toR x))) as [H0|H0]. easy. evar_last. apply H. apply (f_equal Xreal). apply Rabs_pos_eq. apply Rmult_le_neg_neg with (1 := Hs). apply Rlt_le, Rinv_lt_0_compat. apply Rnot_le_lt. contradict H0. apply Rle_antisym with (2 := H0). now specialize (Hc' _ Hc). rewrite <- (Xneg_involutive (if is_zero _ then _ else _)). apply I.neg_correct. destruct (is_zero_spec (cos (toR x))) as [H0|H0]. easy. evar_last. apply H. apply (f_equal Xreal). apply Rabs_left1. apply Rmult_le_neg_pos with (1 := Hs). apply Rlt_le, Rinv_0_lt_compat. apply Rnot_le_lt. contradict H0. apply Rle_antisym with (1 := H0). now specialize (Hc' _ Hc). rewrite <- (Xneg_involutive (if is_zero _ then _ else _)). apply I.neg_correct. destruct (is_zero_spec (cos (toR x))) as [H0|H0]. easy. evar_last. apply H. apply (f_equal Xreal). apply Rabs_left1. apply Rmult_le_pos_neg with (1 := Hs). apply Rlt_le, Rinv_lt_0_compat. apply Rnot_le_lt. contradict H0. apply Rle_antisym with (2 := H0). now specialize (Hc' _ Hc). destruct (is_zero_spec (cos (toR x))) as [H0|H0]. easy. evar_last. apply H. apply (f_equal Xreal). apply Rabs_pos_eq. apply Rmult_le_pos_pos with (1 := Hs). apply Rlt_le, Rinv_0_lt_compat. apply Rnot_le_lt. contradict H0. apply Rle_antisym with (1 := H0). now specialize (Hc' _ Hc). Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float