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 (Sorted r l)

Equations

• l.decidableSorted = l.instDecidablePairwise

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

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

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

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

@[simp]

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

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

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

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

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

theorem List.Sorted.head!_le {α : Type u} [Inhabited α] [Preorder α] {a : α} {l : List α} (h : 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 : 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 α} : Sorted r (a :: l) ↔ (∀ b ∈ l, r a b) ∧ Sorted r l

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

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

theorem List.eq_of_perm_of_sorted {α : Type u} {r : α → α → Prop} [IsAntisymm α r] {l₁ l₂ : List α} (hp : l₁.Perm l₂) (hs₁ : Sorted r l₁) (hs₂ : Sorted r l₂) : l₁ = l₂

theorem List.Sorted.eq_of_mem_iff {α : Type u} {r : α → α → Prop} [IsAntisymm α r] [IsIrrefl α r] {l₁ l₂ : List α} (h₁ : Sorted r l₁) (h₂ : Sorted r l₂) (h : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) : l₁ = l₂

theorem List.sublist_of_subperm_of_sorted {α : Type u} {r : α → α → Prop} [IsAntisymm α r] {l₁ l₂ : List α} (hp : l₁.Subperm l₂) (hs₁ : Sorted r l₁) (hs₂ : Sorted r l₂) : l₁.Sublist l₂

@[simp]

theorem List.sorted_singleton {α : Type u} {r : α → α → Prop} (a : α) : Sorted r [a]

theorem List.sorted_lt_range (n : ℕ) : Sorted (fun (x1 x2 : ℕ) => x1 < x2) (range n)

theorem List.sorted_replicate {α : Type u} {r : α → α → Prop} (n : ℕ) (a : α) : Sorted r (replicate n a) ↔ n ≤ 1 ∨ r a a

theorem List.sorted_le_replicate {α : Type u} (n : ℕ) (a : α) [Preorder α] : Sorted (fun (x1 x2 : α) => x1 ≤ x2) (replicate n a)

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

theorem List.sorted_lt_range' (a b : ℕ) {s : ℕ} (hs : s ≠ 0) : Sorted (fun (x1 x2 : ℕ) => x1 < x2) (range' a b s)

theorem List.sorted_le_range' (a b s : ℕ) : Sorted (fun (x1 x2 : ℕ) => x1 ≤ x2) (range' a b s)

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

theorem List.Sorted.decide {α : Type u} {r : α → α → Prop} [DecidableRel r] (l : List α) (h : Sorted r l) : Sorted (fun (a b : α) => Decidable.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} : Sorted r (ofFn f) ↔ Relator.LiftFun (fun (x1 x2 : Fin n) => x1 < x2) r f f

@[simp]

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

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

@[simp]

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

@[simp]

theorem List.sorted_ge_ofFn_iff {n : ℕ} {α : Type u} {f : Fin n → α} [Preorder α] : Sorted (fun (x1 x2 : α) => x1 ≥ x2) (ofFn f) ↔ Antitone f

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

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

The list obtained from an antitone tuple is sorted.

theorem List.Sorted.filterMap {α : Type u_1} {β : Type u_2} {p : α → Option β} {l : List α} {r : α → α → Prop} {r' : β → β → Prop} (hl : Sorted r l) (hp : ∀ (a b : α) (c d : β), p a = some c → p b = some d → r a b → r' c d) : Sorted r' (List.filterMap p l)

@[simp]

theorem RelEmbedding.sorted_listMap {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ↪r rb) {l : List α} : List.Sorted rb (List.map (⇑e) l) ↔ List.Sorted ra l

@[simp]

theorem RelEmbedding.sorted_swap_listMap {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ↪r rb) {l : List α} : List.Sorted (Function.swap rb) (List.map (⇑e) l) ↔ List.Sorted (Function.swap ra) l

@[simp]

theorem OrderEmbedding.sorted_lt_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) {l : List α} : List.Sorted (fun (x1 x2 : β) => x1 < x2) (List.map (⇑e) l) ↔ List.Sorted (fun (x1 x2 : α) => x1 < x2) l

@[simp]

theorem OrderEmbedding.sorted_gt_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) {l : List α} : List.Sorted (fun (x1 x2 : β) => x1 > x2) (List.map (⇑e) l) ↔ List.Sorted (fun (x1 x2 : α) => x1 > x2) l

