# Documentation

Mathlib.Data.List.Sort

# 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 < 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 Pairwise r l, preferred in the case that r is a < or ≤-like relation (transitive and antisymmetric or asymmetric)

Instances For
instance List.decidableSorted {α : Type uu} {r : ααProp} [] (l : List α) :
theorem List.Sorted.le_of_lt {α : Type uu} [] {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 uu} [] {l : List α} (h₁ : List.Sorted (fun x x_1 => x x_1) l) (h₂ : ) :
List.Sorted (fun x x_1 => x < x_1) l
@[simp]
theorem List.sorted_nil {α : Type uu} {r : ααProp} :
theorem List.Sorted.of_cons {α : Type uu} {r : ααProp} {a : α} {l : List α} :
List.Sorted r (a :: l)
theorem List.Sorted.tail {α : Type uu} {r : ααProp} {l : List α} (h : ) :
theorem List.rel_of_sorted_cons {α : Type uu} {r : ααProp} {a : α} {l : List α} :
List.Sorted r (a :: l)(b : α) → b lr a b
@[simp]
theorem List.sorted_cons {α : Type uu} {r : ααProp} {a : α} {l : List α} :
List.Sorted r (a :: l) ((b : α) → b lr a b)
theorem List.Sorted.nodup {α : Type uu} {r : ααProp} [IsIrrefl α r] {l : List α} (h : ) :
theorem List.eq_of_perm_of_sorted {α : Type uu} {r : ααProp} [] {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) (s₁ : List.Sorted r l₁) (s₂ : List.Sorted r l₂) :
l₁ = l₂
theorem List.sublist_of_subperm_of_sorted {α : Type uu} {r : ααProp} [] {l₁ : List α} {l₂ : List α} (p : l₁ <+~ l₂) (s₁ : List.Sorted r l₁) (s₂ : List.Sorted r l₂) :
List.Sublist l₁ l₂
@[simp]
theorem List.sorted_singleton {α : Type uu} {r : ααProp} (a : α) :
theorem List.Sorted.rel_get_of_lt {α : Type uu} {r : ααProp} {l : List α} (h : ) {a : Fin ()} {b : Fin ()} (hab : a < b) :
r (List.get l a) (List.get l b)
theorem List.Sorted.rel_nthLe_of_lt {α : Type uu} {r : ααProp} {l : List α} (h : ) {a : } {b : } (ha : a < ) (hb : b < ) (hab : a < b) :
r (List.nthLe l a ha) (List.nthLe l b hb)
theorem List.Sorted.rel_get_of_le {α : Type uu} {r : ααProp} [IsRefl α r] {l : List α} (h : ) {a : Fin ()} {b : Fin ()} (hab : a b) :
r (List.get l a) (List.get l b)
theorem List.Sorted.rel_nthLe_of_le {α : Type uu} {r : ααProp} [IsRefl α r] {l : List α} (h : ) {a : } {b : } (ha : a < ) (hb : b < ) (hab : a b) :
r (List.nthLe l a ha) (List.nthLe l b hb)
theorem List.Sorted.rel_of_mem_take_of_mem_drop {α : Type uu} {r : ααProp} {l : List α} (h : ) {k : } {x : α} {y : α} (hx : x ) (hy : y ) :
r x y
theorem List.sorted_ofFn_iff {n : } {α : Type uu} {f : Fin nα} {r : ααProp} :
@[simp]
theorem List.sorted_lt_ofFn_iff {n : } {α : Type uu} [] {f : Fin nα} :
List.Sorted (fun x x_1 => x < x_1) ()

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 uu} [] {f : Fin nα} :
List.Sorted (fun x x_1 => x x_1) ()

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 uu} [] {f : Fin nα} :
List.Sorted (fun x x_1 => x x_1) ()

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

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

The list obtained from a monotone tuple is sorted.

### Insertion sort #

def List.orderedInsert {α : Type uu} (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 uu} (r : ααProp) [] :
List αList α

insertionSort l returns l sorted using the insertion sort algorithm.

