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
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 α} :
list.sorted r l → list.sorted r l.tail
theorem
list.rel_of_sorted_cons
{α : Type uu}
{r : α → α → Prop}
{a : α}
{l : list α}
(a_1 : list.sorted r (a :: l))
(b : α) :
b ∈ l → r a b
@[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
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]
@[simp]
ordered_insert a l inserts a into l at such that
ordered_insert a l is sorted if l is.
Equations
- list.ordered_insert r a (b :: l) = ite (r a b) (a :: b :: l) (b :: list.ordered_insert r a l)
- list.ordered_insert r a list.nil = [a]
@[simp]
insertion_sort l returns l sorted using the insertion sort algorithm.
Equations
- list.insertion_sort r (b :: l) = list.ordered_insert r b (list.insertion_sort r l)
- list.insertion_sort r list.nil = list.nil
@[simp]
theorem
list.ordered_insert_nil
{α : Type uu}
(r : α → α → Prop)
[decidable_rel r]
(a : α) :
list.ordered_insert r a list.nil = [a]
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
theorem
list.perm_ordered_insert
{α : Type uu}
(r : α → α → Prop)
[decidable_rel r]
(a : α)
(l : list α) :
list.ordered_insert r a l ~ a :: l
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 α) :
list.insertion_sort r l ~ l
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)
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)
@[simp]
Split l into two lists of approximately equal length.
split [1, 2, 3, 4, 5] = ([1, 3, 5], [2, 4])
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
- list.merge r (a :: l) (b :: l') = ite (r a b) (a :: list.merge r l (b :: l')) (b :: list.merge r (a :: l) l')
- list.merge r (hd :: tl) list.nil = hd :: tl
- list.merge r list.nil (hd :: tl) = hd :: tl
- list.merge r list.nil list.nil = list.nil
Implementation of a merge sort algorithm to sort a list.
Equations
- list.merge_sort r (a :: b :: l) = (λ (_x : list α × list α) (e : (a :: b :: l).split = _x), _x.cases_on (λ (l₁ l₂ : list α) (e : (a :: b :: l).split = (l₁, l₂)), _.dcases_on (λ (h₁ : l₁.length < (a :: b :: l).length) (h₂ : l₂.length < (a :: b :: l).length), list.merge r (list.merge_sort r l₁) (list.merge_sort r l₂))) e) (a :: b :: l).split _
- list.merge_sort r [a] = [a]
- list.merge_sort r list.nil = list.nil
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 α) :
list.merge_sort r l ~ l
@[simp]
theorem
list.length_merge_sort
{α : Type uu}
(r : α → α → Prop)
[decidable_rel r]
(l : list α) :
(list.merge_sort r l).length = l.length
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')
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)
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