From 3150019069826e29948aa3122c33abebea734110 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 20 Jan 2026 15:56:29 +0100 Subject: [PATCH 1/4] Document Rstruct.v --- reals_stdlib/Rstruct.v | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index ec34553cf..7fda64acc 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -1,3 +1,21 @@ +(* see below (after doc) for copyright notice *) +From Coq Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf. +From Coq Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. +From Coq Require Import Rtrigo1 Reals. +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg poly ssrnum archimedean. + + +(**md**************************************************************************) +(* # Compatibility with the real numbers of Coq *) +(* *) +(* This essentially builds an instance of realType for the R type from the *) +(* Stdlib library. This enable to specialize all proofs on realType (that is *) +(* many thing in the Analysis library) to the real numbers of Stdlib. To this *) +(* end, one can use tactics like `apply: RleP` or `rewrite !(RplusE, RmultE)` *) +(* (see below for more compatibility lemmas). *) +(******************************************************************************) + (* This file is a modification of an eponymous file from the CoqApprox *) (* library. The header of the original file is reproduced below. Changes are *) (* part of the analysis library and enjoy the same licence as this library. *) @@ -21,16 +39,6 @@ the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details. *) -(**md**************************************************************************) -(* # Compatibility with the real numbers of Coq *) -(******************************************************************************) - -From Coq Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf. -From Coq Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. -From Coq Require Import Rtrigo1 Reals. -From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg poly ssrnum archimedean. - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. From 11af4acc77a17b0e52ebbaddaee065bd88571109 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 6 Feb 2026 03:44:59 +0900 Subject: [PATCH 2/4] Apply suggestion from @affeldt-aist --- reals_stdlib/Rstruct.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index 7fda64acc..059499769 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -7,7 +7,7 @@ From mathcomp Require Import all_ssreflect ssralg poly ssrnum archimedean. (**md**************************************************************************) -(* # Compatibility with the real numbers of Coq *) +(* # Compatibility with the real numbers of Rocq *) (* *) (* This essentially builds an instance of realType for the R type from the *) (* Stdlib library. This enable to specialize all proofs on realType (that is *) From 70e83519535cd1bc069a62840c88a9f6d60ea73e Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 6 Feb 2026 03:45:07 +0900 Subject: [PATCH 3/4] Apply suggestion from @affeldt-aist --- reals_stdlib/Rstruct.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index 059499769..4167bd327 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -11,7 +11,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 enable to specialize all proofs on realType (that is *) -(* many thing in the Analysis library) to the real numbers of Stdlib. To this *) +(* 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 c6153dbe76d81897d01f93a0be8d6ee9de23ce7b Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 6 Feb 2026 03:45:45 +0900 Subject: [PATCH 4/4] Apply suggestion from @affeldt-aist --- reals_stdlib/Rstruct.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index 4167bd327..5cced6024 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -10,7 +10,7 @@ From mathcomp Require Import all_ssreflect ssralg poly ssrnum archimedean. (* # Compatibility with the real numbers of Rocq *) (* *) (* This essentially builds an instance of realType for the R type from the *) -(* Stdlib library. This enable to specialize 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). *)