From 3b6ed083299d308cf121268f259f332e754b00da Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:28:29 +0000 Subject: [PATCH] feat(data-structures): support ordered-set deletion and minimum extraction Connect verified search-tree deletion to the shared typed ordered-set interface and adaptive-client correctness/resource certificates. Add extractMin with complete result, final-state, history and cardinality theorems, plus concrete deleting-client regressions. Pinned Lean 4.36.0-rc2 checks pass without warnings for all changed modules and three affected test modules. Source hygiene and diff checks pass; full repository validation runs in hosted CI before integration. Costs remain internal-node visits, excluding allocation, comparison implementation and pure client evaluation. AI assistance: OpenAI ChatGPT implementation by /root and /root/data_structures_survey; independent non-authoring API/correctness review by /root/ordered_set_review approved exact tree e18fa6138fdd9c749ee085f45c432f76a04f7af3 with no findings. This is AI review, not maintainer approval. --- Complexity.lean | 1 + .../Algorithms/Lean/SearchTree/Stateful.lean | 10 ++- .../Data/OrderedSet/ExtractMin.lean | 89 +++++++++++++++++++ .../Foundations/Data/OrderedSet/Spec.lean | 12 ++- ComplexityTests/OrderedSet.lean | 24 ++++- ComplexityTests/SearchTree.lean | 40 +++++++++ ROADMAP.md | 6 +- UPSTREAM.md | 12 +-- 8 files changed, 179 insertions(+), 15 deletions(-) create mode 100644 Complexity/Foundations/Data/OrderedSet/ExtractMin.lean diff --git a/Complexity.lean b/Complexity.lean index 9735d61c91..823f69a2ac 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Algorithms/Lean/SearchTree/Stateful.lean b/Complexity/Algorithms/Lean/SearchTree/Stateful.lean index 56a8af9aff..78c95fabb1 100644 --- a/Complexity/Algorithms/Lean/SearchTree/Stateful.lean +++ b/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 diff --git a/Complexity/Foundations/Data/OrderedSet/ExtractMin.lean b/Complexity/Foundations/Data/OrderedSet/ExtractMin.lean new file mode 100644 index 0000000000..fb8251bd9a --- /dev/null +++ b/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 diff --git a/Complexity/Foundations/Data/OrderedSet/Spec.lean b/Complexity/Foundations/Data/OrderedSet/Spec.lean index eb408398e2..0afbef344c 100644 --- a/Complexity/Foundations/Data/OrderedSet/Spec.lean +++ b/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 < ·))) diff --git a/ComplexityTests/OrderedSet.lean b/ComplexityTests/OrderedSet.lean index 6621fa1042..3d019e9545 100644 --- a/ComplexityTests/OrderedSet.lean +++ b/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 diff --git a/ComplexityTests/SearchTree.lean b/ComplexityTests/SearchTree.lean index e9d80466b3..beb9b0f055 100644 --- a/ComplexityTests/SearchTree.lean +++ b/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 : diff --git a/ROADMAP.md b/ROADMAP.md index db07115f67..cdcd9ccff3 100644 --- a/ROADMAP.md +++ b/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 diff --git a/UPSTREAM.md b/UPSTREAM.md index 986a138871..d2c6548072 100644 --- a/UPSTREAM.md +++ b/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.