diff --git a/CHANGELOG.md b/CHANGELOG.md index c53e570a9..2dc9f65c9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,196 @@ # Changelog -Latest releases: [[0.6.6] - 2023-11-14](#066---2023-11-14) and [[0.6.5] - 2023-10-02](#065---2023-10-02) +Latest releases: [[0.6.7] - 2024-01-09](#067---2024-01-09) and [[0.6.6] - 2023-11-14](#066---2023-11-14) + +## [0.6.7] - 2024-01-09 + +### Added + +- 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 `topology.v`, + + new lemmas `perfect_set2`, and `ent_closure`. + + lemma `clopen_surj` + + lemma `nbhs_dnbhs_neq` + + lemma `dnbhs_ball` + +- in `constructive_ereal.v` + + lemma `lee_subgt0Pr` + +- in `ereal.v`: + + lemmas `ereal_sup_le`, `ereal_inf_le` + +- in `normedtype.v`: + + hints for `at_right_proper_filter` and `at_left_proper_filter` + + definition `lower_semicontinuous` + + lemma `lower_semicontinuousP` + + lemma `not_near_at_rightP` + + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP` + + lemma `dnbhsN` + + lemma `limf_esup_dnbhsN` + + definitions `limf_esup`, `limf_einf` + + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN` + +- 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` + + lemmas `limn_esup_lim`, `limn_einf_lim` + +- 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 `numfun.v`: + + lemma `patch_indic` + +- 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` + + 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` + + lemmas `lime_sup_lim`, `lime_inf_lim` + +- in file `measure.v` + + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`. + +- 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 `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` + +### Changed + +- in `boolp.v` + - lemmas `orC` and `andC` now use `commutative` + +- moved from `topology.v` to `mathcomp_extra.v` + + definition `monotonous` + +- in `normedtype.v`: + + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns + duplicate-free lists of indices + +- in `sequences.v`: + + change the implicit arguments of `trivIset_seqDU` + + `limn_esup` now defined from `lime_sup` + + `limn_einf` now defined from `limn_esup` + +- moved from `lebesgue_integral.v` to `measure.v`: + + definition `ae_eq` + + lemmas + `ae_eq0`, + `ae_eq_comp`, + `ae_eq_funeposneg`, + `ae_eq_refl`, + `ae_eq_trans`, + `ae_eq_sub`, + `ae_eq_mul2r`, + `ae_eq_mul2l`, + `ae_eq_mul1l`, + `ae_eq_abse` + +- in `charge.v` + + definition `jordan_decomp` now uses `cadd` and `cscale` + + definition `Radon_Nikodym_SigmaFinite` now in a module `Radon_Nikodym_SigmaFinite` with + * definition `f` + * lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral` + * lemma `change_of_variables` + * lemma `integralM` + * lemma `chain_rule` + +### Renamed + +- in `exp.v`: + + `lnX` -> `lnXn` + +- in `charge.v`: + + `dominates_caddl` -> `dominates_cadd` + +### Generalized + +- in `lebesgue_measure.v` + + an hypothesis of lemma `integral_ae_eq` is weakened + +- in `lebesgue_integral.v` + + `ge0_integral_bigsetU` generalized from `nat` to `eqType` + +### Removed + +- in `boolp.v`: + + lemma `pdegen` + +- in `forms.v`: + + lemmas `eq_map_mx`, `map_mx_id` ## [0.6.6] - 2023-11-14 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e14a1c9d5..971b02c98 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,209 +4,16 @@ ### 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 `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` - ### Changed - -- in `normedtype.v`: - + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns - duplicate-free lists of indices - -- moved from `lebesgue_integral.v` to `measure.v`: - + definition `ae_eq` - + lemmas - `ae_eq0`, - `ae_eq_comp`, - `ae_eq_funeposneg`, - `ae_eq_refl`, - `ae_eq_trans`, - `ae_eq_sub`, - `ae_eq_mul2r`, - `ae_eq_mul2l`, - `ae_eq_mul1l`, - `ae_eq_abse` - -- in `charge.v` - + definition `jordan_decomp` now uses `cadd` and `cscale` - + definition `Radon_Nikodym_SigmaFinite` now in a module `Radon_Nikodym_SigmaFinite` with - * definition `f` - * lemmas `f_ge0`, `f_fin_num`, `f_integrable`, `f_integral` - * lemma `change_of_variables` - * lemma `integralM` - * lemma `chain_rule` - -- in `sequences.v`: - + change the implicit arguments of `trivIset_seqDU` -- moved from `topology.v` to `mathcomp_extra.v` - + definition `monotonous` - -- in `sequences.v`: - + `limn_esup` now defined from `lime_sup` - + `limn_einf` now defined from `limn_esup` - --in `boolp.v` - - lemmas `orC` and `andC` now use `commutative` ### Renamed -- in `exp.v`: - + `lnX` -> `lnXn` -- in `charge.v`: - + `dominates_caddl` -> `dominates_cadd` - ### Generalized -- in `lebesgue_integral.v` - + `ge0_integral_bigsetU` generalized from `nat` to `eqType` -- in `lebesgue_measure.v` - + an hypothesis of lemma `integral_ae_eq` is weakened - ### Deprecated ### Removed -- in `forms.v`: - + lemmas `eq_map_mx`, `map_mx_id` - -- in `boolp.v`: - + lemma `pdegen` - - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 673be1e46..fb7ee64fb 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -4,6 +4,7 @@ - [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 - [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) @@ -47,7 +48,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.0.6.6 +$ opam install coq-mathcomp-analysis.0.6.7 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/README.md b/README.md index 4527098b4..a7dbff5d4 100644 --- a/README.md +++ b/README.md @@ -33,12 +33,12 @@ the Coq proof-assistant and using the Mathematical Components library. - Pierre-Yves Strub (initial) - Laurent Théry - License: [CeCILL-C](LICENSE) -- Compatible Coq versions: Coq 8.14 to 8.17 (or dev) +- 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.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 finmap 1.5.1](https://github.com/math-comp/finmap) - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough) @@ -80,7 +80,7 @@ own risk. ## Documentation Each file is documented in its header -([coqdoc presentation for the last version](https://math-comp.github.io/analysis/htmldoc_0_6_6/index.html)). +([coqdoc presentation for the last version](https://math-comp.github.io/analysis/htmldoc_0_6_7/index.html)). Changes are documented in [CHANGELOG.md](CHANGELOG.md) and [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md). @@ -93,6 +93,7 @@ Other work using MathComp-Analysis: - [A Formal Classical Proof of Hahn-Banach in Coq](https://lipn.univ-paris13.fr/~kerjean/slides/slidesTYPES19.pdf) (2019) - [Semantics of Probabilistic Programs using s-Finite Kernels in Coq](https://hal.inria.fr/hal-03917948/document) (2023) - [CoqQ: Foundational Verification of Quantum Programs](https://arxiv.org/pdf/2207.11350.pdf) (2023) +- [Experimenting with an intrinsically-typed probabilistic programming language in Coq](https://staff.aist.go.jp/reynald.affeldt/documents/syntax-aplas2023.pdf) (2023) ## Mathematical structures