changelog for version 0.7.0

math-comp · Jan 19, 2024 · 7183d3e · 7183d3e
1 parent 8d49e8e
commit 7183d3e
Show file tree

Hide file tree

Showing 3 changed files with 131 additions and 123 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,127 @@
 # Changelog
 
-Latest releases: [[0.6.7] - 2024-01-09](#067---2024-01-09) and [[0.6.6] - 2023-11-14](#066---2023-11-14)
+Latest releases: [[0.7.0] - 2024-01-19](#070---2024-01-19) and [[0.6.7] - 2024-01-09](#067---2024-01-09)
+
+## [0.7.0] - 2024-01-19
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + lemmas `last_filterP`,
+    `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`,
+	`path_lt_le_last`
+
+- new file `contra.v`
+  + lemma `assume_not`
+  + tactic `assume_not`
+  + lemma `absurd_not`
+  + tactics `absurd_not`, `contrapose`
+  + tactic notations `contra`, `contra : constr(H)`, `contra : ident(H)`,
+    `contra : { hyp_list(Hs) } constr(H)`, `contra : { hyp_list(Hs) } ident(H)`,
+	 `contra : { - } constr(H)`
+  + lemma `absurd`
+  + tactic notations `absurd`, `absurd constr(P)`, `absurd : constr(H)`,
+    `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`,
+	 `absurd : { hyp_list(Hs) } ident(H)`
+
+- in `topology.v`:
+  + lemma `filter_bigI_within`
+  + lemma `near_powerset_map`
+  + lemma `near_powerset_map_monoE`
+  + lemma `fst_open`
+  + lemma `snd_open`
+  + definition `near_covering_within`
+  + lemma `near_covering_withinP`
+  + lemma `compact_setM`
+  + lemma `compact_regular`
+  + lemma `fam_compact_nbhs`
+  + definition `compact_open`, notation `{compact-open, U -> V}`
+  + notation `{compact-open, F --> f}`
+  + definition `compact_openK`
+  + definition `compact_openK_nbhs`
+  + instance `compact_openK_nbhs_filter`
+  + definition `compact_openK_topological_mixin`
+  + canonicals `compact_openK_filter`, `compact_openK_topological`,
+	`compact_open_pointedType`
+  + definition `compact_open_topologicalType`
+  + canonicals `compact_open_filtered`, `compact_open_topological`
+  + lemma `compact_open_cvgP`
+  + lemma `compact_open_open`
+  + lemma `compact_closedI`
+  + lemma `compact_open_fam_compactP`
+  + lemma `compact_equicontinuous`
+  + lemma `uniform_regular`
+  + lemma `continuous_curry`
+  + lemma `continuous_uncurry_regular`
+  + lemma `continuous_uncurry`
+  + lemma `curry_continuous`
+  + lemma `uncurry_continuous`
+
+- in `ereal.v`:
+  + lemma `ereal_supy`
+
+- in file `normedtype.v`,
+  + new lemma `continuous_within_itvP`.
+
+- in file `realfun.v`,
+  + new definitions `itv_partition`, `itv_partitionL`, `itv_partitionR`, 
+    `variation`, `variations`, `bounded_variation`, `total_variation`, 
+    `neg_tv`, and `pos_tv`.
+
+  + new lemmas `left_right_continuousP`,
+    `nondecreasing_funN`, `nonincreasing_funN`
+
+  + new lemmas `itv_partition_nil`, `itv_partition_cons`, `itv_partition1`,
+    `itv_partition_size_neq0`, `itv_partitionxx`, `itv_partition_le`,
+    `itv_partition_cat`, `itv_partition_nth_size`,
+    `itv_partition_nth_ge`, `itv_partition_nth_le`, 
+    `nondecreasing_fun_itv_partition`, `nonincreasing_fun_itv_partition`, 
+    `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, 
+    `notin_itv_partition`, `itv_partition_rev`,
+
+  + new lemmas `variation_zip`, `variation_prev`, `variation_next`, `variation_nil`,
+    `variation_ge0`, `variationN`, `variation_le`, `nondecreasing_variation`, 
+    `nonincreasing_variation`, `variationD`, `variation_itv_partitionLR`, 
+    `le_variation`, `variation_opp_rev`, `variation_rev_opp`
+
+  + new lemmas `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx`
+
+  + new lemmas `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`,
+    `bounded_variationl`, `bounded_variationr`, `variations_opp`, 
+    `nondecreasing_bounded_variation`
+
+  + new lemmas `total_variationxx`, `total_variation_ge`, `total_variation_ge0`,
+    `bounded_variationP`, `nondecreasing_total_variation`, `total_variationN`,
+	  `total_variation_le`, `total_variationD`, `neg_tv_nondecreasing`,
+    `total_variation_pos_neg_tvE`, `fine_neg_tv_nondecreasing`,
+    `neg_tv_bounded_variation`, `total_variation_right_continuous`,
+    `neg_tv_right_continuous`, `total_variation_opp`,
+    `total_variation_left_continuous`, `total_variation_continuous`
+
+- in `lebesgue_stieltjes_measure.v`:
+  + `sigma_finite_measure` HB instance on `lebesgue_stieltjes_measure`
+
+- in `lebesgue_measure.v`:
+  + `sigma_finite_measure` HB instance on `lebesgue_measure`
+
+- in `lebesgue_integral.v`:
+  + `sigma_finite_measure` instance on product measure `\x`
+
+### Changed
+
+- in `topology.v`:
+  + lemmas `nbhsx_ballx` and `near_ball` take a parameter of type `R` instead of `{posnum R}`
+  + lemma `pointwise_compact_cvg`
+
+### Generalized
+
+- in `realfun.v`:
+  + lemmas `nonincreasing_at_right_cvgr`, `nonincreasing_at_left_cvgr`
+  + lemmas `nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`,
+    `nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge`
+
+- in `realfun.v`:
+  + lemmas `nonincreasing_at_right_is_cvgr`, `nondecreasing_at_right_is_cvgr`
 
 ## [0.6.7] - 2024-01-09
 

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -4,125 +4,12 @@
 
 ### Added
 
-- in `lebesgue_stieltjes_measure.v`:
-  + `sigma_finite_measure` HB instance on `lebesgue_stieltjes_measure`
-
-- in `lebesgue_measure.v`:
-  + `sigma_finite_measure` HB instance on `lebesgue_measure`
-
-- in `lebesgue_integral.v`:
-  + `sigma_finite_measure` instance on product measure `\x`
-
-- file `contra.v`
-- in `contra.v`
-  + lemma `assume_not`
-  + tactic `assume_not`
-  + lemma `absurd_not`
-  + tactics `absurd_not`, `contrapose`
-  + tactic notations `contra`, `contra : constr(H)`, `contra : ident(H)`,
-    `contra : { hyp_list(Hs) } constr(H)`, `contra : { hyp_list(Hs) } ident(H)`,
-	 `contra : { - } constr(H)`
-  + lemma `absurd`
-  + tactic notations `absurd`, `absurd constr(P)`, `absurd : constr(H)`,
-    `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`,
-	 `absurd : { hyp_list(Hs) } ident(H)`
-
-- in `topology.v`:
-  + lemma `filter_bigI_within`
-  + lemma `near_powerset_map`
-  + lemma `near_powerset_map_monoE`
-  + lemma `fst_open`
-  + lemma `snd_open`
-  + definition `near_covering_within`
-  + lemma `near_covering_withinP`
-  + lemma `compact_setM`
-  + lemma `compact_regular`
-  + lemma `fam_compact_nbhs`
-  + definition `compact_open`, notation `{compact-open, U -> V}`
-  + notation `{compact-open, F --> f}`
-  + definition `compact_openK`
-  + definition `compact_openK_nbhs`
-  + instance `compact_openK_nbhs_filter`
-  + definition `compact_openK_topological_mixin`
-  + canonicals `compact_openK_filter`, `compact_openK_topological`,
-	`compact_open_pointedType`
-  + definition `compact_open_topologicalType`
-  + canonicals `compact_open_filtered`, `compact_open_topological`
-  + lemma `compact_open_cvgP`
-  + lemma `compact_open_open`
-  + lemma `compact_closedI`
-  + lemma `compact_open_fam_compactP`
-  + lemma `compact_equicontinuous`
-  + lemma `uniform_regular`
-  + lemma `continuous_curry`
-  + lemma `continuous_uncurry_regular`
-  + lemma `continuous_uncurry`
-  + lemma `curry_continuous`
-  + lemma `uncurry_continuous`
-- in file `normedtype.v`,
-  + new lemma `continuous_within_itvP`.
-
-- in `ereal.v`:
-  + lemma `ereal_supy`
-
-- in `mathcomp_extra.v`:
-  + lemmas `last_filterP`,
-    `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`,
-	`path_lt_le_last`
-
-- in file `realfun.v`,
-  + new definitions `itv_partition`, `itv_partitionL`, `itv_partitionR`, 
-    `variation`, `variations`, `bounded_variation`, `total_variation`, 
-    `neg_tv`, and `pos_tv`.
-
-  + new lemmas `left_right_continuousP`,
-    `nondecreasing_funN`, `nonincreasing_funN`
-
-  + new lemmas `itv_partition_nil`, `itv_partition_cons`, `itv_partition1`,
-    `itv_partition_size_neq0`, `itv_partitionxx`, `itv_partition_le`,
-    `itv_partition_cat`, `itv_partition_nth_size`,
-    `itv_partition_nth_ge`, `itv_partition_nth_le`, 
-    `nondecreasing_fun_itv_partition`, `nonincreasing_fun_itv_partition`, 
-    `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, 
-    `notin_itv_partition`, `itv_partition_rev`,
-
-  + new lemmas `variation_zip`, `variation_prev`, `variation_next`, `variation_nil`,
-    `variation_ge0`, `variationN`, `variation_le`, `nondecreasing_variation`, 
-    `nonincreasing_variation`, `variationD`, `variation_itv_partitionLR`, 
-    `le_variation`, `variation_opp_rev`, `variation_rev_opp`
-
-  + new lemmas `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx`
-
-  + new lemmas `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`,
-    `bounded_variationl`, `bounded_variationr`, `variations_opp`, 
-    `nondecreasing_bounded_variation`
-
-  + new lemmas `total_variationxx`, `total_variation_ge`, `total_variation_ge0`,
-    `bounded_variationP`, `nondecreasing_total_variation`, `total_variationN`,
-	  `total_variation_le`, `total_variationD`, `neg_tv_nondecreasing`,
-    `total_variation_pos_neg_tvE`, `fine_neg_tv_nondecreasing`,
-    `neg_tv_bounded_variation`, `total_variation_right_continuous`,
-    `neg_tv_right_continuous`, `total_variation_opp`,
-    `total_variation_left_continuous`, `total_variation_continuous`
-
 ### Changed
 
-- in `topology.v`:
-  + lemmas `nbhsx_ballx` and `near_ball` take a parameter of type `R` instead of `{posnum R}`
-  + lemma `pointwise_compact_cvg`
-
 ### Renamed
 
 ### Generalized
 
-- in `realfun.v`:
-  + lemmas `nonincreasing_at_right_cvgr`, `nonincreasing_at_left_cvgr`
-  + lemmas `nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`,
-    `nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge`
-
-- in `realfun.v`:
-  + lemmas `nonincreasing_at_right_is_cvgr`, `nondecreasing_at_right_is_cvgr`
-
 ### Deprecated
 
 ### Removed

diff --git a/INSTALL.md b/INSTALL.md
@@ -3,10 +3,10 @@
 ## Requirements
 
 - [The Coq Proof Assistant version ≥ 8.15](https://coq.inria.fr)
-- [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp)
-  + except `coq-mathcomp-solvable` ≥ 1.17.0
+- [Mathematical Components version ≥ 1.17.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
 - [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder)
+- [bigenough >= 1.0.0](https://github.com/math-comp/bigenough)
 
 These requirements can be installed in a custom way, or through
 [opam](https://opam.ocaml.org/) (the recommended way) using
@@ -48,7 +48,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.6.7
+$ opam install coq-mathcomp-analysis.0.7.0
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
@@ -71,7 +71,7 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
 
-With the example of Coq 8.15.0 and MathComp 1.13.0. For other versions, update the
+With the example of Coq 8.15.0 and MathComp 1.17.0. For other versions, update the
 version numbers accordingly.
 
 1. Install Coq 8.15.0
@@ -80,11 +80,11 @@ $ opam install coq.8.15.0
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.1.13.0
-$ opam install coq-mathcomp-fingroup.1.13.0
-$ opam install coq-mathcomp-algebra.1.13.0
-$ opam install coq-mathcomp-solvable.1.13.0
-$ opam install coq-mathcomp-field.1.13.0
+$ opam install coq-mathcomp-ssreflect.1.17.0
+$ opam install coq-mathcomp-fingroup.1.17.0
+$ opam install coq-mathcomp-algebra.1.17.0
+$ opam install coq-mathcomp-solvable.1.17.0
+$ opam install coq-mathcomp-field.1.17.0
 ```
 3. Install the Finite maps library
 ```