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

• @List.Sorted = @List.Pairwise

instance List.decidableSorted {α : Type uu} {r : α → α → Prop} [DecidableRel r] (l : List α) : Decidable (List.Sorted r l)

Equations

• l.decidableSorted = l.instDecidablePairwise

theorem List.Sorted.le_of_lt {α : Type uu} [Preorder α] {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} [PartialOrder α] {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 uu} [Preorder α] {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 uu} [PartialOrder α] {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 uu} {r : α → α → Prop} : List.Sorted r []

theorem List.Sorted.of_cons {α : Type uu} {r : α → α → Prop} {a : α} {l : List α} : List.Sorted r (a :: l) → List.Sorted r l

theorem List.Sorted.tail {α : Type uu} {r : α → α → Prop} {l : List α} (h : List.Sorted r l) : List.Sorted r l.tail

theorem List.rel_of_sorted_cons {α : Type uu} {r : α → α → Prop} {a : α} {l : List α} : List.Sorted r (a :: l) → ∀ b ∈ l, r a b

theorem List.Sorted.head!_le {α : Type uu} [Inhabited α] [Preorder α] {a : α} {l : List α} (h : List.Sorted (fun (x x_1 : α) => x < x_1) l) (ha : a ∈ l) : l.head! ≤ a

theorem List.Sorted.le_head! {α : Type uu} [Inhabited α] [Preorder α] {a : α} {l : List α} (h : List.Sorted (fun (x x_1 : α) => x > x_1) l) (ha : a ∈ l) : a ≤ l.head!

@[simp]

theorem List.sorted_cons {α : Type uu} {r : α → α → Prop} {a : α} {l : List α} : List.Sorted r (a :: l) ↔ (∀ b ∈ l, r a b) ∧ List.Sorted r l

theorem List.Sorted.nodup {α : Type uu} {r : α → α → Prop} [IsIrrefl α r] {l : List α} (h : List.Sorted r l) : l.Nodup

theorem List.eq_of_perm_of_sorted {α : Type uu} {r : α → α → Prop} [IsAntisymm α r] {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 uu} {r : α → α → Prop} [IsAntisymm α r] {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 uu} {r : α → α → Prop} (a : α) : List.Sorted r [a]

theorem List.Sorted.rel_get_of_lt {α : Type uu} {r : α → α → Prop} {l : List α} (h : List.Sorted r l) {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 uu} {r : α → α → Prop} {l : List α} (h : List.Sorted r l) {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 uu} {r : α → α → Prop} [IsRefl α r] {l : List α} (h : List.Sorted r l) {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 uu} {r : α → α → Prop} [IsRefl α r] {l : List α} (h : List.Sorted r l) {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 uu} {r : α → α → Prop} {l : List α} (h : List.Sorted r l) {k : ℕ} {x : α} {y : α} (hx : x ∈ List.take k l) (hy : y ∈ List.drop k l) : r x y

theorem List.sorted_ofFn_iff {n : ℕ} {α : Type uu} {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 uu} [Preorder α] {f : Fin n → α} : List.Sorted (fun (x x_1 : α) => x < x_1) (List.ofFn f) ↔ StrictMono 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 uu} [Preorder α] {f : Fin n → α} : List.Sorted (fun (x x_1 : α) => x ≤ x_1) (List.ofFn f) ↔ Monotone 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 uu} [Preorder α] {f : Fin n → α} : Monotone f ↔ 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 uu} [Preorder α] {f : Fin n → α} : Monotone f → 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 uu} (r : α → α → Prop) [DecidableRel r] (a : α) : List α → List α

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

def List.insertionSort {α : Type uu} (r : α → α → Prop) [DecidableRel r] : List α → List α

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)

@[simp]

theorem List.orderedInsert_nil {α : Type uu} (r : α → α → Prop) [DecidableRel r] (a : α) : List.orderedInsert r a [] = [a]

theorem List.orderedInsert_length {α : Type uu} (r : α → α → Prop) [DecidableRel r] (L : List α) (a : α) : (List.orderedInsert r a L).length = L.length + 1

theorem List.orderedInsert_eq_take_drop {α : Type uu} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : List.orderedInsert r a l = 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) [DecidableRel r] (a : α) (l : List α) : List.insertionSort r (a :: l) = List.takeWhile (fun (b : α) => decide ¬r a b) (List.insertionSort r l) ++ a :: List.dropWhile (fun (b : α) => decide ¬r a b) (List.insertionSort r l)

@[simp]

