A stateful ordered set realized by a binary search tree

Clients see finite-set semantics and operation-dependent result types. The representation relation hides the tree's shape. Correctness transfers to every adaptive client through the common stateful calculus; node-visit costs are supplied afterwards as a separate resource certificate.

Main definitions

• Cslib.OrderedSet.spec: the shared representation-independent finite-set specification.
• step, Exec: concrete tree operations with their exact node-visit charge.
• realization: the search tree realizes the finite-set interface.

Main results

• exec_visits_le_height: every native operation visits at most the initial tree height.
• nodeVisitBound: a representation-independent bound by the current set cardinality.
• realized_client: adaptive clients have correct executions with additive node-visit bounds.

The cardinality bound is deliberately worst-case: these trees have no balancing invariant. The cost model excludes allocation, pure continuations and comparison implementation, and makes no RAM or Turing-machine time claim.

References

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

def Cslib.Algorithms.Lean.SearchTree.step {α : Type} [LinearOrder α] (t : BinaryTree α) (o : OrderedSet.Op α) : BinaryTree α × (OrderedSet.spec α).Result o × ℕ

Concrete operation and exact charge in the internal-node-visit model.

def Cslib.Algorithms.Lean.SearchTree.Exec {α : Type} [LinearOrder α] : Stateful.Execution (OrderedSet.spec α) (BinaryTree α) ℕ

A native execution records an actual tree operation and its exact node-visit charge.

def Cslib.Algorithms.Lean.SearchTree.Rep {α : Type} [LinearOrder α] (s : Finset α) (t : BinaryTree α) : Prop

Representation includes both set semantics and strict subtree ordering.

theorem Cslib.Algorithms.Lean.SearchTree.rep_empty {α : Type} [LinearOrder α] : Rep ∅ BinaryTree.nil

Empty trees represent empty sets without an initialization assumption.

def Cslib.Algorithms.Lean.SearchTree.realization {α : Type} [LinearOrder α] : Stateful.Realization (OrderedSet.spec α) Exec

Semantic correctness is independent of the later resource certificate.

theorem Cslib.Algorithms.Lean.SearchTree.exec_visits_le_height {α : Type} [LinearOrder α] {t t' : BinaryTree α} {o : OrderedSet.Op α} {a : (OrderedSet.spec α).Result o} {n : ℕ} (he : Exec t o a t' n) : n ≤ t.height

Costs depend on the actual initial tree height, even for an unsuccessful query.

theorem Cslib.Algorithms.Lean.SearchTree.nodeVisitBound {α : Type} [LinearOrder α] : Stateful.Bound realization id fun (s : (OrderedSet.spec α).State) (x : (OrderedSet.spec α).Op) => Finset.card s

Forgetting shape gives a safe linear bound, not a logarithmic claim.

theorem Cslib.Algorithms.Lean.SearchTree.realized_client {α : Type} [LinearOrder α] {β : Type} (p : (OrderedSet.spec α).Client β) {s : Finset α} {t : BinaryTree α} (hr : Rep s t) : ∃ (t' : BinaryTree α) (ns : List ℕ), Stateful.Executes Exec p t ((OrderedSet.spec α).runClient s p).1 t' ns ∧ Rep ((OrderedSet.spec α).runClient s p).2.1 t' ∧ Stateful.total id ns ≤ (OrderedSet.spec α).totalCost (fun (s : (OrderedSet.spec α).State) (x : (OrderedSet.spec α).Op) => Finset.card s) s ((OrderedSet.spec α).runClient s p).2.2

Every adaptive client has the specified result and final set, together with a bound summing current-set cardinalities along the selected history. Pure continuation evaluation is uncharged.

def Cslib.Algorithms.Lean.SearchTree.run {α : Type} [LinearOrder α] {β : Type} (t : BinaryTree α) : (OrderedSet.spec α).Client β → β × BinaryTree α × List ℕ

Execute a client concretely, retaining one exact node-visit count per operation.

theorem Cslib.Algorithms.Lean.SearchTree.run_exec {α : Type} [LinearOrder α] {β : Type} (p : (OrderedSet.spec α).Client β) (t : BinaryTree α) : Stateful.Executes Exec p t (run t p).1 (run t p).2.1 (run t p).2.2

The executable interpreter supplies native execution evidence rather than assuming it.

theorem Cslib.Algorithms.Lean.SearchTree.run_correct {α : Type} [LinearOrder α] {β : Type} (p : (OrderedSet.spec α).Client β) {s : Finset α} {t : BinaryTree α} (hr : Rep s t) : (run t p).1 = ((OrderedSet.spec α).runClient s p).1 ∧ Rep ((OrderedSet.spec α).runClient s p).2.1 (run t p).2.1 ∧ Stateful.total id (run t p).2.2 ≤ (OrderedSet.spec α).totalCost (fun (s : (OrderedSet.spec α).State) (x : (OrderedSet.spec α).Op) => Finset.card s) s ((OrderedSet.spec α).runClient s p).2.2

Running the concrete interpreter agrees with finite-set semantics and retains its cost bound.