proposition: Theorem sin_correct : forall prec, extension Xsin (sin 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 sin, c2. case_eq (F'.le' xu xl). intros Hl. apply F'.le'_correct in Hl. assert (Hsxl := T.sin_fast_correct prec xl). destruct (F.toX xu) as [|xur] ; try easy. destruct (F.toX xl) as [|xlr] ; try easy. replace x with xlr. exact Hsxl. apply Rle_antisym with (1 := Hxl). now apply Rle_trans with (2 := Hl). intros _. set (pi2 := F.mul_DN prec (lower (T.pi4 prec)) (F.fromZ 2)). case_eq (F'.le' (F.neg pi2) xl). intros Hpl. generalize (F'.le'_correct _ _ Hpl). xreal_tac xl. now case (F.toX (F.neg pi2)). clear Hpl. intros Hpl. case_eq (F'.le' xu pi2). intros Hpu. generalize (F'.le'_correct _ _ Hpu). xreal_tac xu. easy. xreal_tac pi2. easy. clear Hpu. intros Hpu. revert Hpl. rewrite F'.neg_correct, X1. simpl. intros Hpl. 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. } fold pi2. intros Vpi2. unfold le_lower, le_upper. rewrite X1, F.fromZ_correct by easy. simpl. generalize (T.pi4_correct prec). unfold T.I.convert. case T.pi4; [now simpl; rewrite F'.nan_correct|]. intros pl pu. case (_ && _)%bool; [|intros [H0 H1]; lra]. simpl. case F.toX; [easy|]. intros rpl [Hrpl _]. simpl. intro Hrpl'. assert (Hpl' : (-(PI/2) <= r)%R) by lra. assert (Hpu' : (r0 <= PI/2)%R) by lra. cut (match F.toX (upper (T.sin_fast prec xu)) with | Xnan => True | Xreal r3 => (Rtrigo_def.sin x <= r3)%R end). { cut (match F.toX (lower (T.sin_fast prec xl)) with | Xnan => True | Xreal r3 => (r3 <= Rtrigo_def.sin x)%R end). { generalize (T.sin_fast_correct prec xu). generalize (T.sin_fast_correct prec xl). destruct (T.sin_fast prec xl) as [|yl yu]; simpl; [rewrite F'.valid_lb_nan|]; (destruct (T.sin_fast prec xu) as [|zl zu]; simpl; [rewrite F'.valid_ub_nan|]); rewrite ?F'.nan_correct; [easy|..]; try (case (F.valid_lb yl); [|now simpl; case Xsin; [|intros rs [H0 H1]; lra]]); try (case (F.valid_ub zu); [|now intros _; rewrite Bool.andb_comm; case Xsin; [|intros rs [H0 H1]; lra]]); try (case (F.valid_ub yu); [|now simpl; case Xsin; [|intros rs [H0 H1]; lra]]); try (case (F.valid_lb zl); [|now intros _; rewrite Bool.andb_comm; case Xsin; [|intros rs [H0 H1]; lra]]); now case Xsin. } generalize (T.sin_fast_correct prec xl). destruct (T.sin_fast prec xl) as [|yl yu]. simpl. now rewrite F'.nan_correct. rewrite X. simpl. xreal_tac yl. easy. case (_ && _)%bool; [|intros [H0 H1]; lra]. intros [Hy _]. apply Rle_trans with (1 := Hy). assert (H' := Rle_trans _ _ _ Hxu Hpu'). apply sin_incr_1; try easy. now apply Rle_trans with x. now apply Rle_trans with r. } generalize (T.sin_fast_correct prec xu). destruct (T.sin_fast prec xu) as [|yl yu]. simpl. now rewrite F'.nan_correct. rewrite X0. simpl. xreal_tac yu. easy. case (_ && _)%bool; [|intros [H0 H1]; lra]. intros [_ Hy]. apply Rle_trans with (2 := Hy). assert (H' := Rle_trans _ _ _ Hpl' Hxl). apply sin_incr_1 ; try easy. now apply Rle_trans with r0. now apply Rle_trans with x. intros _. unfold Xsin. rewrite <- cos_shift. change (Xreal (Rtrigo_def.cos (PI / 2 - x))) with (Xcos (Xsub (Xreal (PI / 2)) (Xreal x))). apply cos_correct. apply sub_correct with (2 := Hx). replace (PI / 2)%R with (PI / 4 * 2)%R by field. change (Xreal (PI / 4 * 2)) with (Xreal (PI / 4) * Xreal 2)%XR. apply mul2_correct. apply T.pi4_correct. intros _. rewrite <- (Ropp_involutive x). unfold Xsin. rewrite sin_neg. apply (neg_correct _ (Xreal _)). rewrite <- cos_shift. replace (PI / 2 - - x)%R with (x + PI / 2)%R by ring. change (Xreal (Rtrigo_def.cos (x + PI / 2))) with (Xcos (Xadd (Xreal x) (Xreal (PI / 2)))). apply cos_correct. apply (add_correct _ _ _ _ _ Hx). replace (PI / 2)%R with (PI / 4 * 2)%R by field. change (Xreal (PI / 4 * 2)) with (Xreal (PI / 4) * Xreal 2)%XR. apply mul2_correct. apply T.pi4_correct. Qed.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend