Sorting algorithms on lists #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we define
list.sorted r l to be an alias for
pairwise r l. This alias is preferred
in the case that
r is a
≤-like relation. Then we define two sorting algorithms:
list.merge_sort, and prove their correctness.
sorted r l is the same as
pairwise r l, preferred in the case that
≤-like relation (transitive and antisymmetric or asymmetric)
A tuple is monotone if and only if the list obtained from it is sorted.
The list obtained from a monotone tuple is sorted.
ordered_insert a l inserts
l at such that
ordered_insert a l is sorted if
insertion_sort l returns
l sorted using the insertion sort algorithm.
An alternative definition of
l is already
list.sorted with respect to
insertion_sort does not change
l into two lists of approximately equal length.
split [1, 2, 3, 4, 5] = ([1, 3, 5], [2, 4])
Merge two sorted lists into one in linear time.
merge [1, 2, 4, 5] [0, 1, 3, 4] = [0, 1, 1, 2, 3, 4, 4, 5]
Implementation of a merge sort algorithm to sort a list.