Equations
Instances For
@[simp]
theorem List.orderedInsert_nil {α : Type uu} (r : ααProp) [] (a : α) :
= [a]
theorem List.orderedInsert_length {α : Type uu} (r : ααProp) [] (L : List α) (a : α) :
theorem List.orderedInsert_eq_take_drop {α : Type uu} (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 uu} (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) ()
theorem List.perm_orderedInsert {α : Type uu} (r : ααProp) [] (a : α) (l : List α) :
~ a :: l
theorem List.orderedInsert_count {α : Type uu} (r : ααProp) [] [] (L : List α) (a : α) (b : α) :
List.count a () = + if a = b then 1 else 0
theorem List.perm_insertionSort {α : Type uu} (r : ααProp) [] (l : List α) :
~ l
theorem List.Sorted.insertionSort_eq {α : Type uu} {r : ααProp} [] {l : List α} :
= l

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

theorem List.Sorted.orderedInsert {α : Type uu} {r : ααProp} [] [IsTotal α r] [IsTrans α r] (a : α) (l : List α) :
List.Sorted r ()
theorem List.sorted_insertionSort {α : Type uu} (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 uu} :
List αList α × List α

Split l into two lists of approximately equal length.

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

Equations
Instances For
theorem List.split_cons_of_eq {α : Type uu} (a : α) {l : List α} {l₁ : List α} {l₂ : List α} (h : = (l₁, l₂)) :
List.split (a :: l) = (a :: l₂, l₁)
theorem List.length_split_le {α : Type uu} {l : List α} {l₁ : List α} {l₂ : List α} :
= (l₁, l₂)
theorem List.length_split_lt {α : Type uu} {a : α} {b : α} {l : List α} {l₁ : List α} {l₂ : List α} (h : List.split (a :: b :: l) = (l₁, l₂)) :
< List.length (a :: b :: l) < List.length (a :: b :: l)
theorem List.perm_split {α : Type uu} {l : List α} {l₁ : List α} {l₂ : List α} :
= (l₁, l₂)l ~ l₁ ++ l₂
def List.merge {α : Type uu} (r : ααProp) [] :
List αList αList α

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]

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

Implementation of a merge sort algorithm to sort a list.

Equations
• One or more equations did not get rendered due to their size.
• = []
• List.mergeSort r [a] = [a]
Instances For
theorem List.mergeSort_cons_cons {α : Type uu} (r : ααProp) [] {a : α} {b : α} {l : List α} {l₁ : List α} {l₂ : List α} (h : List.split (a :: b :: l) = (l₁, l₂)) :
List.mergeSort r (a :: b :: l) = List.merge r () ()
theorem List.perm_merge {α : Type uu} (r : ααProp) [] (l : List α) (l' : List α) :
List.merge r l l' ~ l ++ l'
theorem List.perm_mergeSort {α : Type uu} (r : ααProp) [] (l : List α) :
~ l
@[simp]
theorem List.length_mergeSort {α : Type uu} (r : ααProp) [] (l : List α) :
theorem List.Sorted.merge {α : Type uu} {r : ααProp} [] [IsTotal α r] [IsTrans α r] {l : List α} {l' : List α} :
List.Sorted r l'List.Sorted r (List.merge r l l')
theorem List.sorted_mergeSort {α : Type uu} (r : ααProp) [] [IsTotal α r] [IsTrans α r] (l : List α) :
theorem List.mergeSort_eq_self {α : Type uu} (r : ααProp) [] [IsTotal α r] [IsTrans α r] [] {l : List α} :
= l
theorem List.mergeSort_eq_insertionSort {α : Type uu} (r : ααProp) [] [IsTotal α r] [IsTrans α r] [] (l : List α) :
@[simp]
theorem List.mergeSort_nil {α : Type uu} (r : ααProp) [] :
= []
@[simp]
theorem List.mergeSort_singleton {α : Type uu} (r : ααProp) [] (a : α) :
List.mergeSort r [a] = [a]