coq-mathcomp-reals package

.nix/coq-overlays/mathcomp-analysis/default.nix

@@ -0,0 +1,123 @@
+{ lib,
+  mkCoqDerivation,
+  mathcomp, mathcomp-finmap, mathcomp-bigenough,
+  hierarchy-builder,
+  single ? false,
+  coqPackages, coq, version ? null }@args:
+
+let
+  repo  = "analysis";
+  owner = "math-comp";
+
+  release."1.5.0".sha256 = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88=";
+  release."1.4.0".sha256 = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg=";
+  release."1.2.0".sha256 = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo=";
+  release."1.1.0".sha256 = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o=";
+  release."1.0.0".sha256 = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4=";
+  release."0.7.0".sha256 = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60=";
+  release."0.6.7".sha256 = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA=";
+  release."0.6.6".sha256 = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y=";
+  release."0.6.5".sha256 = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E=";
+  release."0.6.1".sha256 = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0=";
+  release."0.6.0".sha256 = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg=";
+  release."0.5.3".sha256 = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k=";
+  release."0.5.2".sha256 = "0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw";
+  release."0.5.1".sha256 = "1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68";
+  release."0.3.13".sha256 = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg=";
+  release."0.3.10".sha256 = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI=";
+  release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4=";
+  release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5";
+  release."0.3.4".sha256 = "18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c";
+  release."0.3.3".sha256 = "1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867";
+  release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
+  release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
+
+  defaultVersion = let inherit (lib.versions) range; in
+    lib.switch [ coq.version mathcomp.version ] [
+      { cases = [ (range "8.19" "8.20") (range "2.1.0" "2.2.0") ];   out = "1.5.0"; }
+      { cases = [ (range "8.17" "8.20") (range "2.0.0" "2.2.0") ];   out = "1.1.0"; }
+      { cases = [ (range "8.17" "8.19") (range "1.17.0" "1.19.0") ]; out = "0.7.0"; }
+      { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.7"; }
+      { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.6"; }
+      { cases = [ (range "8.14" "8.18") (range "1.15.0" "1.17.0") ]; out = "0.6.5"; }
+      { cases = [ (range "8.14" "8.18") (range "1.13.0" "1.16.0") ]; out = "0.6.1"; }
+      { cases = [ (range "8.14" "8.18") (range "1.13" "1.15") ];     out = "0.5.2"; }
+      { cases = [ (range "8.13" "8.15") (range "1.13" "1.14") ];     out = "0.5.1"; }
+      { cases = [ (range "8.13" "8.15") (range "1.12" "1.14") ];     out = "0.3.13"; }
+      { cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ];     out = "0.3.10"; }
+      { cases = [ (range "8.10" "8.12") "1.11.0" ];                  out = "0.3.3"; }
+      { cases = [ (range "8.10" "8.11") "1.11.0" ];                  out = "0.3.1"; }
+      { cases = [ (range "8.8"  "8.11") (range "1.8" "1.10") ];      out = "0.2.3"; }
+    ] null;
+
+  # list of analysis packages sorted by dependency order
+  packages = {
+    "classical" = [];
+    "reals" = [ "classical" ];
+    "altreals" = [ "reals" ];
+    "analysis" = [ "reals" ];
+    "reals-stdlib" = [ "reals" ];
+    "analysis-stdlib" = [ "analysis" "reals-stdlib" ];
+  };
+
+  mathcomp_ = package: let
+      classical-deps = [ mathcomp.algebra mathcomp-finmap ];
+      analysis-deps = [ mathcomp.field mathcomp-bigenough ];
+      intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
+      pkgpath = lib.switch package [
+        { case = "single"; out = "."; }
+        { case = "analysis"; out = "theories"; }
+        { case = "reals-stdlib"; out = "reals_stdlib"; }
+        { case = "analysis-stdlib"; out = "analysis_stdlib"; }
+      ] package;
+      pname = if package == "single" then "mathcomp-analysis-single"
+        else "mathcomp-${package}";
+      derivation = mkCoqDerivation ({
+        inherit version pname defaultVersion release repo owner;
+
+        namePrefix = [ "coq" "mathcomp" ];
+
+        propagatedBuildInputs =
+          intra-deps
+          ++ lib.optionals (lib.elem package [ "classical" "single" ]) classical-deps
+          ++ lib.optionals (lib.elem package [ "analysis" "single" ]) analysis-deps;
+
+        preBuild = ''
+          cd ${pkgpath}
+        '';
+
+        meta = {
+          description = "Analysis library compatible with Mathematical Components";
+          maintainers = [ lib.maintainers.cohencyril ];
+          license     = lib.licenses.cecill-c;
+        };
+
+        passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
+      });
+    # split packages didn't exist before 0.6, so bulding nothing in that case
+    patched-derivation1 = derivation.overrideAttrs (o:
+      lib.optionalAttrs (o.pname != null && o.pname != "mathcomp-analysis" &&
+         o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version)
+      { preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; }
+    );
+    patched-derivation2 = patched-derivation1.overrideAttrs (o:
+      lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" &&
+         o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version)
+      { preBuild = ""; }
+    );
+    # only packages classical and analysis existed before 1.7, so bulding nothing in that case
+    patched-derivation3 = patched-derivation2.overrideAttrs (o:
+      lib.optionalAttrs (o.pname != null && o.pname != "mathcomp-classical" && o.pname != "mathcomp-analysis" &&
+         o.version != null && o.version != "dev" && lib.versions.isLt "1.7" o.version)
+      { preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; }
+    );
+    patched-derivation = patched-derivation3.overrideAttrs (o:
+      lib.optionalAttrs (o.version != null
+        && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version))
+      {
+        propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
+      }
+    );
+    in patched-derivation;
+in
+mathcomp_ (if single then "single" else "analysis")

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,39 @@
 
 ### Added
 
