proposition: Lemma sin_cos_reduce_correct : forall prec nb x, F.toX x = Xreal (toR x) -> (0 <= toR x)%R -> match sin_cos_reduce prec x nb with | (ss, ci) => contains (I.convert ci) (Xreal (cos (toR x))) /\ match ss with | Lt => (sin (toR x) <= 0)%R | Gt => (0 <= sin (toR x))%R | _ => True end end.
proof: Proof. intros prec. assert (forall x, F.toX x = Xreal (toR x) -> (0 <= toR x)%R -> F'.le x c1_2 = true -> contains (I.convert (cos_fast0 prec x)) (Xreal (cos (toR x))) /\ (0 <= sin (toR x))%R). { intros x Hxr Hx0 H. unfold c1_2, c1 in H. assert (toR x <= /2)%R. { rewrite F'.le_correct with (1 := Hxr) in H. 2: { unfold F.toR. now fold c1; fold c1_2; rewrite c1_2_correct. } revert H. case Rle_bool_spec ; try easy. unfold F.toR. now fold c1; fold c1_2; rewrite c1_2_correct. } split. { apply cos_fast0_correct with (1 := Hxr). now rewrite Rabs_right; [|apply Rle_ge]. } apply sin_ge_0 with (1 := Hx0). apply Rle_trans with (1 := H0). apply Rlt_le. apply Rmult_lt_reg_l with (/4)%R. { apply Rinv_0_lt_compat. now apply IZR_lt. } rewrite <- (Rmult_comm PI). apply Rlt_le_trans with (2 := proj1 (PI_ineq 0)). unfold tg_alt, PI_tg. simpl. lra. } induction nb ; intros x Hxr Hx. { simpl. case_eq (F'.le x c1_2). { intros. exact (H x Hxr Hx H0). } intros _. simpl. unfold cm1, c1. rewrite F'.valid_lb_real, F'.valid_ub_real by now rewrite F.real_correct, F.fromZ_correct. rewrite 2!F.fromZ_correct by easy. refine (conj _ I). apply COS_bound. } simpl. case_eq (F'.le x c1_2). { intros. exact (H x Hxr Hx H0). } rewrite F'.le_correct; try (unfold F.toR; rewrite c1_2_correct); [simpl|easy..]. intros Hxhalf. refine (_ (IHnb (F.div2 x) _ _)). { destruct (sin_cos_reduce prec (F.div2 x) nb) as (ss, ci). fold (F.toR x). replace (F.toR x) with (2 * (toR (F.div2 x)))%R. { generalize (toR (F.div2 x)). revert Hxr Hxhalf; clear; intros Hxr Hxhalf. intros hx (Hc, Hs). split. { replace (Xreal (cos (2 * hx))) with (Xsub (Xmul (Xsqr (Xreal (cos hx))) (Xreal 2)) (Xreal 1)). { apply I.sub_correct. { apply I.mul2_correct. apply I.sqr_correct. exact Hc. } now apply I.fromZ_small_correct. } simpl. apply f_equal. rewrite cos_2a_cos. unfold Rsqr. ring. } rewrite sin_2a. destruct ss. { exact I. } { change (cos hx) with (proj_val (Xreal (cos hx))). generalize (I.sign_large_correct ci). case (I.sign_large ci) ; intros ; try exact I. { apply Rmult_le_neg_neg. { apply Rmult_le_pos_neg. { now apply IZR_le. } exact Hs. } exact (proj2 (H _ Hc)). } apply Rmult_le_neg_pos. { apply Rmult_le_pos_neg. { now apply IZR_le. } exact Hs. } exact (proj2 (H _ Hc)). } change (cos hx) with (proj_val (Xreal (cos hx))). generalize (I.sign_large_correct ci). case (I.sign_large ci) ; intros ; try exact I. { apply Rmult_le_pos_neg. { apply Rmult_le_pos_pos. { now apply IZR_le. } exact Hs. } exact (proj2 (H _ Hc)). } apply Rmult_le_pos_pos. { apply Rmult_le_pos_pos. { now apply IZR_le. } exact Hs. } exact (proj2 (H _ Hc)). } unfold toR; rewrite F.div2_correct; [|easy|]. { rewrite Xdiv_split; simpl; unfold Xinv'; rewrite is_zero_false; [|easy]. rewrite Hxr; simpl; lra. } rewrite (Rabs_pos_eq _ Hx). revert Hxhalf; case Rle_bool_spec; [easy|]; fold (F.toR x); lra. } { unfold toR; rewrite F.div2_correct; [|easy|]. { rewrite Xdiv_split; simpl; unfold Xinv'; rewrite is_zero_false; [|easy]. now rewrite Hxr. } rewrite (Rabs_pos_eq _ Hx). revert Hxhalf; case Rle_bool_spec; [easy|]; fold (F.toR x); lra. } unfold toR; rewrite F.div2_correct; [|easy|]. { rewrite Xdiv_split; simpl; unfold Xinv'; rewrite is_zero_false; [|easy]. rewrite Hxr; simpl; lra. } rewrite (Rabs_pos_eq _ Hx). revert Hxhalf; case Rle_bool_spec; [easy|]; fold (F.toR x); lra. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float