diff --git a/CHANGELOG.md b/CHANGELOG.md index 2dc9f65c9..bf0a8172d 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 42c6eb1ca..2d1ba5e50 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,266 +4,18 @@ ### Added -- in file `cantor.v`, - + new definitions `cantor_space`, `cantor_like`, `pointed_discrete`, and - `tree_of`. - + new lemmas `cantor_space_compact`, `cantor_space_hausdorff`, - `cantor_zero_dimensional`, `cantor_perfect`, `cantor_like_cantor_space`, - `tree_map_props`, `homeomorphism_cantor_like`, and - `cantor_like_finite_prod`. - + new theorem `cantor_surj`. -- in file `topology.v`, - + new lemmas `perfect_set2`, and `ent_closure`. - + lemma `clopen_surj` - - in `cantor.v`: + definitions `pointed_principal_filter`, `pointed_discrete_topology` + lemma `discrete_pointed` + lemma `discrete_bool_compact` -- in `normedtype.v`: - + hints for `at_right_proper_filter` and `at_left_proper_filter` - -- in `realfun.v`: - + notations `nondecreasing_fun`, `nonincreasing_fun`, - `increasing_fun`, `decreasing_fun` - + lemmas `cvg_addrl`, `cvg_addrr`, `cvg_centerr`, `cvg_shiftr`, - `nondecreasing_cvgr`, - `nonincreasing_at_right_cvgr`, - `nondecreasing_at_right_cvgr`, - `nondecreasing_cvge`, `nondecreasing_is_cvge`, - `nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`, - `nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge` -- in `ereal.v`: - + lemmas `ereal_sup_le`, `ereal_inf_le` - -- in `normedtype.v`: - + definition `lower_semicontinuous` - + lemma `lower_semicontinuousP` - -- in `numfun.v`: - + lemma `patch_indic` - -- in `lebesgue_measure.v` - + lemma `lower_semicontinuous_measurable` - -- in `lebesgue_integral.v`: - + definition `locally_integrable` - + lemmas `integrable_locally`, `locally_integrableN`, `locally_integrableD`, - `locally_integrableB` - + definition `iavg` - + lemmas `iavg0`, `iavg_ge0`, `iavg_restrict`, `iavgD` - + definitions `HL_maximal` - + lemmas `HL_maximal_ge0`, `HL_maximalT_ge0`, - `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`, - `maximal_inequality` - -- in file `measure.v` - + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`. - -- in `charge.v` - + definition `charge_of_finite_measure` (instance of `charge`) - + lemmas `dominates_cscalel`, `dominates_cscaler` - + definition `cpushforward` (instance of `charge`) - + lemma `dominates_pushforward` - + lemma `cjordan_posE` - + lemma `jordan_posE` - + lemma `cjordan_negE` - + lemma `jordan_negE` - + lemma `Radon_Nikodym_sigma_finite` - + lemma `Radon_Nikodym_fin_num` - + lemma `Radon_Nikodym_integral` - + lemma `ae_eq_Radon_Nikodym_SigmaFinite` - + lemma `Radon_Nikodym_change_of_variables` - + lemma `Radon_Nikodym_cscale` - + lemma `Radon_Nikodym_cadd` - + lemma `Radon_Nikodym_chain_rule` - -- in `sequences.v`: - + lemma `minr_cvg_0_cvg_0` - + lemma `mine_cvg_0_cvg_fin_num` - + lemma `mine_cvg_minr_cvg` - + lemma `mine_cvg_0_cvg_0` - + lemma `maxr_cvg_0_cvg_0` - + lemma `maxe_cvg_0_cvg_fin_num` - + lemma `maxe_cvg_maxr_cvg` - + lemma `maxe_cvg_0_cvg_0` -- in `constructive_ereal.v` - + lemma `lee_subgt0Pr` - -- in `topology.v`: - + lemma `nbhs_dnbhs_neq` - -- in `normedtype.v`: - + lemma `not_near_at_rightP` - -- in `realfun.v`: - + lemma `cvg_at_right_left_dnbhs` - + lemma `cvg_at_rightP` - + lemma `cvg_at_leftP` - + lemma `cvge_at_rightP` - + lemma `cvge_at_leftP` - + lemma `lime_sup` - + lemma `lime_inf` - + lemma `lime_supE` - + lemma `lime_infE` - + lemma `lime_infN` - + lemma `lime_supN` - + lemma `lime_sup_ge0` - + lemma `lime_inf_ge0` - + lemma `lime_supD` - + lemma `lime_sup_le` - + lemma `lime_inf_sup` - + lemma `lim_lime_inf` - + lemma `lim_lime_sup` - + lemma `lime_sup_inf_at_right` - + lemma `lime_sup_inf_at_left` - -- in `normedtype.v`: - + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP` - + lemma `dnbhsN` - + lemma `limf_esup_dnbhsN` - -- in `topology.v`: - + lemma `dnbhs_ball` - -- in `normedtype.v` - + definitions `limf_esup`, `limf_einf` - + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN` - -- in `sequences.v`: - + lemmas `limn_esup_lim`, `limn_einf_lim` - -- in `realfun.v`: - + lemmas `lime_sup_lim`, `lime_inf_lim` - -- in `boolp.v`: - + tactic `eqProp` - + variant `BoolProp` - + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`, - `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`, - `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`, - `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`, - `inhabitedE`, `inhabited_witness` -- 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 fb7ee64fb..088565513 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -2,11 +2,11 @@ ## Requirements -- [The Coq Proof Assistant version ≥ 8.14](https://coq.inria.fr) -- [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp) - + except `coq-mathcomp-solvable` ≥ 1.15.0 +- [The Coq Proof Assistant version ≥ 8.15](https://coq.inria.fr) +- [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,20 +71,20 @@ 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.14.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.14.0 +1. Install Coq 8.15.0 ``` -$ opam install coq.8.14.0 +$ 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 a7dbff5d4..a0e4e9569 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.14 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)