diff options
| -rw-r--r-- | CHANGELOG.md | 183 | ||||
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 166 |
2 files changed, 182 insertions, 167 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md index f8c3221..115e397 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,9 +1,190 @@ # Changelog All notable changes to this project will be documented in this file. -Last releases: [[1.9.0] - 2019-05-22](#190---2019-05-22) and [[1.8.0] - 2019-04-08](#180---2019-04-08). +Last releases: [[1.10.0] - 2019-11-29](#1100---2019-29-22) and [[1.9.0] - 2019-05-22](#190---2019-05-22). The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). +## [1.10.0] - 2019-11-29 + +This release is compatible with Coq versions 8.9 and 8.10. + +### Added + +- Added a `void` notation for the `Empty_set` type of the standard library, the + canonical injection `of_void` and its cancellation lemma `of_voidK`, and + `eq`, `choice`, `count` and `fin` instances. + +- Added `ltn_ind` general induction principle for `nat` variables, helper lemmas `ubnP`, `ltnSE`, ubnPleq, ubnPgeq and ubnPeq, in support of a generalized induction idiom for `nat` measures that does not rely on the `{-2}` numerical occurrence selector, and purged this idiom from the `mathcomp` library (see below). + +- Added fixpoint and cofixpoint constructions to `finset`: `fixset`, + `cofixset` and `fix_order`, with a few theorems about them + +- Added functions `tuple_of_finfun`, `finfun_of_tuple`, and their + "cancellation" lemmas. + +- Added theorems `totient_prime` and `Euclid_dvd_prod` in `prime.v` + +- Added theorems `ffact_prod`, `prime_modn_expSn` and `fermat_little` + in `binomial.v` + +- Added theorems `flatten_map1`, `allpairs_consr`, `mask_filter`, + `all_filter`, `all_pmap`, and `all_allpairsP` in `seq.v`. + +- Added theorems `nth_rcons_default`, `undup_rcons`, `undup_cat` and + `undup_flatten_nseq` in `seq.v` + +- Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, + `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`, + `existsPn`, `exists_inPn`, `forallPn`, `forall_inPn`, + `eq_enum_rank_in`, `enum_rank_in_inj`, `lshift_inj`, and + `rshift_inj`. + +- Bigop theorems: `index_enum_uniq`, `big_rmcond`, `bigD1_seq`, + `big_enum_val_cond`, `big_enum_rank_cond`, + `big_enum_val`, `big_enum_rank`, `big_set`, + `big_enumP`, `big_enum_cond`, `big_enum` + +- Arithmetic theorems in ssrnat and div: + - some trivial results in ssrnat: `ltn_predL`, `ltn_predRL`, + `ltn_subrR`, `leq_subrR`, `ltn_subrL` and `predn_sub`, + - theorems about `n <=/< p +/- m` and `m +/- n <=/< p`: + `leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`, `leq_subCl`, + `leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and + `ltn_subCl`, + - some commutations between modulo and division: `modn_divl` and + `divn_modl`, + - theorems about the euclidean division of additions and subtraction, + + without preconditions of divisibility: `edivnD`, `edivnB`, + `divnD`, `divnB`, `modnD`, `modnB`, + + with divisibility of one argument: `divnDMl`, `divnMBl`, + `divnBMl`, `divnBl` and `divnBr`, + + specialization of the former theorems for .+1 and .-1: + `edivnS`, `divnS`, `modnS`, `edivn_pred`, `divn_pred` and + `modn_pred`. + +- Added `sort_rec1` and `sortE` to help inductive reasoning on `sort`. + +- Added map/parametricity theorems about `path`, `sort`, and `sorted`: + `homo_path`, `mono_path`, `homo_path_in`, `mono_path_in`, + `homo_sorted`, `mono_sorted`, `map_merge`, `merge_map`, `map_sort`, + `sort_map`, `sorted_map`, `homo_sorted_in`, `mono_sorted_in`. + +- Extracting lemma `fpathE` from `fpathP`, and shortening the proof of + the latter. + +- Added the theorem `perm_iota_sort` to express that the sorting of + any sequence `s` is equal to a mapping of `iota 0 (size s)` to the + nth elements of `s`, so that one can still reason on `nat`, even + though the elements of `s` are not in an `eqType`. + +- Added stability theorems about `merge` and `sort`: `sorted_merge`, + `merge_stable_path`, `merge_stable_sorted`, `sorted_sort`, `sort_stable`, + `filter_sort`, `mask_sort`, `sorted_mask_sort`, `subseq_sort`, + `sorted_subseq_sort`, and `mem2_sort`. + +- New algebraic interfaces in `ssralg.v`: comAlgebra and + comUnitAlgebra for commutative and commutative-unitary algebras. + +- Initial property for polynomials in algebras: + New canonical lrMoprphism `horner_alg` evaluating a polynomial in an element + of an algebra. The theory include the lemmas `in_alg_comm`, `horner_algC`, + `horner_algX`, `poly_alg_initial`. + +- Added lemmas on commutation with difference, big sum and prod: + `commrB`, `commr_sum`, `commr_prod`. + +- Added a few basic seq lemmas about `nseq`, `take` and `drop`: + `nseq_addn`, `take_take`, `take_drop`, `take_addn`, `takeC`, + `take_nseq`, `drop_nseq`, `rev_nseq`, `take_iota`, `drop_iota`. + +- Added ssrfun theorem `inj_compr`. + +- Added theorems `mem2E`, `nextE`, `mem_fcycle`, `inj_cycle`, + `take_traject`, `trajectD` and `cycle_catC` in `path.v` + +- Added lemmas about `cycle`, `connect`, `fconnect`, `order` and + `orbit` in `fingraph.v`: + - lemma `connect_cycle`, + - lemmas `in_orbit`, `order_gt0`, `findex_eq0`, `mem_orbit`, + `image_orbit`, + - lemmas `fcycle_rconsE`, `fcycle_consE`, `fcycle_consEflatten` and + `undup_cycle_cons` which operate under the precondition that the + sequence `x :: p` is a cycle for f (i.e. `fcycle f (x :: p)`). + - lemmas which operate under the precondition there is a sequence + `p` which is a cycle for `f` (i.e. `fcycle f p`): + `order_le_cycle`, `finv_cycle`, `f_finv_cycle`, `finv_f_cycle`, + `finv_inj_cycle`, `iter_finv_cycle`, `cycle_orbit_cycle`, + `fpath_finv_cycle`, `fpath_finv_f_cycle`, `fpath_f_finv_cycle`, + `prevE`, `fcycleEflatten`, `fcycle_undup`, `in_orbit_cycle`, + `eq_order_cycle`, `iter_order_cycle`, + - lemmas `injectivePcycle`, `orbitPcycle`, `fconnect_eqVf`, + `order_id_cycle`, `orderPcycle`, `fconnect_f`, `fconnect_findex`. + +- Added lemma `rot_index` which explicits the index given by `rot_to`. + +- Added tactic `tfae` to split an equivalence between n+1 propositions + into n+1 goals, and referenced orbitPcycle as a reference of use. + +### Changed + +- Replaced the legacy generalised induction idiom with a more robust one +that does not rely on the `{-2}` numerical occurrence selector, using +new `ssrnat` helper lemmas `ltn_ind`, `ubnP`, `ubnPleq`, ...., (see above). The new idiom is documented in `ssrnat`. + This change anticipates an expected evolution of `fintype` to integrate `finmap`. It is likely that the new definition of the `#|A|` notation will hide multiple occurrences of `A`, which will break the `{-2}` induction idiom. Client libraries should update before the 1.11 release (see [PR #434](https://github.com/math-comp/math-comp/pull/434) for examples). + + - Replaced the use of the accidental convertibility between `enum A` and + `filter A (index_enum T)` with more explicit lemmas `big_enumP`, `big_enum`, `big_enum_cond`, `big_image` added to the `bigop` library, and deprecated the `filter_index_enum` lemma that states the corresponding equality. Both convertibility and equality may no longer hold in future `mathcomp` releases when sets over `finType`s are generalised to finite sets over `choiceType`s, so client libraries should stop relying on this identity. File `bigop.v` has some boilerplate to help with the port; also see [PR #441](https://github.com/math-comp/math-comp/pull/441) for examples. + + - Restricted `big_image`, `big_image_cond`, `big_image_id` and `big_image_cond_id` + to `bigop`s over _abelian_ monoids, anticipating the change in the definition of `enum`. This may introduce some incompatibilities - non-abelian instances should be dealt with a combination of `big_map` and `big_enumP`. + +- `eqVneq` lemma is changed from `{x = y} + {x != y}` to + `eq_xor_neq x y (y == x) (x == y)`, on which a case analysis performs + simultaneous replacement of expressions of the form `x == y` and `y == x` + by `true` or `false`, while keeping the ability to use it in the way + it was used before. + +- Generalized the `allpairs_catr` lemma to the case where the types of `s`, + `t1`, and `t2` are non-`eqType`s in `[seq E | i <- s, j <- t1 ++ t2]`. + +- Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`. + +- Generalized `sort` to non-`eqType`s (as well as `merge`, + `merge_sort_push`, `merge_sort_pop`), together with all the lemmas + that did not really rely on an `eqType`: `size_merge`, `size_sort`, + `merge_path`, `merge_sorted`, `sort_sorted`, `path_min_sorted` + (which statement was modified to remove the dependency in `eqType`), + and `order_path_min`. + +- `compare_nat` type family and `ltngtP` comparison predicate are changed + from `compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)` + to `compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`, + to make it tries to match subterms with `m < n` first, `m <= n`, then + `m == n`. + + The compatibility layer for the version 1.9 is provided as the + `ssrnat.mc_1_9` module. One may compile proofs compatible with the version + 1.9 in newer versions by using this module. + +- Moved `iter_in` to ssrnat and reordered its arguments. + +- Notation `[<-> P0 ; .. ; Pn]` now forces `Pi` to be of type `Prop`. + +### Removed + +- `fin_inj_bij` lemma is removed as a duplicate of `injF_bij` lemma + from `fintype` library. + +### Infrastructure + +- `Makefile` now supports the `test-suite` and `only` targets. Currently, + `make test-suite` will verify the implementation of mathematical structures + and their inheritances of MathComp automatically, by using the `hierarchy.ml` + utility. One can use the `only` target to build the sub-libraries of MathComp + specified by the `TGTS` variable, e.g., + `make only TGTS="ssreflect/all_ssreflect.vo fingroup/all_fingroup.vo"`. + +- `Makefile`now supports a `doc` target to build the documentation as made + available on https://mathcomp.github.io/htmldoc/index.html ## [1.9.0] - 2019-05-22 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 045733d..b429e78 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,175 +10,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Added -- Added a `void` notation for the `Empty_set` type of the standard library, the - canonical injection `of_void` and its cancellation lemma `of_voidK`, and - `eq`, `choice`, `count` and `fin` instances. - -- Added `ltn_ind` general induction principle for `nat` variables, helper lemmas `ubnP`, `ltnSE`, ubnPleq, ubnPgeq and ubnPeq, in support of a generalized induction idiom for `nat` measures that does not rely on the `{-2}` numerical occurrence selector, and purged this idiom from the `mathcomp` library (see below). - -- Added fixpoint and cofixpoint constructions to `finset`: `fixset`, - `cofixset` and `fix_order`, with a few theorems about them - -- Added functions `tuple_of_finfun`, `finfun_of_tuple`, and their - "cancellation" lemmas. - -- Added theorems `totient_prime` and `Euclid_dvd_prod` in `prime.v` - -- Added theorems `ffact_prod`, `prime_modn_expSn` and `fermat_little` - in `binomial.v` - -- Added theorems `flatten_map1`, `allpairs_consr`, `mask_filter`, - `all_filter`, `all_pmap`, and `all_allpairsP` in `seq.v`. - -- Added theorems `nth_rcons_default`, `undup_rcons`, `undup_cat` and - `undup_flatten_nseq` in `seq.v` - -- Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, - `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`, - `existsPn`, `exists_inPn`, `forallPn`, `forall_inPn`, - `eq_enum_rank_in`, `enum_rank_in_inj`, `lshift_inj`, and - `rshift_inj`. - -- Bigop theorems: `index_enum_uniq`, `big_rmcond`, `bigD1_seq`, - `big_enum_val_cond`, `big_enum_rank_cond`, - `big_enum_val`, `big_enum_rank`, `big_set`, - `big_enumP`, `big_enum_cond`, `big_enum` - -- Arithmetic theorems in ssrnat and div: - - some trivial results in ssrnat: `ltn_predL`, `ltn_predRL`, - `ltn_subrR`, `leq_subrR`, `ltn_subrL` and `predn_sub`, - - theorems about `n <=/< p +/- m` and `m +/- n <=/< p`: - `leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`, `leq_subCl`, - `leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and - `ltn_subCl`, - - some commutations between modulo and division: `modn_divl` and - `divn_modl`, - - theorems about the euclidean division of additions and subtraction, - + without preconditions of divisibility: `edivnD`, `edivnB`, - `divnD`, `divnB`, `modnD`, `modnB`, - + with divisibility of one argument: `divnDMl`, `divnMBl`, - `divnBMl`, `divnBl` and `divnBr`, - + specialization of the former theorems for .+1 and .-1: - `edivnS`, `divnS`, `modnS`, `edivn_pred`, `divn_pred` and - `modn_pred`. - -- Added `sort_rec1` and `sortE` to help inductive reasoning on `sort`. - -- Added map/parametricity theorems about `path`, `sort`, and `sorted`: - `homo_path`, `mono_path`, `homo_path_in`, `mono_path_in`, - `homo_sorted`, `mono_sorted`, `map_merge`, `merge_map`, `map_sort`, - `sort_map`, `sorted_map`, `homo_sorted_in`, `mono_sorted_in`. - -- Extracting lemma `fpathE` from `fpathP`, and shortening the proof of - the latter. - -- Added the theorem `perm_iota_sort` to express that the sorting of - any sequence `s` is equal to a mapping of `iota 0 (size s)` to the - nth elements of `s`, so that one can still reason on `nat`, even - though the elements of `s` are not in an `eqType`. - -- Added stability theorems about `merge` and `sort`: `sorted_merge`, - `merge_stable_path`, `merge_stable_sorted`, `sorted_sort`, `sort_stable`, - `filter_sort`, `mask_sort`, `sorted_mask_sort`, `subseq_sort`, - `sorted_subseq_sort`, and `mem2_sort`. - -- New algebraic interfaces in `ssralg.v`: comAlgebra and - comUnitAlgebra for commutative and commutative-unitary algebras. - -- Initial property for polynomials in algebras: - New canonical lrMoprphism `horner_alg` evaluating a polynomial in an element - of an algebra. The theory include the lemmas `in_alg_comm`, `horner_algC`, - `horner_algX`, `poly_alg_initial`. - -- Added lemmas on commutation with difference, big sum and prod: - `commrB`, `commr_sum`, `commr_prod`. - -- Added a few basic seq lemmas about `nseq`, `take` and `drop`: - `nseq_addn`, `take_take`, `take_drop`, `take_addn`, `takeC`, - `take_nseq`, `drop_nseq`, `rev_nseq`, `take_iota`, `drop_iota`. - -- Added ssrfun theorem `inj_compr`. - -- Added theorems `mem2E`, `nextE`, `mem_fcycle`, `inj_cycle`, - `take_traject`, `trajectD` and `cycle_catC` in `path.v` - -- Added lemmas about `cycle`, `connect`, `fconnect`, `order` and - `orbit` in `fingraph.v`: - - lemma `connect_cycle`, - - lemmas `in_orbit`, `order_gt0`, `findex_eq0`, `mem_orbit`, - `image_orbit`, - - lemmas `fcycle_rconsE`, `fcycle_consE`, `fcycle_consEflatten` and - `undup_cycle_cons` which operate under the precondition that the - sequence `x :: p` is a cycle for f (i.e. `fcycle f (x :: p)`). - - lemmas which operate under the precondition there is a sequence - `p` which is a cycle for `f` (i.e. `fcycle f p`): - `order_le_cycle`, `finv_cycle`, `f_finv_cycle`, `finv_f_cycle`, - `finv_inj_cycle`, `iter_finv_cycle`, `cycle_orbit_cycle`, - `fpath_finv_cycle`, `fpath_finv_f_cycle`, `fpath_f_finv_cycle`, - `prevE`, `fcycleEflatten`, `fcycle_undup`, `in_orbit_cycle`, - `eq_order_cycle`, `iter_order_cycle`, - - lemmas `injectivePcycle`, `orbitPcycle`, `fconnect_eqVf`, - `order_id_cycle`, `orderPcycle`, `fconnect_f`, `fconnect_findex`. - -- Added lemma `rot_index` which explicits the index given by `rot_to`. - -- Added tactic `tfae` to split an equivalence between n+1 propositions - into n+1 goals, and referenced orbitPcycle as a reference of use. - ### Changed -- Replaced the legacy generalised induction idiom with a more robust one -that does not rely on the `{-2}` numerical occurrence selector, using -new `ssrnat` helper lemmas `ltn_ind`, `ubnP`, `ubnPleq`, ...., (see above). The new idiom is documented in `ssrnat`. - This change anticipates an expected evolution of `fintype` to integrate `finmap`. It is likely that the new definition of the `#|A|` notation will hide multiple occurrences of `A`, which will break the `{-2}` induction idiom. Client libraries should update before the 1.11 release (see [PR #434](https://github.com/math-comp/math-comp/pull/434) for examples). - - - Replaced the use of the accidental convertibility between `enum A` and - `filter A (index_enum T)` with more explicit lemmas `big_enumP`, `big_enum`, `big_enum_cond`, `big_image` added to the `bigop` library, and deprecated the `filter_index_enum` lemma that states the corresponding equality. Both convertibility and equality may no longer hold in future `mathcomp` releases when sets over `finType`s are generalised to finite sets over `choiceType`s, so client libraries should stop relying on this identity. File `bigop.v` has some boilerplate to help with the port; also see [PR #441](https://github.com/math-comp/math-comp/pull/441) for examples. - - - Restricted `big_image`, `big_image_cond`, `big_image_id` and `big_image_cond_id` - to `bigop`s over _abelian_ monoids, anticipating the change in the definition of `enum`. This may introduce some incompatibilities - non-abelian instances should be dealt with a combination of `big_map` and `big_enumP`. - -- `eqVneq` lemma is changed from `{x = y} + {x != y}` to - `eq_xor_neq x y (y == x) (x == y)`, on which a case analysis performs - simultaneous replacement of expressions of the form `x == y` and `y == x` - by `true` or `false`, while keeping the ability to use it in the way - it was used before. - -- Generalized the `allpairs_catr` lemma to the case where the types of `s`, - `t1`, and `t2` are non-`eqType`s in `[seq E | i <- s, j <- t1 ++ t2]`. - -- Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`. - -- Generalized `sort` to non-`eqType`s (as well as `merge`, - `merge_sort_push`, `merge_sort_pop`), together with all the lemmas - that did not really rely on an `eqType`: `size_merge`, `size_sort`, - `merge_path`, `merge_sorted`, `sort_sorted`, `path_min_sorted` - (which statement was modified to remove the dependency in `eqType`), - and `order_path_min`. - -- `compare_nat` type family and `ltngtP` comparison predicate are changed - from `compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)` - to `compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`, - to make it tries to match subterms with `m < n` first, `m <= n`, then - `m == n`. - + The compatibility layer for the version 1.9 is provided as the - `ssrnat.mc_1_9` module. One may compile proofs compatible with the version - 1.9 in newer versions by using this module. - -- Moved `iter_in` to ssrnat and reordered its arguments. - -- Notation `[<-> P0 ; .. ; Pn]` now forces `Pi` to be of type `Prop`. - ### Removed -- `fin_inj_bij` lemma is removed as a duplicate of `injF_bij` lemma - from `fintype` library. - ### Infrastructure -- `Makefile` now supports the `test-suite` and `only` targets. Currently, - `make test-suite` will verify the implementation of mathematical structures - and their inheritances of MathComp automatically, by using the `hierarchy.ml` - utility. One can use the `only` target to build the sub-libraries of MathComp - specified by the `TGTS` variable, e.g., - `make only TGTS="ssreflect/all_ssreflect.vo fingroup/all_fingroup.vo"`. |