Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Lock sin and cos #1218

Merged
merged 3 commits into from
Apr 26, 2024
Merged

Lock sin and cos #1218

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
008e274
Lock sin and cos
affeldt-aist Apr 24, 2024
9319ba7
changelog
affeldt-aist Apr 24, 2024
915780c
lock asin, acos, atan
affeldt-aist Apr 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,11 @@
- in `forms.v`:
+ notation ``` u ``_ _ ```

- in `trigo.v`:
+ definitions `sin`, `cos`, `acos`, `asin`, `atan` are now HB.locked
- in `sequences.v`:
+ definition `expR` is now HB.locked

### Renamed

- in `constructive_ereal.v`:
Expand Down
95 changes: 55 additions & 40 deletions theories/trigo.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
Expand Down Expand Up @@ -132,13 +133,22 @@ Qed.

End alternating.

Definition sin_coeff {R : realType} (x : R) :=
[sequence (odd n)%:R * (-1) ^+ n.-1./2 * x ^+ n / n`!%:R]_n.

HB.lock Definition sin {R : realType} x : R := lim (series (sin_coeff x) @ \oo).
Canonical locked_sin := Unlockable sin.unlock.

Definition cos_coeff {R : realType} (x : R) :=
[sequence (~~ odd n)%:R * (-1)^n./2 * x ^+ n / n`!%:R]_n.

HB.lock Definition cos {R : realType} x : R := lim (series (cos_coeff x) @ \oo).
Canonical locked_cos := Unlockable cos.unlock.

Section CosSin.
Variable R : realType.
Implicit Types x y : R.

Definition sin_coeff x :=
[sequence (odd n)%:R * (-1) ^+ n.-1./2 * x ^+ n / n`!%:R]_n.

Lemma sin_coeffE x : sin_coeff x =
(fun n => (fun n => (odd n)%:R * (-1) ^+ n.-1./2 * (n`!%:R)^-1) n * x ^+ n).
Proof. by apply/funext => i; rewrite /sin_coeff /= -!mulrA [_ / _]mulrC. Qed.
Expand All @@ -157,11 +167,9 @@ apply: series_le_cvg; last exact: (@is_cvg_series_exp_coeff _ `|x|).
by case: odd; [rewrite mul1r| rewrite !mul0r].
Qed.

Definition sin x : R := lim (series (sin_coeff x) @ \oo).

Lemma sinE : sin = fun x =>
lim (pseries (fun n => (odd n)%:R * (-1) ^+ n.-1./2 * (n`!%:R)^-1) x @ \oo).
Proof. by apply/funext => x; rewrite /pseries -sin_coeffE. Qed.
Proof. by apply/funext => x; rewrite /pseries unlock -sin_coeffE. Qed.

Definition sin_coeff' x (n : nat) := (-1)^n * x ^+ n.*2.+1 / n.*2.+1`!%:R.

Expand All @@ -172,6 +180,7 @@ Qed.

Lemma cvg_sin_coeff' x : series (sin_coeff' x) @ \oo --> sin x.
Proof.
rewrite unlock.
have /(@cvg_series_cvg_series_group _ _ 2) := @is_cvg_series_sin_coeff x.
move=> /(_ isT); apply: cvg_trans.
rewrite [X in _ --> series X @ \oo](_ : _ = (fun n => sin_coeff x n.*2.+1)).
Expand All @@ -189,22 +198,20 @@ apply/funext => i; rewrite /pseries_diffs /= factS natrM invfM.
by rewrite [_.+1%:R * _]mulrC -!mulrA [_.+1%:R^-1 * _]mulrC mulfK.
Qed.

Lemma series_sin_coeff0 n : series (sin_coeff 0) n.+1 = 0.
Lemma series_sin_coeff0 n : series (@sin_coeff R 0) n.+1 = 0.
Proof.
rewrite /series /= big_nat_recl //= /sin_coeff /= expr0n divr1 !mulr1.
by rewrite big1 ?addr0 // => i _; rewrite expr0n !(mul0r, mulr0).
Qed.

Lemma sin0 : sin 0 = 0.
Lemma sin0 : sin 0 = 0 :> R.
Proof.
rewrite unlock.
apply: lim_near_cst => //; near=> m; rewrite -[m]prednK; last by near: m.
rewrite -addn1 series_addn series_sin_coeff0 big_add1 big1 ?addr0//.
by move=> i _; rewrite /sin_coeff /= expr0n !(mulr0, mul0r).
Unshelve. all: by end_near. Qed.

