proposition: Lemma atan_fastP_correct : forall prec x, F.toX x = Xreal (toR x) -> (0 <= toR x)%R -> contains (I.convert (atan_fastP prec x)) (Xreal (atan (toR x))).
proof: Proof. intros prec x Rx Bx. unfold atan_fastP, c1_2, c1, c2. rewrite F'.lt_correct with (2 := Rx). 2: { unfold F.toR. now fold c1; fold c1_2; rewrite c1_2_correct. } unfold F.toR at 1. fold c1; fold c1_2; rewrite c1_2_correct. simpl Rlt_bool. assert (Ix: contains (I.convert (I.bnd x x)) (Xreal (toR x))). { rewrite I.bnd_correct; [|apply I.valid_lb_real|apply I.valid_ub_real]; rewrite Rx; [|easy..]. split ; apply Rle_refl. } case Rlt_bool_spec ; intros Bx'. 2: { apply atan_fast0_correct with (2 := Ix). now rewrite Rabs_pos_eq. } rewrite F'.lt_correct with (2 := Rx); [|now unfold F.toR; rewrite F.fromZ_correct; [..|lia]]. unfold F.toR at 1. rewrite F.fromZ_correct by easy. simpl Rlt_bool. case Rlt_bool_spec ; intros Bx'' ; cycle 1. replace (Xreal (atan (toR x))) with (Xadd (Xreal (PI / 4)) (Xatan (Xreal ((toR x - 1) / (toR x + 1))))). apply I.add_correct. apply pi4_correct. apply atan_fast0_correct. apply Rabs_le. assert (Bx1: (0 < toR x + 1)%R) by (clear -Bx ; lra). split. apply Rmult_le_reg_r with (1 := Bx1). unfold Rdiv. rewrite Rmult_assoc, Rinv_l, Rmult_1_r. apply Rminus_le. replace (- / 2 * (toR x + 1) - (toR x - 1))%R with (-3/2 * toR x + /2)%R by field. clear -Bx' ; lra. now apply Rgt_not_eq. apply Rmult_le_reg_r with (1 := Bx1). unfold Rdiv. rewrite Rmult_assoc, Rinv_l, Rmult_1_r. apply Rminus_le. replace (toR x - 1 - / 2 * (toR x + 1))%R with (/2 * toR x - 3/2)%R by field. lra. now apply Rgt_not_eq. apply J.div_correct. apply J.sub_correct with (1 := Ix). now apply I.fromZ_small_correct. apply J.add_correct with (1 := Ix). now apply I.fromZ_small_correct. simpl. apply (f_equal Xreal). rewrite Rplus_comm. apply atan_plus_PI4. lra. replace (Xreal (atan (toR x))) with (Xsub (Xmul (Xreal (PI/4)) (Xreal 2)) (Xatan (Xreal (/ toR x)))). apply I.sub_correct. apply I.mul2_correct. apply pi4_correct. apply atan_fast0_correct. rewrite Rabs_pos_eq. apply Rle_Rinv_pos. apply Rlt_0_2. now apply Rlt_le. apply Rlt_le, Rinv_0_lt_compat. lra. now apply J.inv_correct. simpl. apply f_equal. rewrite atan_inv; lra. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float