add compatibility lemmas for Stdlib Rcos and Rsin

CHANGELOG_UNRELEASED.md

@@ -52,6 +52,9 @@
   + global instance `is_derive_exp`
   + lemma `derive1_shift`
 
+- in `Rstruct_topology.v`:
+  + lemmas `RcosE`, `Rtrigo_PIE`, `RsinE`
+
 ### Changed
 
 - in `derive.v`:
@@ -69,6 +72,9 @@
 - moved from `realfun.v` to `derive.v`: 
   + lemmas `is_deriveV`, `is_derive1_comp`
 
+- in `Rstruct_topology.v`:
+  + lemma `RealsE` to include `RcosE`, `Rtrigo_PIE`, `RsinE`
+
 ### Renamed
 
 - in `esum.v`:

analysis_stdlib/Rstruct_topology.v

@@ -9,13 +9,18 @@ From Stdlib Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def
 From Stdlib Require Import Rtrigo1 Reals.
 From HB Require Import structures.
 From mathcomp Require Import boot order ssralg ssrnum archimedean.
+From mathcomp Require Import interval arithmetic_tactic.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets reals interval_inference.
 From mathcomp Require Export Rstruct.
 From mathcomp Require Import topology.
-(* The following line is for RexpE. *)
+(* The following line is for RexpE and RcosE. *)
 From mathcomp Require normedtype sequences.
 (* The following line is for RlnE. *)
 From mathcomp Require exp.
