Init.Data.List.Sort.Basic

List.nil_merge theorem

(ys : List α) : merge [] ys le = ys

Full source

@[simp] theorem nil_merge (ys : List α) : merge [] ys le = ys := by simp [merge]

Merge with Empty List Yields Original List

Informal description

For any list `ys` of elements of type `α`, merging the empty list `[]` with `ys` using a comparison function `le` results in `ys`. That is, $\text{merge}([], \text{ys}, \text{le}) = \text{ys}$.

List.merge_right theorem

(xs : List α) : merge xs [] le = xs

Full source

@[simp] theorem merge_right (xs : List α) : merge xs [] le = xs := by
  induction xs with
  | nil => simp [merge]
  | cons x xs ih => simp [merge, ih]

Merge with Empty List Yields Original List (Right Version)

Informal description

For any list `xs` of elements of type `α`, merging `xs` with the empty list `[]` using a comparison function `le` results in `xs`. That is, $\text{merge}(\text{xs}, [], \text{le}) = \text{xs}$.

List.MergeSort.Internal.splitInTwo definition

 (l : { l : List α // l.length = n }) : { l : List α // l.length = (n + 1) / 2 } × { l : List α // l.length = n / 2 }

Full source

/--
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`.
-/
def MergeSort.Internal.splitInTwo (l : { l : List α // l.length = n }) :
    { l : List α // l.length = (n+1)/2 }{ l : List α // l.length = (n+1)/2 } × { l : List α // l.length = n/2 } :=
  let r := splitAt ((n+1)/2) l.1
  (⟨r.1, by simp [r, splitAt_eq, l.2]; omega⟩, ⟨r.2, by simp [r, splitAt_eq, l.2]; omega⟩)

Splitting a list into two equal parts (with first part longer if odd length)

Informal description

Given a list $l$ of length $n$, the function splits $l$ into two parts: the first part has length $\lceil n/2 \rceil$ and the second part has length $\lfloor n/2 \rfloor$. Specifically, if $n$ is odd, the first part will be one element longer than the second part.

List.mergeSort definition

: ∀ (xs : List α) (le : α → α → Bool := by exact fun a b => a ≤ b), List α

Full source

/--
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.
-/
-- Because we want the sort to be stable, it is essential that we split the list in two contiguous
-- sublists.
def mergeSort : ∀ (xs : List α) (le : α → α → Bool := by exact fun a b => a ≤ b), List α
  | [], _ => []
  | [a], _ => [a]
  | a :: b :: xs, le =>
    let lr := splitInTwo ⟨a :: b :: xs, rfl⟩
    have := by simpa using lr.2.2
    have := by simpa using lr.1.2
    merge (mergeSort lr.1 le) (mergeSort lr.2 le) le
termination_by xs => xs.length

Merge sort for lists

Informal description

The function `mergeSort` implements a stable merge sort algorithm for lists of type `α`. Given a list `xs` and an optional comparison function `le` (defaulting to the standard less-than-or-equal comparison), it returns a sorted version of `xs`. The algorithm works by recursively splitting the list into two halves, sorting each half, and then merging the sorted halves. This implementation is designed for verification purposes and is not optimized for efficiency.

List.zipIdxLE definition

(le : α → α → Bool) (a b : α × Nat) : Bool

Full source

/--
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`.
-/
def zipIdxLE (le : α → α → Bool) (a b : α × Nat) : Bool :=
  if le a.1 b.1 then if le b.1 a.1 then a.2 ≤ b.2 else true else false

Lexicographic ordering on pairs for merge sort stability

Informal description

Given an ordering relation $\le : \alpha \to \alpha \to \mathtt{Bool}$, the function defines a lexicographic ordering on pairs $\alpha \times \mathbb{N}$. It first compares the first components using $\le$. If the first components are equivalent (i.e., both $\le$ and its reverse hold), then it compares the second components using the natural number ordering $\leq$. This function is used to state stability properties of merge sort.