Definition cos_coeff x :=
[sequence (~~ odd n)%:R * (-1)^n./2 * x ^+ n / n`!%:R]_n.

Lemma cos_coeff_odd n x : cos_coeff x n.*2.+1 = 0.
Proof. by rewrite /cos_coeff /= odd_double /= !mul0r. Qed.

Expand Down Expand Up @@ -240,13 +247,11 @@ apply: series_le_cvg; last exact: (@is_cvg_series_exp_coeff _ `|x|).
by case: odd; [rewrite !mul0r | rewrite mul1r].
Qed.

Definition cos x : R := lim (series (cos_coeff x) @ \oo).

Lemma cosE : cos = fun x =>
lim (series (fun n =>
(fun n => (~~(odd n))%:R * (-1)^+ n./2 * (n`!%:R)^-1) n
* x ^+ n) @ \oo).
Proof. by apply/funext => x; rewrite -cos_coeffE. Qed.
Proof. by rewrite unlock; apply/funext => x; rewrite -cos_coeffE. Qed.

Definition cos_coeff' x (n : nat) := (-1)^n * x ^+ n.*2 / n.*2`!%:R.

Expand All @@ -258,6 +263,7 @@ Qed.

Lemma cvg_cos_coeff' x : series (cos_coeff' x) @ \oo --> cos x.
Proof.
rewrite unlock.
have /(@cvg_series_cvg_series_group _ _ 2) := @is_cvg_series_cos_coeff x.
move=> /(_ isT); apply: cvg_trans.
rewrite [X in _ --> series X @ \oo](_ : _ = (fun n => cos_coeff x n.*2)); last first.
Expand All @@ -278,14 +284,15 @@ rewrite factS natrM invfM.
by rewrite [_.+1%:R * _]mulrC -!mulrA [_.+1%:R^-1 * _]mulrC mulfK.
Qed.

Lemma series_cos_coeff0 n : series (cos_coeff 0) n.+1 = 1.
Lemma series_cos_coeff0 n : series (cos_coeff 0) n.+1 = 1 :> R.
Proof.
rewrite /series /= big_nat_recl //= /cos_coeff /= expr0n divr1 !mulr1.
by rewrite big1 ?addr0 // => i _; rewrite expr0n !(mul0r, mulr0).
Qed.

Lemma cos0 : cos 0 = 1.
Lemma cos0 : cos 0 = 1 :> R.
Proof.
rewrite unlock.
apply: lim_near_cst => //; near=> m; rewrite -[m]prednK; last by near: m.
rewrite -addn1 series_addn series_cos_coeff0 big_add1 big1 ?addr0//.
by move=> i _; rewrite /cos_coeff /= expr0n !(mulr0, mul0r).
Expand All @@ -312,7 +319,7 @@ Qed.
Lemma derivable_sin x : derivable sin x 1.
Proof. by apply: ex_derive; apply: is_derive_sin. Qed.

Lemma continuous_sin : continuous sin.
Lemma continuous_sin : continuous (@sin R).
Proof.
by move=> x; apply/differentiable_continuous/derivable1_diffP/derivable_sin.
Qed.
Expand Down Expand Up @@ -344,7 +351,7 @@ Qed.
Lemma derivable_cos x : derivable cos x 1.
Proof. by apply: ex_derive; apply: is_derive_cos. Qed.

Lemma continuous_cos : continuous cos.
Lemma continuous_cos : continuous (@cos R).
Proof.
by move=> x; exact/differentiable_continuous/derivable1_diffP/derivable_cos.
Qed.
Expand Down Expand Up @@ -899,15 +906,18 @@ Arguments tan {R}.
#[global] Hint Extern 0 (is_derive _ _ tan _) =>
(eapply is_derive_tan; first by []) : typeclass_instances.

HB.lock Definition acos {R : realType} (x : R) : R :=
get [set y | 0 <= y <= pi /\ cos y = x].
Canonical locked_acos := Unlockable acos.unlock.

Section Acos.
Variable R : realType.

Definition acos (x : R) : R := get [set y | 0 <= y <= pi /\ cos y = x].
Implicit Type x : R.

Lemma acos_def x :
-1 <= x <= 1 -> 0 <= acos x <= pi /\ cos (acos x) = x.
Proof.
move=> xB; rewrite /acos; case: xgetP => //= He.
move=> xB; rewrite unlock /acos; case: xgetP => //= He.
pose f y := cos y - x.
have /(IVT (@pi_ge0 _))[] // : minr (f 0) (f pi) <= 0 <= maxr (f 0) (f pi).
rewrite /f cos0 cospi /minr /maxr ltrD2r -subr_lt0 opprK (_ : 1 + 1 = 2)//.
Expand All @@ -925,7 +935,7 @@ Proof. by move=> /acos_def[/andP[]]. Qed.
Lemma acos_lepi x : -1 <= x <= 1 -> acos x <= pi.
Proof. by move=> /acos_def[/andP[]]. Qed.

Lemma acosK : {in `[(-1),1], cancel acos cos}.
Lemma acosK : {in `[(-1),1], cancel (@acos R) cos}.
Proof. by move=> x; rewrite in_itv/==> /acos_def[/andP[]]. Qed.

Lemma acos_gt0 x : -1 <= x < 1 -> 0 < acos x.
Expand All @@ -944,7 +954,7 @@ have : cos (acos x) = x by rewrite acosK// in_itv/= x_le1 ltW.
by case: (ltrgtP (acos x) pi) => // ->; rewrite cospi => ->; rewrite ltxx.
Qed.

Lemma cosK : {in `[0, pi], cancel cos acos}.
Lemma cosK : {in `[0, pi], cancel (@cos R) acos}.
Proof.
move=> x xB; apply: cos_inj => //; rewrite ?acosK//; last first.
by move: xB; rewrite !in_itv/= => /andP[? ?];rewrite cos_geN1 cos_le1.
Expand All @@ -964,7 +974,7 @@ rewrite cos_pihalf => -> //; rewrite in_itv//= divr_ge0 ?ler0n ?pi_ge0//=.
by rewrite ler_pdivrMr ?ltr0n// ler_peMr ?pi_ge0// ler1n.
Qed.

Lemma acosN a : -1 <= a <= 1 -> acos (- a) = pi - acos a.
Lemma acosN a : -1 <= a <= 1 -> acos (- a) = pi - acos a :> R.
Proof.
move=> a1; have ? : -1 <= - a <= 1 by rewrite lerNl opprK lerNl andbC.
apply: cos_inj; first by rewrite in_itv/= acos_ge0//= acos_lepi.
Expand All @@ -975,9 +985,9 @@ Qed.
Lemma acosN1 : acos (- 1) = (pi : R).
Proof. by rewrite acosN ?acos1 ?subr0 ?lexx// -subr_ge0 opprK addr_ge0. Qed.

Lemma cosKN a : - pi <= a <= 0 -> acos (cos a) = - a.
Lemma cosKN x : - pi <= x <= 0 -> acos (cos x) = - x.
Proof.
by move=> pia0; rewrite -(cosN a) cosK// in_itv/= lerNr oppr0 lerNl andbC.
by move=> pia0; rewrite -(cosN x) cosK// in_itv/= lerNr oppr0 lerNl andbC.
Qed.

Lemma sin_acos x : -1 <= x <= 1 -> sin (acos x) = Num.sqrt (1 - x^+2).
Expand All @@ -1001,7 +1011,7 @@ suff /itvP zI : z \in `]0, pi[ by have : 0 <= z <= pi by rewrite ltW ?zI.
by near: z.
Unshelve. all: by end_near. Qed.

Lemma is_derive1_acos (x : R) :
Lemma is_derive1_acos x :
-1 < x < 1 -> is_derive x 1 acos (- (Num.sqrt (1 - x ^+ 2))^-1).
Proof.
move=> /andP[x_gtN1 x_lt1]; rewrite -sin_acos ?ltW // -invrN.
Expand All @@ -1024,15 +1034,18 @@ End Acos.
#[global] Hint Extern 0 (is_derive _ 1 (@acos _) _) =>
(eapply is_derive1_acos; first by []) : typeclass_instances.

HB.lock Definition asin {R : realType} (x : R) : R :=
get [set y | -(pi / 2) <= y <= pi / 2 /\ sin y = x].
Canonical locked_asin := Unlockable asin.unlock.

Section Asin.
Variable R : realType.

Definition asin (x : R) : R := get [set y | -(pi / 2) <= y <= pi / 2 /\ sin y = x].
Implicit Type x : R.

Lemma asin_def x :
-1 <= x <= 1 -> -(pi / 2) <= asin x <= pi / 2 /\ sin (asin x) = x.
Proof.
move=> xB; rewrite /asin; case: xgetP => //= He.
move=> xB; rewrite unlock /asin; case: xgetP => //= He.
pose f y := sin y - x.
have /IVT[] // :
minr (f (-(pi/2))) (f (pi/2)) <= 0 <= maxr (f (-(pi/2))) (f (pi/2)).
Expand All @@ -1051,7 +1064,7 @@ Proof. by move=> /asin_def[/andP[]]. Qed.
Lemma asin_lepi2 x : -1 <= x <= 1 -> asin x <= pi / 2.
Proof. by move=> /asin_def[/andP[]]. Qed.

Lemma asinK : {in `[(-1),1], cancel asin sin}.
Lemma asinK : {in `[(-1),1], cancel (@asin R) sin}.
Proof. by move=> x; rewrite in_itv/= => /asin_def[/andP[]]. Qed.

Lemma asin_ltpi2 x : -1 <= x < 1 -> asin x < pi/2.
Expand All @@ -1071,7 +1084,7 @@ have : sin (asin x) = x by rewrite asinK// in_itv/= x_le1 ltW.
by case: (ltrgtP (asin x)) => //->; rewrite sinN sin_pihalf => <-; rewrite ltxx.
Qed.

Lemma sinK : {in `[(- (pi / 2)), pi / 2], cancel sin asin}.
Lemma sinK : {in `[(- (pi / 2)), pi / 2], cancel (@sin R) asin}.
Proof.
move=> x; rewrite !in_itv/= => xB ; apply: sin_inj => //; last first.
by rewrite asinK// in_itv/= sin_geN1 sin_le1.
Expand Down Expand Up @@ -1099,7 +1112,7 @@ suff /itvP zI : z \in `](-(pi/2)), (pi/2)[.
by near: z.
Unshelve. all: by end_near. Qed.

Lemma is_derive1_asin (x : R) :
Lemma is_derive1_asin x :
-1 < x < 1 -> is_derive x 1 asin ((Num.sqrt (1 - x ^+ 2))^-1).
Proof.
move=> /andP[x_gtN1 x_lt1]; rewrite -cos_asin ?ltW //.
Expand All @@ -1123,16 +1136,18 @@ End Asin.
#[global] Hint Extern 0 (is_derive _ 1 (@asin _) _) =>
(eapply is_derive1_asin; first by []) : typeclass_instances.

HB.lock Definition atan {R : realType} (x : R) : R :=
get [set y | -(pi / 2) < y < pi / 2 /\ tan y = x].
Canonical locked_atan := Unlockable atan.unlock.

Section Atan.
Variable R : realType.

Definition atan (x : R) : R :=
get [set y | -(pi / 2) < y < pi / 2 /\ tan y = x].
Implicit Type x : R.

(* Did not see how to use ITV like in the other *)
Lemma atan_def x : -(pi / 2) < atan x < pi / 2 /\ tan (atan x) = x.
Proof.
rewrite /atan; case: xgetP => //= He.
rewrite unlock /atan; case: xgetP => //= He.
pose x1 := Num.sqrt (1 + x^+ 2) ^-1.
have ox2_gt0 : 0 < 1 + x^2.
by apply: lt_le_trans (_ : 1 <= _); rewrite ?lerDl ?sqr_ge0.
Expand Down Expand Up @@ -1166,7 +1181,7 @@ Proof. by case: (atan_def x) => [] /andP[]. Qed.
Lemma atan_ltpi2 x : atan x < pi / 2.
Proof. by case: (atan_def x) => [] /andP[]. Qed.

Lemma atanK : cancel atan tan.
Lemma atanK : cancel (@atan R) tan.
Proof. by move=> x; case: (atan_def x). Qed.

Lemma atan0 : atan 0 = 0 :> R.
Expand Down Expand Up @@ -1195,7 +1210,7 @@ apply: tan_inj; first by rewrite in_itv/= atan_ltpi2 atan_gtNpi2.
- by rewrite tanN !atanK.
Qed.

Lemma tanK : {in `](- (pi / 2)), (pi / 2)[ , cancel tan atan}.
Lemma tanK : {in `](- (pi / 2)), (pi / 2)[ , cancel (@tan R) atan}.
Proof.
move=> x xB; apply tan_inj => //; rewrite ?atanK//.
by rewrite in_itv/= atan_gtNpi2 atan_ltpi2.
Expand Down Expand Up @@ -1224,7 +1239,7 @@ move: cos_gt0; rewrite cosE ltNge; case/negP.
by rewrite oppr_le0 invr_ge0 sqrtr_ge0.
Qed.

Global Instance is_derive1_atan (x : R) : is_derive x 1 atan (1 + x ^+ 2)^-1.
Global Instance is_derive1_atan x : is_derive x 1 atan (1 + x ^+ 2)^-1.
Proof.
rewrite -{1}[x]atanK.
have cosD0 : cos (atan x) != 0.
Expand Down
Loading