Add a RealsE multirule

CHANGELOG_UNRELEASED.md

@@ -9,6 +9,10 @@
 - in set_interval.v
   + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
 
+- in `Rstruct.v`:
+  + lemmas `R0E` and `R1E`
+  + multirule `RealsE` to convert from Stdlib reals to Analysis ones
+
 - in `Rstruct_topology.v`:
   + lemma `RlnE`
 

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.
@@ -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).

reals_stdlib/Rstruct.v

@@ -7,12 +7,12 @@ 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)` *)
+(* end, one can use tactics like `apply: RleP` or `rewrite !RealsE`           *)
 (* (see below for more compatibility lemmas).                                 *)
 (******************************************************************************)
 
@@ -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).
@@ -547,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}.