From 1388bac8fcd8f5e1e84e75046904b8b8c50a1f4c Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 14 Mar 2025 13:49:47 +0900 Subject: [PATCH 1/4] equivalence between exp in stdlib and mca --- CHANGELOG_UNRELEASED.md | 1 + reals_stdlib/Rstruct.v | 74 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 75 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ec9184a236..afb50dd04a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -9,6 +9,7 @@ - file `Rstruct.v` + lemma `Pos_to_natE` (from `mathcomp_extra.v`) + + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE`, `RexpE` - new file `internal_Eqdep_dec.v` (don't use, internal, to be removed) diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index 2eda987b0c..d4da7bff6f 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -32,6 +32,9 @@ From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum. From mathcomp Require Import archimedean. From HB Require Import structures. From mathcomp Require Import mathcomp_extra. +(* The following two lines are for RexpE *) +From mathcomp Require functions filter topology separation_axioms. +From mathcomp Require normedtype sequences. Set Implicit Arguments. Unset Strict Implicit. @@ -525,6 +528,27 @@ case: (lerP x y) => H; first by rewrite Rmin_left //; apply: RlebP. by rewrite ?ltW // Rmin_right //; apply/RlebP; move/ltW : H. Qed. +Lemma RabsE x : Rabs x = Num.norm x. +Proof. +rewrite /Rabs. +case: Rcase_abs. + by move/RltP/ltW; rewrite -eqr_normN=> /eqP. +by move/Rge_le/RleP; rewrite -eqr_norm_id=> /eqP. +Qed. + +Lemma RdistE x y : Rdist x y = Num.norm (x - y). +Proof. by rewrite /Rdist RabsE RminusE. Qed. + +Lemma sum_f_R0E f n : sum_f_R0 f n = \sum_(0 <= k < n.+1) f k. +Proof. +elim: n; first by rewrite big_nat1. +move=> n IHn /=. +by rewrite RplusE big_nat_recr//= IHn. +Qed. + +Lemma factE n : fact n = factorial n. +Proof. by elim: n=> //= n IHn; rewrite factS mulSn IHn. Qed. + Section bigmaxr. Context {R : realDomainType}. @@ -719,3 +743,53 @@ Qed. End bigmaxr. End ssreal_struct_contd. + +Module RexpE. +Import functions filter topology separation_axioms. +Import normedtype sequences. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports numFieldNormedType.Exports. +Local Open Scope classical_set_scope. + +(* proof by comparing the defining power series *) +Lemma RexpE (x : R) : Rtrigo_def.exp x = expR x. +Proof. +move: x; change R with R^o; move=> z. +apply/esym. +rewrite /exp /exist_exp. +case: Alembert_C3; change R with R^o; move=> x /=. +rewrite /Pser /infinite_sum /=. +move=> Hexp. +rewrite /expR /exp_coeff. +rewrite /series /mk_sequence. +apply: (@cvg_lim R^o _ nat \oo _ _ x)=> //. +suff: \sum_(0 <= k < n.+1) z ^+ k / k`!%:R @[n --> \oo] --> (x : R^o). + set f' : nat -> R^o := (f in fmap f); move=> H. + set f : nat -> R^o := (f in fmap f); move: H. + have->: f' = fun n=> f n.+1 by []. + clear f'; move=> fx. + have:= (cvgB fx (cvg_exp_coeff z)). + have->: (fun n : nat => f n.+1) - exp_coeff z = f. + apply: funext=> n. + rewrite /GRing.add/= /f big_nat_recr//=. + by rewrite -addrA subrr addr0. + by rewrite subr0; exact. +rewrite /nbhs /= => A. +rewrite /nbhs_ball_ /=. +case=> eps /= /RltP /Rlt_gt eps0. +rewrite /ball_ => xyA. +rewrite /filter.eventually/= /filter_from/=. +move: Hexp=> /(_ eps eps0) -[] i Hexp. +exists i=> // n /= /ssrnat.leP ni. +apply: xyA=> /=. +move: Hexp=> /(_ n ni) /[!RdistE] /RltP /=. +rewrite distrC. +suff->: sum_f_R0 (fun n0 : nat => (/ INR (fact n0) * z ^ n0)%R) n = + \sum_(0 <= k < n.+1) z ^+ k / k`!%:R by []. +rewrite sum_f_R0E. +apply: eq_bigr=> k _. +by rewrite RinvE RpowE mulrC factE INRE. +Qed. +End RexpE. + +Definition RexpE := RexpE.RexpE. From 82c6663b66306e95165b061fb7ccc396b880dcdd Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 Mar 2025 19:49:38 +0900 Subject: [PATCH 2/4] more idiomatic proof --- reals_stdlib/Rstruct.v | 77 ++++++++++++------------------------------ 1 file changed, 22 insertions(+), 55 deletions(-) diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index d4da7bff6f..da44a60525 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -32,9 +32,8 @@ From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum. From mathcomp Require Import archimedean. From HB Require Import structures. From mathcomp Require Import mathcomp_extra. -(* The following two lines are for RexpE *) -From mathcomp Require functions filter topology separation_axioms. -From mathcomp Require normedtype sequences. +(* The following line is for RexpE. *) +From mathcomp Require topology normedtype sequences. Set Implicit Arguments. Unset Strict Implicit. @@ -528,26 +527,23 @@ case: (lerP x y) => H; first by rewrite Rmin_left //; apply: RlebP. by rewrite ?ltW // Rmin_right //; apply/RlebP; move/ltW : H. Qed. -Lemma RabsE x : Rabs x = Num.norm x. +Lemma RabsE x : Rabs x = `|x|. Proof. -rewrite /Rabs. -case: Rcase_abs. - by move/RltP/ltW; rewrite -eqr_normN=> /eqP. -by move/Rge_le/RleP; rewrite -eqr_norm_id=> /eqP. +by rewrite /Rabs; case: Rcase_abs => [/RltP x0|/Rge_le/RleP x0]; + [rewrite ltr0_norm|rewrite ger0_norm]. Qed. -Lemma RdistE x y : Rdist x y = Num.norm (x - y). +Lemma RdistE x y : Rdist x y = `|x - y|. Proof. by rewrite /Rdist RabsE RminusE. Qed. Lemma sum_f_R0E f n : sum_f_R0 f n = \sum_(0 <= k < n.+1) f k. Proof. -elim: n; first by rewrite big_nat1. -move=> n IHn /=. -by rewrite RplusE big_nat_recr//= IHn. +elim: n => [|n ih/=]; first by rewrite big_nat1. +by rewrite RplusE big_nat_recr//= ih. Qed. -Lemma factE n : fact n = factorial n. -Proof. by elim: n=> //= n IHn; rewrite factS mulSn IHn. Qed. +Lemma factE n : fact n = n`!. +Proof. by elim: n => //= n ih; rewrite factS mulSn ih. Qed. Section bigmaxr. Context {R : realDomainType}. @@ -745,51 +741,22 @@ End bigmaxr. End ssreal_struct_contd. Module RexpE. -Import functions filter topology separation_axioms. -Import normedtype sequences. -Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Import numFieldTopology.Exports numFieldNormedType.Exports. -Local Open Scope classical_set_scope. +Import topology normedtype sequences. (* proof by comparing the defining power series *) Lemma RexpE (x : R) : Rtrigo_def.exp x = expR x. Proof. -move: x; change R with R^o; move=> z. -apply/esym. -rewrite /exp /exist_exp. -case: Alembert_C3; change R with R^o; move=> x /=. -rewrite /Pser /infinite_sum /=. -move=> Hexp. -rewrite /expR /exp_coeff. -rewrite /series /mk_sequence. -apply: (@cvg_lim R^o _ nat \oo _ _ x)=> //. -suff: \sum_(0 <= k < n.+1) z ^+ k / k`!%:R @[n --> \oo] --> (x : R^o). - set f' : nat -> R^o := (f in fmap f); move=> H. - set f : nat -> R^o := (f in fmap f); move: H. - have->: f' = fun n=> f n.+1 by []. - clear f'; move=> fx. - have:= (cvgB fx (cvg_exp_coeff z)). - have->: (fun n : nat => f n.+1) - exp_coeff z = f. - apply: funext=> n. - rewrite /GRing.add/= /f big_nat_recr//=. - by rewrite -addrA subrr addr0. - by rewrite subr0; exact. -rewrite /nbhs /= => A. -rewrite /nbhs_ball_ /=. -case=> eps /= /RltP /Rlt_gt eps0. -rewrite /ball_ => xyA. -rewrite /filter.eventually/= /filter_from/=. -move: Hexp=> /(_ eps eps0) -[] i Hexp. -exists i=> // n /= /ssrnat.leP ni. -apply: xyA=> /=. -move: Hexp=> /(_ n ni) /[!RdistE] /RltP /=. -rewrite distrC. -suff->: sum_f_R0 (fun n0 : nat => (/ INR (fact n0) * z ^ n0)%R) n = - \sum_(0 <= k < n.+1) z ^+ k / k`!%:R by []. -rewrite sum_f_R0E. -apply: eq_bigr=> k _. -by rewrite RinvE RpowE mulrC factE INRE. -Qed. +apply/esym; rewrite /exp /exist_exp; case: Alembert_C3 => y. +rewrite /Pser /infinite_sum /= => exp_ub. +rewrite /expR /exp_coeff /series/=; apply: (@cvg_lim R^o) => //. +rewrite -cvg_shiftS /=; apply/cvgrPdist_lt => /= e /RltP /exp_ub[N Nexp_ub]. +near=> n. +have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge. +move: Nexp_ub => /(_ _ nN) /[!RdistE] /RltP /=. +rewrite distrC sum_f_R0E; congr (`| _ - _ | < e). +by apply: eq_bigr=> k _; rewrite RinvE RpowE mulrC factE INRE. +Unshelve. all: by end_near. Qed. + End RexpE. Definition RexpE := RexpE.RexpE. From 98e13c3e0cc42178dfda573d43b8d770d264a314 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 Mar 2025 21:54:46 +0900 Subject: [PATCH 3/4] fix CI --- CHANGELOG_UNRELEASED.md | 5 ++++- analysis_stdlib/Rstruct_topology.v | 28 +++++++++++++++++++++++++--- reals_stdlib/Rstruct.v | 23 ----------------------- 3 files changed, 29 insertions(+), 27 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index afb50dd04a..2374ee3d45 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -9,7 +9,7 @@ - file `Rstruct.v` + lemma `Pos_to_natE` (from `mathcomp_extra.v`) - + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE`, `RexpE` + + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE` - new file `internal_Eqdep_dec.v` (don't use, internal, to be removed) @@ -30,6 +30,9 @@ + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp` + lemma `preimage_set_system_id` +- in `Rstruct_topology.v`: + + lemma `RexpE` + ### Changed - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index 1a9452c602..fd55a1d4f3 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -10,11 +10,12 @@ Require Import Rtrigo1 Reals. From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum. From mathcomp Require Import archimedean. From HB Require Import structures. -From mathcomp Require Import mathcomp_extra. -From mathcomp Require Import boolp classical_sets. +From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import reals interval_inference. -From mathcomp Require Import topology. From mathcomp Require Export Rstruct. +From mathcomp Require Import topology. +(* The following line is for RexpE. *) +From mathcomp Require normedtype sequences. Set Implicit Arguments. Unset Strict Implicit. @@ -87,3 +88,24 @@ Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) : Proof. by move=> Lf /continuity_pt_cvg; apply. Qed. End analysis_struct. + +Module RexpE. +Import topology normedtype sequences. + +(* proof by comparing the defining power series *) +Lemma RexpE (x : R) : Rtrigo_def.exp x = expR x. +Proof. +apply/esym; rewrite /exp /exist_exp; case: Alembert_C3 => y. +rewrite /Pser /infinite_sum /= => exp_ub. +rewrite /expR /exp_coeff /series/=; apply: (@cvg_lim R^o) => //. +rewrite -cvg_shiftS /=; apply/cvgrPdist_lt => /= e /RltP /exp_ub[N Nexp_ub]. +near=> n. +have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge. +move: Nexp_ub => /(_ _ nN) /[!RdistE] /RltP /=. +rewrite distrC sum_f_R0E; congr (`| _ - _ | < e). +by apply: eq_bigr=> k _; rewrite RinvE RpowE mulrC factE INRE. +Unshelve. all: by end_near. Qed. + +End RexpE. + +Definition RexpE := RexpE.RexpE. diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index da44a60525..65699ed8cd 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -32,8 +32,6 @@ From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum. From mathcomp Require Import archimedean. From HB Require Import structures. From mathcomp Require Import mathcomp_extra. -(* The following line is for RexpE. *) -From mathcomp Require topology normedtype sequences. Set Implicit Arguments. Unset Strict Implicit. @@ -739,24 +737,3 @@ Qed. End bigmaxr. End ssreal_struct_contd. - -Module RexpE. -Import topology normedtype sequences. - -(* proof by comparing the defining power series *) -Lemma RexpE (x : R) : Rtrigo_def.exp x = expR x. -Proof. -apply/esym; rewrite /exp /exist_exp; case: Alembert_C3 => y. -rewrite /Pser /infinite_sum /= => exp_ub. -rewrite /expR /exp_coeff /series/=; apply: (@cvg_lim R^o) => //. -rewrite -cvg_shiftS /=; apply/cvgrPdist_lt => /= e /RltP /exp_ub[N Nexp_ub]. -near=> n. -have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge. -move: Nexp_ub => /(_ _ nN) /[!RdistE] /RltP /=. -rewrite distrC sum_f_R0E; congr (`| _ - _ | < e). -by apply: eq_bigr=> k _; rewrite RinvE RpowE mulrC factE INRE. -Unshelve. all: by end_near. Qed. - -End RexpE. - -Definition RexpE := RexpE.RexpE. From 6f0a87c670980938293aded65e3fffc61b3f4c28 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 Mar 2025 22:06:48 +0900 Subject: [PATCH 4/4] fix --- analysis_stdlib/Rstruct_topology.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index fd55a1d4f3..fd608d05b8 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -90,7 +90,7 @@ Proof. by move=> Lf /continuity_pt_cvg; apply. Qed. End analysis_struct. Module RexpE. -Import topology normedtype sequences. +Import normedtype sequences. (* proof by comparing the defining power series *) Lemma RexpE (x : R) : Rtrigo_def.exp x = expR x.