theorem List.mem_orderedInsert {α : Type uu} (r : α → α → Prop) [DecidableRel r] {a : α} {b : α} {l : List α} : a ∈ List.orderedInsert r b l ↔ a = b ∨ a ∈ l

theorem List.perm_orderedInsert {α : Type uu} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : (List.orderedInsert r a l).Perm (a :: l)

theorem List.orderedInsert_count {α : Type uu} (r : α → α → Prop) [DecidableRel r] [DecidableEq α] (L : List α) (a : α) (b : α) : List.count a (List.orderedInsert r b L) = List.count a L + if a = b then 1 else 0

theorem List.perm_insertionSort {α : Type uu} (r : α → α → Prop) [DecidableRel r] (l : List α) : (List.insertionSort r l).Perm l

theorem List.Sorted.insertionSort_eq {α : Type uu} {r : α → α → Prop} [DecidableRel r] {l : List α} : List.Sorted r l → List.insertionSort r l = l

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

theorem List.erase_orderedInsert {α : Type uu} {r : α → α → Prop} [DecidableRel r] [DecidableEq α] [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 uu} {r : α → α → Prop} [DecidableRel r] [DecidableEq α] {x : α} {xs : List α} (hx : x ∉ xs) : (List.orderedInsert r x xs).erase x = xs

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

theorem List.orderedInsert_erase {α : Type uu} {r : α → α → Prop} [DecidableRel r] [DecidableEq α] [IsAntisymm α r] (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 uu} {r : α → α → Prop} [DecidableRel r] (x : α) (xs : List α) : xs.Sublist (List.orderedInsert r x xs)

theorem List.Sorted.orderedInsert {α : Type uu} {r : α → α → Prop} [DecidableRel r] [IsTotal α r] [IsTrans α r] (a : α) (l : List α) : List.Sorted r l → List.Sorted r (List.orderedInsert r a l)

theorem List.sorted_insertionSort {α : Type uu} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l : List α) : List.Sorted r (List.insertionSort r l)

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

• [].split = ([], [])
• (b :: l).split = match l.split with | (l₁, l₂) => (b :: l₂, l₁)

theorem List.split_cons_of_eq {α : Type uu} (a : α) {l : List α} {l₁ : List α} {l₂ : List α} (h : l.split = (l₁, l₂)) : (a :: l).split = (a :: l₂, l₁)

theorem List.length_split_le {α : Type uu} {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 uu} (l : List α) : l.split.1.length ≤ l.length

theorem List.length_split_snd_le {α : Type uu} (l : List α) : l.split.2.length ≤ l.length

theorem List.length_split_lt {α : Type uu} {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 uu} {l : List α} {l₁ : List α} {l₂ : List α} : l.split = (l₁, l₂) → l.Perm (l₁ ++ l₂)

def List.mergeSort {α : Type uu} (r : α → α → Prop) [DecidableRel r] : List α → List α

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)

theorem List.mergeSort_cons_cons {α : Type uu} (r : α → α → Prop) [DecidableRel r] {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₂)

theorem List.perm_mergeSort {α : Type uu} (r : α → α → Prop) [DecidableRel r] (l : List α) : (List.mergeSort r l).Perm l

@[simp]

theorem List.length_mergeSort {α : Type uu} (r : α → α → Prop) [DecidableRel r] (l : List α) : (List.mergeSort r l).length = l.length

theorem List.Sorted.merge {α : Type uu} {r : α → α → Prop} [DecidableRel r] [IsTotal α r] [IsTrans α r] {l : List α} {l' : List α} : List.Sorted r l → List.Sorted r l' → List.Sorted r (List.merge (fun (x x_1 : α) => decide (r x x_1)) l l')

theorem List.sorted_mergeSort {α : Type uu} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l : List α) : List.Sorted r (List.mergeSort r l)

theorem List.mergeSort_eq_self {α : Type uu} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] [IsAntisymm α r] {l : List α} : List.Sorted r l → List.mergeSort r l = l

theorem List.mergeSort_eq_insertionSort {α : Type uu} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] [IsAntisymm α r] (l : List α) : List.mergeSort r l = List.insertionSort r l

@[simp]

theorem List.mergeSort_nil {α : Type uu} (r : α → α → Prop) [DecidableRel r] : List.mergeSort r [] = []

@[simp]

theorem List.mergeSort_singleton {α : Type uu} (r : α → α → Prop) [DecidableRel r] (a : α) : List.mergeSort r [a] = [a]