A representation-independent stateful ordered set

The abstract state is a finite set over any linear order. Membership, insertion, minimum and strict successor have operation-dependent result types. All operations are admissible, including empty queries and duplicate insertion. A bounded-key implementation can specialize spec.valid for insertion while preserving arbitrary membership and successor queries. This module does not choose a representation or charge a computational cost.

Main definitions

• Cslib.OrderedSet.Op, Cslib.OrderedSet.spec: shared typed ordered-set interface and semantics.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Chapter 12

The adaptive client syntax uses Quang Dao's upstream free monad via Cslib.Stateful.Spec.

inductive Cslib.OrderedSet.Op (α : Type) : Type

Typed finite-set operations, independent of any representation.

• contains {α : Type} (key : α) : Op α
• insert {α : Type} (key : α) : Op α
• minimum {α : Type} : Op α
• successor {α : Type} (key : α) : Op α

def Cslib.OrderedSet.instDecidableEqOp.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : Op α✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.OrderedSet.instDecidableEqOp {α✝ : Type} [DecidableEq α✝] : DecidableEq (Op α✝)

@[reducible, inline]

abbrev Cslib.OrderedSet.spec (α : Type) [LinearOrder α] : Stateful.Spec

Mathematical ordered-set semantics. All operations are admissible, including empty queries.