# 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#

def List.Sorted {α : Type u_1} (R : ααProp) :
List αProp

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
instance List.decidableSorted {α : Type u} {r : ααProp} [] (l : List α) :
Equations
• l.decidableSorted = l.instDecidablePairwise
theorem List.Sorted.le_of_lt {α : Type u} [] {l : List α} (h : List.Sorted (fun (x x_1 : α) => x < x_1) l) :
List.Sorted (fun (x x_1 : α) => x x_1) l
theorem List.Sorted.lt_of_le {α : Type u} [] {l : List α} (h₁ : List.Sorted (fun (x x_1 : α) => x x_1) l) (h₂ : l.Nodup) :
List.Sorted (fun (x x_1 : α) => x < x_1) l
theorem List.Sorted.ge_of_gt {α : Type u} [] {l : List α} (h : List.Sorted (fun (x x_1 : α) => x > x_1) l) :
List.Sorted (fun (x x_1 : α) => x x_1) l
theorem List.Sorted.gt_of_ge {α : Type u} [] {l : List α} (h₁ : List.Sorted (fun (x x_1 : α) => x x_1) l) (h₂ : l.Nodup) :
List.Sorted (fun (x x_1 : α) => x > x_1) l
@[simp]
theorem List.sorted_nil {α : Type u} {r : ααProp} :
theorem List.Sorted.of_cons {α : Type u} {r : ααProp} {a : α} {l : List α} :
List.Sorted r (a :: l)
theorem List.Sorted.tail {α : Type u} {r : ααProp} {l : List α} (h : ) :
List.Sorted r l.tail
theorem List.rel_of_sorted_cons {α : Type u} {r : ααProp} {a : α} {l : List α} :
List.Sorted r (a :: l)bl, r a b
theorem List.Sorted.head!_le {α : Type u} [] [] {a : α} {l : List α} (h : List.Sorted (fun (x x_1 : α) => x < x_1) l) (ha : a l) :
theorem List.Sorted.le_head! {α : Type u} [] [] {a : α} {l : List α} (h : List.Sorted (fun (x x_1 : α) => x > x_1) l) (ha : a l) :
@[simp]
theorem List.sorted_cons {α : Type u} {r : ααProp} {a : α} {l : List α} :
List.Sorted r (a :: l) (∀ bl, r a b)
theorem List.Sorted.nodup {α : Type u} {r : ααProp} [IsIrrefl α r] {l : List α} (h : ) :
l.Nodup
theorem List.eq_of_perm_of_sorted {α : Type u} {r : ααProp} [] {l₁ : List α} {l₂ : List α} (hp : l₁.Perm l₂) (hs₁ : List.Sorted r l₁) (hs₂ : List.Sorted r l₂) :
l₁ = l₂
theorem List.sublist_of_subperm_of_sorted {α : Type u} {r : ααProp} [] {l₁ : List α} {l₂ : List α} (hp : l₁.Subperm l₂) (hs₁ : List.Sorted r l₁) (hs₂ : List.Sorted r l₂) :
l₁.Sublist l₂
@[simp]
theorem List.sorted_singleton {α : Type u} {r : ααProp} (a : α) :
theorem List.Sorted.rel_get_of_lt {α : Type u} {r : ααProp} {l : List α} (h : ) {a : Fin l.length} {b : Fin l.length} (hab : a < b) :
r (l.get a) (l.get b)
@[deprecated List.Sorted.rel_get_of_lt]
theorem List.Sorted.rel_nthLe_of_lt {α : Type u} {r : ααProp} {l : List α} (h : ) {a : } {b : } (ha : a < l.length) (hb : b < l.length) (hab : a < b) :
r (l.nthLe a ha) (l.nthLe b hb)
theorem List.Sorted.rel_get_of_le {α : Type u} {r : ααProp} [IsRefl α r] {l : List α} (h : ) {a : Fin l.length} {b : Fin l.length} (hab : a b) :
r (l.get a) (l.get b)
@[deprecated List.Sorted.rel_get_of_le]
theorem List.Sorted.rel_nthLe_of_le {α : Type u} {r : ααProp} [IsRefl α r] {l : List α} (h : ) {a : } {b : } (ha : a < l.length) (hb : b < l.length) (hab : a b) :
r (l.nthLe a ha) (l.nthLe b hb)
theorem List.Sorted.rel_of_mem_take_of_mem_drop {α : Type u} {r : ααProp} {l : List α} (h : ) {k : } {x : α} {y : α} (hx : x ) (hy : y ) :
r x y
theorem List.sorted_ofFn_iff {n : } {α : Type u} {f : Fin nα} {r : ααProp} :
List.Sorted r (List.ofFn f) ((fun (x x_1 : Fin n) => x < x_1) r) f f
@[simp]
theorem List.sorted_lt_ofFn_iff {n : } {α : Type u} {f : Fin nα} [] :
List.Sorted (fun (x x_1 : α) => x < x_1) (List.ofFn f)

