diff options
| author | Kazuhiko Sakaguchi | 2020-11-13 11:30:59 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-11-19 05:24:58 +0900 |
| commit | b3d31c4b66581c78ce23b7fc2e76b41a1a4adf60 (patch) | |
| tree | 2d435d1b99a06dabd7e6a0091769004f8d8215eb /CHANGELOG_UNRELEASED.md | |
| parent | 0606b6bf22e258dc3b7cf440f10c108f785904b5 (diff) | |
Refactor, reshuffle, and rename sorting lemmas in `path.v`
- Lemmas `sorted_(lt|le)_nth` have been renamed to `sorted_(ltn|leq)_nth`.
- Lemmas `(ltn|leq)_index` have been renamed to `sorted_(ltn|leq)_index` and
generalized for non-`eqType`s.
- Lemmas `order_path_min`, `path_sortedE`, `subseq_order_path`, `subseq_sorted`,
`sorted_uniq`, `sorted_eq`, `irr_sorted_eq`, `sorted_(ltn|leq)_nth`, and
`sorted_(ltn|leq)_index` have been relocated since their proofs are
independent from `merge` and `sort`.
- The stability proofs for `iota` sequences (`push_stable`, `pop_stable`, and
`sort_iota_stable`) have been simplified by sorting out their hypotheses and
by redefining `push_invariant` to include the `sorted` condition. Their main
result `sort_iota_stable`, formerly a local `Let` to prove `sort_stable`, has
been turned into a lemma.
- Some stability proofs for general sequences (`sort_stable` and `filter_sort`)
have also been simplified, of which the former one uses the above
`sorted_ltn_nth` lemma for a non-`eqType`.
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ac8ce25..58eb93d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -276,6 +276,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `(path|sorted)_(mask|filter)_in`, `rev_cycle`, `cycle_map`, `(homo|mono)_cycle(_in)`. +- in `path.v`, new lemma `sort_iota_stable`. + - in `seq.v` new lemmas `index_pivot`, `take_pivot`, `rev_pivot`, `eqseq_pivot2l`, `eqseq_pivot2r`, `eqseq_pivotl`, `eqseq_pivotr` `uniq_eqseq_pivotl`, `uniq_eqseq_pivotr`, `mask_rcons`, `rev_mask`, @@ -366,6 +368,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, generalized lemmas `sub_path_in`, `sub_sorted_in`, and `eq_path_in` for non-`eqType`s. +- in `path.v`, generalized lemmas `sorted_ltn_nth` and `sorted_leq_nth` + (formerly `sorted_lt_nth` and `sorted_le_nth`, cf Renamed section) for + non-`eqType`s. + - in `order.v`, generalized `sort_le_id` for any `porderType`. ### Renamed @@ -415,7 +421,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). (`allpairs_consr` and `allpairs_catr` are now deprecated alias, and will be attributed to the new `perm_allpairs_catr`). -- in `path.v`, `eq_sorted(_irr)` -> `(irr_)sorted_eq` +- in `path.v`, + + `eq_sorted(_irr)` -> `(irr_)sorted_eq` + + `sorted_(lt|le)_nth` -> `sorted_(ltn|leq)_nth` + + `(ltn|leq)_index` -> `sorted_(ltn|leq)_index` - in `div.v` + `coprime_mul(l|r)` -> `coprimeM(l|r)` |