changelog for version 0.5.3

CHANGELOG.md

@@ -1,6 +1,115 @@
 # Changelog
 
-Lastest releases: [[0.5.2] - 2022-06-08](#052---2022-07-08) and [[0.5.1] - 2022-06-04](#051---2022-06-04)
+Lastest releases: [[0.5.3] - 2022-08-10](#053---2022-08-10) and [[0.5.2] - 2022-06-08](#052---2022-07-08)
+
+## [0.5.3] - 2022-08-10
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + lemma `big_const_idem`
+  + lemma `big_id_idem`
+  + lemma `big_rem_AC`
+  + lemma `bigD1_AC`
+  + lemma `big_mkcond_idem`
+  + lemma `big_split_idem`
+  + lemma `big_id_idem_AC`
+  + lemma `bigID_idem`
+  + lemmas `bigmax_le` and `bigmax_lt`
+  + lemma `bigmin_idr`
+  + lemma `bigmax_idr`
+- in file `boolp.v`:
+  + lemmas `iter_compl`, `iter_compr`, `iter0`
+- in file `functions.v`:
+  + lemmas `oinv_iter`, `some_iter_inv`, `inv_iter`,
+  + Instances for functions interfaces for `iter` (partial inverse up to
+      bijective function)
+- in `classical_sets.v`:
+  + lemma `preimage10P`
+  + lemma `setT_unit`
+  + lemma `subset_refl`
+- in `ereal.v`:
+  + notations `_ < _ :> _` and `_ <= _ :> _`
+  + lemmas `lee01`, `lte01`, `lee0N1`, `lte0N1`
+  + lemmas `lee_pmul2l`, `lee_pmul2r`, `lte_pmul`, `lee_wpmul2l`
+  + lemmas `lee_lt_add`, `lee_lt_dadd`, `lee_paddl`, `lee_pdaddl`,
+    `lte_paddl`, `lte_pdaddl`, `lee_paddr`, `lee_pdaddr`,
+    `lte_paddr`, `lte_pdaddr`
+  + lemmas `muleCA`, `muleAC`, `muleACA`
+- in `reals.v`:
+  + lemmas `Rfloor_lt_int`, `floor_lt_int`, `floor_ge_int`
+  + lemmas `ceil_ge_int`, `ceil_lt_int`
+- in `lebesgue_integral.v`:
+  + lemma `ge0_emeasurable_fun_sum`
+  + lemma `integrableMr`
+
+### Changed
+
+- in `ereal.v`:
+  + generalize `lee_pmul`
+  + simplify `lte_le_add`, `lte_le_dadd`, `lte_le_sub`, `lte_le_dsub`
+- in `measure.v`:
+  + generalize `pushforward`
+- in `lebesgue_integral.v`
+  + change `Arguments` of `eq_integrable`
+  + fix pretty-printing of `{mfun _ >-> _}`, `{sfun _ >-> _}`, `{nnfun _ >-> _}`
+  + minor generalization of `eq_measure_integral`
+- from `topology.v` to `mathcomp_extra.v`:
+  + generalize `ltr_bigminr` to `porderType` and rename to `bigmin_lt`
+  + generalize `bigminr_ler` to `orderType` and rename to `bigmin_le`
+- moved out of module `Bigminr` in `normedtype.v` to `mathcomp_extra.v`
+  and generalized to `orderType`:
+  + lemma `bigminr_ler_cond`, renamed to `bigmin_le_cond`
+- moved out of module `Bigminr` in `normedtype.v` to `mathcomp_extra.v`:
+  + lemma `bigminr_maxr`
+- moved from from module `Bigminr` in `normedtype.v`
+  + to `mathcomp_extra.v` and generalized to `orderType`
+    * `bigminr_mkcond` -> `bigmin_mkcond`
+    * `bigminr_split` -> `bigmin_split`
+    * `bigminr_idl` -> `bigmin_idl`
+    * `bigminrID` -> `bigminID`
+    * `bigminrD1` -> `bigminD1`
+    * `bigminr_inf` -> `bigmin_inf`
+    * `bigminr_gerP` -> `bigmin_geP`
+    * `bigminr_gtrP` -> ``bigmin_gtP``
+    * `bigminr_eq_arg` -> `bigmin_eq_arg`
+    * `eq_bigminr` -> `eq_bigmin`
+  + to `topology.v` and generalized to `orderType`
+    * `bigminr_lerP` -> `bigmin_leP`
+    * `bigminr_ltrP` -> `bigmin_ltP`
+- moved from `topology.v` to `mathcomp_extra.v`:
+  + `bigmax_lerP` -> `bigmax_leP`
+  + `bigmax_ltrP` -> `bigmax_ltP`
+  + `ler_bigmax_cond` -> `le_bigmax_cond`
+  + `ler_bigmax` -> `le_bigmax`
+  + `le_bigmax` -> `homo_le_bigmax`
+
+### Renamed
+
+- in `ereal.v`:
+  + `lee_pinfty_eq` -> `leye_eq`
+  + `lee_ninfty_eq` -> `leeNy_eq`
+- in `classical_sets.v`:
+  + `set_bool` -> `setT_bool`
+- in `topology.v`:
+  + `bigmax_gerP` -> `bigmax_geP`
+  + `bigmax_gtrP` -> `bigmax_gtP`
+- in `lebesgue_integral.v`:
+  + `emeasurable_funeM` -> `measurable_funeM`
+
+### Removed
+
+- in `topology.v`:
+  + `bigmax_seq1`, `bigmax_pred1_eq`, `bigmax_pred1`
+- in `normedtype.v` (module `Bigminr`)
+  + `bigminr_ler_cond`, `bigminr_ler`.
+  + `bigminr_seq1`, `bigminr_pred1_eq`, `bigminr_pred1`
+
+### Misc
+
+- file `ereal.v` split in two files `constructive_ereal.v` and
+  `ereal.v` (the latter exports the former, so the "Require Import
+  ereal" can just be kept unchanged)
 
 ## [0.5.2] - 2022-07-08
 

CHANGELOG_UNRELEASED.md

@@ -4,114 +4,12 @@
 
 ### Added
 
-- in file `boolp.v`:
-  + lemmas `iter_compl`, `iter_compr`, `iter0`
-- in file `functions.v`:
-  + lemmas `oinv_iter`, `some_iter_inv`, `inv_iter`,
-  + Instances for functions interfaces for `iter` (partial inverse up to 
-      bijective function) 
-- in `ereal.v`:
-  + notations `_ < _ :> _` and `_ <= _ :> _`
-  + lemmas `lee01`, `lte01`, `lee0N1`, `lte0N1`
-  + lemmas `lee_pmul2l`, `lee_pmul2r`, `lte_pmul`, `lee_wpmul2l`
-  + lemmas `lee_lt_add`, `lee_lt_dadd`, `lee_paddl`, `lee_pdaddl`,
-    `lte_paddl`, `lte_pdaddl`, `lee_paddr`, `lee_pdaddr`,
-    `lte_paddr`, `lte_pdaddr`
-- in `lebesgue_integral.v`:
-  + lemma `ge0_emeasurable_fun_sum`
-  + lemma `integrableMr`
-- in `ereal.v`:
-  + lemmas `muleCA`, `muleAC`, `muleACA`
-- in `classical_sets.v`:
-  + lemma `preimage10P`
-- in `classical_sets.v`:
-  + lemma `setT_unit`
-- in `mathcomp_extra.v`:
-  + lemma `big_const_idem`
-  + lemma `big_id_idem`
-  + lemma `big_rem_AC`
-  + lemma `bigD1_AC`
-  + lemma `big_mkcond_idem`
-  + lemma `big_split_idem`
-  + lemma `big_id_idem_AC`
-  + lemma `bigID_idem`
-- in `mathcomp_extra.v`:
-  + lemmas `bigmax_le` and `bigmax_lt`
-  + lemma `bigmin_idr`
-  + lemma `bigmax_idr`
-- in `classical_sets.v`:
-  + lemma `subset_refl`
-- in `reals.v`:
-  + lemmas `Rfloor_lt_int`, `floor_lt_int`, `floor_ge_int`
-  + lemmas `ceil_ge_int`, `ceil_lt_int`
-
 ### Changed
 
-- in `ereal.v`:
-  + generalize `lee_pmul`
-  + simplify `lte_le_add`, `lte_le_dadd`, `lte_le_sub`, `lte_le_dsub`
-- in `measure.v`:
-  + generalize `pushforward`
-- in `lebesgue_integral.v`
-  + change `Arguments` of `eq_integrable`
-- in `lebesgue_integral.v`:
-  + fix pretty-printing of `{mfun _ >-> _}`, `{sfun _ >-> _}`, `{nnfun _ >-> _}`
-- in `lebesgue_integral.v`
-  + minor generalization of `eq_measure_integral`
-- from `topology.v` to `mathcomp_extra.v`:
-  + generalize `ltr_bigminr` to `porderType` and rename to `bigmin_lt`
-  + generalize `bigminr_ler` to `orderType` and rename to `bigmin_le`
-- moved out of module `Bigminr` in `normedtype.v` to `mathcomp_extra.v` and generalized to `orderType`:
-  + lemma `bigminr_ler_cond`, renamed to `bigmin_le_cond`
-- moved out of module `Bigminr` in `normedtype.v` to `mathcomp_extra.v`:
-  + lemma `bigminr_maxr`
-- moved from from module `Bigminr` in `normedtype.v`
-  + to `mathcomp_extra.v` and generalized to `orderType`
-    * `bigminr_mkcond` -> `bigmin_mkcond`
-    * `bigminr_split` -> `bigmin_split`
-    * `bigminr_idl` -> `bigmin_idl`
-    * `bigminrID` -> `bigminID`
-    * `bigminrD1` -> `bigminD1`
-    * `bigminr_inf` -> `bigmin_inf`
-    * `bigminr_gerP` -> `bigmin_geP`
-    * `bigminr_gtrP` -> ``bigmin_gtP``
-    * `bigminr_eq_arg` -> `bigmin_eq_arg`
-    * `eq_bigminr` -> `eq_bigmin`
-  + to `topology.v` and generalized to `orderType`
-    * `bigminr_lerP` -> `bigmin_leP`
-    * `bigminr_ltrP` -> `bigmin_ltP`
-- moved from `topology.v` to `mathcomp_extra.v`:
-  + `bigmax_lerP` -> `bigmax_leP`
-  + `bigmax_ltrP` -> `bigmax_ltP`
-  + `ler_bigmax_cond` -> `le_bigmax_cond`
-  + `ler_bigmax` -> `le_bigmax`
-  + `le_bigmax` -> `homo_le_bigmax`
-
 ### Renamed
 
-- in `ereal.v`:
-  + `lee_pinfty_eq` -> `leye_eq`
-  + `lee_ninfty_eq` -> `leeNy_eq`
-- in `classical_sets.v`:
-  + `set_bool` -> `setT_bool`
-- in `topology.v`:
-  + `bigmax_gerP` -> `bigmax_geP`
-  + `bigmax_gtrP` -> `bigmax_gtP`
-- in `lebesgue_integral.v`:
-  + `emeasurable_funeM` -> `measurable_funeM`
-
 ### Removed
 
-- in `normedtype.v` (module `Bigminr`)
-  + `bigminr_ler_cond`, `bigminr_ler`.
-  + `bigminr_seq1`, `bigminr_pred1_eq`, `bigminr_pred1`
-- in `topology.v`:
-  + `bigmax_seq1`, `bigmax_pred1_eq`, `bigmax_pred1`
-
 ### Infrastructure
 
 ### Misc
-
-- file `ereal.v` split in two files `constructive_ereal.v` and
-  `ereal.v` (the latter exports the former, so the "Require Import
-  ereal" can just be kept unchanged)

INSTALL.md

@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.5.1
+$ opam install coq-mathcomp-analysis.0.5.3
 ```
 4. Everytime you want to work in this same context, you need to type
 ```