mathlib documentation

data.list.sort

def list.sorted {α : Type u_1} :
(α → α → 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
@[instance]
def list.decidable_sorted {α : Type uu} {r : α → α → Prop} [decidable_rel r] (l : list α) :

Equations
@[simp]
theorem list.sorted_nil {α : Type uu} {r : α → α → Prop} :

theorem list.sorted_of_sorted_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 α} :

theorem list.rel_of_sorted_cons {α : Type uu} {r : α → α → Prop} {a : α} {l : list α} (a_1 : list.sorted r (a :: l)) (b : α) :
b lr a b

@[simp]
theorem list.sorted_cons {α : Type uu} {r : α → α → Prop} {a : α} {l : list α} :
list.sorted r (a :: l) (∀ (b : α), b lr a b) list.sorted r l

theorem list.eq_of_sorted_of_perm {α : Type uu} {r : α → α → Prop} [is_antisymm α r] {l₁ l₂ : list α} :
l₁ ~ l₂list.sorted r l₁list.sorted r l₂l₁ = l₂

@[simp]
theorem list.sorted_singleton {α : Type uu} {r : α → α → Prop} (a : α) :

theorem list.nth_le_of_sorted_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} :
a br (l.nth_le a ha) (l.nth_le b hb)

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

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

Equations
@[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
@[simp]
theorem list.ordered_insert_nil {α : Type uu} (r : α → α → Prop) [decidable_rel r] (a : α) :

theorem list.ordered_insert_length {α : Type uu} (r : α → α → Prop) [decidable_rel r] (L : list α) (a : α) :

theorem list.perm_ordered_insert {α : Type uu} (r : α → α → Prop) [decidable_rel r] (a : α) (l : list α) :

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

theorem list.perm_insertion_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] (l : list α) :

theorem list.sorted_ordered_insert {α : Type uu} (r : α → α → Prop) [decidable_rel r] [is_total α r] [is_trans α r] (a : α) (l : list α) :

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

@[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
theorem list.split_cons_of_eq {α : Type uu} (a : α) {l l₁ l₂ : list α} :
l.split = (l₁, l₂)(a :: l).split = (a :: l₂, l₁)

theorem list.length_split_le {α : Type uu} {l l₁ l₂ : list α} :
l.split = (l₁, l₂)l₁.length l.length l₂.length l.length

theorem list.length_split_lt {α : Type uu} {a b : α} {l l₁ l₂ : list α} :
(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 l₁ l₂ : list α} :
l.split = (l₁, l₂)l ~ l₁ ++ l₂

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
def list.merge_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] :
list αlist α

Implementation of a merge sort algorithm to sort a list.

Equations
theorem list.merge_sort_cons_cons {α : Type uu} (r : α → α → Prop) [decidable_rel r] {a b : α} {l l₁ l₂ : list α} :
(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₂)

theorem list.perm_merge {α : Type uu} (r : α → α → Prop) [decidable_rel r] (l l' : list α) :
list.merge r l l' ~ l ++ l'

theorem list.perm_merge_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] (l : list α) :

@[simp]
theorem list.length_merge_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] (l : list α) :

theorem list.sorted_merge {α : Type uu} (r : α → α → Prop) [decidable_rel r] [is_total α r] [is_trans α r] {l l' : list α} :
list.sorted r llist.sorted r l'list.sorted r (list.merge r l l')

theorem list.sorted_merge_sort {α : Type uu} (r : α → α → Prop) [decidable_rel r] [is_total α r] [is_trans α r] (l : list α) :

theorem list.merge_sort_eq_self {α : Type uu} (r : α → α → Prop) [decidable_rel r] [is_total α r] [is_trans α r] [is_antisymm α r] {l : list α} :