diff options
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 97ee41a..a1b0b78 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -21,7 +21,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Added theorems `ffact_prod`, `prime_modn_expSn` and `fermat_little` in `binomial.v` -- Added theorems `flatten_map1` and `allpairs_consr` in `seq.v`. +- Added theorems `flatten_map1`, `allpairs_consr`, and `mask_filter` in `seq.v`. - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`. @@ -32,6 +32,27 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Arithmetic theorems: `modn_divl` and `divn_modl`. +- Added map/parametricity theorems about `path`, `sort` and `sorted`: + +- Added `mem2E` in `path.v`. + +- 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`. + +- 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`. + ### Changed - `eqVneq` lemma is changed from `{x = y} + {x != y}` to @@ -45,6 +66,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - 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`. + ### Infrastructure - `Makefile` now supports the `test-suite` and `only` targets. Currently, |