Definition of merge and mergeSort.

These definitions are intended for verification purposes, and are replaced at runtime by efficient versions in Init.Data.List.Sort.Impl.

@[irreducible]

def List.merge {α : Type u_1} (xs ys : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α

Merges two lists, using le to select the first element of the resulting list if both are non-empty.

If both input lists are sorted according to le, then the resulting list is also sorted according to le. O(|xs| + |ys|).

This implementation is not tail-recursive, but it is replaced at runtime by a proven-equivalent tail-recursive merge.

Equations

• [].merge ys le = ys
• xs.merge [] le = xs
• (x :: xs_2).merge (y :: ys_2) le = if le x y = true then x :: xs_2.merge (y :: ys_2) le else y :: (x :: xs_2).merge ys_2 le

@[simp]

theorem List.nil_merge {α : Type u_1} {le : α → α → Bool} (ys : List α) : [].merge ys le = ys

@[simp]

theorem List.merge_right {α : Type u_1} {le : α → α → Bool} (xs : List α) : xs.merge [] le = xs

def List.MergeSort.Internal.splitInTwo {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : { l : List α // l.length = (n + 1) / 2 } × { l : List α // l.length = n / 2 }

Split a list in two equal parts. If the length is odd, the first part will be one element longer.

This is an implementation detail of mergeSort.

Equations

• List.MergeSort.Internal.splitInTwo l = (⟨(List.splitAt ((n + 1) / 2) l.val).fst, ⋯⟩, ⟨(List.splitAt ((n + 1) / 2) l.val).snd, ⋯⟩)

@[irreducible]

def List.mergeSort {α : Type u_1} (xs : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α

A stable merge sort.

This function is a simplified implementation that's designed to be easy to reason about, rather than for efficiency. In particular, it uses the non-tail-recursive List.merge function and traverses lists unnecessarily.

It is replaced at runtime by an efficient implementation that has been proven to be equivalent.

Equations

• One or more equations did not get rendered due to their size.
• [].mergeSort x✝ = []
• [a].mergeSort x✝ = [a]

def List.zipIdxLE {α : Type u_1} (le : α → α → Bool) (a b : α × Nat) : Bool

Given an ordering relation le : α → α → Bool, construct the lexicographic ordering on α × Nat. which first compares the first components using le, but if these are equivalent (in the sense le a.2 b.2 && le b.2 a.2) then compares the second components using ≤.

This function is only used in stating the stability properties of mergeSort.

Equations

• List.zipIdxLE le a b = if le a.fst b.fst = true then if le b.fst a.fst = true then decide (a.snd ≤ b.snd) else true else false