Union-find realization and logarithmic step bounds

This module realizes Cslib.DataStructure.DisjointSet.spec using Batteries.UnionFind (disjoint-set forests with union by rank and path compression) together with an explicit component counter, and establishes worst-case O(log n) per-operation parent-pointer traversal bounds.

Under path compression, internal nodes can lose descendants when compressed paths bypass them, so the naive subtree-size invariant 2 ^ rank u ≤ |subtree u| is not preserved at internal nodes. Following Cormen et al., Exercise 21.4-2, ValidRank instead bounds the equivalence-class size of each root r < uf.size by 2 ^ uf.rank r ≤ (equivClass uf r).card. Path compression preserves rootD, all node ranks, and the set of roots, so ValidRank is preserved immediately across find as well as across push, root link, checkEquiv, and union. Because node ranks strictly increase along non-root parent pointers (uf.rank_lt and le_rank_root, matching Cormen et al., Lemma 21.4 and Corollary 21.5), every node satisfies uf.rank i ≤ Nat.log 2 uf.size, and every find traverses at most Nat.log 2 uf.size + 1 nodes.

Cost model and limitations

The native trace of Exec counts parent-pointer inspections during find (1 at the root plus 1 per parent hop, matching recursive calls of Batteries.UnionFind.findAux), plus 1 link step for Op.union and 1 counter read for Op.numComponents. Because Batteries.UnionFind.rankMax is marked noncomputable, the helpers rankBound, findGo, and compressWithSteps are exposed solely so that findSteps, step, and run reduce in the Lean kernel (rfl / decide) while remaining propositionally equal to Batteries.UnionFind.find. This gives a worst-case O(log n) bound from union by rank alone (not Tarjan's inverse-Ackermann O(α(n)) amortized bound), and counts abstract forest steps in Lean rather than word-RAM instructions or array-copying overhead if a Batteries.UnionFind value is shared non-linearly.

Main definitions

• ofSize: initialize a Batteries.UnionFind forest of n singleton classes.
• equivClass, ValidRank: root equivalence-class finsets and the root rank-size invariant 2 ^ uf.rank r ≤ (equivClass uf r).card.
• findSteps, rankBound, findGo, compressWithSteps: computable path-compression step counter and kernel-reducible helpers propositionally equal to Batteries.UnionFind.find.
• State, init, step, Exec, Rep, impl, run: concrete disjoint-set state, operations, Cslib.DataStructure.StateTransitionImpl, and executable client runner.
• charge: worst-case per-operation step budget on Fin n.

Main results

• find_rank, union_size, checkEquiv_size, checkEquiv_snd_eq_true: structural lemmas for Batteries.UnionFind.
• ValidRank.empty, ValidRank.push, ValidRank.ofSize, ValidRank.find, ValidRank.link, ValidRank.checkEquiv, ValidRank.union: preservation of the root rank-size invariant.
• ValidRank.two_pow_rank_le_size, ValidRank.rank_le_log: exponential class-size lower bound and logarithmic rank bound uf.rank i ≤ Nat.log 2 uf.size.
• findSteps_eq, findSteps_le_rank_sub_add_one, ValidRank.findSteps_le_log_add_one: recursive characterization and Nat.log 2 uf.size + 1 bound on find traversal length.
• Rep.validRank, Rep.rel_iff_equiv, Rep.numComp_eq, rep_init: representation invariant projections and initialization.
• stepBound, uniformStepBound, realized_client, run_correct: stateful resource certificates and adaptive-client correctness and cost theorems.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 21

Structural lemmas for Batteries.UnionFind

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.size_empty : Batteries.UnionFind.empty.size = 0

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.size_push (uf : Batteries.UnionFind) : uf.push.size = uf.size + 1

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.find_rank (uf : Batteries.UnionFind) (x : Fin uf.size) (i : ℕ) : (uf.find x).fst.rank i = uf.rank i

Path compression preserves every node's rank.

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.union_size (uf : Batteries.UnionFind) (x y : Fin uf.size) : (uf.union x y).size = uf.size

Batteries.UnionFind.union preserves universe size.

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.checkEquiv_size (uf : Batteries.UnionFind) (x y : Fin uf.size) : (uf.checkEquiv x y).1.size = uf.size

Batteries.UnionFind.checkEquiv preserves universe size.

theorem Cslib.DataStructure.DisjointSet.UnionFind.equiv_checkEquiv (uf : Batteries.UnionFind) (x y : Fin uf.size) {a b : ℕ} : (uf.checkEquiv x y).1.Equiv a b ↔ uf.Equiv a b

Batteries.UnionFind.checkEquiv preserves the equivalence relation.

theorem Cslib.DataStructure.DisjointSet.UnionFind.checkEquiv_snd_eq_true (uf : Batteries.UnionFind) (x y : Fin uf.size) : (uf.checkEquiv x y).2 = true ↔ uf.Equiv ↑x ↑y

Batteries.UnionFind.checkEquiv returns true iff x and y are equivalent.

def Cslib.DataStructure.DisjointSet.UnionFind.ofSize : ℕ → Batteries.UnionFind

Initialize a Batteries.UnionFind forest of n singleton classes {0}, …, {n - 1}.

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.size_ofSize (n : ℕ) : (ofSize n).size = n

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.parent_ofSize (n i : ℕ) : (ofSize n).parent i = i

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.rank_ofSize (n i : ℕ) : (ofSize n).rank i = 0

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.rootD_ofSize (n i : ℕ) : (ofSize n).rootD i = i

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.equiv_ofSize {n a b : ℕ} : (ofSize n).Equiv a b ↔ a = b

Root rank-size invariant and logarithmic rank bound

def Cslib.DataStructure.DisjointSet.UnionFind.equivClass (uf : Batteries.UnionFind) (r : ℕ) : Finset ℕ

The finite set of in-bounds elements of uf whose canonical root is r.

@[simp]

theorem Cslib.DataStructure.DisjointSet.UnionFind.mem_equivClass {uf : Batteries.UnionFind} {r i : ℕ} : i ∈ equivClass uf r ↔ i < uf.size ∧ uf.rootD i = r

theorem Cslib.DataStructure.DisjointSet.UnionFind.card_equivClass_le_size (uf : Batteries.UnionFind) (r : ℕ) : (equivClass uf r).card ≤ uf.size

theorem Cslib.DataStructure.DisjointSet.UnionFind.disjoint_equivClass_of_ne (uf : Batteries.UnionFind) {r₁ r₂ : ℕ} (hne : r₁ ≠ r₂) : Disjoint (equivClass uf r₁) (equivClass uf r₂)

def Cslib.DataStructure.DisjointSet.UnionFind.ValidRank (uf : Batteries.UnionFind) : Prop

Root rank-size invariant (Cormen et al., Exercise 21.4-2): every root r < uf.size has equivalence class of cardinality at least 2 ^ uf.rank r.

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.empty : ValidRank Batteries.UnionFind.empty

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.push {uf : Batteries.UnionFind} (h : ValidRank uf) : ValidRank uf.push

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.ofSize (n : ℕ) : ValidRank (UnionFind.ofSize n)

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.find {uf : Batteries.UnionFind} (h : ValidRank uf) (x : Fin uf.size) : ValidRank (uf.find x).fst

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.link {uf : Batteries.UnionFind} (h : ValidRank uf) {x y : Fin uf.size} (hx : uf.parent ↑x = ↑x) (hy : uf.parent ↑y = ↑y) : ValidRank (uf.link x y hy)

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.checkEquiv {uf : Batteries.UnionFind} (h : ValidRank uf) (x y : Fin uf.size) : ValidRank (uf.checkEquiv x y).1

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.union {uf : Batteries.UnionFind} (h : ValidRank uf) (x y : Fin uf.size) : ValidRank (uf.union x y)

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.two_pow_rank_le_size {uf : Batteries.UnionFind} (h : ValidRank uf) {i : ℕ} (hi : i < uf.size) : 2 ^ uf.rank i ≤ uf.size

Every in-bounds node i < uf.size satisfies 2 ^ uf.rank i ≤ uf.size.

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.rank_le_log {uf : Batteries.UnionFind} (h : ValidRank uf) (i : ℕ) : uf.rank i ≤ Nat.log 2 uf.size

Logarithmic rank bound (Cormen et al., Exercise 21.4-2): every node in a rank-valid Batteries.UnionFind forest has rank at most Nat.log 2 uf.size.

Computable path-compression wrapper and step bounds

def Cslib.DataStructure.DisjointSet.UnionFind.rankBound (uf : Batteries.UnionFind) : ℕ

Computable strict upper bound on all node ranks in uf (matching Batteries.UnionFind.rankMax without noncomputable).

def Cslib.DataStructure.DisjointSet.UnionFind.findGo (uf : Batteries.UnionFind) : ℕ → Fin uf.size → Batteries.UnionFind.FindAux uf.size × ℕ

Structural-fuel traversal matching Batteries.UnionFind.findAux while counting visited nodes (1 at the root check plus 1 per parent hop).

def Cslib.DataStructure.DisjointSet.UnionFind.findSteps (uf : Batteries.UnionFind) (x : Fin uf.size) : ℕ

Number of nodes inspected by Batteries.UnionFind.find starting at x (1 at the root plus 1 per parent pointer traversed).

theorem Cslib.DataStructure.DisjointSet.UnionFind.findSteps_eq (uf : Batteries.UnionFind) (x : Fin uf.size) : findSteps uf x = if uf.arr[↑x].parent = ↑x then 1 else findSteps uf ⟨uf.arr[↑x].parent, ⋯⟩ + 1

Recursive unfolding equation for findSteps.

theorem Cslib.DataStructure.DisjointSet.UnionFind.findSteps_pos (uf : Batteries.UnionFind) (x : Fin uf.size) : 0 < findSteps uf x

Every find inspects at least 1 node.

theorem Cslib.DataStructure.DisjointSet.UnionFind.findSteps_le_rank_sub_add_one (uf : Batteries.UnionFind) (x : Fin uf.size) : findSteps uf x ≤ uf.rank (uf.rootD ↑x) - uf.rank ↑x + 1

Because uf.rank increases strictly at every non-root parent hop, findSteps uf x is bounded by (uf.rank (uf.rootD x) - uf.rank x) + 1.

theorem Cslib.DataStructure.DisjointSet.UnionFind.ValidRank.findSteps_le_log_add_one {uf : Batteries.UnionFind} (h : ValidRank uf) (x : Fin uf.size) : findSteps uf x ≤ Nat.log 2 uf.size + 1

Under ValidRank uf, every find inspects at most Nat.log 2 uf.size + 1 nodes.

def Cslib.DataStructure.DisjointSet.UnionFind.compressWithSteps (uf : Batteries.UnionFind) (x : Fin uf.size) : Batteries.UnionFind × Fin uf.size × ℕ

Kernel-reducible path-compression find returning the updated Batteries.UnionFind, the root in Fin uf.size, and findSteps uf x. Propositionally equal to Batteries.UnionFind.find.

Stateful realization of DisjointSet.spec

structure Cslib.DataStructure.DisjointSet.UnionFind.State (n : ℕ) : Type

Concrete union-find state over Fin n: a Batteries.UnionFind forest of size n paired with the maintained number of equivalence classes.

• uf : Batteries.UnionFind

  Underlying Batteries.UnionFind forest.

• size_eq : self.uf.size = n

  Fixed universe size invariant.

• numComp : ℕ

  Maintained number of connected components.

def Cslib.DataStructure.DisjointSet.UnionFind.init (n : ℕ) : State n

Initial concrete disjoint-set state of n singleton components.

def Cslib.DataStructure.DisjointSet.UnionFind.step {n : ℕ} (s : State n) (o : Op n) : State n × (spec n).Result o × ℕ

Execute a single DisjointSet.Op n on s, returning the updated state, answer, and step count.

def Cslib.DataStructure.DisjointSet.UnionFind.Exec (n : ℕ) : Execution (spec n).signature (State n) ℕ

Native execution relation for DisjointSet.spec n over State n.

def Cslib.DataStructure.DisjointSet.UnionFind.Rep {n : ℕ} (p : Partition n) (s : State n) : Prop

Representation relation coupling an abstract Partition n with a concrete State n.

theorem Cslib.DataStructure.DisjointSet.UnionFind.Rep.validRank {n : ℕ} {p : Partition n} {s : State n} (h : Rep p s) : ValidRank s.uf

Extract the root rank-size invariant from Rep.

theorem Cslib.DataStructure.DisjointSet.UnionFind.Rep.rel_iff_equiv {n : ℕ} {p : Partition n} {s : State n} (h : Rep p s) (x y : Fin n) : p.rel x y = true ↔ s.uf.Equiv ↑x ↑y

Extract the element-equivalence coupling from Rep.

theorem Cslib.DataStructure.DisjointSet.UnionFind.Rep.numComp_eq {n : ℕ} {p : Partition n} {s : State n} (h : Rep p s) : s.numComp = p.numComponents

Extract the maintained component-count equality from Rep.

theorem Cslib.DataStructure.DisjointSet.UnionFind.rep_init (n : ℕ) : Rep (Partition.discrete n) (init n)

init n represents the discrete partition Partition.discrete n of n singletons.

def Cslib.DataStructure.DisjointSet.UnionFind.impl (n : ℕ) : StateTransitionImpl (spec n) (Exec n)

Semantic realization of DisjointSet.spec n by Batteries.UnionFind with path compression and union by rank.

def Cslib.DataStructure.DisjointSet.UnionFind.charge (n : ℕ) : Partition n → Op n → ℕ

Worst-case per-operation step budget on Fin n: at most Nat.log 2 n + 1 nodes inspected per find, plus 1 link step in Op.union and 1 counter read in Op.numComponents.

theorem Cslib.DataStructure.DisjointSet.UnionFind.charge_le (n : ℕ) (p : Partition n) (o : Op n) : charge n p o ≤ 2 * Nat.log 2 n + 3

Every disjoint-set operation has worst-case charge at most 2 * Nat.log 2 n + 3.

theorem Cslib.DataStructure.DisjointSet.UnionFind.stepBound (n : ℕ) : Bound (impl n) id (charge n)

Per-operation logarithmic step certificate for impl n.

theorem Cslib.DataStructure.DisjointSet.UnionFind.uniformStepBound (n : ℕ) : Bound (impl n) id fun (x : (spec n).State) (x_1 : (spec n).Op) => 2 * Nat.log 2 n + 3

Uniform per-operation logarithmic step certificate 2 * Nat.log 2 n + 3.

theorem Cslib.DataStructure.DisjointSet.UnionFind.realized_client {n : ℕ} {β : Type} (client : (spec n).Client β) {p : Partition n} {s : State n} (hr : Rep p s) : ∃ (s' : State n) (traces : List ℕ), Executes (Exec n) client s ((spec n).runClient p client).1 s' traces ∧ Rep ((spec n).runClient p client).2.1 s' ∧ total id traces ≤ (spec n).totalCost (charge n) p ((spec n).runClient p client).2.2

Every adaptive disjoint-set client has a valid execution matching abstract partition semantics and satisfying the additive O(log n) per-operation step bound.

def Cslib.DataStructure.DisjointSet.UnionFind.run {n : ℕ} {β : Type} (s : State n) : (spec n).Client β → β × State n × List ℕ

Execute a disjoint-set client concretely, recording the exact step count of each operation.

theorem Cslib.DataStructure.DisjointSet.UnionFind.run_exec {n : ℕ} {β : Type} (client : (spec n).Client β) (s : State n) : Executes (Exec n) client s (run s client).1 (run s client).2.1 (run s client).2.2

The concrete runner produces a valid Executes (Exec n) derivation.

theorem Cslib.DataStructure.DisjointSet.UnionFind.run_correct {n : ℕ} {β : Type} (client : (spec n).Client β) {p : Partition n} {s : State n} (hr : Rep p s) : (run s client).1 = ((spec n).runClient p client).1 ∧ Rep ((spec n).runClient p client).2.1 (run s client).2.1 ∧ total id (run s client).2.2 ≤ (spec n).totalCost (charge n) p ((spec n).runClient p client).2.2 ∧ total id (run s client).2.2 ≤ ((spec n).runClient p client).2.2.length * (2 * Nat.log 2 n + 3)

Running the concrete union-find interpreter agrees with abstract Partition n semantics, preserves Rep, and satisfies both the exact per-operation and uniform O(log n) step bounds.