From 5c25df4fdf0019849b9b3954702af792621466cb Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 11 Nov 2020 23:16:02 +0900 Subject: [PATCH 1/2] changelog for version 0.3.3 --- CHANGELOG.md | 132 +++++++++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 122 ------------------------------------- 2 files changed, 131 insertions(+), 123 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 55b22a71a..c065ba76e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,136 @@ # Changelog -Last releases: [[0.3.2] - 2020-08-11](#032---2020-08-11) and [[0.3.1] - 2020-06-11](#031---2020-06-11) +Last releases: [[0.3.3] - 2020-11-11](#033---2020-11-11) and [[0.3.2] - 2020-08-11](#032---2020-08-11) + +## [0.3.3] - 2020-11-11 + +### Added + +- in `boolp.v`: + + lemma `not_andP` + + lemma `not_exists2P` +- in `classical_sets.v`: + + lemmas `setIIl`, `setIIr`, `setCS`, `setSD`, `setDS`, `setDSS`, `setCI`, + `setDUr`, `setDUl`, `setIDA`, `setDD` + + definition `dep_arrow_choiceType` + + lemma `bigcup_set0` + + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `subsetPset`, `properPset` + + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType` + + lemmas `set0M`, `setM0`, `image_set0_set0`, `subset_set1`, `preimage_set0` + + lemmas `setICr`, `setUidPl`, `subsets_disjoint`, `disjoints_subset`, `setDidPl`, + `setIidPl`, `setIS`, `setSI`, `setISS`, `bigcup_recl`, `bigcup_distrr`, + `setMT` + + new lemmas: `lb_set1`, `ub_lb_set1`, `ub_lb_refl`, `lb_ub_lb` + + new definitions and lemmas: `infimums`, `infimum`, `infimums_set1`, `is_subset1_infimum` + + new lemmas: `ge_supremum_Nmem`, `le_infimum_Nmem`, `nat_supremums_neq0` + + lemmas `setUCl`, `setDv` + + lemmas `image_preimage_subset`, `image_subset`, `preimage_subset` + + definition `proper` and its notation `<` + + lemmas `setUK`, `setKU`, `setIK`, `setKI` + + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `properEneq` + + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType` on classical `set`. +- file `nngnum.v` +- in `topology.v`: + + definition `meets` and its notation `#` + + lemmas `meetsC`, `meets_openr`, `meets_openl`, `meets_globallyl`, + `meets_globallyr `, `meetsxx` and `proper_meetsxx`. + + definition `limit_point` + + lemmas `subset_limit_point`, `closure_limit_point`, + `closure_subset`, `closureE`, `closureC`, `closure_id` + + lemmas `cluster_nbhs`, `clusterEonbhs`, `closureEcluster` + + definition `separated` + + lemmas `connected0`, `connectedPn`, `connected_continuous_connected` + + lemmas `closureEnbhs`, `closureEonbhs`, `limit_pointEnbhs`, + `limit_pointEonbhs`, `closeEnbhs`, `closeEonbhs`. +- in `ereal.v`: + + notation `\+` (`ereal_scope`) for function addition + + notations `>` and `>=` for comparison of extended real numbers + + definition `is_real`, lemmas `is_realN`, `is_realD`, `ERFin_real_of_er` + + basic lemmas: `addooe`, `adde_Neq_pinfty`, `adde_Neq_ninfty`, `addERFin`, + `subERFin`, `real_of_erN`, `lb_ereal_inf_adherent` + + arithmetic lemmas: `oppeD`, `subre_ge0`, `suber_ge0`, `lee_add2lE`, `lte_add2lE`, + `lte_add`, `lte_addl`, `lte_le_add`, `lte_subl_addl`, `lee_subr_addr`, + `lee_subl_addr`, `lte_spaddr` + + lemmas `gee0P`, `sume_ge0`, `lee_sum_nneg`, `lee_sum_nneg_ord`, `lee_sum_nneg_subset`, `lee_sum_nneg_subfset` + + lemma `lee_addr` + + lemma `lee_adde` + + lemma `oppe_continuous` + + lemmas `ereal_nbhs_pinfty_ge`, `ereal_nbhs_ninfty_le` +- in `sequences.v`: + + definitions `arithmetic`, `geometric`, `geometric_invn` + + lemmas `increasing_series`, `cvg_shiftS`, `mulrn_arithmetic`, + `exprn_geometric`, `cvg_arithmetic`, `cvg_expr`, + `geometric_seriesE`, `cvg_geometric_series`, + `is_cvg_geometric_series`. + + lemmas `ereal_cvgN`, `ereal_cvg_ge0`, `ereal_lim_ge`, `ereal_lim_le` + + lemma `ereal_cvg_real` + + lemmas `is_cvg_ereal_nneg_series_cond`, `is_cvg_ereal_nneg_series`, `ereal_nneg_series_lim_ge0`, + `ereal_nneg_series_pinfty` + + lemmas `ereal_cvgPpinfty`, `ereal_cvgPninfty`, `lee_lim` + + lemma `ereal_cvgD` + * with intermediate lemmas `ereal_cvgD_pinfty_fin`, `ereal_cvgD_ninfty_fin`, `ereal_cvgD_pinfty_pinfty`, + `ereal_cvgD_ninfty_ninfty` + + lemma `ereal_limD` +- in `normedtype.v`: + + lemma `closed_ereal_le_ereal` + + lemma `closed_ereal_ge_ereal` + + lemmas `natmul_continuous`, `cvgMn` and `is_cvgMn`. + + `uniformType` structure for `ereal` + +### Changed + +- in `classical_sets.v`: + + the index in `bigcup_set1` generalized from `nat` to some `Type` + + lemma `bigcapCU` generalized + + lemmas `preimage_setU` and `preimage_setI` are about the `setU` and `setI` (instead of `bigcup` and `bigcap`) + + `eqEsubset` changed from an implication to an equality +- lemma `asboolb` moved from `discrete.v` to `boolp.v` +- lemma `exists2NP` moved from `discrete.v` to `boolp.v` +- lemma `neg_or` moved from `discrete.v` to `boolp.v` and renamed to `not_orP` +- definitions `dep_arrow_choiceClass` and `dep_arrow_pointedType` + slightly generalized and moved from `topology.v` to + `classical_sets.v` +- the types of the topological notions for `numFieldType` have been moved from `normedtype.v` to `topology.v` +- the topology of extended real numbers has been moved from `normedtype.v` to `ereal.v` (including the notions of filters) +- `numdFieldType_lalgType` in `normedtype.v` renamed to `numFieldType_lalgType` in `topology.v` +- in `ereal.v`: + + the first argument of `real_of_er` is now maximal implicit + + the first argument of `is_real` is now maximal implicit + + generalization of `lee_sum` +- in `boolp.v`: + + rename `exists2NP` to `forall2NP` and make it bidirectionnal +- moved the definition of `{nngnum _}` and the related bigmax theory to the new `nngnum.v` file + +### Renamed + +- in `classical_sets.v`: + + `setIDl` -> `setIUl` + + `setUDl` -> `setUIl` + + `setUDr` -> `setUIr` + + `setIDr` -> `setIUl` + + `setCE` -> `setTD` + + `preimage_setU` -> `preimage_bigcup`, `preimage_setI` -> `preimage_bigcap` +- in `boolp.v`: + + `contrap` -> `contra_not` + + `contrapL` -> `contraPnot` + + `contrapR` -> `contra_notP` + + `contrapLR` -> `contraPP` + +### Removed + +- in `boolp.v`: + + `contrapNN`, `contrapTN`, `contrapNT`, `contrapTT` + + `eqNN` +- in `normedtype.v`: + + `forallN` + + `eqNNP` + + `existsN` +- in `discrete.v`: + + `existsP` + + `existsNP` +- in `topology.v`: + + `close_to` + + `close_cluster`, which is subsumed by `closeEnbhs` ## [0.3.2] - 2020-08-11 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f5f17e64c..c1ee5bdc8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,134 +4,12 @@ ### Added -- in `boolp.v`: - + lemma `not_andP` -- in `classical_sets.v`: - + lemmas `setIIl`, `setIIr`, `setCS`, `setSD`, `setDS`, `setDSS`, `setCI`, - `setDUr`, `setDUl`, `setIDA`, `setDD` - + definition `dep_arrow_choiceType` - + lemma `bigcup_set0` - + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `subsetPset`, `properPset` - + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType` - + lemma `not_exists2P` - -- in `normedtype.v`: - + lemma `closed_ereal_le_ereal` - + lemma `closed_ereal_ge_ereal` - + lemmas `set0M`, `setM0`, `image_set0_set0`, `subset_set1`, `preimage_set0` - + lemmas `setICr`, `setUidPl`, `subsets_disjoint`, `disjoints_subset`, `setDidPl`, - `setIidPl`, `setIS`, `setSI`, `setISS`, `bigcup_recl`, `bigcup_distrr`, - `setMT` -- in `ereal.v`: - + notation `\+` (`ereal_scope`) for function addition - + notations `>` and `>=` for comparison of extended real numbers - + definition `is_real`, lemmas `is_realN`, `is_realD`, `ERFin_real_of_er` - + basic lemmas: `addooe`, `adde_Neq_pinfty`, `adde_Neq_ninfty`, `addERFin`, - `subERFin`, `real_of_erN`, `lb_ereal_inf_adherent` - + arithmetic lemmas: `oppeD`, `subre_ge0`, `suber_ge0`, `lee_add2lE`, `lte_add2lE`, - `lte_add`, `lte_addl`, `lte_le_add`, `lte_subl_addl`, `lee_subr_addr`, - `lee_subl_addr`, `lte_spaddr` - + lemmas `gee0P`, `sume_ge0`, `lee_sum_nneg`, `lee_sum_nneg_ord`, `lee_sum_nneg_subset`, `lee_sum_nneg_subfset` - + lemma `lee_addr` - + lemma `lee_adde` -- in `normedtype.v`: - + lemmas `natmul_continuous`, `cvgMn` and `is_cvgMn`. - + `uniformType` structure for `ereal` -- in `sequences.v`: - + definitions `arithmetic`, `geometric`, `geometric_invn` - + lemmas `increasing_series`, `cvg_shiftS`, `mulrn_arithmetic`, - `exprn_geometric`, `cvg_arithmetic`, `cvg_expr`, - `geometric_seriesE`, `cvg_geometric_series`, - `is_cvg_geometric_series`. - + lemmas `ereal_cvgN`, `ereal_cvg_ge0`, `ereal_lim_ge`, `ereal_lim_le` - + lemma `ereal_cvg_real` - + lemmas `is_cvg_ereal_nneg_series_cond`, `is_cvg_ereal_nneg_series`, `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty` - + lemmas `ereal_cvgPpinfty`, `ereal_cvgPninfty`, `lee_lim` - + lemma `ereal_cvgD` - * with intermediate lemmas `ereal_cvgD_pinfty_fin`, `ereal_cvgD_ninfty_fin`, `ereal_cvgD_pinfty_pinfty`, `ereal_cvgD_ninfty_ninfty` - + lemma `ereal_limD` -- in `classical_sets.v`: - + new lemmas: `lb_set1`, `ub_lb_set1`, `ub_lb_refl`, `lb_ub_lb` - + new definitions and lemmas: `infimums`, `infimum`, `infimums_set1`, `is_subset1_infimum` - + new lemmas: `ge_supremum_Nmem`, `le_infimum_Nmem`, `nat_supremums_neq0` - + lemmas `ereal_nbhs_pinfty_ge`, `ereal_nbhs_ninfty_le` - + lemma `oppe_continuous` - + lemmas `setUCl`, `setDv` - + lemmas `image_preimage_subset`, `image_subset`, `preimage_subset` - + definition `proper` and its notation `<` - + lemmas `setUK`, `setKU`, `setIK`, `setKI` - + lemmas `setUK`, `setKU`, `setIK`, `setKI`, `subsetEset`, `subEset`, `complEset`, `botEset`, `topEset`, `meetEset`, `joinEset`, `properEneq` - + Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType` on classical `set`. -- file `nngnum.v` - - + definition `meets` and its notation `#` - + lemmas `meetsC`, `meets_openr`, `meets_openl`, `meets_globallyl`, - `meets_globallyr `, `meetsxx` and `proper_meetsxx`. -- in `topology.v`: - + definition `limit_point` - + lemmas `subset_limit_point`, `closure_limit_point`, - `closure_subset`, `closureE`, `closureC`, `closure_id` - + lemmas `cluster_nbhs`, `clusterEonbhs`, `closureEcluster` - + definition `separated` - + lemmas `connected0`, `connectedPn`, `connected_continuous_connected` - + lemmas `closureEnbhs`, `closureEonbhs`, `limit_pointEnbhs`, - `limit_pointEonbhs`, `closeEnbhs`, `closeEonbhs`. - ### Changed -- in `classical_sets.v`: - + the index in `bigcup_set1` generalized from `nat` to some `Type` - + lemma `bigcapCU` generalized - + lemmas `preimage_setU` and `preimage_setI` are about the `setU` and `setI` (instead of `bigcup` and `bigcap`) - + `eqEsubset` changed from an implication to an equality -- lemma `asboolb` moved from `discrete.v` to `boolp.v` -- lemma `exists2NP` moved from `discrete.v` to `boolp.v` -- lemma `neg_or` moved from `discrete.v` to `boolp.v` and renamed to `not_orP` -- definitions `dep_arrow_choiceClass` and `dep_arrow_pointedType` - slightly generalized and moved from `topology.v` to - `classical_sets.v` -- the types of the topological notions for `numFieldType` have been moved from `normedtype.v` to `topology.v` -- the topology of extended real numbers has been moved from `normedtype.v` to `ereal.v` (including the notions of filters) -- `numdFieldType_lalgType` in `normedtype.v` renamed to `numFieldType_lalgType` in `topology.v` -- in `ereal.v`: - + the first argument of `real_of_er` is now maximal implicit - + the first argument of `is_real` is now maximal implicit - + generalization of `lee_sum` -- in `boolp.v`: - + rename `exists2NP` to `forall2NP` and make it bidirectionnal -- moved the definition of `{nngnum _}` and the related bigmax theory to the new `nngnum.v` file - ### Renamed -- in `classical_sets.v`: - + `setIDl` -> `setIUl` - + `setUDl` -> `setUIl` - + `setUDr` -> `setUIr` - + `setIDr` -> `setIUl` - + `setCE` -> `setTD` - + `preimage_setU` -> `preimage_bigcup`, `preimage_setI` -> `preimage_bigcap` -- in `boolp.v`: - + `contrap` -> `contra_not` - + `contrapL` -> `contraPnot` - + `contrapR` -> `contra_notP` - + `contrapLR` -> `contraPP` - ### Removed -- in `boolp.v`: - + `contrapNN`, `contrapTN`, `contrapNT`, `contrapTT` - + `eqNN` -- in `normedtype.v`: - + `forallN` - + `eqNNP` - + `existsN` -- in `discrete.v`: - + `existsP` - + `existsNP` -- in `topology.v`: - + `close_to` - + `close_cluster`, which is subsumed by `closeEnbhs` - ### Infrastructure ### Misc From 7a688d4d022b72b393955755fe9e1f2f889b0d13 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 12 Nov 2020 00:04:55 +0900 Subject: [PATCH 2/2] update opam and INSTALL.md --- INSTALL.md | 2 +- opam | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index ae04aa4b9..e277333af 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -45,7 +45,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.0.3.2 +$ opam install coq-mathcomp-analysis.0.3.3 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/opam b/opam index dc6a0b573..51e14cdd9 100644 --- a/opam +++ b/opam @@ -36,5 +36,5 @@ tags: [ "keyword: topology" "keyword: real numbers" "logpath: mathcomp.analysis" - "date:2020-08-11" + "date:2020-11-11" ]