feat(data-structures): support ordered-set deletion and minimum extraction

Complexity.lean

@@ -2642,6 +2642,7 @@ public import Complexity.Foundations.Data.Nat.Radix.Measurement
 public import Complexity.Foundations.Data.Nat.SqrtRatio
 public import Complexity.Foundations.Data.Option
 public import Complexity.Foundations.Data.OrderedSet
+public import Complexity.Foundations.Data.OrderedSet.ExtractMin
 public import Complexity.Foundations.Data.OrderedSet.Spec
 public import Complexity.Foundations.Data.Polynomial.BivariateCoeffNorm1
 public import Complexity.Foundations.Data.Polynomial.CoeffList

Complexity/Algorithms/Lean/SearchTree/Stateful.lean

@@ -7,7 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Algorithms.Lean.SearchTree.Cost
+public import Complexity.Algorithms.Lean.SearchTree.Erase
 public import Complexity.Foundations.Data.OrderedSet.Spec
 public import Complexity.Foundations.Semantics.Stateful.Resource
 
@@ -16,7 +16,8 @@ public import Complexity.Foundations.Semantics.Stateful.Resource
 
 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.
+calculus; node-visit costs are supplied afterwards as a separate resource certificate. Deletion
+uses the existing successor-splicing operation, including unsuccessful and repeated deletions.
 
 ## Main definitions
 
@@ -54,6 +55,7 @@ def step (t : BinaryTree α) (o : Op α) : BinaryTree α × (spec α).Result o 
   match o with
   | .contains x => (t, contains x t, searchVisits x t)
   | .insert x => (insert x t, (), searchVisits x t)
+  | .erase x => (erase x t, (), eraseVisits x t)
   | .minimum => (t, minimum t, minimumVisits t)
   | .successor x => (t, successor x t, successorVisits x t)
 
@@ -82,6 +84,9 @@ def realization : Realization (spec α) Exec where
     | insert x =>
       cases he
       exact ⟨rfl, ordered_insert ht x, elements_insert x t⟩
+    | erase x =>
+      cases he
+      exact ⟨rfl, ordered_erase ht x, elements_erase ht x⟩
     | minimum =>
       cases he
       exact ⟨(minimum_spec ht).eq_least, ht, rfl⟩
