Commit 2024-10-25 01:40 87ee1f25

View on Github →

chore: cleanup of mergeSort' (#16902) This PR removes the old mergeSort' in Mathlib (which was not a stable sort algorithm), replacing all uses with the stable mergeSort from Lean, mostly preserving the API.

Estimated changes

Modified Mathlib/Data/List/Sort.lean

added theorem List.Sorted.decide

modified theorem List.Sorted.merge

deleted theorem List.length_mergeSort'

deleted theorem List.length_split_fst_le

deleted theorem List.length_split_le

deleted theorem List.length_split_lt

deleted theorem List.length_split_snd_le

deleted theorem List.map_mergeSort'

deleted theorem List.map_split

deleted theorem List.mem_mergeSort'

deleted theorem List.mem_split_iff

deleted def List.mergeSort'

deleted theorem List.mergeSort'_cons_cons

deleted theorem List.mergeSort'_eq_insertionSort

deleted theorem List.mergeSort'_eq_self

deleted theorem List.mergeSort'_nil

deleted theorem List.mergeSort'_singleton

added theorem List.mergeSort_eq_insertionSort

added theorem List.mergeSort_eq_self

deleted theorem List.perm_mergeSort'

deleted theorem List.perm_split

modified theorem List.sorted_mergeSort'

deleted def List.split

deleted theorem List.split_cons_of_eq

Modified Mathlib/Data/Multiset/Sort.lean

modified theorem Multiset.coe_sort

Modified Mathlib/Logic/Equiv/List.lean

Modified Mathlib/Order/Defs.lean