Representation-independent disjoint-set specification

This module specifies a dynamic partition (disjoint-set / union-find abstract state machine) over a finite universe Fin n in the Cslib.DataStructure framework.

Mathematical states are equivalence relations Partition n with decidable Boolean membership, starting from the discrete partition Partition.discrete n of n singleton classes. The interface (Op, spec) exposes:

• Op.same x y: test whether x and y belong to the same equivalence class;
• Op.union x y: merge the classes of x and y, returning true iff two distinct classes merged;
• Op.numComponents: return the current number of equivalence classes.

Unlike concrete union-find forests, spec intentionally does not expose raw tree-root indices: under union by rank, two histories reaching the same mathematical partition can choose different canonical roots, so exposing root indices would leak internal forest history rather than abstract partition state. Returning the effective-merge Boolean from Op.union gives single-pass edge filters such as spanningForestEdges (the unweighted Kruskal / cycle-filtering loop, whose returned edge list depends on observed answers while its issued operation sequence is fixed at one Op.union per input edge), while clients such as connectIfNew branch on same so that the issued operation sequence itself adapts to the current partition.

Main definitions

• Cslib.DataStructure.DisjointSet.Partition: decidable equivalence relations on Fin n.
• Partition.toSetoid, Partition.discrete, Partition.classOf, Partition.components, Partition.numComponents, Partition.merge: setoid view, singleton partition, equivalence classes, quotient component set, component count, and binary class merge.
• Cslib.DataStructure.DisjointSet.Op, Cslib.DataStructure.DisjointSet.spec: typed disjoint-set operations and Cslib.DataStructure.StateTransitionSpec.
• same, union, getNumComponents, connectIfNew, spanningForestEdges: primitive client operations, history-adaptive conditional union, and the single-pass spanning-forest edge filter.

Main results

• Partition.rel_merge_iff_eqvGen: p.merge x y is the exact equivalence closure Relation.EqvGen generated by p and the pair (x, y).
• Partition.numComponents_discrete, Partition.numComponents_merge_of_rel, Partition.numComponents_merge_of_not_rel: exact component counts initially and across redundant versus effective merges.
• runClient_connectIfNew, runClient_spanningForestEdges_history: exact operation histories for history-adaptive conditional union and single-pass spanning-forest filtering.
• spanningForestEdges_sublist, spanningForestEdges_rel_iff_eqvGen, spanningForestEdges_numComponents_add_length, spanningForestEdges_idempotent_partition: correctness, connectivity preservation, and component-count conservation for spanningForestEdges.

References

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

structure Cslib.DataStructure.DisjointSet.Partition (n : ℕ) : Type

A decidable partition (equivalence relation) on Fin n.

• rel : Fin n → Fin n → Bool

  Boolean equivalence test between elements of Fin n.

• refl (x : Fin n) : self.rel x x = true

  Reflexivity of rel.

• symm {x y : Fin n} : self.rel x y = true → self.rel y x = true

  Symmetry of rel.

• trans {x y z : Fin n} : self.rel x y = true → self.rel y z = true → self.rel x z = true

  Transitivity of rel.

theorem Cslib.DataStructure.DisjointSet.Partition.ext {n : ℕ} {p q : Partition n} (h : ∀ (x y : Fin n), p.rel x y = q.rel x y) : p = q

theorem Cslib.DataStructure.DisjointSet.Partition.ext_iff {n : ℕ} {p q : Partition n} : p = q ↔ ∀ (x y : Fin n), p.rel x y = q.rel x y

@[instance_reducible]

instance Cslib.DataStructure.DisjointSet.Partition.instDecidableEq (n : ℕ) : DecidableEq (Partition n)

@[simp]

theorem Cslib.DataStructure.DisjointSet.Partition.rel_refl {n : ℕ} (p : Partition n) (x : Fin n) : p.rel x x = true

theorem Cslib.DataStructure.DisjointSet.Partition.rel_comm {n : ℕ} (p : Partition n) (x y : Fin n) : p.rel x y = p.rel y x

Boolean symmetry of p.rel.

def Cslib.DataStructure.DisjointSet.Partition.toSetoid {n : ℕ} (p : Partition n) : Setoid (Fin n)

View a Partition n as a Setoid (Fin n).