@@ -95,6 +100,7 @@ theorem exec_visits_le_height {t t' : BinaryTree α} {o : Op α}
   cases o with
   | contains x => cases he; exact searchVisits_le_height x t
   | insert x => cases he; exact searchVisits_le_height x t
+  | erase x => cases he; exact eraseVisits_le_height x t
   | minimum => cases he; exact minimumVisits_le_height t
   | successor x => cases he; exact successorVisits_le_height x t
 

Complexity/Foundations/Data/OrderedSet/ExtractMin.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Data.OrderedSet.Spec
+
+/-!
+# Minimum extraction through the shared ordered-set interface
+
+The client `extractMin` queries the minimum and, when one exists, deletes that observed key.
+Its semantics and chosen operation history are independent of a representation. Execution and
+resource guarantees come from the realization used by the caller; pure client computation has
+no machine-time claim here.
+
+## Main definitions
+
+* `extractMin`: an adaptive minimum-and-deletion client.
+
+## Main results
+
+* `extractMin_run`: the complete result, final set and answer-dependent operation history.
+* `extractMin_spec`, `extractMin_state_of_some`: the returned minimum and its removal.
+* `extractMin_card`: extraction reduces cardinality by one, with natural subtraction at zero.
+-/
+
+public section
+
+namespace Cslib.OrderedSet
+
+open Cslib.Stateful
+
+variable {α : Type} [LinearOrder α]
+
+/-- Return and remove the least key, or return `none` without deletion when the set is empty. -/
+@[expose] def extractMin : (spec α).Client (Option α) := do
+  let result ← PFunctor.FreeM.lift (P := (spec α).signature) .minimum
+  match result with
+  | none => pure none
+  | some x =>
+    let _ ← PFunctor.FreeM.lift (P := (spec α).signature) (.erase x)
+    pure (some x)
+
+/-- The deletion argument and operation history depend on the observed minimum. -/
+theorem extractMin_run (s : Finset α) :
+    (spec α).runClient s extractMin =
+      match least s with
+      | none => (none, s, [.minimum])
+      | some x => (some x, s.erase x, [.minimum, .erase x]) := by
+  simp only [extractMin, Spec.runClient_lift_bind', spec]
+  cases least s <;> rfl
+
+/-- Extraction returns the minimum of the original set. -/
+@[simp] theorem extractMin_result (s : Finset α) :
+    ((spec α).runClient s extractMin).1 = least s := by
+  rw [extractMin_run]
+  cases least s <;> rfl
+
+/-- The result has the complete optional-minimum contract, including empty-set detection. -/
+theorem extractMin_spec (s : Finset α) :
+    LeastResult s ((spec α).runClient s extractMin).1 := by
+  rw [extractMin_result]
+  exact least_spec s
+
+/-- When extraction returns a key, its final state removes exactly that key. -/
+theorem extractMin_state_of_some {s : Finset α} {x : α}
+    (h : ((spec α).runClient s extractMin).1 = some x) :
+    ((spec α).runClient s extractMin).2.1 = s.erase x := by
+  rw [extractMin_result] at h
+  rw [extractMin_run, h]
+
+/-- Exactly one element is removed from a nonempty set; an empty set stays empty. -/
+theorem extractMin_card (s : Finset α) :
+    ((spec α).runClient s extractMin).2.1.card = s.card - 1 := by
+  rw [extractMin_run]
+  have hs := least_spec s
+  cases he : least s with
+  | none =>
+    simp only [he, LeastResult] at hs
+    simp [hs]
+  | some x =>
+    simp only [he, LeastResult] at hs
+    exact Finset.card_erase_of_mem hs.1
+
+end Cslib.OrderedSet

Complexity/Foundations/Data/OrderedSet/Spec.lean

@@ -13,10 +13,11 @@ public import Complexity.Foundations.Semantics.Stateful.Basic
 /-!
 # 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
+The abstract state is a finite set over any linear order. Membership, insertion, deletion, minimum
+and strict successor have operation-dependent result types. All operations are admissible,
+including empty queries, duplicate insertion and deletion of absent keys. 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
@@ -42,6 +43,7 @@ variable {α : Type} [LinearOrder α]
 inductive Op (α : Type) where
   | contains (key : α)
   | insert (key : α)
+  | erase (key : α)
   | minimum
   | successor (key : α)
   deriving DecidableEq
@@ -53,11 +55,13 @@ abbrev spec (α : Type) [LinearOrder α] : Spec where
   Result
     | .contains _ => Bool
     | .insert _ => Unit
+    | .erase _ => Unit
     | .minimum => Option α
     | .successor _ => Option α
   step s
     | .contains x => (s, decide (x ∈ s))
     | .insert x => (Insert.insert x s, ())
+    | .erase x => (s.erase x, ())
     | .minimum => (s, least s)
     | .successor x => (s, least (s.filter (x < ·)))
 

ComplexityTests/OrderedSet.lean

@@ -7,7 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: local-only (test driver)
 
-public import Complexity.Foundations.Data.OrderedSet.Spec
+public import Complexity.Foundations.Data.OrderedSet.ExtractMin
 
 /-!
 # Representation-independent ordered-set clients
@@ -72,6 +72,27 @@ example (s : Finset (Fin 3)) : (least s : WithTop (Fin 3)) = s.min := least_eq_m
 example : (spec (Fin 3)).step {0, 2} (.successor 1) = ({0, 2}, some 2) := by decide
 example : (spec (Fin 3)).step {0, 2} (.successor 2) = ({0, 2}, none) := by decide
 
+-- Deletion is total: present, absent, and empty-set cases have the same typed interface.
+example : (spec (Fin 3)).step {0, 2} (.erase 0) = ({2}, ()) := by decide
+example : (spec (Fin 3)).step {0, 2} (.erase 1) = ({0, 2}, ()) := by decide
+example : (spec (Fin 3)).step ∅ (.erase 0) = (∅, ()) := by decide
+
+-- The erased key comes from the minimum answer; an empty query performs no deletion.
+example : (spec (Fin 3)).runClient {0, 2} extractMin =
+    (some 0, {2}, [.minimum, .erase 0]) := by decide
+example : (spec (Fin 3)).runClient ∅ extractMin = (none, ∅, [.minimum]) := by decide
+
+private def extractThree :
+    (spec (Fin 3)).Client (Option (Fin 3) × Option (Fin 3) × Option (Fin 3)) := do
+  let first ← extractMin
+  let second ← extractMin
+  let third ← extractMin
+  pure (first, second, third)
+
+-- Sequential composition sees the updated set, including exhaustion after the last key.
+example : (spec (Fin 3)).runClient {0, 2} extractThree =
+    ((some 0, some 2, none), ∅, [.minimum, .erase 0, .minimum, .erase 2, .minimum]) := by decide
+
 -- The same adaptive client can be interpreted without choosing a data structure.
 example : (spec (Fin 3)).runClient ∅ firstTwo = ((none, none), ∅, [.minimum]) := by decide
 example : (spec (Fin 3)).runClient {0, 2} firstTwo =
@@ -99,6 +120,7 @@ abbrev bounded (bound : Nat) : Spec :=
 example : ¬ (bounded 4).valid ∅ (.insert 4) := by decide
 example : (bounded 4).valid ∅ (.contains 99) := trivial
 example : (bounded 4).valid ∅ (.successor 99) := trivial
+example : (bounded 4).valid ∅ (.erase 99) := trivial
 example : (spec Nat).valid ∅ (.insert 99) := trivial
 
 end ComplexityTests.OrderedSet

ComplexityTests/SearchTree.lean

@@ -88,6 +88,46 @@ example :
       successor 4 (build [5]) = some 5 :=
   ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩
 
+-- The shared deletion operation uses successor splicing at a root with two children and retains
+-- the exact charge, including for missing keys and an empty initial tree.
+example :
+    run medianFirst (.liftBind (.erase 4) .pure) = ((), erase 4 medianFirst, [3]) ∧
+      run sortedFirst (.liftBind (.erase 4) .pure) = ((), erase 4 sortedFirst, [5]) ∧
+      run medianFirst (.liftBind (.erase 8) .pure) = ((), medianFirst, [3]) ∧
+      run (.nil : BinaryTree Nat) (.liftBind (.erase 0) .pure) = ((), .nil, [0]) :=
+  ⟨rfl, rfl, rfl, rfl⟩
+
+private def eraseTwiceAndCheck (x : Nat) : (spec Nat).Client Bool := do
+  PFunctor.FreeM.lift (P := (spec Nat).signature) (.erase x)
+  PFunctor.FreeM.lift (P := (spec Nat).signature) (.erase x)
+  PFunctor.FreeM.lift (P := (spec Nat).signature) (.contains x)
+
+-- A repeated deletion is still charged for its unsuccessful search, and later queries see the
+-- updated state through the same interpreter and representation-independent correctness theorem.
+example :
+    (run medianFirst (eraseTwiceAndCheck 4)).1 = false ∧
+      (run medianFirst (eraseTwiceAndCheck 4)).2.1 = erase 4 medianFirst ∧
+      (run medianFirst (eraseTwiceAndCheck 4)).2.2 = [3, 3, 3] ∧
+      (run medianFirst (eraseTwiceAndCheck 4)).1 =
+        ((spec Nat).runClient (elements medianFirst) (eraseTwiceAndCheck 4)).1 :=
+  ⟨rfl, rfl, rfl, (run_correct _ ⟨ordered_build _, rfl⟩).1⟩
+
+-- Minimum extraction charges the query and the answer-dependent deletion separately. Their
+-- costs differ on the two shapes even though both implement the same finite-set client.
+example :
+    run medianFirst extractMin = (some 1, erase 1 medianFirst, [3, 3]) ∧
+      run sortedFirst extractMin = (some 1, erase 1 sortedFirst, [1, 2]) ∧
+      run (build [5]) extractMin = (some 5, .nil, [1, 1]) ∧
+      run (.nil : BinaryTree Nat) extractMin = (none, .nil, [0]) :=
+  ⟨rfl, rfl, rfl, rfl⟩
+
+-- The generic resource certificate applies to the new adaptive deleting client unchanged.
+example :
+    total id (run medianFirst extractMin).2.2 ≤
+      (spec Nat).totalCost (fun s _ => s.card) (elements medianFirst)
+        ((spec Nat).runClient (elements medianFirst) extractMin).2.2 :=
+  (run_correct extractMin ⟨ordered_build _, rfl⟩).2.2
+
 -- The exact native trace counts minimum and the answer-dependent successor separately, and agrees
 -- with finite-set semantics through the shared realization theorem.
 example :

ROADMAP.md

@@ -573,9 +573,9 @@ each statement against the numbered result. Organize modules by subject, not cha
   iterative clients, including the two-stack queue and timeline-editing controllers; reusable
   allocation and deallocation, shrinking, and live and peak space accounting; ownership and
   recursive procedures; model realizations for cell probes, caches and randomness; present and
-  historical queries for the retroactive interface; deletion in the shared ordered-set interface,
-  balancing, and heap or RAM representations of search trees; uniform preprocessing and dynamic
-  updates for fusion trees; deletion and predecessor for van Emde Boas sets; and deallocation,
+  historical queries for the retroactive interface; balancing and heap or RAM representations of
+  search trees; uniform preprocessing and dynamic updates for fusion trees; deletion and
+  predecessor for van Emde Boas sets; and deallocation,
   shrinking and compiled client controllers for the doubling array.
 - **A typed-call evaluator** for fixed-program Word-RAM clients, returning the typed observation,
   final state and halt-inclusive instruction cost, so the prefix-sum and stack clients no longer

UPSTREAM.md

@@ -481,13 +481,15 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   representation from the standard input. `WordRAM/Function` gives separate nonuniform and
   uniform RAM function-time predicates, with named-certificate reuse by `polytime`. Arbitrary continuation
   synthesis, iterative clients and a Turing-machine simulation remain open.
-  `Foundations/Data/OrderedSet` and `Foundations/Semantics/Stateful/OrderedSet` provide neutral
-  optional-minimum contracts, a typed finite-set interface and adaptive clients, with no tree or
-  cost dependency. Bounded-key implementations may specialize insertion admissibility.
+  `Foundations/Data/OrderedSet` and `Foundations/Data/OrderedSet/*` provide neutral
+  optional-minimum contracts, a typed finite-set interface including deletion, and adaptive
+  minimum extraction, with no tree or cost dependency. Bounded-key implementations may specialize
+  insertion admissibility.
   `Algorithms/Lean/SearchTree/*` reuses Mathlib's `BinaryTree`, height and node count for an
   unbalanced ordered-set realization. Finite-set behavior, strict invariants and height-bounded
-  node visits are proved, including for the pure deletion operation `erase`; allocation,
-  comparison implementation and client computation are excluded from that cost model. It is not
+  node visits are proved, including deletion through the shared interface and adaptive clients;
+  allocation, comparison implementation and client computation are excluded from that cost model.
+  It is not
   a balanced tree or machine-time certificate.
   `WordRAM/Dynamic` separately connects
   fixed bounded-word operation programs and faithful memory transcripts to those contracts.