+- file `Rstruct_topology.v`
+
+- package `coq-mathcomp-reals` depending on `coq-mathcomp-classical`
+  with files
+  + `constructive_ereal.v`
+  + `reals.v`
+  + `real_interval.v`
+  + `signed.v`
+  + `itv.v`
+  + `prodnormedzmodule.v`
+  + `nsatz_realtype.v`
+  + `all_reals.v`
+
+- in file `separation_axioms.v`,
+  + new lemmas `compact_normal_local`, and `compact_normal`.
+
+- package `coq-mathcomp-altreals` depending on `coq-mathcomp-reals`
+  with files
+  + `xfinmap.v`
+  + `discrete.v`
+  + `realseq.v`
+  + `realsum.v`
+  + `distr.v`
+
+- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals`
+  with file
+  + `Rstruct.v`
+
+- package `coq-mathcomp-analysis-stdlib` depending on
+  `coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files
+  + `Rstruct_topology.v`
+  + `showcase/uniform_bigO.v`
+
 - in file `separation_axioms.v`,
   + new lemmas `compact_normal_local`, and `compact_normal`.
 
@@ -31,6 +64,16 @@
      which removes the dependency on `R`.  The old formulation can be
      recovered easily with `uniform_separatorP`.
 
+- moved from `Rstruct.v` to `Rstruct_topology.v`
+  + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`,
+    `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs`
+    and `nbhs_pt_comp`
+
+- moved from `real_interval.v` to `normedtype.v`
+  + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`,
+    `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`,
+    `disj_itv_Rhull`
+
 ### Renamed
 
 ### Generalized

_CoqProject

@@ -1,5 +1,9 @@
 -Q classical mathcomp.classical
+-Q reals mathcomp.reals
+-Q reals_stdlib mathcomp.reals_stdlib
+-Q altreals mathcomp.altreals
 -Q theories mathcomp.analysis
+-Q analysis_stdlib mathcomp.analysis_stdlib
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope
@@ -20,11 +24,22 @@ classical/fsbigop.v
 classical/set_interval.v
 classical/classical_orders.v
 classical/filter.v
+reals/constructive_ereal.v
+reals/reals.v
+reals/real_interval.v
+reals/signed.v
+reals/itv.v
+reals/prodnormedzmodule.v
+reals/nsatz_realtype.v
+reals/all_reals.v
+altreals/xfinmap.v
+altreals/discrete.v
+altreals/realseq.v
+altreals/realsum.v
+altreals/distr.v
+reals_stdlib/Rstruct.v
 theories/all_analysis.v
-theories/constructive_ereal.v
-theories/reals.v
 theories/landau.v
-theories/Rstruct.v
 
 theories/topology_theory/topology.v
 theories/topology_theory/bool_topology.v
@@ -48,15 +63,12 @@ theories/separation_axioms.v
 theories/function_spaces.v
 theories/ereal.v
 theories/cantor.v
-theories/prodnormedzmodule.v
 theories/normedtype.v
 theories/realfun.v
 theories/sequences.v
 theories/exp.v
 theories/trigo.v
-theories/nsatz_realtype.v
 theories/esum.v
-theories/real_interval.v
 theories/lebesgue_measure.v
 theories/lebesgue_stieltjes_measure.v
 theories/forms.v
@@ -67,15 +79,9 @@ theories/lebesgue_integral.v
 theories/ftc.v
 theories/hoelder.v
 theories/probability.v
-theories/signed.v
-theories/itv.v
 theories/convex.v
 theories/charge.v
 theories/kernel.v
-theories/showcase/uniform_bigO.v
 theories/showcase/summability.v
