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 the sorting algorithm
List.insertionSort
and prove its 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
If a list is sorted with respect to a decidable relation, then it is sorted with respect to the corresponding Bool-valued relation.
The list obtained from a monotone tuple is sorted.
The list obtained from an antitone tuple is sorted.
Insertion sort #
orderedInsert a l
inserts a
into l
at such that
orderedInsert a l
is sorted if l
is.
Equations
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.
Alias of List.erase_orderedInsert_of_notMem
.
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
.
If c
is a sorted sublist of l
, then c
is still a sublist of insertionSort r l
.
Another statement of stability of insertion sort.
If a pair [a, b]
is a sublist of l
and r a b
,
then [a, b]
is still a sublist of insertionSort r l
.
A version of insertionSort_stable
which only assumes c <+~ l
(instead of c <+ l
), but
additionally requires IsAntisymm α r
, IsTotal α r
and IsTrans α r
.
Another statement of stability of insertion sort.
If a pair [a, b]
is a sublist of a permutation of l
and a ≼ b
,
then [a, b]
is still a sublist of insertionSort r l
.
Merge sort #
We provide some wrapper functions around the theorems for mergeSort
provided in Lean,
which rather than using explicit hypotheses for transitivity and totality,
use Mathlib order typeclasses instead.