# 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` #

source
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

Instances For

source
instance List.decidableSorted {α : Type u} {r : α → α → Prop} [DecidableRel r] (l : List α) :
Decidable (Sorted r l)
Equations

- l.decidableSorted = l.instDecidablePairwise

source
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
source
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
source
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
source
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
source
@[simp]
theorem List.sorted_nil {α : Type u} {r : α → α → Prop} :
Sorted r []
source
theorem List.Sorted.of_cons {α : Type u} {r : α → α → Prop} {a : α} {l : List α} :
Sorted r (a :: l) → Sorted r l
source
theorem List.Sorted.tail {α : Type u} {r : α → α → Prop} {l : List α} (h : Sorted r l) :
Sorted r l.tail
source
theorem List.rel_of_sorted_cons {α : Type u} {r : α → α → Prop} {a : α} {l : List α} :
Sorted r (a :: l) → ∀ b ∈ l, r a b
source
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)
source
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)
source
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
source
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!
source
@[simp]
theorem List.sorted_cons {α : Type u} {r : α → α → Prop} {a : α} {l : List α} :
Sorted r (a :: l) ↔ (∀ b ∈ l, r a b) ∧ Sorted r l
source
theorem List.Sorted.nodup {α : Type u} {r : α → α → Prop} [IsIrrefl α r] {l : List α} (h : Sorted r l) :
l.Nodup
source
theorem List.Sorted.filter {α : Type u} {r : α → α → Prop} {l : List α} (f : α → Bool) (h : Sorted r l) :
Sorted r (filter f l)
source
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₂
source
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₂
source
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₂
source
@[simp]
theorem List.sorted_singleton {α : Type u} {r : α → α → Prop} (a : α) :
Sorted r [a]
source
theorem List.sorted_lt_range (n : ℕ) :
Sorted (fun (x1 x2 : ℕ) => x1 < x2) (range n)
source
theorem List.sorted_replicate {α : Type u} {r : α → α → Prop} (n : ℕ) (a : α) :
Sorted r (replicate n a) ↔ n ≤ 1 ∨ r a a
source
theorem List.sorted_le_replicate {α : Type u} (n : ℕ) (a : α) [Preorder α] :
Sorted (fun (x1 x2 : α) => x1 ≤ x2) (replicate n a)
source
theorem List.sorted_le_range (n : ℕ) :
Sorted (fun (x1 x2 : ℕ) => x1 ≤ x2) (range n)
source
theorem List.sorted_lt_range' (a b : ℕ) {s : ℕ} (hs : s ≠ 0) :
Sorted (fun (x1 x2 : ℕ) => x1 < x2) (range' a b s)
source
theorem List.sorted_le_range' (a b s : ℕ) :
Sorted (fun (x1 x2 : ℕ) => x1 ≤ x2) (range' a b s)
source
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)
source
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)
source
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
source
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.

source
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
source
@[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.

source
@[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.

source
@[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.

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

source
@[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.

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

source
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)
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 #

source
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

Instances For

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

Instances For

source
@[simp]
theorem List.orderedInsert_nil {α : Type u} (r : α → α → Prop) [DecidableRel r] (a : α) :
orderedInsert r a [] = [a]
source
theorem List.orderedInsert_length {α : Type u} (r : α → α → Prop) [DecidableRel r] (L : List α) (a : α) :
(orderedInsert r a L).length = L.length + 1
source
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`.

source
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)
source
@[simp]
theorem List.mem_orderedInsert {α : Type u} (r : α → α → Prop) [DecidableRel r] {a b : α} {l : List α} :
a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l
source
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)
source
theorem List.perm_orderedInsert {α : Type u} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) :
(orderedInsert r a l).Perm (a :: l)
source
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
source
theorem List.perm_insertionSort {α : Type u} (r : α → α → Prop) [DecidableRel r] (l : List α) :
(insertionSort r l).Perm l
source
@[simp]
theorem List.mem_insertionSort {α : Type u} (r : α → α → Prop) [DecidableRel r] {l : List α} {x : α} :
x ∈ insertionSort r l ↔ x ∈ l
source
@[simp]
theorem List.length_insertionSort {α : Type u} (r : α → α → Prop) [DecidableRel r] (l : List α) :
(insertionSort r l).length = l.length
source
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
source
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)
source
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.

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

source
theorem List.erase_orderedInsert_of_notMem {α : 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.

source
@[deprecated List.erase_orderedInsert_of_notMem (since := "2025-05-23")]
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

Alias of `List.erase_orderedInsert_of_notMem`.

Inserting then erasing an element that is absent is the identity.

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

source
theorem List.sublist_orderedInsert {α : Type u} {r : α → α → Prop} [DecidableRel r] (x : α) (xs : List α) :
xs.Sublist (orderedInsert r x xs)
source
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)
source
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)
source
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)
source
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`.

source
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`.

source
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`.

source
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`.

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

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

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