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 u} {r : α → α → Prop} [DecidableRel r] (l : List α) : Decidable (List.Sorted r l)

Equations

• l.decidableSorted = l.instDecidablePairwise

theorem List.Sorted.le_of_lt {α : Type u} [Preorder α] {l : List α} (h : List.Sorted (fun (x1 x2 : α) => x1 < x2) l) : List.Sorted (fun (x1 x2 : α) => x1 ≤ x2) l

theorem List.Sorted.lt_of_le {α : Type u} [PartialOrder α] {l : List α} (h₁ : List.Sorted (fun (x1 x2 : α) => x1 ≤ x2) l) (h₂ : l.Nodup) : List.Sorted (fun (x1 x2 : α) => x1 < x2) l

theorem List.Sorted.ge_of_gt {α : Type u} [Preorder α] {l : List α} (h : List.Sorted (fun (x1 x2 : α) => x1 > x2) l) : List.Sorted (fun (x1 x2 : α) => x1 ≥ x2) l

theorem List.Sorted.gt_of_ge {α : Type u} [PartialOrder α] {l : List α} (h₁ : List.Sorted (fun (x1 x2 : α) => x1 ≥ x2) l) (h₂ : l.Nodup) : List.Sorted (fun (x1 x2 : α) => x1 > x2) l

@[simp]

theorem List.sorted_nil {α : Type u} {r : α → α → Prop} : List.Sorted r []

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

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

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

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

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

@[simp]

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

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

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

theorem List.Sorted.rel_get_of_lt {α : Type u} {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)

theorem List.Sorted.rel_get_of_le {α : Type u} {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)

theorem List.Sorted.rel_of_mem_take_of_mem_drop {α : Type u} {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 u} {f : Fin n → α} {r : α → α → Prop} : List.Sorted r (List.ofFn f) ↔ ((fun (x1 x2 : Fin n) => x1 < x2) ⇒ r) f f

@[simp]

theorem List.sorted_lt_ofFn_iff {n : ℕ} {α : Type u} {f : Fin n → α} [Preorder α] : List.Sorted (fun (x1 x2 : α) => x1 < x2) (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 u} {f : Fin n → α} [Preorder α] : List.Sorted (fun (x1 x2 : α) => x1 ≤ x2) (List.ofFn f) ↔ Monotone f

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

theorem Monotone.ofFn_sorted {n : ℕ} {α : Type u} {f : Fin n → α} [Preorder α] : Monotone f → List.Sorted (fun (x1 x2 : α) => x1 ≤ x2) (List.ofFn f)

The list obtained from a monotone tuple is sorted.

Insertion sort

def List.orderedInsert {α : Type u} (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 u} (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 u} (r : α → α → Prop) [DecidableRel r] (a : α) : List.orderedInsert r a [] = [a]

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

theorem List.orderedInsert_eq_take_drop {α : Type u} (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 u} (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 u} (r : α → α → Prop) [DecidableRel r] {a : α} {b : α} {l : List α} : a ∈ List.orderedInsert r b l ↔ a = b ∨ a ∈ l

theorem List.map_orderedInsert {α : Type u} {β : Type v} (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] (f : α → β) (l : List α) (x : α) (hl₁ : ∀ a ∈ l, r a x ↔ s (f a) (f x)) (hl₂ : ∀ a ∈ l, r x a ↔ s (f x) (f a)) : List.map f (List.orderedInsert r x l) = List.orderedInsert s (f x) (List.map f l)

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

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

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

@[simp]

theorem List.mem_insertionSort {α : Type u} (r : α → α → Prop) [DecidableRel r] {l : List α} {x : α} : x ∈ List.insertionSort r l ↔ x ∈ l

@[simp]

theorem List.length_insertionSort {α : Type u} (r : α → α → Prop) [DecidableRel r] (l : List α) : (List.insertionSort r l).length = l.length

theorem List.map_insertionSort {α : Type u} {β : Type v} (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] (f : α → β) (l : List α) (hl : ∀ a ∈ l, ∀ b ∈ l, r a b ↔ s (f a) (f b)) : List.map f (List.insertionSort r l) = List.insertionSort s (List.map f l)

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

theorem List.Sorted.orderedInsert {α : Type u} {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 u} (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 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₁)

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₁)

@[simp]

theorem List.map_split {α : Type u} {β : Type v} (f : α → β) (l : List α) : (List.map f l).split = (List.map f l.split.1, List.map f l.split.2)

@[simp]

theorem List.mem_split_iff {α : Type u} {x : α} {l : List α} : x ∈ l.split.1 ∨ x ∈ l.split.2 ↔ x ∈ 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) [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 (x1 x2 : α) => decide (r x1 x2)) (List.mergeSort' r (a :: b :: l).split.1) (List.mergeSort' r (a :: b :: l).split.2)

theorem List.mergeSort'_cons_cons {α : Type u} (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 (x1 x2 : α) => decide (r x1 x2)) (List.mergeSort' r l₁) (List.mergeSort' r l₂)

@[irreducible]

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

@[simp]

theorem List.mem_mergeSort' {α : Type u} (r : α → α → Prop) [DecidableRel r] {l : List α} {x : α} : x ∈ List.mergeSort' r l ↔ x ∈ l

@[simp]

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

@[irreducible]

theorem List.Sorted.merge {α : Type u} {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 (x1 x2 : α) => decide (r x1 x2)) l l')

@[irreducible]

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

theorem List.mergeSort'_eq_self {α : Type u} (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 u} (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 u} (r : α → α → Prop) [DecidableRel r] : List.mergeSort' r [] = []

@[simp]

theorem List.mergeSort'_singleton {α : Type u} (r : α → α → Prop) [DecidableRel r] (a : α) : List.mergeSort' r [a] = [a]

@[irreducible]

theorem List.map_merge {α : Type u} {β : Type v} (f : α → β) (r : α → α → Bool) (s : β → β → Bool) (l : List α) (l' : List α) (hl : ∀ a ∈ l, ∀ b ∈ l', r a b = s (f a) (f b)) : List.map f (List.merge r l l') = List.merge s (List.map f l) (List.map f l')

@[irreducible]

theorem List.map_mergeSort' {α : Type u} {β : Type v} (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] (f : α → β) (l : List α) (hl : ∀ a ∈ l, ∀ b ∈ l, r a b ↔ s (f a) (f b)) : List.map f (List.mergeSort' r l) = List.mergeSort' s (List.map f l)