Sorting algorithms on lists #
In this file we define List.Sorted r l
to be an alias for List.Pairwise r l
.
This alias is preferred in the case that r
is a <
or ≤
-like relation.
Then we define two sorting algorithms:
List.insertionSort
and List.mergeSort
, and prove their correctness.
The predicate List.Sorted
#
Sorted r l
is the same as List.Pairwise r l
, preferred in the case that r
is a <
or ≤
-like relation (transitive and antisymmetric or asymmetric)
Equations
Instances For
Equations
- l.decidableSorted = l.instDecidablePairwise
The list List.ofFn f
is strictly sorted with respect to (· ≤ ·)
if and only if f
is
strictly monotone.
The list obtained from a monotone tuple is sorted.
Insertion sort #
orderedInsert a l
inserts a
into l
at such that
orderedInsert a l
is sorted if l
is.
Equations
- List.orderedInsert r a [] = [a]
- List.orderedInsert r a (b :: l) = if r a b then a :: b :: l else b :: List.orderedInsert r a l
Instances For
insertionSort l
returns l
sorted using the insertion sort algorithm.
Equations
- List.insertionSort r [] = []
- List.insertionSort r (b :: l) = List.orderedInsert r b (List.insertionSort r l)
Instances For
An alternative definition of orderedInsert
using takeWhile
and dropWhile
.
If l
is already List.Sorted
with respect to r
, then insertionSort
does not change
it.
For a reflexive relation, insert then erasing is the identity.
Inserting then erasing an element that is absent is the identity.
For an antisymmetric relation, erasing then inserting is the identity.
The list List.insertionSort r l
is List.Sorted
with respect to r
.
Merge sort #
Implementation of a merge sort algorithm to sort a list.
Equations
- List.mergeSort r [] = []
- List.mergeSort r [a] = [a]
- List.mergeSort r (a :: b :: l) = List.merge (fun (x x_1 : α) => decide (r x x_1)) (List.mergeSort r (a :: b :: l).split.1) (List.mergeSort r (a :: b :: l).split.2)