mathlib3 documentation

data.list.sort

Sorting algorithms on lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.insertion_sort and list.merge_sort, and prove their correctness.

The predicate list.sorted #

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

Equations
Instances for list.sorted
source
@[protected, instance]
def list.decidable_sorted {α : Type uu} {r : α → α → Prop} [decidable_rel r] (l : list α) :
decidable (list.sorted r l)
Equations
source
@[simp]
theorem list.sorted_nil {α : Type uu} {r : α → α → Prop} :
list.sorted r list.nil
source
theorem list.sorted.of_cons {α : Type uu} {r : α → α → Prop} {a : α} {l : list α} :
list.sorted r (a :: l) → list.sorted r l
source
theorem list.sorted.tail {α : Type uu} {r : α → α → Prop} {l : list α} (h : list.sorted r l) :
list.sorted r l.tail
source
theorem list.rel_of_sorted_cons {α : Type uu} {r : α → α → Prop} {a : α} {l : list α} :
list.sorted r (a :: l) → ∀ (b : α), b ∈ l → r a b
source
@[simp]
theorem list.sorted_cons {α : Type uu} {r : α → α → Prop} {a : α} {l : list α} :
list.sorted r (a :: l) ↔ (∀ (b : α), b ∈ l → r a b) ∧ list.sorted r l
source
@[protected]
theorem list.sorted.nodup {α : Type uu} {r : α → α → Prop} [is_irrefl α r] {l : list α} (h : list.sorted r l) :
l.nodup
source
theorem list.eq_of_perm_of_sorted {α : Type uu} {r : α → α → Prop} [is_antisymm α r] {l₁ l₂ : list α} (p : l₁ ~ l₂) (s₁ : list.sorted r l₁) (s₂ : list.sorted r l₂) :
l₁ = l₂
source
theorem list.sublist_of_subperm_of_sorted {α : Type uu} {r : α → α → Prop} [is_antisymm α r] {l₁ l₂ : list α} (p : l₁ <+~ l₂) (s₁ : list.sorted r l₁) (s₂ : list.sorted r l₂) :
l₁ <+ l₂
source
@[simp]
theorem list.sorted_singleton {α : Type uu} {r : α → α → Prop} (a : α) :
list.sorted r [a]
source
theorem list.sorted.rel_nth_le_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.nth_le a ha) (l.nth_le b hb)
source
theorem list.sorted.rel_nth_le_of_le {α : Type uu} {r : α → α → Prop} [is_refl α r] {l : list α} (h : list.sorted r l) {a b : ℕ} (ha : a < l.length) (hb : b < l.length) (hab : a ≤ b) :
r (l.nth_le a ha) (l.nth_le b hb)
source
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
source
theorem list.monotone_iff_of_fn_sorted {n : ℕ} {α : Type uu} [preorder α] {f : fin n → α} :
monotone f ↔ list.sorted has_le.le (list.of_fn f)

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

source
theorem list.monotone.of_fn_sorted {n : ℕ} {α : Type uu} [preorder α] {f : fin n → α} (h : monotone f) :
list.sorted has_le.le (list.of_fn f)

The list obtained from a monotone tuple is sorted.

Insertion sort #

source
@[simp]
def list.ordered_insert {α : Type uu} (r : α → α → Prop) [decidable_rel r] (a : α) :
list α → list α

ordered_insert a l inserts a into l at such that ordered_insert a l is sorted if l is.

Equations
source
@[simp]
def list.insertion_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] :
list α → list α

insertion_sort l returns l sorted using the insertion sort algorithm.

Equations
source
@[simp]
theorem list.ordered_insert_nil {α : Type uu} (r : α → α → Prop) [decidable_rel r] (a : α) :
list.ordered_insert r a list.nil = [a]
source
theorem list.ordered_insert_length {α : Type uu} (r : α → α → Prop) [decidable_rel r] (L : list α) (a : α) :
(list.ordered_insert r a L).length = L.length + 1
source
theorem list.ordered_insert_eq_take_drop {α : Type uu} (r : α → α → Prop) [decidable_rel r] (a : α) (l : list α) :
list.ordered_insert r a l = list.take_while (λ (b : α), ¬r a b) l ++ a :: list.drop_while (λ (b : α), ¬r a b) l

An alternative definition of ordered_insert using take_while and drop_while.

