# Basic properties of `mergeSort`. #

- `sorted_mergeSort`: `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`.
- `sublist_mergeSort`: if `c` is a sorted sublist of `l`, then `c` is still a sublist of `mergeSort le l`.

### splitInTwo #

source
@[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, ⋯⟩
source
@[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, ⋯⟩
source
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
source
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
source
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)
source
theorem 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
source
theorem 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).snd.val
source
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 #

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

source
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
source
@[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
source
@[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
source
@[simp, irreducible]
theorem List.length_merge {α : Type u_1} (s : α → α → Bool) (l r : List α) :
(l.merge r s).length = l.length + r.length
source
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`.

source
theorem List.mem_merge_left {α : Type u_1} {l : List α} {x : α} {r : List α} (s : α → α → Bool) (h : x ∈ l) :
x ∈ l.merge r s
source
theorem List.mem_merge_right {α : Type u_1} {r : List α} {x : α} {l : List α} (s : α → α → Bool) (h : x ∈ r) :
x ∈ l.merge r s
source
@[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
source
theorem 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)

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.

source
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
source
@[irreducible]
theorem List.merge_perm_append {α : Type u_1} (le : α → α → Bool) {xs ys : List α} :
(xs.merge ys le).Perm (xs ++ ys)
source
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 #

source
@[simp]
theorem List.mergeSort_nil {α✝ : Type u_1} {r : α✝ → α✝ → Bool} :
[].mergeSort r = []
source
@[simp]
theorem List.mergeSort_singleton {α : Type u_1} {r : α → α → Bool} (a : α) :
[a].mergeSort r = [a]
source
@[irreducible]
theorem List.mergeSort_perm {α : Type u_1} (l : List α) (le : α → α → Bool) :
(l.mergeSort le).Perm l
source
@[simp]
theorem List.length_mergeSort {α : Type u_1} {le : α → α → Bool} (l : List α) :
(l.mergeSort le).length = l.length
source
@[simp]
theorem List.mem_mergeSort {α : Type u_1} {le : α → α → Bool} {a : α} {l : List α} :
a ∈ l.mergeSort le ↔ a ∈ l
source
@[irreducible]
theorem 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)

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

source
@[irreducible]
theorem List.mergeSort_of_sorted {α : 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.

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

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

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

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