diff --git a/CHANGELOG.md b/CHANGELOG.md index a47b58ba8..3ac6cb1aa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,107 @@ # Changelog -Last releases: [[0.3.6] - 2021-03-04](#036---2021-03-04) and [[0.3.5] - 2020-12-21](#035---2020-12-21) +Last releases: [[0.3.7] - 2021-04-01](#037---2021-04-01) and [[0.3.6] - 2021-03-04](#036---2021-03-04) + +## [0.3.7] - 2021-04-01 + +### 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` + + definition `dense` and lemma `denseNE` +- 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` +- in `reals.v`: + + lemmas `Rfloor_lt0`, `floor_lt0`, `ler_floor`, `ceil_gt0`, `ler_ceil` + + lemmas `has_sup1`, `has_inf1` +- in `ereal.v`: + + lemmas `ereal_ballN`, `le_ereal_ball`, `ereal_ball_ninfty_oversize`, + `contract_ereal_ball_pinfty`, `expand_ereal_ball_pinfty`, + `contract_ereal_ball_fin_le`, `contract_ereal_ball_fin_lt`, + `expand_ereal_ball_fin_lt`, `ball_ereal_ball_fin_lt`, `ball_ereal_ball_fin_le`, + `sumERFin`, `ereal_inf1`, `eqe_oppP`, `eqe_oppLRP`, `oppe_subset`, + `ereal_inf_pinfty` + + definition `er_map` + + definition `er_map` + + lemmas `adde_undefC`, `real_of_erD`, `fin_num_add_undef`, `addeK`, + `subeK`, `subee`, `sube_le0`, `lee_sub` + + lemmas `addeACA`, `muleC`, `mule1`, `mul1e`, `abseN` + + enable notation `x \is a fin_num` + * definition `fin_num`, fact `fin_num_key`, lemmas `fin_numE`, `fin_numP` +- in `classical_sets.v`: + + notation `[disjoint ... & ..]` + + lemmas `mkset_nil`, `bigcup_mkset`, `bigcup_nonempty`, `bigcup0`, `bigcup0P`, + `subset_bigcup_r`, `eqbigcup_r`, `eq_set_inl`, `set_in_in` +- in `nngnum.v`: + + instance `invr_nngnum` +- in `posnum.v`: + + instance `posnum_nngnum` + +## Changed + +- in `ereal.v`: + + generalize lemma `lee_sum_nneg_subfset` + + lemmas `nbhs_oo_up_e1`, `nbhs_oo_down_e1`, `nbhs_oo_up_1e`, `nbhs_oo_down_1e` + `nbhs_fin_out_above`, `nbhs_fin_out_below`, `nbhs_fin_out_above_below` + `nbhs_fin_inbound` +- in `sequences.v`: + + generalize lemmas `ereal_nondecreasing_series`, `is_cvg_ereal_nneg_series`, + `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty` +- in `measure.v`: + + generalize lemma `bigUB_of` + + generalize theorem `Boole_inequality` +- in `classical_sets.v`: + + change the order of arguments of `subset_trans` + +- 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]` +- `sequences.v` now imports `numFieldNormedType.Exports` +- `topology.v` now imports `reals` +- `normedtype.v` now imports `vector`, `fieldext`, `falgebra`, + `numFieldTopology.Exports` +- `derive.v` now imports `numFieldNormedType.Exports` + +### Renamed + +- in `ereal.v`: + + `is_realN` -> `fin_numN` + + `is_realD` -> `fin_numD` + + `ereal_sup_set0` -> `ereal_sup0` + + `ereal_sup_set1` -> `ereal_sup1` + + `ereal_inf_set0` -> `ereal_inf0` + +### 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` +- in `ereal.v`: + + definition `is_real` ## [0.3.6] - 2021-03-04 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0d3888481..5a426cd4b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,107 +4,12 @@ ### 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` -- in `reals.v`: - + lemmas `Rfloor_lt0`, `floor_lt0`, `ler_floor`, `ceil_gt0`, `ler_ceil` -- in `ereal.v`: - + lemmas `ereal_ballN`, `le_ereal_ball`, `ereal_ball_ninfty_oversize`, - `contract_ereal_ball_pinfty`, `expand_ereal_ball_pinfty`, - `contract_ereal_ball_fin_le`, `contract_ereal_ball_fin_lt`, - `expand_ereal_ball_fin_lt`, `ball_ereal_ball_fin_lt`, `ball_ereal_ball_fin_le`, - `sumERFin`, `ereal_inf1`, `eqe_oppP`, `eqe_oppLRP`, `oppe_subset`, - `ereal_inf_pinfty` - + definition `er_map` - + definition `er_map` -- in `classical_sets.v`: - + notation `[disjoint ... & ..]` - + lemmas `mkset_nil`, `bigcup_mkset`, `bigcup_nonempty`, `bigcup0`, `bigcup0P`, - `subset_bigcup_r`, `eqbigcup_r`, `eq_set_inl`, `set_in_in` -- in `ereal.v`: - + lemmas `adde_undefC`, `real_of_erD`, `fin_num_add_undef`, `addeK`, - `subeK`, `subee`, `sube_le0`, `lee_sub` - + lemmas `addeACA`, `muleC`, `mule1`, `mul1e`, `abseN` - + enable notation `x \is a fin_num` - * definition `fin_num`, fact `fin_num_key`, lemmas `fin_numE`, `fin_numP` - + definition `dense` and lemma `denseNE` -- in `reals.v`: - + lemmas `has_sup1`, `has_inf1` -- in `nngnum.v`: - + instance `invr_nngnum` -- in `posnum.v`: - + instance `posnum_nngnum` - ### Changed -- in `ereal.v`: - + generalize lemma `lee_sum_nneg_subfset` -- in `sequences.v`: - + generalize lemmas `ereal_nondecreasing_series`, `is_cvg_ereal_nneg_series`, - `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty` -- in `measure.v`: - + 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` -- in `ereal.v`: - + lemmas `nbhs_oo_up_e1`, `nbhs_oo_down_e1`, `nbhs_oo_up_1e`, `nbhs_oo_down_1e` - `nbhs_fin_out_above`, `nbhs_fin_out_below`, `nbhs_fin_out_above_below` - `nbhs_fin_inbound` -- in `classical_sets.v`: - + change the order of arguments of `subset_trans` - ### Renamed -- in `ereal.v`: - + `is_realN` -> `fin_numN` - + `is_realD` -> `fin_numD` - + `ereal_sup_set0` -> `ereal_sup0` - + `ereal_sup_set1` -> `ereal_sup1` - + `ereal_inf_set0` -> `ereal_inf0` - ### 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` -- in `ereal.v`: - + definition `is_real` - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 980af57ba..ae56a135f 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.0.3.6 +$ opam install coq-mathcomp-analysis.0.3.7 ``` 4. Everytime you want to work in this same context, you need to type ```