From ccdc20fd80ffc985d1f6309e6cb0b22eb3c48a31 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 6 Feb 2026 07:56:56 +0100 Subject: [PATCH 1/3] Minor doc improvements --- analysis_stdlib/Rstruct_topology.v | 4 ++-- reals_stdlib/Rstruct.v | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index 47ddf19f8..a414d07f1 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -1,7 +1,7 @@ (**md**************************************************************************) -(* # Compatibility with the real numbers of Coq *) +(* # Compatibility with the real numbers of Stdlib *) (* *) -(* Lemmas about continuity *) +(* Extension to Rstruct.v (lemmas about continuity) *) (******************************************************************************) Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf. diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index 5cced6024..df6cbff97 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -7,10 +7,10 @@ From mathcomp Require Import all_ssreflect ssralg poly ssrnum archimedean. (**md**************************************************************************) -(* # Compatibility with the real numbers of Rocq *) +(* # Compatibility with the real numbers of Stdlib *) (* *) (* This essentially builds an instance of realType for the R type from the *) -(* Stdlib library. This enables specializing all proofs on realType (that is *) +(* Stdlib library. This enables specializing all proofs on realType (that is, *) (* many things in the Analysis library) to Stdlib's real numbers. To this *) (* end, one can use tactics like `apply: RleP` or `rewrite !(RplusE, RmultE)` *) (* (see below for more compatibility lemmas). *) From 01f4c8c719b1836294703e98e1171196f8504007 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 5 Feb 2026 16:53:06 +0100 Subject: [PATCH 2/3] Add lemmas R0E and R1E Backported from infotheo: https://github.com/affeldt-aist/infotheo/blob/master/lib/coqRE.v Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 3 +++ reals_stdlib/Rstruct.v | 3 +++ 2 files changed, 6 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b7fcc4b73..4ce8e74bc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -9,6 +9,9 @@ - in set_interval.v + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends` +- in `Rstruct.v`: + + lemmas `R0E` and `R1E` + - in `Rstruct_topology.v`: + lemma `RlnE` diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index df6cbff97..33885e0fd 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -491,6 +491,9 @@ by elim: p => //= p <-; rewrite ?(Pnat.Pos2Nat.inj_xI,Pnat.Pos2Nat.inj_xO) NatTrec.doubleE -mul2n. Qed. +Lemma R0E : IZR 0 = 0%R. Proof. by []. Qed. +Lemma R1E : IZR 1 = 1%R. Proof. by []. Qed. + (**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). From 50667e7a0ea04a7ce9dce6c91fece52cf9e7772f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 4 Feb 2026 13:55:22 +0100 Subject: [PATCH 3/3] Add a RealsE multirule --- CHANGELOG_UNRELEASED.md | 1 + analysis_stdlib/Rstruct_topology.v | 3 +++ reals_stdlib/Rstruct.v | 6 +++++- 3 files changed, 9 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4ce8e74bc..71715142d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -11,6 +11,7 @@ - in `Rstruct.v`: + lemmas `R0E` and `R1E` + + multirule `RealsE` to convert from Stdlib reals to Analysis ones - in `Rstruct_topology.v`: + lemma `RlnE` diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index a414d07f1..850645998 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -118,3 +118,6 @@ have [xle0|xgt0] := leP x 0. 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). diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index 33885e0fd..eff6041d5 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -12,7 +12,7 @@ From mathcomp Require Import all_ssreflect ssralg poly ssrnum archimedean. (* This essentially builds an instance of realType for the R type from the *) (* Stdlib library. This enables specializing all proofs on realType (that is, *) (* many things in the Analysis library) to Stdlib's real numbers. To this *) -(* end, one can use tactics like `apply: RleP` or `rewrite !(RplusE, RmultE)` *) +(* end, one can use tactics like `apply: RleP` or `rewrite !RealsE` *) (* (see below for more compatibility lemmas). *) (******************************************************************************) @@ -550,6 +550,10 @@ Qed. Lemma factE n : fact n = n`!. Proof. by elim: n => //= n ih; rewrite factS mulSn ih. Qed. +Definition RealsE := (RplusE, RminusE, RmultE, RoppE, RinvE, RdivE, + INRE, R0E, R1E, Pos_to_natE, IZRposE, RsqrtE, RpowE, RmaxE, RminE, + RabsE, RdistE, sum_f_R0E, factE). + Section bigmaxr. Context {R : realDomainType}.