From 205c469135d38ae06404cd6986ec6de4dc7ca355 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 30 May 2024 12:51:44 +0900 Subject: [PATCH 1/5] strengthen RinvE and RdivE; add Pos_to_natE and IZposRE --- classical/mathcomp_extra.v | 9 +++++++++ theories/Rstruct.v | 19 ++++++++++++++++--- 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index bbec2949a..be5e2bc05 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -364,3 +364,12 @@ rewrite /Order.min/=; case: ifPn => xz; case: ifPn => yz; rewrite ?ltxx//. Qed. End order_min. + +Section positive. +Lemma Pos_to_natE p : Pos.to_nat p = nat_of_pos p. +Proof. +by elim: p => //= p <-; rewrite ?Pnat.Pos2Nat.inj_xI ?Pnat.Pos2Nat.inj_xO; + change (2 * Pos.to_nat p)%coq_nat with (2 * Pos.to_nat p)%nat; + rewrite mul2n NatTrec.doubleE. +Qed. +End positive. diff --git a/theories/Rstruct.v b/theories/Rstruct.v index 0ab9e873d..96e3c75bd 100644 --- a/theories/Rstruct.v +++ b/theories/Rstruct.v @@ -30,6 +30,7 @@ Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. Require Import Rtrigo1 Reals. From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum. From HB Require Import structures. +Require Import mathcomp_extra. Set Implicit Arguments. Unset Strict Implicit. @@ -456,11 +457,23 @@ Lemma RmultE x y : Rmult x y = x * y. Proof. by []. Qed. Lemma RoppE x : Ropp x = - x. Proof. by []. Qed. -Lemma RinvE x : x != 0 -> Rinv x = x^-1. +Let neq0_RinvE x : x != 0 -> Rinv x = x^-1. Proof. by move=> x_neq0; rewrite -[RHS]/(if _ then _ else _) x_neq0. Qed. -Lemma RdivE x y : y != 0 -> Rdiv x y = x / y. -Proof. by move=> y_neq0; rewrite /Rdiv RinvE. Qed. +Lemma RinvE (x : R) : Rinv x = x^-1. +Proof. +have [-> | ] := eqVneq x R0; last exact: neq0_RinvE. +rewrite /GRing.inv /GRing.mul /= /Rinvx eqxx /=. +rewrite RinvImpl.Rinv_def. +case: (Req_appart_dec 0 R0) => //. +by move=> /[dup] -[] => /RltP; rewrite Order.POrderTheory.ltxx. +Qed. + +Lemma RdivE (x y : R) : Rdiv x y = x / y. +Proof. by rewrite /Rdiv RinvE. Qed. + +Lemma IZposRE (p : positive) : IZR (Z.pos p) = INR (nat_of_pos p). +Proof. by rewrite -Pos_to_natE INR_IPR. Qed. Lemma INRE n : INR n = n%:R. Proof. elim: n => // n IH; by rewrite S_INR IH RplusE -addn1 natrD. Qed. From 9161ad935a6f5652db94eca5545840313aad2e07 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 30 May 2024 12:59:02 +0900 Subject: [PATCH 2/5] doc --- CHANGELOG_UNRELEASED.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f7e702087..3e5f08242 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,6 +4,12 @@ ### Added +- in `mathcomp_extra.v`: + + lemma `Pos_to_natE` + +- in `Rstruct.v`: + + lemma `IZposRE` + - in `classical_sets.v`: + lemma `bigcup_recl` @@ -136,6 +142,9 @@ ### Generalized +- in `Rstruct.v`: + + lemmas `RinvE`, `RdivE` + - in `constructive_ereal.v`: + `gee_pMl` (was `gee_pmull`) From 5c392d4caa2ea98eda0522eaab0e065e04c25f66 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 31 May 2024 07:57:12 +0900 Subject: [PATCH 3/5] review --- CHANGELOG_UNRELEASED.md | 12 ++++++------ theories/Rstruct.v | 22 ++++++++++++---------- 2 files changed, 18 insertions(+), 16 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3e5f08242..537c37008 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,12 +4,6 @@ ### Added -- in `mathcomp_extra.v`: - + lemma `Pos_to_natE` - -- in `Rstruct.v`: - + lemma `IZposRE` - - in `classical_sets.v`: + lemma `bigcup_recl` @@ -74,6 +68,12 @@ - in `measure.v`: + lemma `measurableID` +- in `mathcomp_extra.v`: + + lemma `Pos_to_natE` + +- in `Rstruct.v`: + + lemma `IZRposE` + ### Changed - in `forms.v`: diff --git a/theories/Rstruct.v b/theories/Rstruct.v index 96e3c75bd..59fdf179b 100644 --- a/theories/Rstruct.v +++ b/theories/Rstruct.v @@ -460,24 +460,26 @@ Lemma RoppE x : Ropp x = - x. Proof. by []. Qed. Let neq0_RinvE x : x != 0 -> Rinv x = x^-1. Proof. by move=> x_neq0; rewrite -[RHS]/(if _ then _ else _) x_neq0. Qed. -Lemma RinvE (x : R) : Rinv x = x^-1. +Lemma RinvE x : Rinv x = x^-1. Proof. -have [-> | ] := eqVneq x R0; last exact: neq0_RinvE. +have [->| ] := eqVneq x R0; last exact: neq0_RinvE. rewrite /GRing.inv /GRing.mul /= /Rinvx eqxx /=. -rewrite RinvImpl.Rinv_def. -case: (Req_appart_dec 0 R0) => //. -by move=> /[dup] -[] => /RltP; rewrite Order.POrderTheory.ltxx. +rewrite RinvImpl.Rinv_def; case: Req_appart_dec => //. +by move=> /[dup] -[] /RltP; rewrite Order.POrderTheory.ltxx. Qed. -Lemma RdivE (x y : R) : Rdiv x y = x / y. -Proof. by rewrite /Rdiv RinvE. Qed. - -Lemma IZposRE (p : positive) : IZR (Z.pos p) = INR (nat_of_pos p). -Proof. by rewrite -Pos_to_natE INR_IPR. Qed. +Lemma RdivE x y : Rdiv x y = x / y. Proof. by rewrite /Rdiv RinvE. Qed. Lemma INRE n : INR n = n%:R. Proof. elim: n => // n IH; by rewrite S_INR IH RplusE -addn1 natrD. Qed. +(**md Though not strictly about the type of real numbers from the Coq + standard library, the following lemma `IZRposE` is often needed in + practice as its left-hand side often appears as a result of other + rewritings using `R*E` lemmas. *) +Lemma IZRposE (p : positive) : IZR (Z.pos p) = INR (nat_of_pos p). +Proof. by rewrite -Pos_to_natE INR_IPR. Qed. + Lemma RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x. Proof. move => x0; apply/eqP; have [t1 t2] := conj (sqrtr_ge0 x) (sqrt_pos x). From dbcb64c99552f22e92e183efad5d01aa8a622c87 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 31 May 2024 08:03:08 +0900 Subject: [PATCH 4/5] fix --- classical/mathcomp_extra.v | 7 ++++--- theories/Rstruct.v | 10 ++++------ 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index be5e2bc05..0e82043f4 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -366,10 +366,11 @@ Qed. End order_min. Section positive. + Lemma Pos_to_natE p : Pos.to_nat p = nat_of_pos p. Proof. -by elim: p => //= p <-; rewrite ?Pnat.Pos2Nat.inj_xI ?Pnat.Pos2Nat.inj_xO; - change (2 * Pos.to_nat p)%coq_nat with (2 * Pos.to_nat p)%nat; - rewrite mul2n NatTrec.doubleE. +by elim: p => //= p <-; + rewrite ?(Pnat.Pos2Nat.inj_xI,Pnat.Pos2Nat.inj_xO) NatTrec.doubleE -mul2n. Qed. + End positive. diff --git a/theories/Rstruct.v b/theories/Rstruct.v index 59fdf179b..33780781a 100644 --- a/theories/Rstruct.v +++ b/theories/Rstruct.v @@ -473,18 +473,16 @@ Lemma RdivE x y : Rdiv x y = x / y. Proof. by rewrite /Rdiv RinvE. Qed. Lemma INRE n : INR n = n%:R. Proof. elim: n => // n IH; by rewrite S_INR IH RplusE -addn1 natrD. Qed. -(**md Though not strictly about the type of real numbers from the Coq - standard library, the following lemma `IZRposE` is often needed in - practice as its left-hand side often appears as a result of other - rewritings using `R*E` lemmas. *) +(**md Note that rewrites using the following lemma `IZRposE` are + systematically followed by a rewrite using the lemma `INRE`. *) Lemma IZRposE (p : positive) : IZR (Z.pos p) = INR (nat_of_pos p). Proof. by rewrite -Pos_to_natE INR_IPR. Qed. Lemma RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x. Proof. move => x0; apply/eqP; have [t1 t2] := conj (sqrtr_ge0 x) (sqrt_pos x). -rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; last by apply /RleP. -rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; by apply/RleP. +rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; last exact/RleP. +by rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; exact/RleP. Qed. Lemma RpowE x n : pow x n = x ^+ n. From 7f24c49f53f3efc324c80b558c6874bfda0c5d74 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 31 May 2024 09:35:22 +0900 Subject: [PATCH 5/5] fix for the CI --- theories/Rstruct.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Rstruct.v b/theories/Rstruct.v index 33780781a..50a515281 100644 --- a/theories/Rstruct.v +++ b/theories/Rstruct.v @@ -30,7 +30,7 @@ Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. Require Import Rtrigo1 Reals. From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum. From HB Require Import structures. -Require Import mathcomp_extra. +From mathcomp Require Import mathcomp_extra. Set Implicit Arguments. Unset Strict Implicit.