Basic properties of mergeSort.

• mergeSort_sorted: mergeSort produces a sorted list.
• mergeSort_perm: mergeSort is a permutation of the input list.
• mergeSort_of_sorted: 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.
• mergeSort_stable: if c is a sorted sublist of l, then c is still a sublist of mergeSort le l.

splitInTwo

@[simp]

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

@[simp]

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

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

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

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

theorem List.splitInTwo_fst_sorted {α : Type u_1} {le : α → α → Bool} {n : Nat} (l : { l : List α // l.length = n }) (h : List.Pairwise (fun (a b : α) => le a b = true) l.val) : List.Pairwise (fun (a b : α) => le a b = true) (List.splitInTwo l).fst.val

theorem List.splitInTwo_snd_sorted {α : Type u_1} {le : α → α → Bool} {n : Nat} (l : { l : List α // l.length = n }) (h : List.Pairwise (fun (a b : α) => le a b = true) l.val) : List.Pairwise (fun (a b : α) => le a b = true) (List.splitInTwo l).snd.val

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

enumLE

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

theorem List.enumLE_total {α : Type u_1} {le : α → α → Bool} (total : ∀ (a b : α), (!le a b) = true → le b a = true) (a : Nat × α) (b : Nat × α) : (!List.enumLE le a b) = true → List.enumLE le b a = true

merge

@[irreducible]

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

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

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

theorem List.merge_sorted {α : 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) = true → le b a = true) (l₁ : List α) (l₂ : List α) (h₁ : List.Pairwise (fun (a b : α) => le a b = true) l₁) (h₂ : List.Pairwise (fun (a b : α) => le a b = true) l₂) : List.Pairwise (fun (a b : α) => le a b = true) (List.merge le l₁ l₂)

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.

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

@[irreducible]

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

mergeSort

@[simp]

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

@[simp]

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

@[irreducible]

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

@[simp]

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

@[simp]

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

@[irreducible]

theorem List.mergeSort_sorted {α : 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) = true → le b a = true) (l : List α) : List.Pairwise (fun (a b : α) => le a b = true) (List.mergeSort le l)

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.

@[irreducible]

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

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

theorem List.mergeSort_enum {α : Type u_1} {le : α → α → Bool} {l : List α} : List.map (fun (x : Nat × α) => x.snd) (List.mergeSort (List.enumLE le) l.enum) = List.mergeSort le l

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:

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

@[irreducible]

theorem List.mergeSort_enum.go {α : Type u_1} {le : α → α → Bool} (i : Nat) (l : List α) : List.map (fun (x : Nat × α) => x.snd) (List.mergeSort (List.enumLE le) (List.enumFrom i l)) = List.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) = true → le b a = true) (a : α) (l : List α) : ∃ (l₁ : List α), ∃ (l₂ : List α), List.mergeSort le (a :: l) = l₁ ++ a :: l₂ ∧ List.mergeSort le l = l₁ ++ l₂ ∧ ∀ (b : α), b ∈ l₁ → (!le a b) = true

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

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.mergeSort_stable_pair {α : 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) = true → le b a = true) (hab : le a b = true) (h : [a, b].Sublist l) : [a, b].Sublist (List.mergeSort le l)

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.