Merge Sort: Correctness and Upper Bound

Proofs that mergeSort is a correct comparison sort and uses at most n * ⌈log₂ n⌉ queries.

eval_mergeSort identifies the query program with List.mergeSort: evaluating against any oracle produces the same list as List.mergeSort with the comparator induced by the oracle. Correctness properties (permutation, sortedness) transfer directly from the List.mergeSort API. The query bound is proved by equational reasoning on FreeM.countQueries, which has no List counterpart.

Evaluation

@[simp]

theorem Cslib.Query.eval_merge {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (xs ys : List α) : FreeM.eval (fun {ι : Type} => oracle) (merge xs ys) = xs.merge ys fun (a b : α) => oracle (LEQuery.le a b)

Evaluating the query-based merge agrees with List.merge using the relation supplied by the oracle.

@[simp]

theorem Cslib.Query.eval_mergeSort {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) : FreeM.eval (fun {ι : Type} => oracle) (mergeSort xs) = xs.mergeSort fun (a b : α) => oracle (LEQuery.le a b)

Evaluating query-based merge sort agrees with List.mergeSort using the relation supplied by the oracle.

This is the essential correctness statement: it identifies the query program as the merge sort operation, so correctness properties (permutation, sortedness, stability) transfer directly from the List.mergeSort API rather than being restated here.

Correctness, transferred from the List.mergeSort API

theorem Cslib.Query.mergeSort_perm {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) : (FreeM.eval (fun {ι : Type} => oracle) (mergeSort xs)).Perm xs

theorem Cslib.Query.mergeSort_sorted {α : Type} (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (oracle : {ι : Type} → LEQuery α ι → ι) (horacle : ∀ (a b : α), oracle (LEQuery.le a b) = decide (r a b)) (xs : List α) : List.Pairwise r (FreeM.eval (fun {ι : Type} => oracle) (mergeSort xs))

Query count simp lemmas

theorem Cslib.Query.countQueries_merge_nil_left {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (ys : List α) : FreeM.countQueries (fun {ι : Type} => oracle) (merge [] ys) = 0

theorem Cslib.Query.countQueries_merge_nil_right {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) : FreeM.countQueries (fun {ι : Type} => oracle) (merge xs []) = 0

theorem Cslib.Query.countQueries_merge_cons_cons {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (x : α) (xs' : List α) (y : α) (ys' : List α) : FreeM.countQueries (fun {ι : Type} => oracle) (merge (x :: xs') (y :: ys')) = 1 + if oracle (LEQuery.le x y) = true then FreeM.countQueries (fun {ι : Type} => oracle) (merge xs' (y :: ys')) else FreeM.countQueries (fun {ι : Type} => oracle) (merge (x :: xs') ys')

theorem Cslib.Query.countQueries_mergeSort_nil {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) : FreeM.countQueries (fun {ι : Type} => oracle) (mergeSort []) = 0

theorem Cslib.Query.countQueries_mergeSort_singleton {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (x : α) : FreeM.countQueries (fun {ι : Type} => oracle) (mergeSort [x]) = 0

@[simp]

theorem Cslib.Query.countQueries_mergeSort_cons_cons {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (x y : α) (zs : List α) : FreeM.countQueries (fun {ι : Type} => oracle) (mergeSort (x :: y :: zs)) = FreeM.countQueries (fun {ι : Type} => oracle) (mergeSort (x :: y :: zs).split.1) + (FreeM.countQueries (fun {ι : Type} => oracle) (mergeSort (x :: y :: zs).split.2) + FreeM.countQueries (fun {ι : Type} => oracle) (merge ((x :: y :: zs).split.1.mergeSort fun (a b : α) => oracle (LEQuery.le a b)) ((x :: y :: zs).split.2.mergeSort fun (a b : α) => oracle (LEQuery.le a b))))

Query count proofs

theorem Cslib.Query.merge_countQueries_le {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (xs ys : List α) : FreeM.countQueries (fun {ι : Type} => oracle) (merge xs ys) ≤ xs.length + ys.length

theorem Cslib.Query.mergeSort_countQueries_le {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) : FreeM.countQueries (fun {ι : Type} => oracle) (mergeSort xs) ≤ xs.length * Nat.clog 2 xs.length

UpperBound and IsSort instances

theorem Cslib.Query.mergeSort_upperBound {α : Type} : UpperBound mergeSort List.length fun (n : ℕ) => n * Nat.clog 2 n

theorem Cslib.Query.mergeSort_isSort {α : Type} : IsSort mergeSort