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 /mathcomp/solvable | |
| 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 'mathcomp/solvable')
0 files changed, 0 insertions, 0 deletions