Library Coq.Reals.Rtrigo_calc
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
SeqSeries
.
Require
Import
Rtrigo
.
Require
Import
R_sqrt
.
Open
Local
Scope
R_scope
.
Lemma
tan_PI
:
tan
PI
= 0.
Lemma
sin_3PI2
:
sin
(3 * (
PI
/ 2)) = -1.
Lemma
tan_2PI
:
tan
(2 *
PI
) = 0.
Lemma
sin_cos_PI4
:
sin
(
PI
/ 4) =
cos
(
PI
/ 4).
Lemma
sin_PI3_cos_PI6
:
sin
(
PI
/ 3) =
cos
(
PI
/ 6).
Lemma
sin_PI6_cos_PI3
:
cos
(
PI
/ 3) =
sin
(
PI
/ 6).
Lemma
PI6_RGT_0
: 0 <
PI
/ 6.
Lemma
PI6_RLT_PI2
:
PI
/ 6 <
PI
/ 2.
Lemma
sin_PI6
:
sin
(
PI
/ 6) = 1 / 2.
Lemma
sqrt2_neq_0
:
sqrt
2 <> 0.
Lemma
R1_sqrt2_neq_0
: 1 /
sqrt
2 <> 0.
Lemma
sqrt3_2_neq_0
: 2 *
sqrt
3 <> 0.
Lemma
Rlt_sqrt2_0
: 0 <
sqrt
2.
Lemma
Rlt_sqrt3_0
: 0 <
sqrt
3.
Lemma
PI4_RGT_0
: 0 <
PI
/ 4.
Lemma
cos_PI4
:
cos
(
PI
/ 4) = 1 /
sqrt
2.
Lemma
sin_PI4
:
sin
(
PI
/ 4) = 1 /
sqrt
2.
Lemma
tan_PI4
:
tan
(
PI
/ 4) = 1.
Lemma
cos3PI4
:
cos
(3 * (
PI
/ 4)) = -1 /
sqrt
2.
Lemma
sin3PI4
:
sin
(3 * (
PI
/ 4)) = 1 /
sqrt
2.
Lemma
cos_PI6
:
cos
(
PI
/ 6) =
sqrt
3 / 2.
Lemma
tan_PI6
:
tan
(
PI
/ 6) = 1 /
sqrt
3.
Lemma
sin_PI3
:
sin
(
PI
/ 3) =
sqrt
3 / 2.
Lemma
cos_PI3
:
cos
(
PI
/ 3) = 1 / 2.
Lemma
tan_PI3
:
tan
(
PI
/ 3) =
sqrt
3.
Lemma
sin_2PI3
:
sin
(2 * (
PI
/ 3)) =
sqrt
3 / 2.
Lemma
cos_2PI3
:
cos
(2 * (
PI
/ 3)) = -1 / 2.
Lemma
tan_2PI3
:
tan
(2 * (
PI
/ 3)) = -
sqrt
3.
Lemma
cos_5PI4
:
cos
(5 * (
PI
/ 4)) = -1 /
sqrt
2.
Lemma
sin_5PI4
:
sin
(5 * (
PI
/ 4)) = -1 /
sqrt
2.
Lemma
sin_cos5PI4
:
cos
(5 * (
PI
/ 4)) =
sin
(5 * (
PI
/ 4)).
Lemma
Rgt_3PI2_0
: 0 < 3 * (
PI
/ 2).
Lemma
Rgt_2PI_0
: 0 < 2 *
PI
.
Lemma
Rlt_PI_3PI2
:
PI
< 3 * (
PI
/ 2).
Lemma
Rlt_3PI2_2PI
: 3 * (
PI
/ 2) < 2 *
PI
.
Radian -> Degree | Degree -> Radian
Definition
plat
:
R
:= 180.
Definition
toRad
(
x
:R) :
R
:=
x
*
PI
* /
plat
.
Definition
toDeg
(
x
:R) :
R
:=
x
*
plat
* /
PI
.
Lemma
rad_deg
:
forall
x
:R,
toRad
(
toDeg
x
) =
x
.
Lemma
toRad_inj
:
forall
x
y
:R,
toRad
x
=
toRad
y
->
x
=
y
.
Lemma
deg_rad
:
forall
x
:R,
toDeg
(
toRad
x
) =
x
.
Definition
sind
(
x
:R) :
R
:=
sin
(
toRad
x
).
Definition
cosd
(
x
:R) :
R
:=
cos
(
toRad
x
).
Definition
tand
(
x
:R) :
R
:=
tan
(
toRad
x
).
Lemma
Rsqr_sin_cos_d_one
:
forall
x
:R,
Rsqr
(
sind
x
) +
Rsqr
(
cosd
x
) = 1.
Other properties
Lemma
sin_lb_ge_0
:
forall
a
:R, 0 <=
a
->
a
<=
PI
/ 2 -> 0 <=
sin_lb
a
.