Lock sin and cos (#1218)

* Lock sin, cos, asin, acos, atan

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`:

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.