Sorting algorithms on lists #
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.mergeSort, and prove their correctness.
Insertion sort #
An alternative definition of
Merge sort #
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]