proposition: Lemma sin_fastP_correct : forall prec x, F.toX x = Xreal (toR x) -> (0 <= toR x)%R -> contains (I.convert (sin_fastP prec x)) (Xreal (sin (toR x))).
proof: Proof. intros prec x Hxr Hx0. unfold sin_fastP, cm1, c1. case_eq (F'.le' x c1_2) ; intros Hx. { apply sin_fast0_correct. { easy. } rewrite Rabs_pos_eq with (1 := Hx0). apply F'.le'_correct in Hx. revert Hx. unfold toR, c1. now rewrite Hxr, c1_2_correct. } generalize (S (Z2nat (F.StoZ (F.mag x)))) (F.incr_prec prec (Z2P (F.StoZ (F.mag x) + 6))). intros nb prec'. generalize (sin_cos_reduce_correct prec' nb x Hxr Hx0). destruct sin_cos_reduce as [ss ci]. intros [Hc Hs]. destruct ss. { simpl. 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. apply SIN_bound. } { rewrite <- (Ropp_involutive (sin (toR x))). change (Xreal (- - sin (toR x))) with (Xneg (Xreal (- sin (toR x)))). apply I.neg_correct. rewrite <- Rabs_left1 with (1 := Hs). rewrite <- sqrt_Rsqr_abs. replace (Xreal (sqrt (sin (toR x))²)) with (Xsqrt (Xreal (sin (toR x))²)). { apply I.sqrt_correct. rewrite sin2. change (Xreal (1 - (cos (toR x))²)) with (Xsub (Xreal 1) (Xsqr (Xreal (cos (toR x))))). apply I.sub_correct. now apply I.fromZ_small_correct. now apply I.sqr_correct. } unfold Xsqrt'. simpl. destruct (is_negative_spec (sin (toR x))²). { elim (Rlt_not_le _ _ H). apply Rle_0_sqr. } apply refl_equal. } rewrite <- (Rabs_pos_eq (sin (toR x))) with (1 := Hs). rewrite <- sqrt_Rsqr_abs. replace (Xreal (sqrt (sin (toR x))²)) with (Xsqrt (Xreal (sin (toR x))²)). { apply I.sqrt_correct. rewrite sin2. change (Xreal (1 - (cos (toR x))²)) with (Xsub (Xreal 1) (Xsqr (Xreal (cos (toR x))))). apply I.sub_correct. now apply I.fromZ_small_correct. now apply I.sqr_correct. } unfold Xsqrt'. simpl. destruct (is_negative_spec (sin (toR x))²). { elim (Rlt_not_le _ _ H). apply Rle_0_sqr. } apply refl_equal. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float