From b889616abb11747f1feb126e55e97cc5695649e1 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Mon, 17 Aug 2026 04:34:54 +0900 Subject: [PATCH 1/5] add RcosE, PIE, RsinE --- analysis_stdlib/Rstruct_topology.v | 126 ++++++++++++++++++++++++++++- 1 file changed, 123 insertions(+), 3 deletions(-) diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index 2fa87fe480..c28061aafe 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -9,13 +9,16 @@ 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. 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 trigo. Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. @@ -120,5 +123,122 @@ case: (Rlt_dec 0 x) => [/= ? | /RltP/[!xgt0]//]. by case: ln_exists => y ->; rewrite RexpE exp.expRK. Qed. -(* extend RealsE from Rstruct.v *) -Definition RealsE := (RealsE, RexpE, RlnE). +(* PRed to mathcomp (#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. + +Module RcosE. +Import normedtype sequences. +Local Open Scope classical_set_scope. + +Lemma RcosE (x : R) : Rtrigo_def.cos x = trigo.cos x. +Proof. +apply/esym; rewrite /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 trigo.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. + +End RcosE. + +Definition RcosE := RcosE.RcosE. + +Section PIE. + +Let pihalf_spec (x : R) := 0 <= x <= 2 /\ trigo.cos.body 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: trigo.cos_inj. +- rewrite in_itv/=; apply/andP; split => //. + by rewrite (le_trans x2)// trigo.pi_ge2. +- rewrite in_itv/=; apply/andP; split => //. + by rewrite (le_trans y2)// trigo.pi_ge2. +by rewrite cosx0 cosy0. +Qed. + +Let PI2E : PI2 = trigo.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 trigo.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 = trigo.pi. +Proof. by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed. + +End PIE. + +Lemma RsinE (x : R) : Rtrigo_def.sin x = trigo.sin x. +Proof. by rewrite sin_cos RcosE PIE !RealsE/= addrC trigo.cosDpihalf opprK. Qed. + +Definition RealsE := (RealsE, RexpE, RlnE, RcosE, PIE, RsinE). From d6d425be8886dbc47ddcedd50f45b9835fe73ae8 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Mon, 17 Aug 2026 05:09:27 +0900 Subject: [PATCH 2/5] move big_nat_dvdn to unstable.v --- analysis_stdlib/Rstruct_topology.v | 78 +++++++++--------------------- classical/unstable.v | 36 ++++++++++++++ 2 files changed, 59 insertions(+), 55 deletions(-) diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index c28061aafe..933d08cc38 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -10,6 +10,8 @@ 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. @@ -18,7 +20,7 @@ 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 trigo. +From mathcomp Require trigonometry_functions. Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. @@ -123,49 +125,13 @@ case: (Rlt_dec 0 x) => [/= ? | /RltP/[!xgt0]//]. by case: ln_exists => y ->; rewrite RexpE exp.expRK. Qed. -(* PRed to mathcomp (#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. - -Module RcosE. -Import normedtype sequences. +Module RtrigoE. +Import normedtype sequences trigonometry_functions. Local Open Scope classical_set_scope. -Lemma RcosE (x : R) : Rtrigo_def.cos x = trigo.cos x. +Lemma RcosE (x : R) : Rtrigo_def.cos x = cos x. Proof. -apply/esym; rewrite /cos. +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). @@ -176,7 +142,7 @@ have Gy : series G x @[x --> \oo] --> y. 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 trigo.cosE /series/=; apply: (@cvg_lim R^o) => //. +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. @@ -201,30 +167,26 @@ rewrite /G/= plusE addn0 addnn Rsqr_def !RealsE. by rewrite -expr2 -exprM mul2n doubleK mulrA. Unshelve. all: by end_near. Qed. -End RcosE. - -Definition RcosE := RcosE.RcosE. - Section PIE. -Let pihalf_spec (x : R) := 0 <= x <= 2 /\ trigo.cos.body x = 0. +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: trigo.cos_inj. +apply: cos_inj. - rewrite in_itv/=; apply/andP; split => //. - by rewrite (le_trans x2)// trigo.pi_ge2. + by rewrite (le_trans x2)// pi_ge2. - rewrite in_itv/=; apply/andP; split => //. - by rewrite (le_trans y2)// trigo.pi_ge2. + by rewrite (le_trans y2)// pi_ge2. by rewrite cosx0 cosy0. Qed. -Let PI2E : PI2 = trigo.pi / 2. +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 trigo.pihalfE. +rewrite pihalfE. have x_pihalf : pihalf_spec x. split; [|by rewrite -RcosE]. rewrite (le_trans _ x78)/= ?RealsE/=; [lra|]. @@ -233,12 +195,18 @@ apply/esym/get_unique => //= y y_pihalf. exact: pihalf_unique. Qed. -Lemma PIE : PI = trigo.pi. +Lemma PIE : PI = pi. Proof. by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed. End PIE. -Lemma RsinE (x : R) : Rtrigo_def.sin x = trigo.sin x. -Proof. by rewrite sin_cos RcosE PIE !RealsE/= addrC trigo.cosDpihalf opprK. Qed. +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 PIE := RtrigoE.PIE. +Definition RsinE := RtrigoE.RsinE. Definition RealsE := (RealsE, RexpE, RlnE, RcosE, PIE, RsinE). diff --git a/classical/unstable.v b/classical/unstable.v index 3d634c27c1..95136b09c4 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -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. From 06e76e6c7d17cb668644cea311d3bcbba000cf19 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Mon, 17 Aug 2026 05:13:35 +0900 Subject: [PATCH 3/5] changelog --- CHANGELOG_UNRELEASED.md | 6 ++++++ classical/unstable.v | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c676bc2941..80b0f96cbd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -52,6 +52,9 @@ + global instance `is_derive_exp` + lemma `derive1_shift` +- in `Rstruct_topology.v`: + + lemmas `RcosE`, `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`, `PIE`, `RsinE` + ### Renamed - in `esum.v`: diff --git a/classical/unstable.v b/classical/unstable.v index 95136b09c4..47536ebce7 100644 --- a/classical/unstable.v +++ b/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. *) (* *) From 5379a1ec581049f091307f3beb0382e466d2ea38 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Mon, 17 Aug 2026 05:34:32 +0900 Subject: [PATCH 4/5] fix comment; rename PIE to Rtrigo_PIE --- CHANGELOG_UNRELEASED.md | 4 ++-- analysis_stdlib/Rstruct_topology.v | 7 ++++--- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 80b0f96cbd..253eb2e83d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -53,7 +53,7 @@ + lemma `derive1_shift` - in `Rstruct_topology.v`: - + lemmas `RcosE`, `PIE`, `RsinE` + + lemmas `RcosE`, `Rtrigo_PIE`, `RsinE` ### Changed @@ -73,7 +73,7 @@ + lemmas `is_deriveV`, `is_derive1_comp` - in `Rstruct_topology.v`: - + lemma `RealsE` to include `RcosE`, `PIE`, `RsinE` + + lemma `RealsE` to include `RcosE`, `Rtrigo_PIE`, `RsinE` ### Renamed diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index 933d08cc38..2642bf5f42 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -195,7 +195,7 @@ apply/esym/get_unique => //= y y_pihalf. exact: pihalf_unique. Qed. -Lemma PIE : PI = pi. +Lemma Rtrigo_PIE : PI = pi. Proof. by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed. End PIE. @@ -206,7 +206,8 @@ Proof. by rewrite sin_cos RcosE PIE !RealsE/= addrC cosDpihalf opprK. Qed. End RtrigoE. Definition RcosE := RtrigoE.RcosE. -Definition PIE := RtrigoE.PIE. +Definition Rtrigo_PIE := RtrigoE.Rtrigo_PIE. Definition RsinE := RtrigoE.RsinE. -Definition RealsE := (RealsE, RexpE, RlnE, RcosE, PIE, RsinE). +(* extend RealsE from Rstruct.v *) +Definition RealsE := (RealsE, RexpE, RlnE, RcosE, Rtrigo_PIE, RsinE). From f80cb0cd2a789c435e034dcac4ff1655cfc18c5f Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Mon, 17 Aug 2026 05:48:51 +0900 Subject: [PATCH 5/5] fix --- analysis_stdlib/Rstruct_topology.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index 2642bf5f42..43d477f980 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -195,7 +195,7 @@ apply/esym/get_unique => //= y y_pihalf. exact: pihalf_unique. Qed. -Lemma Rtrigo_PIE : PI = pi. +Lemma PIE : PI = pi. Proof. by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed. End PIE. @@ -206,7 +206,7 @@ Proof. by rewrite sin_cos RcosE PIE !RealsE/= addrC cosDpihalf opprK. Qed. End RtrigoE. Definition RcosE := RtrigoE.RcosE. -Definition Rtrigo_PIE := RtrigoE.Rtrigo_PIE. +Definition Rtrigo_PIE := RtrigoE.PIE. Definition RsinE := RtrigoE.RsinE. (* extend RealsE from Rstruct.v *)