changelog, meta

- add inheritance diagram to readme

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)

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)

theories/derive.v

@@ -25,7 +25,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
-Import nonforgetful_inheritance.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope ring_scope.
 Local Open Scope classical_set_scope.

theories/ereal.v

@@ -58,7 +58,7 @@ Unset Printing Implicit Defensive.
 Declare Scope ereal_scope.
 
 Import Order.TTheory GRing.Theory Num.Theory.
-Import nonforgetful_inheritance.Exports.
+Import numFieldTopology.Exports.
 
 Local Open Scope ring_scope.
 

theories/normedtype.v

@@ -84,7 +84,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import nonforgetful_inheritance.Exports.
+Import numFieldTopology.Exports.
 
 Local Open Scope ring_scope.
 Local Open Scope classical_set_scope.
@@ -706,7 +706,7 @@ End Exports.
 End regular_topology.
 Export regular_topology.Exports.
 
-Module nonforgetful_inheritance.
+Module numFieldNormedType.
 
 Section realType.
 Variable (R : realType).
@@ -1038,7 +1038,7 @@ Definition normedMod_numDomainType := [numDomainType of numField_normedModType].
 End numFieldType.
 
 Module Exports.
-Export topology.nonforgetful_inheritance.Exports.
+Export topology.numFieldTopology.Exports.
 (* realType *)
 Canonical real_lmodType.
 Canonical real_lalgType.
@@ -1349,8 +1349,8 @@ Coercion numField_pseudoMetricNormedZmodType :
 Coercion numField_normedModType : numFieldType >-> normedModType.
 End Exports.
 
-End nonforgetful_inheritance.
-Import nonforgetful_inheritance.Exports.
+End numFieldNormedType.
+Import numFieldNormedType.Exports.
 
 Section NormedModule_numDomainType.
 Variables (R : numDomainType) (V : normedModType R).

theories/sequences.v

@@ -48,7 +48,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def  Num.Theory.
-Import nonforgetful_inheritance.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.

theories/topology.v

@@ -4358,7 +4358,7 @@ End Exports.
 End regular_topology.
 Export regular_topology.Exports.
 
-Module nonforgetful_inheritance.
+Module numFieldTopology.
 
 Section realType.
 Variable (R : realType).
@@ -4680,8 +4680,8 @@ Coercion numField_uniformType : numFieldType >-> uniformType.
 Coercion numField_pseudoMetricType : numFieldType >-> pseudoMetricType.
 End Exports.
 
-End nonforgetful_inheritance.
-Import nonforgetful_inheritance.Exports.
+End numFieldTopology.
+Import numFieldTopology.Exports.
 
 Global Instance Proper_nbhs'_regular_numFieldType (R : numFieldType) (x : R^o) :
   ProperFilter (nbhs' x).