Sine

Sine is defined in terms of its alternating Taylor's series.
Section SinSeries.
Variable a:Q.

Definition sinSequence := (mult_Streams (everyOther (tl recip_factorials)) (powers_help (a^2) a)).

Lemma Str_nth_sinSequence : forall n, (Str_nth n sinSequence == (1#P_of_succ_nat (pred (fac (1+2*n))))*a^(1+2*n)%nat)%Q.

Sine is first defined on [0,1].
Hypothesis Ha: 0 <= a <= 1.

Lemma square_zero_one : 0 <= a^2 <= 1.

Lemma sinSequence_dnn : DecreasingNonNegative sinSequence.

Lemma sinSequence_zl : Limit sinSequence 0.

End SinSeries.

Definition rational_sin_small_pos (a:Q) (p: 0 <= a <= 1) : CR :=
 InfiniteAlternatingSum (sinSequence_dnn p) (sinSequence_zl p).

Lemma rational_sin_small_pos_correct : forall (a:Q) Ha,
 (@rational_sin_small_pos a Ha == IRasCR (Sin (inj_Q IR a)))%CR.

Sine's range can then be extended to [0,3^n] by n applications of the identity sin(x) = 3*sin(x/3) - 4*(sin(x/3))^3.
Section Sin_Poly.

Definition sin_poly_fun (x:Q) :Q := x*(3 - 4*x*x).

Lemma sin_poly_fun_correct : forall (q:Q),
 inj_Q IR (sin_poly_fun q)[=]3[*]inj_Q IR q[-]4[*](inj_Q IR q[^]3).

Definition sin_poly_modulus (e:Qpos) := Qpos2QposInf ((1#9)*e).

Let X:((-(1))<1)%Q.
Qed.

Let D : Derivative ([⋅,⋅] (inj_Q IR (-(1))) (inj_Q IR (1:Q))) (inj_Q_less _ _ _ X) ((3:IR){**}FId{-}(Four:IR){**}FId{^}3)
 ((3:IR){**}[-C-](1:IR){-}(Four:IR){**}((nring 3){**}([-C-]1{*}FId{^}2))).
Qed.

Lemma sin_poly_prf : is_UniformlyContinuousFunction (fun x => sin_poly_fun (QboundAbs (1#1) x)) sin_poly_modulus.

Definition sin_poly_uc : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction sin_poly_prf.

Definition sin_poly : CR --> CR := uc_compose compress (Cmap QPrelengthSpace sin_poly_uc).

Lemma sin_poly_correct : forall x, AbsSmall (inj_Q IR (1)) x -> (IRasCR (3[*]x[-]4[*]x[^]3)==sin_poly (IRasCR x))%CR.

Lemma Sin_triple_angle : forall x, (Sin(3[*]x)[=]3[*]Sin x[-]4[*]Sin x[^]3).

Lemma shrink_by_three : forall n a, 0 <= a <= (3^(S n))%Z -> 0 <= a/3 <= (3^n)%Z.

Fixpoint rational_sin_pos_bounded (n:nat) (a:Q) : 0 <= a <= (3^n)%Z -> CR :=
match n return 0 <= a <= (3^n)%Z -> CR with
| O => @rational_sin_small_pos a
| S n' =>
  match (Qlt_le_dec_fast 1 a) with
  | left _ => fun H => sin_poly (rational_sin_pos_bounded n' (shrink_by_three n' H))
  | right H' => fun H => rational_sin_small_pos (conj (proj1 H) H')
  end
end.

Lemma rational_sin_pos_bounded_correct : forall n (a:Q) Ha,
 (@rational_sin_pos_bounded n a Ha == IRasCR (Sin (inj_Q IR a)))%CR.

End Sin_Poly.

Therefore sin works on all nonnegative numbers.
Definition rational_sin_pos (a:Q) (Ha:0 <= a) : CR :=
 @rational_sin_pos_bounded _ a (conj Ha (power3bound a)).

Lemma rational_sin_pos_correct : forall (a:Q) Ha,
 (@rational_sin_pos a Ha == IRasCR (Sin (inj_Q IR a)))%CR.

By symmetry sin is extented to its entire range.
Definition rational_sin (a:Q) : CR :=
match (Qle_total 0 a) with
| left H => rational_sin_pos H
| right H => (-rational_sin_pos (Qopp_le_compat _ _ H))%CR
end.

Lemma rational_sin_correct : forall (a:Q),
 (@rational_sin a == IRasCR (Sin (inj_Q IR a)))%CR.

Sine is uniformly continuous everywhere.
Definition sin_uc_prf : is_UniformlyContinuousFunction rational_sin Qpos2QposInf.

Definition sin_uc : Q_as_MetricSpace --> CR :=
Build_UniformlyContinuousFunction sin_uc_prf.

Definition sin_slow : CR --> CR := Cbind QPrelengthSpace sin_uc.

Lemma sin_slow_correct : forall x,
 (IRasCR (Sin x) == sin_slow (IRasCR x))%CR.

Definition sin (x:CR) := sin_slow (x - (compress (scale (2*Qceiling (approximate (x*(CRinv_pos (6#1) (scale 2 CRpi))) (1#2)%Qpos -(1#2))) CRpi)))%CR.

Lemma sin_correct : forall x,
  (IRasCR (Sin x) == sin (IRasCR x))%CR.