IsSort: Specification for Comparison Sorts

IsSort sort asserts that sort is a correct comparison sort when viewed as a FreeM over LEQuery α. Correctness means: for any oracle, the result is a permutation of the input; and for any oracle implementing a total order, the result is sorted.

structure Cslib.Query.IsSort {α : Type} (sort : List α → FreeM (LEQuery α) (List α)) : Prop

A FreeM-based function is a correct comparison sort if it always produces a permutation of its input, and produces a sorted list when the oracle implements a total order.

• perm (xs : List α) (oracle : {ι : Type} → LEQuery α ι → ι) : (FreeM.eval (fun {ι : Type} => oracle) (sort xs)).Perm xs

  The sort produces a permutation of its input, for any oracle.

• sorted (xs : List α) (oracle : {ι : Type} → LEQuery α ι → ι) (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] : (∀ (a b : α), oracle (LEQuery.le a b) = decide (r a b)) → List.Pairwise r (FreeM.eval (fun {ι : Type} => oracle) (sort xs))

  The sort produces a sorted list, when the oracle implements a total order.

theorem Cslib.Query.IsSort.eval_eq {α : Type} {sort₁ sort₂ : List α → FreeM (LEQuery α) (List α)} (h₁ : IsSort sort₁) (h₂ : IsSort sort₂) (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] [Std.Antisymm r] (oracle : {ι : Type} → LEQuery α ι → ι) (horacle : ∀ (a b : α), oracle (LEQuery.le a b) = decide (r a b)) (xs : List α) : FreeM.eval (fun {ι : Type} => oracle) (sort₁ xs) = FreeM.eval (fun {ι : Type} => oracle) (sort₂ xs)

IsSort determines the output: under an oracle implementing an antisymmetric total transitive relation, all correct comparison sorts produce the same list.