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

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.cons {α : Type u} {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α} (hab : r a b) (h : List.Sorted r (b :: l)) : List.Sorted r (a :: b :: l)

theorem List.sorted_cons_cons {α : Type u} {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α} : List.Sorted r (b :: a :: l) ↔ r b a ∧ List.Sorted r (a :: l)

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.Sorted.filter {α : Type u} {r : α → α → Prop} {l : List α} (f : α → Bool) (h : List.Sorted r l) : List.Sorted r (List.filter f l)

theorem List.eq_of_perm_of_sorted {α : Type u} {r : α → α → Prop} [IsAntisymm α r] {l₁ 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₁ 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_lt_range (n : ℕ) : List.Sorted (fun (x1 x2 : ℕ) => x1 < x2) (List.range n)

theorem List.sorted_le_range (n : ℕ) : List.Sorted (fun (x1 x2 : ℕ) => x1 ≤ x2) (List.range n)

theorem List.Sorted.rel_get_of_lt {α : Type u} {r : α → α → Prop} {l : List α} (h : List.Sorted r l) {a 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 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.decide {α : Type u} {r : α → α → Prop} [DecidableRel r] (l : List α) (h : List.Sorted r l) : List.Sorted (fun (a b : α) => decide (r a b) = true) l

If a list is sorted with respect to a decidable relation, then it is sorted with respect to the corresponding Bool-valued relation.

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

theorem List.orderedInsert_of_le {α : Type u} (r : α → α → Prop) [DecidableRel r] {a b : α} (l : List α) (h : r a b) : List.orderedInsert r a (b :: l) = a :: b :: 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.insertionSort_cons {α : Type u} (r : α → α → Prop) [DecidableRel r] {a : α} {l : List α} (h : ∀ b ∈ l, r a b) : List.insertionSort r (a :: l) = a :: List.insertionSort r l

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.cons_sublist_orderedInsert {α : Type u} {r : α → α → Prop} [DecidableRel r] {l c : List α} {a : α} (hl : c.Sublist l) (ha : ∀ a' ∈ c, r a a') : (a :: c).Sublist (List.orderedInsert r a l)

theorem List.Sublist.orderedInsert_sublist {α : Type u} {r : α → α → Prop} [DecidableRel r] [IsTrans α r] {as bs : List α} (x : α) (hs : as.Sublist bs) (hb : List.Sorted r bs) : (List.orderedInsert r x as).Sublist (List.orderedInsert r x bs)

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.

theorem List.sublist_insertionSort {α : Type u} {r : α → α → Prop} [DecidableRel r] {l c : List α} (hr : List.Pairwise r c) (hc : c.Sublist l) : c.Sublist (List.insertionSort r l)

If c is a sorted sublist of l, then c is still a sublist of insertionSort r l.

theorem List.pair_sublist_insertionSort {α : Type u} {r : α → α → Prop} [DecidableRel r] {a b : α} {l : List α} (hab : r a b) (h : [a, b].Sublist l) : [a, b].Sublist (List.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.

theorem List.sublist_insertionSort' {α : Type u} {r : α → α → Prop} [DecidableRel r] [IsAntisymm α r] [IsTotal α r] [IsTrans α r] {l c : List α} (hs : List.Sorted r c) (hc : c.Subperm l) : c.Sublist (List.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.

theorem List.pair_sublist_insertionSort' {α : Type u} {r : α → α → Prop} [DecidableRel r] [IsAntisymm α r] [IsTotal α r] [IsTrans α r] {a b : α} {l : List α} (hab : r a b) (h : [a, b].Subperm l) : [a, b].Sublist (List.insertionSort r l)

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.

theorem List.Sorted.merge {α : Type u} {r : α → α → Prop} [DecidableRel r] [IsTotal α r] [IsTrans α r] {l l' : List α} (h : List.Sorted r l) (h' : List.Sorted r l') : List.Sorted r (l.merge l' fun (x1 x2 : α) => decide (r x1 x2))

theorem List.sorted_mergeSort' {α : Type u} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] (l : List α) : List.Sorted (fun (x1 x2 : α) => x1 ≤ x2) (l.mergeSort fun (a b : α) => decide (a ≤ b))

Variant of sorted_mergeSort using order typeclasses.

theorem List.mergeSort_eq_self {α : Type u} [LinearOrder α] {l : List α} : List.Sorted (fun (x1 x2 : α) => x1 ≤ x2) l → (l.mergeSort fun (a b : α) => decide (a ≤ b)) = l

theorem List.mergeSort_eq_insertionSort {α : Type u} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] [IsAntisymm α r] (l : List α) : (l.mergeSort fun (x1 x2 : α) => decide (r x1 x2)) = List.insertionSort r l