diff --git a/CHANGELOG.md b/CHANGELOG.md index 2dc9f65c9..445d1fb7a 100644 --- 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 index 06fa683ac..67bb43c3b 100644 --- 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 index 000e07ad1..088565513 100644 --- 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 ``` diff --git a/README.md b/README.md index 2278a5a77..c5c087342 100644 --- a/README.md +++ b/README.md @@ -35,11 +35,11 @@ the Coq proof-assistant and using the Mathematical Components library. - License: [CeCILL-C](LICENSE) - Compatible Coq versions: Coq 8.15 to 8.18 (or dev) - Additional dependencies: - - [MathComp ssreflect 1.13 or later](https://math-comp.github.io) - - [MathComp fingroup 1.13 or later](https://math-comp.github.io) - - [MathComp algebra 1.13 or later](https://math-comp.github.io) - - [MathComp solvable 1.15 or later](https://math-comp.github.io) - - [MathComp field 1.13 or later](https://math-comp.github.io) + - [MathComp ssreflect 1.17 or later](https://math-comp.github.io) + - [MathComp fingroup 1.17 or later](https://math-comp.github.io) + - [MathComp algebra 1.17 or later](https://math-comp.github.io) + - [MathComp solvable 1.17 or later](https://math-comp.github.io) + - [MathComp field 1.17 or later](https://math-comp.github.io) - [MathComp finmap 1.5.1](https://github.com/math-comp/finmap) - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough) - [Hierarchy Builder >= 1.2.0](https://github.com/math-comp/hierarchy-builder)