Merge Sort as a Query Program

Merge sort implemented as a FreeM (LEQuery α), making all comparison queries explicit. The definitions mirror List.merge and List.mergeSort exactly: the list is split into contiguous halves and the merge prefers the left element on ties. Consequently evaluating the query program against any oracle produces literally the same list as List.mergeSort with the comparator induced by the oracle (eval_mergeSort in Cslib.Algorithms.Lean.Query.Sort.Merge.Lemmas); in particular the sort is stable. The recursive calls of mergeSort are not structural, since the two halves are not syntactic subterms, and are justified separately using their lengths.

def List.split {α : Type u_1} (xs : List α) : List α × List α

Split a list into contiguous halves; if the length is odd, the first half is one element longer. This agrees with List.MergeSort.Internal.splitInTwo, so that mergeSort agrees with List.mergeSort.

Equations

• xs.split = (List.take ((xs.length + 1) / 2) xs, List.drop ((xs.length + 1) / 2) xs)

@[simp]

theorem List.split_fst_length_eq {α : Type u_1} (xs : List α) : xs.split.1.length = (xs.length + 1) / 2

@[simp]

theorem List.split_snd_length_eq {α : Type u_1} (xs : List α) : xs.split.2.length = xs.length / 2

theorem List.split_fst_append_split_snd {α : Type u_1} (xs : List α) : xs.split.1 ++ xs.split.2 = xs

theorem List.splitInTwo_fst {α : Type u_1} {n : ℕ} (xs : { l : List α // l.length = n }) : ↑(MergeSort.Internal.splitInTwo xs).1 = (↑xs).split.1

theorem List.splitInTwo_snd {α : Type u_1} {n : ℕ} (xs : { l : List α // l.length = n }) : ↑(MergeSort.Internal.splitInTwo xs).2 = (↑xs).split.2

@[reducible, inline]

abbrev Cslib.Query.merge {α : Type} (xs ys : List α) : FreeM (LEQuery α) (List α)

Merge two sorted lists using comparison queries.

Equations

• Cslib.Query.merge xs ys = xs.mergeM ys Cslib.Query.LEQuery.ask

@[reducible, inline]

abbrev Cslib.Query.mergeSort {α : Type} (xs : List α) : FreeM (LEQuery α) (List α)

Sort a list using merge sort with comparison queries.

Equations

• Cslib.Query.mergeSort xs = xs.mergeSortM Cslib.Query.LEQuery.ask