LEQuery: Comparison Queries for Sorting

LEQuery α is the query type for comparison-based sorting algorithms. A query LEQuery.le a b asks whether a ≤ b and returns a Bool.

inductive Cslib.Query.LEQuery (α : Type) : Type → Type

Comparison query: asks whether a ≤ b, returning a Bool.

• le {α : Type} (a b : α) : LEQuery α Bool

@[reducible, inline]

abbrev Cslib.Query.LEQuery.ask {α : Type} (a b : α) : FreeM (LEQuery α) Bool

Lift LEQuery.le a b into a FreeM that returns the comparison result.

Equations

• Cslib.Query.LEQuery.ask a b = Cslib.FreeM.lift (Cslib.Query.LEQuery.le a b)

@[simp]

theorem Cslib.Query.LEQuery.eval_ask {α : Type} (oracle : {ι : Type} → LEQuery α ι → ι) (a b : α) : FreeM.eval (fun {ι : Type} => oracle) (ask a b) = oracle (le a b)

def Cslib.Query.LEQuery.oracleOf {α : Type} (f : α → α → Bool) {ι : Type} : LEQuery α ι → ι

Build an oracle for LEQuery α from a binary predicate α → α → Bool.

Equations

• Cslib.Query.LEQuery.oracleOf f (Cslib.Query.LEQuery.le a b) = f a b

@[simp]

theorem Cslib.Query.LEQuery.oracleOf_le {α : Type} (f : α → α → Bool) (a b : α) : oracleOf f (le a b) = f a b

theorem Cslib.Query.LEQuery.cardResponse_eq_two {α ι : Type} : ∀ (a : LEQuery α ι), Cardinal.mk ι = 2

Every LEQuery α ι has response type ι = Bool, of cardinality two.

theorem Cslib.Query.LEQuery.cardResponse_le_two {α ι : Type} (op : LEQuery α ι) : Cardinal.mk ι ≤ 2