theorem Subarray.toList_mergeSort {α : Type u_1} {xs : Subarray α} {le : α → α → Bool} : (xs.mergeSort le).toList = (Std.Slice.toList xs).mergeSort le

@[simp]

theorem Subarray.mergeSort_eq_mergeSort_toArray {α : Type u_1} {xs : Subarray α} {le : α → α → Bool} : xs.mergeSort le = (Std.Slice.toArray xs).mergeSort le

theorem Subarray.mergeSort_toArray {α : Type u_1} {xs : Subarray α} {le : α → α → Bool} : (Std.Slice.toArray xs).mergeSort le = xs.mergeSort le

theorem Array.toList_mergeSort {α : Type u_1} {xs : Array α} {le : α → α → Bool} : (xs.mergeSort le).toList = xs.toList.mergeSort le

theorem Array.mergeSort_eq_toArray_mergeSort_toList {α : Type u_1} {xs : Array α} {le : α → α → Bool} : xs.mergeSort le = (xs.toList.mergeSort le).toArray

Basic properties of Array.mergeSort.

• pairwise_mergeSort: mergeSort produces a sorted array.
• mergeSort_perm: mergeSort is a permutation of the input array.
• mergeSort_of_pairwise: mergeSort does not change a sorted array.
• sublist_mergeSort: if c is a sorted sublist of l, then c is still a sublist of mergeSort le l.

@[simp]

theorem Array.mergeSort_empty {α : Type u_1} {r : α → α → Bool} : #[].mergeSort r = #[]

@[simp]

theorem Array.mergeSort_singleton {α : Type u_1} {r : α → α → Bool} {a : α} : #[a].mergeSort r = #[a]

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

@[simp]

theorem Array.size_mergeSort {α : Type u_1} {le : α → α → Bool} {xs : Array α} : (xs.mergeSort le).size = xs.size

@[simp]

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

theorem Array.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) {xs : Array α} : List.Pairwise (fun (x1 x2 : α) => le x1 x2 = true) (xs.mergeSort le).toList

The result of Array.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.

theorem Array.mergeSort_of_pairwise {α : Type u_1} {le : α → α → Bool} {xs : Array α} : List.Pairwise (fun (x1 x2 : α) => le x1 x2 = true) xs.toList → xs.mergeSort le = xs

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

theorem Array.mergeSort_zipIdx {α : Type u_1} {le : α → α → Bool} {xs : Array α} : map (fun (x : α × Nat) => x.fst) ((map (fun (x : α × Nat) => match x with | (a, i) => (a, i)) xs.zipIdx).mergeSort (List.zipIdxLE le)) = xs.mergeSort le

This merge sort algorithm is stable, in the sense that breaking ties in the ordering function using the position in the array 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 array as they were in the input array.

See also:

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

theorem Array.sublist_mergeSort {α : Type u_1} {xs : Array α} {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) {ys : List α} : List.Pairwise (fun (x1 x2 : α) => le x1 x2 = true) ys → ys.Sublist xs.toList → ys.Sublist (xs.mergeSort le).toList

Another statement of stability of merge sort. If c is a sorted sublist of xs.toList, then c is still a sublist of (mergeSort le xs).toList.

theorem Array.pair_sublist_mergeSort {α : Type u_1} {le : α → α → Bool} {a b : α} {xs : Array α} (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 xs.toList) : [a, b].Sublist (xs.mergeSort le).toList

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

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