+(* The following line is for RcosE, PIE and RsinE. *)
+From mathcomp Require trigonometry_functions.
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
@@ -120,5 +125,89 @@ case: (Rlt_dec 0 x) => [/= ? | /RltP/[!xgt0]//].
 by case: ln_exists => y ->; rewrite RexpE exp.expRK.
 Qed.
 
+Module RtrigoE.
+Import normedtype sequences trigonometry_functions.
+Local Open Scope classical_set_scope.
+
+Lemma RcosE (x : R) : Rtrigo_def.cos x = cos x.
+Proof.
+apply/esym; rewrite /Rtrigo_def.cos.
+case: exist_cos => y.
+rewrite /cos_in /cos_n /infinite_sum/=.
+set G : nat -> R^o := (G in sum_f_R0 G).
+move=> cos_ub.
+have Gy : series G x @[x --> \oo] --> y.
+  rewrite -cvg_shiftS/=; apply/cvgrPdist_lt => /= e /RltP /cos_ub[N Ncos_ub].
+  near=> n.
+  have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge.
+  move: Ncos_ub => /(_ _ nN) /[!RdistE] /RltP /=.
+  by rewrite /G distrC sum_f_R0E.
+rewrite cosE /series/=; apply: (@cvg_lim R^o) => //.
+evar (F : nat -> R); rewrite [X in fmap X](_ : _ = fun n => F n.+1).
+  apply: funext => n.
+  under eq_bigr do rewrite -dvdn2 -!mulrA mulr_natl mulrb.
+  rewrite -big_mkcond/=.
+  rewrite big_nat_dvdn.
+  rewrite addn1.
+  pattern n.+1; rewrite [EQ in EQ n.+1]lock.
+  have : forall f g, f = g -> forall y, locked (fun x => f x = g x) y.
+    by move=> ? ? ? ? ->; rewrite -lock.
+  by apply; unlock; rewrite {}/F; reflexivity.
+rewrite -/(mk_sequence F) cvg_shiftS/= -[X in _ --> X]/(nbhs y).
+have divn2_cofinal : divn^~ 2 @ \oo --> \oo.
+  move=> N [] n _ nN.
+  exists (n * 2)%N => // m/=.
+  have := nN (m %/ 2)%N => /=.
+  by rewrite leq_divRL.
+have := (cvg_comp (divn^~ 2%N) _ divn2_cofinal Gy).
+rewrite [X in fmap X](_ : _ = F)//.
+apply: funext => n/=.
+apply: eq_bigr => i _.
+rewrite /G/= plusE addn0 addnn Rsqr_def !RealsE.
+by rewrite -expr2 -exprM mul2n doubleK mulrA.
+Unshelve. all: by end_near. Qed.
+
+Section PIE.
+
+Let pihalf_spec (x : R) := 0 <= x <= 2 /\ cos x = 0.
+
+Let pihalf_unique (x y : R) : pihalf_spec x -> pihalf_spec y -> x = y.
+Proof.
+case=> /andP[] x0 x2 cosx0 [] /andP[] y0 y2 cosy0.
+apply: cos_inj.
+- rewrite in_itv/=; apply/andP; split => //.
+  by rewrite (le_trans x2)// pi_ge2.
+- rewrite in_itv/=; apply/andP; split => //.
+  by rewrite (le_trans y2)// pi_ge2.
+by rewrite cosx0 cosy0.
+Qed.
+
+Let PI2E : PI2 = pi / 2.
+Proof.
+rewrite /PI2; case: PI_2_aux => x /= [] [] /RleP x78 /RleP x74.
+move/Ropp_eq_compat; rewrite Ropp_involutive Ropp_0 RealsE => cosx0.
+rewrite pihalfE.
+have x_pihalf : pihalf_spec x.
+  split; [|by rewrite -RcosE].
+  rewrite (le_trans _ x78)/= ?RealsE/=; [lra|].
+  by rewrite (le_trans x74)// ?RealsE/=; lra.
+apply/esym/get_unique => //= y y_pihalf.
+exact: pihalf_unique.
+Qed.
+
+Lemma PIE : PI = pi.
+Proof. by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed.
+
+End PIE.
+
+Lemma RsinE (x : R) : Rtrigo_def.sin x = sin x.
+Proof. by rewrite sin_cos RcosE PIE !RealsE/= addrC cosDpihalf opprK. Qed.
+
+End RtrigoE.
+
+Definition RcosE := RtrigoE.RcosE.
+Definition Rtrigo_PIE := RtrigoE.PIE.
+Definition RsinE := RtrigoE.RsinE.
+
 (* extend RealsE from Rstruct.v *)
-Definition RealsE := (RealsE, RexpE, RlnE).
+Definition RealsE := (RealsE, RexpE, RlnE, RcosE, Rtrigo_PIE, RsinE).

classical/unstable.v

@@ -9,7 +9,7 @@ From mathcomp Require Import vector archimedean interval matrix.
 (* This files contains lemmas that should eventually be backported            *)
 (* to mathcomp. These lemmas may change before being backported to mathcomp,  *)
 (* don't use anything in this file outside of Analysis. For this same reason, *)
-(* nothing in this file should be mentionned in the changelog.                *)
+(* nothing in this file should be mentioned in the changelog.                 *)
 (* Once a result is backported to mathcomp, please move it to mathcomp_extra.v*)
 (* and mention it in the changelog.                                           *)
 (*                                                                            *)
@@ -647,3 +647,39 @@ End Theory.
 Module Import Exports. HB.reexport. End Exports.
 End Norm.
 Export Norm.Exports.
+
+(* PR to mathcomp in progress (#1637) *)
+Section big_nat_dvdn.
+
+Lemma iotaS (m n : nat) : iota m n.+1 = rcons (iota m n) (m + n)%N.
+Proof. by rewrite -addn1 iotaD cats1. Qed.
+
+Lemma index_iotaS (m n : nat) :
+  (m <= n)%N -> index_iota m n.+1 = rcons (index_iota m n) n.
+Proof. by move=> ?; rewrite /index_iota subSn// iotaS subnKC. Qed.
+
+Lemma big_nat_recr_op (R : Type) (idx : R) (op : R -> R -> R)
+  (n m : nat) (P : pred nat) (F : nat -> R) :
+  (m <= n)%N ->
+  let idx' := if P n then op (F n) idx else idx in
+  \big[op/idx]_(m <= i < n.+1 | P i) F i = \big[op/idx']_(m <= i < n | P i) F i.
+Proof. by move=> ?; rewrite index_iotaS// big_rcons_op. Qed.
+
+Lemma big_nat_dvdn (R : Type) (idx : R) (op : R -> R -> R)
+  (n d : nat) (F : nat -> R) :
+  \big[op/idx]_(0 <= i < n | d.+1 %| i) F i =
+  \big[op/idx]_(0 <= i < (n + d) %/ d.+1) F (d.+1 * i)%N.
+Proof.
+elim: n idx.
+  by move=> ?; rewrite divn_small// !big_nil.
+move=> n IHn idx.
+rewrite addSn divnS// -addnS dvdn_addl// big_nat_recr_op// IHn.
+case/boolP: (d.+1 %| n) => H /=.
+  rewrite add1n big_nat_recr_op//.
+  rewrite divnDl// (@divn_small d)// addn0.
+  congr bigop.body; congr op; congr F.
+  by rewrite muln_divCA// divnn muln1.
+by rewrite add0n.
+Qed.
+
+End big_nat_dvdn.