source
theorem list.insertion_sort_cons_eq_take_drop {α : Type uu} (r : α → α → Prop) [decidable_rel r] (a : α) (l : list α) :
list.insertion_sort r (a :: l) = list.take_while (λ (b : α), ¬r a b) (list.insertion_sort r l) ++ a :: list.drop_while (λ (b : α), ¬r a b) (list.insertion_sort r l)
source
theorem list.perm_ordered_insert {α : Type uu} (r : α → α → Prop) [decidable_rel r] (a : α) (l : list α) :
list.ordered_insert r a l ~ a :: l
source
theorem list.ordered_insert_count {α : Type uu} (r : α → α → Prop) [decidable_rel r] [decidable_eq α] (L : list α) (a b : α) :
list.count a (list.ordered_insert r b L) = list.count a L + ite (a = b) 1 0
source
theorem list.perm_insertion_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] (l : list α) :
list.insertion_sort r l ~ l
source
theorem list.sorted.insertion_sort_eq {α : Type uu} {r : α → α → Prop} [decidable_rel r] {l : list α} (h : list.sorted r l) :
list.insertion_sort r l = l

If l is already list.sorted with respect to r, then insertion_sort does not change it.

source
theorem list.sorted.ordered_insert {α : Type uu} {r : α → α → Prop} [decidable_rel r] [is_total α r] [is_trans α r] (a : α) (l : list α) :
list.sorted r l → list.sorted r (list.ordered_insert r a l)
source
theorem list.sorted_insertion_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] [is_total α r] [is_trans α r] (l : list α) :
list.sorted r (list.insertion_sort r l)

The list list.insertion_sort r l is list.sorted with respect to r.

Merge sort #

source
@[simp]
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
source
theorem list.split_cons_of_eq {α : Type uu} (a : α) {l l₁ l₂ : list α} (h : l.split = (l₁, l₂)) :
(a :: l).split = (a :: l₂, l₁)
source
theorem list.length_split_le {α : Type uu} {l l₁ l₂ : list α} :
l.split = (l₁, l₂) → l₁.length ≤ l.length ∧ l₂.length ≤ l.length
source
theorem list.length_split_lt {α : Type uu} {a b : α} {l l₁ l₂ : list α} (h : (a :: b :: l).split = (l₁, l₂)) :
l₁.length < (a :: b :: l).length ∧ l₂.length < (a :: b :: l).length
source
theorem list.perm_split {α : Type uu} {l l₁ l₂ : list α} :
l.split = (l₁, l₂) → l ~ l₁ ++ l₂
source
def list.merge {α : Type uu} (r : α → α → Prop) [decidable_rel r] :
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
source
def list.merge_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] :
list α → list α

Implementation of a merge sort algorithm to sort a list.

Equations
source
theorem list.merge_sort_cons_cons {α : Type uu} (r : α → α → Prop) [decidable_rel r] {a b : α} {l l₁ l₂ : list α} (h : (a :: b :: l).split = (l₁, l₂)) :
list.merge_sort r (a :: b :: l) = list.merge r (list.merge_sort r l₁) (list.merge_sort r l₂)
source
theorem list.perm_merge {α : Type uu} (r : α → α → Prop) [decidable_rel r] (l l' : list α) :
list.merge r l l' ~ l ++ l'
source
theorem list.perm_merge_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] (l : list α) :
list.merge_sort r l ~ l
source
@[simp]
theorem list.length_merge_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] (l : list α) :
(list.merge_sort r l).length = l.length
source
theorem list.sorted.merge {α : Type uu} {r : α → α → Prop} [decidable_rel r] [is_total α r] [is_trans α r] {l l' : list α} :
list.sorted r l → list.sorted r l' → list.sorted r (list.merge r l l')
source
theorem list.sorted_merge_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] [is_total α r] [is_trans α r] (l : list α) :
list.sorted r (list.merge_sort r l)
source
theorem list.merge_sort_eq_self {α : Type uu} (r : α → α → Prop) [decidable_rel r] [is_total α r] [is_trans α r] [is_antisymm α r] {l : list α} :
list.sorted r l → list.merge_sort r l = l
source
theorem list.merge_sort_eq_insertion_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] [is_total α r] [is_trans α r] [is_antisymm α r] (l : list α) :
list.merge_sort r l = list.insertion_sort r l
source
@[simp]
theorem list.merge_sort_nil {α : Type uu} (r : α → α → Prop) [decidable_rel r] :
list.merge_sort r list.nil = list.nil
source
@[simp]
theorem list.merge_sort_singleton {α : Type uu} (r : α → α → Prop) [decidable_rel r] (a : α) :
list.merge_sort r [a] = [a]