Insertion Sort: Correctness and Upper Bound

Proofs that insertionSort is a correct comparison sort and uses at most n * (n - 1) / 2 queries (with n² as a corollary). All proofs are by plain equational reasoning on FreeM.eval and FreeM.countQueries.

Evaluation

@[simp]

theorem Cslib.Query.eval_orderedInsert {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (x : α) (xs : List α) : FreeM.eval (fun {ι : Type} => oracle) (orderedInsert x xs) = List.orderedInsert (fun (x y : α) => oracle (LEQuery.le x y) = true) x xs

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

@[simp]

theorem Cslib.Query.eval_insertionSort {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) : FreeM.eval (fun {ι : Type} => oracle) (insertionSort xs) = List.insertionSort (fun (x y : α) => oracle (LEQuery.le x y) = true) xs

Evaluating query-based insertion sort agrees with List.insertionSort using the relation supplied by the oracle.

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

Query count proofs

theorem Cslib.Query.orderedInsert_countQueries_le {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (x : α) (xs : List α) : FreeM.countQueries (fun {ι : Type} => oracle) (orderedInsert x xs) ≤ xs.length

theorem Cslib.Query.insertionSort_countQueries_le {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) : FreeM.countQueries (fun {ι : Type} => oracle) (insertionSort xs) ≤ xs.length * (xs.length - 1) / 2

Insertion sort makes at most n * (n - 1) / 2 queries: inserting into the sorted prefix of length k costs at most k queries. This bound is attained by the all-false oracle.

theorem Cslib.Query.insertionSort_countQueries_le_sq {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) : FreeM.countQueries (fun {ι : Type} => oracle) (insertionSort xs) ≤ xs.length ^ 2

UpperBound and IsSort instances

theorem Cslib.Query.insertionSort_upperBound {α : Type} : UpperBound insertionSort List.length fun (x : ℕ) => x ^ 2

theorem Cslib.Query.insertionSort_isSort {α : Type} : IsSort insertionSort