-theories/altreals/xfinmap.v
-theories/altreals/discrete.v
-theories/altreals/realseq.v
-theories/altreals/realsum.v
-theories/altreals/distr.v
+analysis_stdlib/Rstruct_topology.v
+analysis_stdlib/showcase/uniform_bigO.v

altreals/Make

@@ -0,0 +1,14 @@
+-Q . mathcomp.altreals
+
+-arg -w -arg -parsing
+-arg -w -arg +undeclared-scope
+-arg -w -arg +non-primitive-record
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
+
+xfinmap.v
+discrete.v
+realseq.v
+realsum.v
+distr.v

altreals/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common

analysis_stdlib/Make

@@ -0,0 +1,11 @@
+-Q . mathcomp.analysis_stdlib
+
+-arg -w -arg -parsing
+-arg -w -arg +undeclared-scope
+-arg -w -arg +non-primitive-record
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
+
+Rstruct_topology.v
+showcase/uniform_bigO.v

analysis_stdlib/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common

analysis_stdlib/Rstruct_topology.v

@@ -0,0 +1,89 @@
+(**md**************************************************************************)
+(* # Compatibility with the real numbers of Coq                               *)
+(*                                                                            *)
+(* Lemmas about continuity                                                    *)
+(******************************************************************************)
+
+Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
+Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
+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 reals signed.
+From mathcomp Require Import topology.
+From mathcomp Require Export Rstruct.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Import Order.TTheory GRing.Theory Num.Theory.
+
+Local Open Scope R_scope.
+Local Open Scope ring_scope.
+
+Section analysis_struct.
+
+HB.instance Definition _ := PseudoMetric.copy R R^o.
+HB.instance Definition _ := Pointed.copy R R^o.
+
+(* TODO: express using ball?*)
+Lemma continuity_pt_nbhs (f : R -> R) x :
+  continuity_pt f x <->
+  forall eps : {posnum R}, nbhs x (fun u => `|f u - f x| < eps%:num).
+Proof.
+split=> [fcont e|fcont _/RltP/posnumP[e]]; last first.
+  have [_/posnumP[d] xd_fxe] := fcont e.
+  exists d%:num; split; first by apply/RltP; have := [gt0 of d%:num].
+  by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /= distrC.
+have /RltP egt0 := [gt0 of e%:num].
+have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0.
+exists d%:num => //= y xyd; case: (eqVneq x y) => [->|xney].
+  by rewrite subrr normr0.
+apply/RltP/dx_fxe; split; first by split=> //; apply/eqP.
+by have /RltP := xyd; rewrite distrC.
+Qed.
+
+Lemma continuity_pt_cvg (f : R -> R) (x : R) :
+  continuity_pt f x <-> {for x, continuous f}.
+Proof.
+eapply iff_trans; first exact: continuity_pt_nbhs.
+apply iff_sym.
+have FF : Filter (f @ x)%classic.
+  by typeclasses eauto.
+  (*by apply fmap_filter; apply: @filter_filter' (locally_filter _).*)
+case: (@fcvg_ballP _ _ (f @ x)%classic FF (f x)) => {FF}H1 H2.
+(* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *)
+split => [{H2} - /H1 {}H1 eps|{H1} H].
+- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num.
+  exists x0%:num => //= Hx0' /Hx0 /=.
+  by rewrite /= distrC; apply.
+- apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0].
+  exists x0%:num => //= y /Hx0 /= {}Hx0.
+  by rewrite /ball /= distrC.
+Qed.
+
+Lemma continuity_ptE (f : R -> R) (x : R) :
+  continuity_pt f x <-> {for x, continuous f}.
+Proof. exact: continuity_pt_cvg. Qed.
+
+Local Open Scope classical_set_scope.
+
+Lemma continuity_pt_cvg' f x :
+  continuity_pt f x <-> f @ x^' --> f x.
+Proof. by rewrite continuity_ptE continuous_withinNx. Qed.
+
+Lemma continuity_pt_dnbhs f x :
+  continuity_pt f x <->
+  forall eps, 0 < eps -> x^' (fun u => `|f x - f u| < eps).
+Proof.
+by rewrite continuity_pt_cvg' -filter_fromP cvg_ballP -filter_fromP.
+Qed.
+
+Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) :
+  nbhs (f x) P -> continuity_pt f x -> \near x, P (f x).
+Proof. by move=> Lf /continuity_pt_cvg; apply. Qed.
+
+End analysis_struct.

theories/showcase/uniform_bigO.v → analysis_stdlib/showcase/uniform_bigO.v

@@ -2,7 +2,7 @@
 From Coq Require Import Reals.
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum.
-From mathcomp Require Import boolp reals Rstruct ereal.
+From mathcomp Require Import boolp reals Rstruct_topology ereal.
 From mathcomp Require Import classical_sets signed topology normedtype landau.
 
 Set Implicit Arguments.