Topological structures on numfields

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,27 @@
 
 ### Added
 
+- in `topology.v`:
+  + global instance `ball_filter`
+  + module `regular_topology` with an `Exports` submodule
+    * canonicals `pointedType`, `filteredType`, `topologicalType`,
+      `uniformType`, `pseudoMetricType`
+  + module `numFieldTopology` with an `Exports` submodule
+    * many canonicals and coercions
+  + global instance `Proper_nbhs'_regular_numFieldType`
+- in `normedtype.v`:
+  + definitions `ball_`, `pointed_of_zmodule`, `filtered_of_normedZmod`
+  + lemmas `ball_norm_center`, `ball_norm_symmetric`, `ball_norm_triangle`
+  + definition `pseudoMetric_of_normedDomain`
+  + lemma `nbhs_ball_normE`
+  + global instances `Proper_nbhs'_numFieldType`, `Proper_nbhs'_realType`
+  + module `regular_topology` with an `Exports` submodule
+    * canonicals `pseudoMetricNormedZmodType`, `normedModType`.
+  + module `numFieldNormedType` with an `Exports` submodule
+    * many canonicals and coercions
+    * exports `Export numFieldTopology.Exports`
+  + canonical `R_regular_completeType`, `R_regular_CompleteNormedModule`
+
 ### Changed
 
 - in `ereal.v`:
@@ -15,10 +36,32 @@
   + generalize lemma `bigUB_of`
   + generalize theorem `Boole_inequality`
 
+- canonicals and coercions have been changed so that there is not need
+  anymore for explicit types casts to `R^o`, `[filteredType R^o of R^o]`,
+  `[filteredType R^o * R^o of R^o * R^o]`, `[lmodType R of R^o]`,
+  `[normedModType R of R^o]`,`[topologicalType of R^o]`, `[pseudoMetricType R of R^o]`
+
+- `topology.v` now imports `reals`
+- `normedtype.v` now imports `vector`, `fieldext, `falgebra`,
+  `numFieldTopology.Exports`
+- `derive.v` now imports `numFieldNormedType.Exports`
+- `sequences.v` now imports `numFieldNormedType.Exports`
+
 ### Renamed
 
 ### Removed
 
+- in `topology.v`:
+  + section `numFieldType_canonical`
+- in `normedtype.v`:
+  + lemma `R_ball`
+  + definition `numFieldType_pseudoMetricNormedZmodMixin`
+  + canonical `numFieldType_pseudoMetricNormedZmodType`
+  + global instance `Proper_nbhs'_realType`
+  + lemma `R_normZ`
+  + definition `numFieldType_NormedModMixin`
+  + canonical `numFieldType_normedModType`
+
 ### Infrastructure
 
 ### Misc

README.md

@@ -78,6 +78,14 @@ Each file is documented in its header.
 Changes are documented in [CHANGELOG.md](CHANGELOG.md) and
 [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md).
 
+MathComp-Analysis adds mathematical structures on top of MathComp's ones.
+The following inheritance diagram displays the resulting hiearchy
+(excluding `countalg` and `finalg` structures). MathComp-Analysis
+mathematical structures are on the right, below `pointedType`
+included.
+
+![Inheritance diagram](./hierarchy.png "Inheritance diagram")
+
 Overview presentation: [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)
 
 Other work using MathComp-Analysis: [A Formal Classical Proof of Hahn-Banach in Coq](https://lipn.univ-paris13.fr/~kerjean/slides/slidesTYPES19.pdf) (2019)

default.nix

@@ -46,7 +46,7 @@ let
                   mathcomp-analysis = {version, coqPackages} @ args:
                     let mca = mec.initial.mathcomp-analysis args; in
                     mca // (
-                      if elem version [ "master" "cauchy_etoile" "holomorphy" ]
+                      if elem version [ "master" "cauchy_etoile" "holomorphy" "numfield_topology" ]
                       then {
                         propagatedBuildInputs = mca.propagatedBuildInputs ++
                                                 [ coqPackages.mathcomp-real-closed coqPackages.hierarchy-builder ];

meta.yml

@@ -50,13 +50,11 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-dev'
-  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.11'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.12'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-dev'
+- version: 'coq-8.13'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
@@ -127,6 +125,14 @@ documentation: |-
   Changes are documented in [CHANGELOG.md](CHANGELOG.md) and
   [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md).
 
+  MathComp-Analysis adds mathematical structures on top of MathComp's ones.
+  The following inheritance diagram displays the resulting hiearchy
+  (excluding `countalg` and `finalg` structures). MathComp-Analysis
+  mathematical structures are on the right, below `pointedType`
+  included.
+
+  ![Inheritance diagram](./hierarchy.png "Inheritance diagram")
+
   Overview presentation: [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)
 
   Other work using MathComp-Analysis: [A Formal Classical Proof of Hahn-Banach in Coq](https://lipn.univ-paris13.fr/~kerjean/slides/slidesTYPES19.pdf) (2019)