@[simp]

theorem Cslib.DataStructure.DisjointSet.Partition.toSetoid_r_iff {n : ℕ} (p : Partition n) (x y : Fin n) : p.toSetoid x y ↔ p.rel x y = true

def Cslib.DataStructure.DisjointSet.Partition.discrete (n : ℕ) : Partition n

The discrete partition of Fin n into n singleton classes.

@[simp]

theorem Cslib.DataStructure.DisjointSet.Partition.rel_discrete {n : ℕ} (x y : Fin n) : (discrete n).rel x y = (x == y)

theorem Cslib.DataStructure.DisjointSet.Partition.rel_discrete_eq_true {n : ℕ} {x y : Fin n} : (discrete n).rel x y = true ↔ x = y

def Cslib.DataStructure.DisjointSet.Partition.classOf {n : ℕ} (p : Partition n) (x : Fin n) : Finset (Fin n)

The equivalence class of x in p.

@[simp]

theorem Cslib.DataStructure.DisjointSet.Partition.mem_classOf {n : ℕ} {p : Partition n} {x y : Fin n} : y ∈ p.classOf x ↔ p.rel x y = true

theorem Cslib.DataStructure.DisjointSet.Partition.self_mem_classOf {n : ℕ} (p : Partition n) (x : Fin n) : x ∈ p.classOf x

theorem Cslib.DataStructure.DisjointSet.Partition.classOf_nonempty {n : ℕ} (p : Partition n) (x : Fin n) : (p.classOf x).Nonempty

theorem Cslib.DataStructure.DisjointSet.Partition.classOf_eq_iff {n : ℕ} {p : Partition n} {x y : Fin n} : p.classOf x = p.classOf y ↔ p.rel x y = true

Two elements have the same equivalence class iff they are related in p.

theorem Cslib.DataStructure.DisjointSet.Partition.disjoint_classOf_of_rel_eq_false {n : ℕ} {p : Partition n} {x y : Fin n} (h : p.rel x y = false) : Disjoint (p.classOf x) (p.classOf y)

Unrelated elements have disjoint equivalence classes.

def Cslib.DataStructure.DisjointSet.Partition.components {n : ℕ} (p : Partition n) : Finset (Finset (Fin n))

The finite set of equivalence classes (connected components) of p.

@[simp]

theorem Cslib.DataStructure.DisjointSet.Partition.mem_components {n : ℕ} {p : Partition n} {c : Finset (Fin n)} : c ∈ p.components ↔ ∃ (x : Fin n), p.classOf x = c

theorem Cslib.DataStructure.DisjointSet.Partition.classOf_mem_components {n : ℕ} (p : Partition n) (x : Fin n) : p.classOf x ∈ p.components

def Cslib.DataStructure.DisjointSet.Partition.numComponents {n : ℕ} (p : Partition n) : ℕ

The number of equivalence classes of p.

@[simp]

theorem Cslib.DataStructure.DisjointSet.Partition.numComponents_zero (p : Partition 0) : p.numComponents = 0

theorem Cslib.DataStructure.DisjointSet.Partition.numComponents_le {n : ℕ} (p : Partition n) : p.numComponents ≤ n

Every partition of Fin n has at most n components.

theorem Cslib.DataStructure.DisjointSet.Partition.numComponents_pos {n : ℕ} (hn : 0 < n) (p : Partition n) : 0 < p.numComponents

Every partition of a nonempty Fin n has at least one component.

@[simp]

theorem Cslib.DataStructure.DisjointSet.Partition.numComponents_discrete (n : ℕ) : (discrete n).numComponents = n

The discrete partition on Fin n has n components.

def Cslib.DataStructure.DisjointSet.Partition.merge {n : ℕ} (p : Partition n) (x y : Fin n) : Partition n

Merge the equivalence classes of x and y in p.

@[simp]

theorem Cslib.DataStructure.DisjointSet.Partition.rel_merge {n : ℕ} (p : Partition n) (x y a b : Fin n) : (p.merge x y).rel a b = (p.rel a b || p.rel a x && p.rel y b || p.rel a y && p.rel x b)