The list List.ofFn f is strictly sorted with respect to (· ≤ ·) if and only if f is strictly monotone.

@[simp]
theorem List.sorted_le_ofFn_iff {n : } {α : Type u} {f : Fin nα} [] :
List.Sorted (fun (x x_1 : α) => x x_1) (List.ofFn f)

The list List.ofFn f is sorted with respect to (· ≤ ·) if and only if f is monotone.

@[deprecated List.sorted_le_ofFn_iff]
theorem List.monotone_iff_ofFn_sorted {n : } {α : Type u} {f : Fin nα} [] :
List.Sorted (fun (x x_1 : α) => x x_1) (List.ofFn f)

A tuple is monotone if and only if the list obtained from it is sorted.

theorem Monotone.ofFn_sorted {n : } {α : Type u} {f : Fin nα} [] :
List.Sorted (fun (x x_1 : α) => x x_1) (List.ofFn f)

The list obtained from a monotone tuple is sorted.

### Insertion sort #

def List.orderedInsert {α : Type u} (r : ααProp) [] (a : α) :
List αList α

orderedInsert a l inserts a into l at such that orderedInsert a l is sorted if l is.

Equations
Instances For
def List.insertionSort {α : Type u} (r : ααProp) [] :
List αList α

insertionSort l returns l sorted using the insertion sort algorithm.

Equations
Instances For
@[simp]
theorem List.orderedInsert_nil {α : Type u} (r : ααProp) [] (a : α) :
= [a]
theorem List.orderedInsert_length {α : Type u} (r : ααProp) [] (L : List α) (a : α) :
(List.orderedInsert r a L).length = L.length + 1
theorem List.orderedInsert_eq_take_drop {α : Type u} (r : ααProp) [] (a : α) (l : List α) :
= List.takeWhile (fun (b : α) => decide ¬r a b) l ++ a :: List.dropWhile (fun (b : α) => decide ¬r a b) l

An alternative definition of orderedInsert using takeWhile and dropWhile.

theorem List.insertionSort_cons_eq_take_drop {α : Type u} (r : ααProp) [] (a : α) (l : List α) :
List.insertionSort r (a :: l) = List.takeWhile (fun (b : α) => decide ¬r a b) ++ a :: List.dropWhile (fun (b : α) => decide ¬r a b)
@[simp]
theorem List.mem_orderedInsert {α : Type u} (r : ααProp) [] {a : α} {b : α} {l : List α} :
a a = b a l
theorem List.perm_orderedInsert {α : Type u} (r : ααProp) [] (a : α) (l : List α) :
(List.orderedInsert r a l).Perm (a :: l)
theorem List.orderedInsert_count {α : Type u} (r : ααProp) [] [] (L : List α) (a : α) (b : α) :
List.count a (List.orderedInsert r b L) = + if b = a then 1 else 0
theorem List.perm_insertionSort {α : Type u} (r : ααProp) [] (l : List α) :
.Perm l
theorem List.Sorted.insertionSort_eq {α : Type u} {r : ααProp} [] {l : List α} :
= l

If l is already List.Sorted with respect to r, then insertionSort does not change it.

theorem List.erase_orderedInsert {α : Type u} {r : ααProp} [] [] [IsRefl α r] (x : α) (xs : List α) :
(List.orderedInsert r x xs).erase x = xs

For a reflexive relation, insert then erasing is the identity.

theorem List.erase_orderedInsert_of_not_mem {α : Type u} {r : ααProp} [] [] {x : α} {xs : List α} (hx : xxs) :
(List.orderedInsert r x xs).erase x = xs

