Union-find node type
Instances For
Parent of a union-find node, defaults to self when the node is a root
Equations
- Batteries.UnionFind.parentD arr i = if h : i < arr.size then (arr.get ⟨i, h⟩).parent else i
Instances For
Rank of a union-find node, defaults to 0 when the node is a root
Equations
- Batteries.UnionFind.rankD arr i = if h : i < arr.size then (arr.get ⟨i, h⟩).rank else 0
Instances For
Union-find data structure #
The UnionFind
structure is an implementation of disjoint-set data structure
that uses path compression to make the primary operations run in amortized
nearly linear time. The nodes of a UnionFind
structure s
are natural
numbers smaller than s.size
. The structure associates with a canonical
representative from its equivalence class. The structure can be extended
using the push
operation and equivalence classes can be updated using the
union
operation.
The main operations for UnionFind
are:
empty
/mkEmpty
are used to create a new empty structure.size
returns the size of the data structure.push
adds a new node to a structure, unlinked to any other node.union
links two nodes of the data structure, joining their equivalence classes, and performs path compression.find
returns the canonical representative of a node and updates the data structure using path compression.root
returns the canonical representative of a node without altering the data structure.checkEquiv
checks whether two nodes have the same canonical representative and updates the structure using path compression.
Most use cases should prefer find
over root
to benefit from the speedup from path-compression.
The main operations use Fin s.size
to represent nodes of the union-find structure.
Some alternatives are provided:
unionN
,findN
,rootN
,checkEquivN
useFin n
with a proof thatn = s.size
.union!
,find!
,root!
,checkEquiv!
useNat
and panic when the indices are out of bounds.findD
,rootD
,checkEquivD
useNat
and treat out of bound indices as isolated nodes.
The noncomputable relation UnionFind.Equiv
is provided to use the equivalence relation from a
UnionFind
structure in the context of proofs.
- arr : Array Batteries.UFNode
Array of union-find nodes
- parentD_lt : ∀ {i : Nat}, i < self.arr.size → Batteries.UnionFind.parentD self.arr i < self.arr.size
Validity for parent nodes
- rankD_lt : ∀ {i : Nat}, Batteries.UnionFind.parentD self.arr i ≠ i → Batteries.UnionFind.rankD self.arr i < Batteries.UnionFind.rankD self.arr (Batteries.UnionFind.parentD self.arr i)
Validity for rank
Instances For
Validity for parent nodes
Validity for rank
Create an empty union-find structure with specific capacity
Equations
- Batteries.UnionFind.mkEmpty c = { arr := Array.mkEmpty c, parentD_lt := ⋯, rankD_lt := ⋯ }
Instances For
Empty union-find structure
Instances For
Equations
- Batteries.UnionFind.instEmptyCollection = { emptyCollection := Batteries.UnionFind.empty }
Parent of union-find node
Equations
- self.parent i = Batteries.UnionFind.parentD self.arr i
Instances For
Rank of union-find node
Equations
- self.rank i = Batteries.UnionFind.rankD self.arr i
Instances For
Maximum rank of nodes in a union-find structure
Equations
- self.rankMax = Array.foldr (fun (x : Batteries.UFNode) => max x.rank) 0 self.arr + 1
Instances For
Add a new node to a union-find structure, unlinked with any other nodes
Equations
- self.push = { arr := self.arr.push { parent := self.arr.size, rank := 0 }, parentD_lt := ⋯, rankD_lt := ⋯ }
Instances For
Root of a union-find node.
Equations
Instances For
Root of a union-find node.
Equations
- self.rootN x_2 ⋯ = self.root x_2
Instances For
Root of a union-find node. Panics if index is out of bounds.
Equations
- self.root! x = if h : x < self.size then ↑(self.root ⟨x, h⟩) else Batteries.UnionFind.panicWith x "index out of bounds"
Instances For
Root of a union-find node. Returns input if index is out of bounds.
Instances For
Auxiliary data structure for find operation
Instances For
Size requirement
Auxiliary function for find operation
Equations
- One or more equations did not get rendered due to their size.
Instances For
Find root of a union-find node, updating the structure using path compression.
Equations
- self.find x = ⟨{ arr := (self.findAux x).s, parentD_lt := ⋯, rankD_lt := ⋯ }, ⟨⟨↑(self.findAux x).root, ⋯⟩, ⋯⟩⟩
Instances For
Find root of a union-find node, updating the structure using path compression.
Instances For
Find root of a union-find node, updating the structure using path compression. Panics if index is out of bounds.
Equations
- self.find! x = if h : x < self.size then match self.find ⟨x, h⟩ with | ⟨s, ⟨r, property⟩⟩ => (s, ↑r) else Batteries.UnionFind.panicWith (self, x) "index out of bounds"
Instances For
Find root of a union-find node, updating the structure using path compression. Returns inputs unchanged when index is out of bounds.
Equations
Instances For
Link two union-find nodes
Equations
- One or more equations did not get rendered due to their size.
Instances For
Link a union-find node to a root node.
Equations
- self.link x y yroot = { arr := Batteries.UnionFind.linkAux self.arr x y, parentD_lt := ⋯, rankD_lt := ⋯ }
Instances For
Link a union-find node to a root node.
Equations
- self.linkN x_2 y_2 yroot_2 ⋯ = self.link x_2 y_2 yroot_2
Instances For
Link a union-find node to a root node. Panics if either index is out of bounds.
Equations
- self.link! x y yroot = if h : x < self.size ∧ y < self.size then self.link ⟨x, ⋯⟩ ⟨y, ⋯⟩ yroot else Batteries.UnionFind.panicWith self "index out of bounds"
Instances For
Link two union-find nodes, uniting their respective classes.
Equations
- self.union x y = match self.find x with | ⟨self₁, ⟨rx, ex⟩⟩ => let_fun hy := ⋯; match eq : self₁.find ⟨↑y, hy⟩ with | ⟨self₂, ⟨ry, ey⟩⟩ => self₂.link ⟨↑rx, ⋯⟩ ry ⋯
Instances For
Link two union-find nodes, uniting their respective classes.
Equations
- self.unionN x_2 y_2 ⋯ = self.union x_2 y_2
Instances For
Link two union-find nodes, uniting their respective classes. Panics if either index is out of bounds.
Equations
- self.union! x y = if h : x < self.size ∧ y < self.size then self.union ⟨x, ⋯⟩ ⟨y, ⋯⟩ else Batteries.UnionFind.panicWith self "index out of bounds"
Instances For
Check whether two union-find nodes are equivalent, updating structure using path compression.
Equations
Instances For
Check whether two union-find nodes are equivalent, updating structure using path compression.
Equations
- self.checkEquivN x_2 y_2 ⋯ = self.checkEquiv x_2 y_2
Instances For
Check whether two union-find nodes are equivalent, updating structure using path compression. Panics if either index is out of bounds.
Equations
Instances For
Check whether two union-find nodes are equivalent with path compression,
returns x == y
if either index is out of bounds
Equations
Instances For
Equivalence relation from a UnionFind
structure