@[simp]

theorem RelIso.sorted_listMap {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ≃r rb) {l : List α} : List.Sorted rb (List.map (⇑e) l) ↔ List.Sorted ra l

@[simp]

theorem RelIso.sorted_swap_listMap {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ≃r rb) {l : List α} : List.Sorted (Function.swap rb) (List.map (⇑e) l) ↔ List.Sorted (Function.swap ra) l

@[simp]

theorem OrderIso.sorted_lt_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) {l : List α} : List.Sorted (fun (x1 x2 : β) => x1 < x2) (List.map (⇑e) l) ↔ List.Sorted (fun (x1 x2 : α) => x1 < x2) l

@[simp]

theorem OrderIso.sorted_gt_listMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) {l : List α} : List.Sorted (fun (x1 x2 : β) => x1 > x2) (List.map (⇑e) l) ↔ List.Sorted (fun (x1 x2 : α) => x1 > x2) l

theorem StrictMono.sorted_le_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictMono f) : List.Sorted (fun (x1 x2 : β) => x1 ≤ x2) (List.map f l) ↔ List.Sorted (fun (x1 x2 : α) => x1 ≤ x2) l

theorem StrictMono.sorted_ge_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictMono f) : List.Sorted (fun (x1 x2 : β) => x1 ≥ x2) (List.map f l) ↔ List.Sorted (fun (x1 x2 : α) => x1 ≥ x2) l

theorem StrictMono.sorted_lt_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictMono f) : List.Sorted (fun (x1 x2 : β) => x1 < x2) (List.map f l) ↔ List.Sorted (fun (x1 x2 : α) => x1 < x2) l

theorem StrictMono.sorted_gt_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictMono f) : List.Sorted (fun (x1 x2 : β) => x1 > x2) (List.map f l) ↔ List.Sorted (fun (x1 x2 : α) => x1 > x2) l

theorem StrictAnti.sorted_le_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictAnti f) : List.Sorted (fun (x1 x2 : β) => x1 ≤ x2) (List.map f l) ↔ List.Sorted (fun (x1 x2 : α) => x1 ≥ x2) l

theorem StrictAnti.sorted_ge_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictAnti f) : List.Sorted (fun (x1 x2 : β) => x1 ≥ x2) (List.map f l) ↔ List.Sorted (fun (x1 x2 : α) => x1 ≤ x2) l

theorem StrictAnti.sorted_lt_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictAnti f) : List.Sorted (fun (x1 x2 : β) => x1 < x2) (List.map f l) ↔ List.Sorted (fun (x1 x2 : α) => x1 > x2) l

theorem StrictAnti.sorted_gt_listMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {l : List α} (hf : StrictAnti f) : List.Sorted (fun (x1 x2 : β) => x1 > x2) (List.map f l) ↔ List.Sorted (fun (x1 x2 : α) => x1 < x2) l

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) : 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 : α) : orderedInsert r a [] = [a]

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

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

@[simp]

theorem List.mem_orderedInsert {α : Type u} (r : α → α → Prop) [DecidableRel r] {a b : α} {l : List α} : a ∈ 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)) : map f (orderedInsert r x l) = orderedInsert s (f x) (map f l)

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

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

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

@[simp]

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

@[simp]

theorem List.length_insertionSort {α : Type u} (r : α → α → Prop) [DecidableRel r] (l : 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) : insertionSort r (a :: l) = a :: 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)) : map f (insertionSort r l) = insertionSort s (map f l)

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

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

theorem List.sorted_insertionSort {α : Type u} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l : List α) : Sorted r (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 : Pairwise r c) (hc : c.Sublist l) : c.Sublist (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 (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 : Sorted r c) (hc : c.Subperm l) : c.Sublist (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 (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 : Sorted r l) (h' : Sorted r l') : Sorted r (l.merge l' fun (x1 x2 : α) => Decidable.decide (r x1 x2))

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

Variant of sorted_mergeSort using relation typeclasses.

theorem List.mergeSort_eq_self {α : Type u} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] [IsAntisymm α r] {l : List α} : Sorted r l → (l.mergeSort fun (x1 x2 : α) => decide (r x1 x2)) = 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)) = insertionSort r l