theorem Cslib.DataStructure.DisjointSet.Partition.rel_merge_eq_true {n : ℕ} {p : Partition n} {x y a b : Fin n} : (p.merge x y).rel a b = true ↔ p.rel a b = true ∨ p.rel a x = true ∧ p.rel y b = true ∨ p.rel a y = true ∧ p.rel x b = true

theorem Cslib.DataStructure.DisjointSet.Partition.rel_merge_iff_eqvGen {n : ℕ} {p : Partition n} {x y a b : Fin n} : (p.merge x y).rel a b = true ↔ Relation.EqvGen (fun (u v : Fin n) => p.rel u v = true ∨ u = x ∧ v = y) a b

p.merge x y is the exact equivalence closure Relation.EqvGen of p together with (x, y).

@[simp]

theorem Cslib.DataStructure.DisjointSet.Partition.merge_self {n : ℕ} (p : Partition n) (x : Fin n) : p.merge x x = p

theorem Cslib.DataStructure.DisjointSet.Partition.merge_comm {n : ℕ} (p : Partition n) (x y : Fin n) : p.merge x y = p.merge y x

theorem Cslib.DataStructure.DisjointSet.Partition.merge_of_rel {n : ℕ} {p : Partition n} {x y : Fin n} (h : p.rel x y = true) : p.merge x y = p

Merging two already-equivalent elements leaves the partition unchanged.

theorem Cslib.DataStructure.DisjointSet.Partition.numComponents_merge_of_rel {n : ℕ} {p : Partition n} {x y : Fin n} (h : p.rel x y = true) : (p.merge x y).numComponents = p.numComponents

Redundant merges preserve the number of components.

theorem Cslib.DataStructure.DisjointSet.Partition.numComponents_merge_of_not_rel {n : ℕ} {p : Partition n} {x y : Fin n} (h : p.rel x y = false) : (p.merge x y).numComponents + 1 = p.numComponents

Merging two distinct equivalence classes decreases the number of components by exactly 1.

inductive Cslib.DataStructure.DisjointSet.Op (n : ℕ) : Type

Typed operations on a disjoint-set partition over Fin n.

• same {n : ℕ} (x y : Fin n) : Op n

  Test whether x and y belong to the same equivalence class.

• union {n : ℕ} (x y : Fin n) : Op n

  Merge the classes of x and y, returning true iff two distinct classes merged.

• numComponents {n : ℕ} : Op n

  Query the current number of equivalence classes.

