From ccbfa1fe19e1086e24096dd8b0b869e71dac5601 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 26 Apr 2024 09:46:55 +0900 Subject: [PATCH] Lock sin and cos (#1218) * Lock sin, cos, asin, acos, atan --- CHANGELOG_UNRELEASED.md | 5 +++ theories/trigo.v | 95 ++++++++++++++++++++++++----------------- 2 files changed, 60 insertions(+), 40 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 45589e26a..af0c30e6a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -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`: diff --git a/theories/trigo.v b/theories/trigo.v index 709eabf1f..b82dad0d8 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -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. @@ -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. @@ -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. @@ -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)). @@ -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. @@ -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. @@ -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. @@ -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). @@ -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. @@ -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. @@ -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)//. @@ -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. @@ -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. @@ -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. @@ -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). @@ -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. @@ -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)). @@ -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. @@ -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. @@ -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 //. @@ -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. @@ -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. @@ -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. @@ -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.