Inserting then erasing an element that is absent is the identity.

theorem List.orderedInsert_erase {α : Type u} {r : ααProp} [] [] [] (x : α) (xs : List α) (hx : x xs) (hxs : List.Sorted r xs) :
List.orderedInsert r x (xs.erase x) = xs

For an antisymmetric relation, erasing then inserting is the identity.

theorem List.sublist_orderedInsert {α : Type u} {r : ααProp} [] (x : α) (xs : List α) :
xs.Sublist (List.orderedInsert r x xs)
theorem List.Sorted.orderedInsert {α : Type u} {r : ααProp} [] [IsTotal α r] [IsTrans α r] (a : α) (l : List α) :
theorem List.sorted_insertionSort {α : Type u} (r : ααProp) [] [IsTotal α r] [IsTrans α r] (l : List α) :

The list List.insertionSort r l is List.Sorted with respect to r.

### Merge sort #

def List.split {α : Type u} :
List αList α × List α

Split l into two lists of approximately equal length.

split [1, 2, 3, 4, 5] = ([1, 3, 5], [2, 4])

Equations
• [].split = ([], [])
• (b :: l).split = match l.split with | (l₁, l₂) => (b :: l₂, l₁)
Instances For
theorem List.split_cons_of_eq {α : Type u} (a : α) {l : List α} {l₁ : List α} {l₂ : List α} (h : l.split = (l₁, l₂)) :
(a :: l).split = (a :: l₂, l₁)
theorem List.length_split_le {α : Type u} {l : List α} {l₁ : List α} {l₂ : List α} :
l.split = (l₁, l₂)l₁.length l.length l₂.length l.length
theorem List.length_split_fst_le {α : Type u} (l : List α) :
l.split.1.length l.length
theorem List.length_split_snd_le {α : Type u} (l : List α) :
l.split.2.length l.length
theorem List.length_split_lt {α : Type u} {a : α} {b : α} {l : List α} {l₁ : List α} {l₂ : List α} (h : (a :: b :: l).split = (l₁, l₂)) :
l₁.length < (a :: b :: l).length l₂.length < (a :: b :: l).length
theorem List.perm_split {α : Type u} {l : List α} {l₁ : List α} {l₂ : List α} :
l.split = (l₁, l₂)l.Perm (l₁ ++ l₂)
@[irreducible]
def List.mergeSort {α : Type u} (r : ααProp) [] :
List αList α

Implementation of a merge sort algorithm to sort a list.

Equations
Instances For
theorem List.mergeSort_cons_cons {α : Type u} (r : ααProp) [] {a : α} {b : α} {l : List α} {l₁ : List α} {l₂ : List α} (h : (a :: b :: l).split = (l₁, l₂)) :
List.mergeSort r (a :: b :: l) = List.merge (fun (x x_1 : α) => decide (r x x_1)) (List.mergeSort r l₁) (List.mergeSort r l₂)
@[irreducible]
theorem List.perm_mergeSort {α : Type u} (r : ααProp) [] (l : List α) :
(List.mergeSort r l).Perm l
@[simp]
theorem List.length_mergeSort {α : Type u} (r : ααProp) [] (l : List α) :
(List.mergeSort r l).length = l.length
@[irreducible]
theorem List.Sorted.merge {α : Type u} {r : ααProp} [] [IsTotal α r] [IsTrans α r] {l : List α} {l' : List α} :
List.Sorted r l'List.Sorted r (List.merge (fun (x x_1 : α) => decide (r x x_1)) l l')
@[irreducible]
theorem List.sorted_mergeSort {α : Type u} (r : ααProp) [] [IsTotal α r] [IsTrans α r] (l : List α) :
theorem List.mergeSort_eq_self {α : Type u} (r : ααProp) [] [IsTotal α r] [IsTrans α r] [] {l : List α} :
= l
theorem List.mergeSort_eq_insertionSort {α : Type u} (r : ααProp) [] [IsTotal α r] [IsTrans α r] [] (l : List α) :
@[simp]
theorem List.mergeSort_nil {α : Type u} (r : ααProp) [] :
= []
@[simp]
theorem List.mergeSort_singleton {α : Type u} (r : ααProp) [] (a : α) :
List.mergeSort r [a] = [a]