def Cslib.DataStructure.DisjointSet.instDecidableEqOp.decEq {n✝ : ℕ} (x✝ x✝¹ : Op n✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.DataStructure.DisjointSet.instDecidableEqOp {n✝ : ℕ} : DecidableEq (Op n✝)

def Cslib.DataStructure.DisjointSet.instReprOp.repr {n✝ : ℕ} : Op n✝ → ℕ → Std.Format

@[instance_reducible]

instance Cslib.DataStructure.DisjointSet.instReprOp {n✝ : ℕ} : Repr (Op n✝)

@[reducible, inline]

abbrev Cslib.DataStructure.DisjointSet.Op.Result {n : ℕ} : Op n → Type

Operation return types for Op n.

@[reducible, inline]

abbrev Cslib.DataStructure.DisjointSet.spec (n : ℕ) : StateTransitionSpec

Total stateful specification of a disjoint-set structure on Fin n.

def Cslib.DataStructure.DisjointSet.same {n : ℕ} (x y : Fin n) : (spec n).Client Bool

Client helper: query whether x and y are in the same equivalence class.

def Cslib.DataStructure.DisjointSet.union {n : ℕ} (x y : Fin n) : (spec n).Client Bool

Client helper: merge the classes of x and y, returning true iff two distinct classes merged.

def Cslib.DataStructure.DisjointSet.getNumComponents {n : ℕ} : (spec n).Client ℕ

Client helper: query the current number of equivalence classes.

def Cslib.DataStructure.DisjointSet.connectIfNew {n : ℕ} (x y : Fin n) : (spec n).Client Bool

History-adaptive connection client: query same x y first, issuing union x y only when x and y belong to distinct equivalence classes. Its operation history has length 1 when x and y are already connected and 2 when they merge.

theorem Cslib.DataStructure.DisjointSet.runClient_connectIfNew {n : ℕ} (x y : Fin n) (p : Partition n) : (spec n).runClient p (connectIfNew x y) = if p.rel x y = true then (false, p, [Op.same x y]) else (true, p.merge x y, [Op.same x y, Op.union x y])

Exact semantics and state-dependent operation history of connectIfNew.

def Cslib.DataStructure.DisjointSet.spanningForestEdges {n : ℕ} {E : Type} (endpts : E → Fin n × Fin n) : List E → (spec n).Client (List E)

Single-pass spanning-forest client (the cycle-filtering loop shared with Kruskal's algorithm) parameterized over an arbitrary edge type E with endpoint map endpts : E → Fin n × Fin n: scan edges in order, retaining an edge e iff union (endpts e).1 (endpts e).2 reports that its endpoints lay in distinct components.

@[simp]

theorem Cslib.DataStructure.DisjointSet.eval_spanningForestEdges_nil {n : ℕ} {E : Type} (endpts : E → Fin n × Fin n) (p : Partition n) : eval (spec n) (spanningForestEdges endpts []) p = ([], p)

@[simp]

theorem Cslib.DataStructure.DisjointSet.eval_spanningForestEdges_cons {n : ℕ} {E : Type} (endpts : E → Fin n × Fin n) (e : E) (es : List E) (p : Partition n) : eval (spec n) (spanningForestEdges endpts (e :: es)) p = have rest := eval (spec n) (spanningForestEdges endpts es) (p.merge (endpts e).1 (endpts e).2); (if (!p.rel (endpts e).1 (endpts e).2) = true then e :: rest.1 else rest.1, rest.2)

theorem Cslib.DataStructure.DisjointSet.runClient_spanningForestEdges_history {n : ℕ} {E : Type} (endpts : E → Fin n × Fin n) (es : List E) (p : Partition n) : ((spec n).runClient p (spanningForestEdges endpts es)).2.2 = List.map (fun (e : E) => Op.union (endpts e).1 (endpts e).2) es

Exact operation history issued by spanningForestEdges endpts es: one Op.union call per input edge in order.

theorem Cslib.DataStructure.DisjointSet.runClient_spanningForestEdges_length {n : ℕ} {E : Type} (endpts : E → Fin n × Fin n) (es : List E) (p : Partition n) : ((spec n).runClient p (spanningForestEdges endpts es)).2.2.length = es.length

spanningForestEdges endpts es issues es.length operations.

theorem Cslib.DataStructure.DisjointSet.spanningForestEdges_sublist {n : ℕ} {E : Type} (endpts : E → Fin n × Fin n) (es : List E) (p : Partition n) : (eval (spec n) (spanningForestEdges endpts es) p).1.Sublist es

Every retained edge belongs to the input edge list in order.

theorem Cslib.DataStructure.DisjointSet.spanningForestEdges_numComponents_add_length {n : ℕ} {E : Type} (endpts : E → Fin n × Fin n) (es : List E) (p : Partition n) : Partition.numComponents (eval (spec n) (spanningForestEdges endpts es) p).2 + (eval (spec n) (spanningForestEdges endpts es) p).1.length = p.numComponents

Exact conservation law: the final component count plus the number of accepted forest edges equals the initial component count.

theorem Cslib.DataStructure.DisjointSet.spanningForestEdges_rel_iff_eqvGen {n : ℕ} {E : Type} (endpts : E → Fin n × Fin n) (es : List E) (p : Partition n) (a b : Fin n) : (eval (spec n) (spanningForestEdges endpts es) p).2.rel a b = true ↔ Relation.EqvGen (fun (u v : Fin n) => p.rel u v = true ∨ ∃ e ∈ es, u = (endpts e).1 ∧ v = (endpts e).2) a b

The final partition after spanningForestEdges endpts es is the exact equivalence closure of p together with all endpoint pairs in es.

theorem Cslib.DataStructure.DisjointSet.spanningForestEdges_idempotent_partition {n : ℕ} {E : Type} (endpts : E → Fin n × Fin n) (es : List E) (p : Partition n) : (eval (spec n) (spanningForestEdges endpts (eval (spec n) (spanningForestEdges endpts es) p).1) p).2 = (eval (spec n) (spanningForestEdges endpts es) p).2

Discarding cycle edges preserves connectivity: running spanningForestEdges on the retained forest edges reaches the exact same partition as running it on es.