Basic properties of mergeSort.

• pairwise_mergeSort: mergeSort produces a sorted list.
• mergeSort_perm: mergeSort is a permutation of the input list.
• mergeSort_of_pairwise: mergeSort does not change a sorted list.
• mergeSort_cons: proves mergeSort le (x :: xs) = l₁ ++ x :: l₂ for some l₁, l₂ so that mergeSort le xs = l₁ ++ l₂, and no a ∈ l₁ satisfies le a x.
• sublist_mergeSort: if c is a sorted sublist of l, then c is still a sublist of mergeSort le l.

splitInTwo

@[simp]

theorem List.MergeSort.Internal.splitInTwo_fst {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : (splitInTwo l).fst = ⟨take ((n + 1) / 2) l.val, ⋯⟩

@[simp]

theorem List.MergeSort.Internal.splitInTwo_snd {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : (splitInTwo l).snd = ⟨drop ((n + 1) / 2) l.val, ⋯⟩

theorem List.MergeSort.Internal.splitInTwo_fst_append_splitInTwo_snd {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : (splitInTwo l).fst.val ++ (splitInTwo l).snd.val = l.val

theorem List.MergeSort.Internal.splitInTwo_cons_cons_zipIdx_fst {α : Type u_1} {a b : α} (i : Nat) (l : List α) : (splitInTwo ⟨(a, i) :: (b, i + 1) :: l.zipIdx (i + 2), ⋯⟩).fst.val = (splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.zipIdx i

theorem List.MergeSort.Internal.splitInTwo_cons_cons_zipIdx_snd {α : Type u_1} {a b : α} (i : Nat) (l : List α) : (splitInTwo ⟨(a, i) :: (b, i + 1) :: l.zipIdx (i + 2), ⋯⟩).snd.val = (splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.zipIdx (i + (l.length + 3) / 2)

theorem List.MergeSort.Internal.splitInTwo_fst_pairwise {α : Type u_1} {n : Nat} {le : α → α → Prop} (l : { l : List α // l.length = n }) (h : Pairwise le l.val) : Pairwise le (splitInTwo l).fst.val

@[reducible, inline, deprecated List.MergeSort.Internal.splitInTwo_fst_pairwise (since := "2025-10-23")]

abbrev List.MergeSort.Internal.splitInTwo_fst_sorted {α : Type u_1} {n : Nat} {le : α → α → Prop} (l : { l : List α // l.length = n }) (h : Pairwise le l.val) : Pairwise le (splitInTwo l).fst.val

Equations

• @List.MergeSort.Internal.splitInTwo_fst_sorted = @List.MergeSort.Internal.splitInTwo_fst_pairwise

theorem List.MergeSort.Internal.splitInTwo_snd_pairwise {α : Type u_1} {n : Nat} {le : α → α → Prop} (l : { l : List α // l.length = n }) (h : Pairwise le l.val) : Pairwise le (splitInTwo l).snd.val

@[reducible, inline, deprecated List.MergeSort.Internal.splitInTwo_snd_pairwise (since := "2025-10-23")]

abbrev List.MergeSort.Internal.splitInTwo_snd_sorted {α : Type u_1} {n : Nat} {le : α → α → Prop} (l : { l : List α // l.length = n }) (h : Pairwise le l.val) : Pairwise le (splitInTwo l).fst.val

Equations

• @List.MergeSort.Internal.splitInTwo_snd_sorted = @List.MergeSort.Internal.splitInTwo_fst_pairwise

theorem List.MergeSort.Internal.splitInTwo_fst_le_splitInTwo_snd {α : Type u_1} {n : Nat} {le : α → α → Prop} {l : { l : List α // l.length = n }} (h : Pairwise le l.val) (a b : α) : a ∈ (splitInTwo l).fst.val → b ∈ (splitInTwo l).snd.val → le a b

zipIdxLE

theorem List.zipIdxLE_trans {α : Type u_1} {le : α → α → Bool} (trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true) (a b c : α × Nat) : zipIdxLE le a b = true → zipIdxLE le b c = true → zipIdxLE le a c = true

theorem List.zipIdxLE_total {α : Type u_1} {le : α → α → Bool} (total : ∀ (a b : α), (le a b || le b a) = true) (a b : α × Nat) : (zipIdxLE le a b || zipIdxLE le b a) = true

merge

theorem List.cons_merge_cons {α : Type u_1} (s : α → α → Bool) (a b : α) (l r : List α) : (a :: l).merge (b :: r) s = if s a b = true then a :: l.merge (b :: r) s else b :: (a :: l).merge r s

@[simp]

theorem List.cons_merge_cons_pos {α : Type u_1} {a b : α} (s : α → α → Bool) (l r : List α) (h : s a b = true) : (a :: l).merge (b :: r) s = a :: l.merge (b :: r) s

@[simp]

theorem List.cons_merge_cons_neg {α : Type u_1} {a b : α} (s : α → α → Bool) (l r : List α) (h : ¬s a b = true) : (a :: l).merge (b :: r) s = b :: (a :: l).merge r s

@[simp, irreducible]

theorem List.length_merge {α : Type u_1} (s : α → α → Bool) (l r : List α) : (l.merge r s).length = l.length + r.length

theorem List.mem_merge {α : Type u_1} {le : α → α → Bool} {a : α} {xs ys : List α} : a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys

The elements of merge le xs ys are exactly the elements of xs and ys.

theorem List.mem_merge_left {α : Type u_1} {l : List α} {x : α} {r : List α} (s : α → α → Bool) (h : x ∈ l) : x ∈ l.merge r s

theorem List.mem_merge_right {α : Type u_1} {r : List α} {x : α} {l : List α} (s : α → α → Bool) (h : x ∈ r) : x ∈ l.merge r s

@[irreducible]

theorem List.merge_stable {α : Type u_1} {le : α → α → Bool} (xs ys : List (α × Nat)) : (∀ (x y : α × Nat), x ∈ xs → y ∈ ys → x.snd ≤ y.snd) → map (fun (x : α × Nat) => x.fst) (xs.merge ys (zipIdxLE le)) = (map (fun (x : α × Nat) => x.fst) xs).merge (map (fun (x : α × Nat) => x.fst) ys) le

theorem List.pairwise_merge {α : Type u_1} {le : α → α → Bool} (trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true) (total : ∀ (a b : α), (le a b || le b a) = true) (l₁ l₂ : List α) (h₁ : Pairwise (fun (a b : α) => le a b = true) l₁) (h₂ : Pairwise (fun (a b : α) => le a b = true) l₂) : Pairwise (fun (a b : α) => le a b = true) (l₁.merge l₂ le)

If the ordering relation le is transitive and total (i.e. le a b || le b a for all a, b) then the merge of two sorted lists is sorted.

@[reducible, inline, deprecated List.pairwise_merge (since := "2025-10-23")]

abbrev List.sorted_merge {α : Type u_1} {le : α → α → Bool} (trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true) (total : ∀ (a b : α), (le a b || le b a) = true) (l₁ l₂ : List α) (h₁ : Pairwise (fun (a b : α) => le a b = true) l₁) (h₂ : Pairwise (fun (a b : α) => le a b = true) l₂) : Pairwise (fun (a b : α) => le a b = true) (l₁.merge l₂ le)

Equations

• @List.sorted_merge = @List.pairwise_merge

theorem List.merge_of_le {α : Type u_1} {le : α → α → Bool} {xs ys : List α} : (∀ (a b : α), a ∈ xs → b ∈ ys → le a b = true) → xs.merge ys le = xs ++ ys

@[irreducible]

theorem List.merge_perm_append {α : Type u_1} (le : α → α → Bool) {xs ys : List α} : (xs.merge ys le).Perm (xs ++ ys)

theorem List.Perm.merge {α : Type u_1} {l₁ l₂ r₁ r₂ : List α} (s₁ s₂ : α → α → Bool) (hl : l₁.Perm l₂) (hr : r₁.Perm r₂) : (l₁.merge r₁ s₁).Perm (l₂.merge r₂ s₂)

mergeSort

@[simp]

theorem List.mergeSort_nil {α✝ : Type u_1} {r : α✝ → α✝ → Bool} : [].mergeSort r = []

@[simp]

theorem List.mergeSort_singleton {α : Type u_1} {r : α → α → Bool} (a : α) : [a].mergeSort r = [a]

@[irreducible]

theorem List.mergeSort_perm {α : Type u_1} (l : List α) (le : α → α → Bool) : (l.mergeSort le).Perm l

@[simp]

theorem List.length_mergeSort {α : Type u_1} {le : α → α → Bool} (l : List α) : (l.mergeSort le).length = l.length

@[simp]

theorem List.mem_mergeSort {α : Type u_1} {le : α → α → Bool} {a : α} {l : List α} : a ∈ l.mergeSort le ↔ a ∈ l

@[irreducible]

theorem List.pairwise_mergeSort {α : Type u_1} {le : α → α → Bool} (trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true) (total : ∀ (a b : α), (le a b || le b a) = true) (l : List α) : Pairwise (fun (a b : α) => le a b = true) (l.mergeSort le)

The result of mergeSort is sorted, as long as the comparison function is transitive (le a b → le b c → le a c) and total in the sense that le a b || le b a.

The comparison function need not be irreflexive, i.e. le a b and le b a is allowed even when a ≠ b.

@[reducible, inline, deprecated List.pairwise_mergeSort (since := "2025-10-23")]

abbrev List.sorted_mergeSort {α : Type u_1} {le : α → α → Bool} (trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true) (total : ∀ (a b : α), (le a b || le b a) = true) (l : List α) : Pairwise (fun (a b : α) => le a b = true) (l.mergeSort le)

Equations

• @List.sorted_mergeSort = @List.pairwise_mergeSort

@[irreducible]

theorem List.mergeSort_of_pairwise {α : Type u_1} {le : α → α → Bool} {l : List α} : Pairwise (fun (a b : α) => le a b = true) l → l.mergeSort le = l

If the input list is already sorted, then mergeSort does not change the list.

@[reducible, inline, deprecated List.mergeSort_of_pairwise (since := "2025-10-23")]

abbrev List.mergeSort_of_sorted {α : Type u_1} {le : α → α → Bool} {l : List α} : Pairwise (fun (a b : α) => le a b = true) l → l.mergeSort le = l

Equations

• @List.mergeSort_of_sorted = @List.mergeSort_of_pairwise

theorem List.mergeSort_zipIdx {α : Type u_1} {le : α → α → Bool} {l : List α} : map (fun (x : α × Nat) => x.fst) (l.zipIdx.mergeSort (zipIdxLE le)) = l.mergeSort le

This merge sort algorithm is stable, in the sense that breaking ties in the ordering function using the position in the list has no effect on the output.

That is, elements which are equal with respect to the ordering function will remain in the same order in the output list as they were in the input list.

See also:

• sublist_mergeSort: if c <+ l and c.Pairwise le, then c <+ mergeSort le l.
• pair_sublist_mergeSort: if [a, b] <+ l and le a b, then [a, b] <+ mergeSort le l)

theorem List.mergeSort_cons {α : Type u_1} {le : α → α → Bool} (trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true) (total : ∀ (a b : α), (le a b || le b a) = true) (a : α) (l : List α) : ∃ (l₁ : List α), ∃ (l₂ : List α), (a :: l).mergeSort le = l₁ ++ a :: l₂ ∧ l.mergeSort le = l₁ ++ l₂ ∧ ∀ (b : α), b ∈ l₁ → (!le a b) = true

theorem List.sublist_mergeSort {α : Type u_1} {le : α → α → Bool} {xs : List α} (trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true) (total : ∀ (a b : α), (le a b || le b a) = true) {ys : List α} : Pairwise (fun (a b : α) => le a b = true) ys → ys.Sublist xs → ys.Sublist (xs.mergeSort le)

Another statement of stability of merge sort. If c is a sorted sublist of l, then c is still a sublist of mergeSort le l.

theorem List.pair_sublist_mergeSort {α : Type u_1} {le : α → α → Bool} {a b : α} {l : List α} (trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true) (total : ∀ (a b : α), (le a b || le b a) = true) (hab : le a b = true) (h : [a, b].Sublist l) : [a, b].Sublist (l.mergeSort le)

Another statement of stability of merge sort. If a pair [a, b] is a sublist of l and le a b, then [a, b] is still a sublist of mergeSort le l.

@[irreducible]

theorem List.map_merge {α : Type u_2} {β : Type u_1} {f : α → β} {r : α → α → Bool} {s : β → β → Bool} {l l' : List α} (hl : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l' → r a b = s (f a) (f b)) : map f (l.merge l' r) = (map f l).merge (map f l') s

@[irreducible]

theorem List.map_mergeSort {α : Type u_2} {β : Type u_1} {r : α → α → Bool} {s : β → β → Bool} {f : α → β} {l : List α} (hl : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b = s (f a) (f b)) : map f (l.mergeSort r) = (map f l).mergeSort s