structure Std.UFNode : Type

Union-find node type

• parent : Nat

  Parent of node

• rank : Nat

  Rank of node

def Std.UnionFind.panicWith {α : Type u_1} (v : α) (msg : String) : α

Panic with return value

Equations

• Std.UnionFind.panicWith v msg = panic msg

@[simp]

theorem Std.UnionFind.panicWith_eq {α : Type u_1} (v : α) (msg : String) : Std.UnionFind.panicWith v msg = v

def Std.UnionFind.parentD (arr : Array Std.UFNode) (i : Nat) : Nat

Parent of a union-find node, defaults to self when the node is a root

Equations

• Std.UnionFind.parentD arr i = if h : i < Array.size arr then (Array.get arr { val := i, isLt := h }).parent else i

def Std.UnionFind.rankD (arr : Array Std.UFNode) (i : Nat) : Nat

Rank of a union-find node, defaults to 0 when the node is a root

Equations

• Std.UnionFind.rankD arr i = if h : i < Array.size arr then (Array.get arr { val := i, isLt := h }).rank else 0

theorem Std.UnionFind.parentD_eq {arr : Array Std.UFNode} {i : Fin (Array.size arr)} : Std.UnionFind.parentD arr ↑i = (Array.get arr i).parent

theorem Std.UnionFind.parentD_eq' {arr : Array Std.UFNode} {i : Nat} (h : i < Array.size arr) : Std.UnionFind.parentD arr i = (Array.get arr { val := i, isLt := h }).parent

theorem Std.UnionFind.rankD_eq {arr : Array Std.UFNode} {i : Fin (Array.size arr)} : Std.UnionFind.rankD arr ↑i = (Array.get arr i).rank

theorem Std.UnionFind.rankD_eq' {arr : Array Std.UFNode} {i : Nat} (h : i < Array.size arr) : Std.UnionFind.rankD arr i = (Array.get arr { val := i, isLt := h }).rank

theorem Std.UnionFind.parentD_of_not_lt {i : Nat} {arr : Array Std.UFNode} : ¬i < Array.size arr → Std.UnionFind.parentD arr i = i

theorem Std.UnionFind.lt_of_parentD {arr : Array Std.UFNode} {i : Nat} : Std.UnionFind.parentD arr i ≠ i → i < Array.size arr

theorem Std.UnionFind.parentD_set {arr : Array Std.UFNode} {x : Fin (Array.size arr)} {v : Std.UFNode} {i : Nat} : Std.UnionFind.parentD (Array.set arr x v) i = if ↑x = i then v.parent else Std.UnionFind.parentD arr i

theorem Std.UnionFind.rankD_set {arr : Array Std.UFNode} {x : Fin (Array.size arr)} {v : Std.UFNode} {i : Nat} : Std.UnionFind.rankD (Array.set arr x v) i = if ↑x = i then v.rank else Std.UnionFind.rankD arr i

structure Std.UnionFind : Type

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 use Fin n with a proof that n = s.size.
• union!, find!, root!, checkEquiv! use Nat and panic when the indices are out of bounds.
• findD, rootD, checkEquivD use Nat 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 Std.UFNode

  Array of union-find nodes

• parentD_lt : ∀ {i : Nat}, i < Array.size self.arr → Std.UnionFind.parentD self.arr i < Array.size self.arr

  Validity for parent nodes

• rankD_lt : ∀ {i : Nat}, Std.UnionFind.parentD self.arr i ≠ i → Std.UnionFind.rankD self.arr i < Std.UnionFind.rankD self.arr (Std.UnionFind.parentD self.arr i)

  Validity for rank

@[inline, reducible]

abbrev Std.UnionFind.size (self : Std.UnionFind) : Nat

Size of union-find structure.

Equations

• Std.UnionFind.size self = Array.size self.arr

def Std.UnionFind.mkEmpty (c : Nat) : Std.UnionFind

Create an empty union-find structure with specific capacity

Equations

• Std.UnionFind.mkEmpty c = { arr := Array.mkEmpty c, parentD_lt := ⋯, rankD_lt := ⋯ }

def Std.UnionFind.empty : Std.UnionFind

Empty union-find structure

Equations

• Std.UnionFind.empty = Std.UnionFind.mkEmpty 0

instance Std.UnionFind.instEmptyCollectionUnionFind : EmptyCollection Std.UnionFind

Equations

• Std.UnionFind.instEmptyCollectionUnionFind = { emptyCollection := Std.UnionFind.empty }

@[inline, reducible]

abbrev Std.UnionFind.parent (self : Std.UnionFind) (i : Nat) : Nat

Parent of union-find node

Equations

• Std.UnionFind.parent self i = Std.UnionFind.parentD self.arr i

theorem Std.UnionFind.parent'_lt (self : Std.UnionFind) (i : Fin (Std.UnionFind.size self)) : (Array.get self.arr i).parent < Std.UnionFind.size self

theorem Std.UnionFind.parent_lt (self : Std.UnionFind) (i : Nat) : Std.UnionFind.parent self i < Std.UnionFind.size self ↔ i < Std.UnionFind.size self

@[inline, reducible]

abbrev Std.UnionFind.rank (self : Std.UnionFind) (i : Nat) : Nat

Rank of union-find node

Equations

• Std.UnionFind.rank self i = Std.UnionFind.rankD self.arr i

theorem Std.UnionFind.rank_lt {self : Std.UnionFind} {i : Nat} : Std.UnionFind.parent self i ≠ i → Std.UnionFind.rank self i < Std.UnionFind.rank self (Std.UnionFind.parent self i)

theorem Std.UnionFind.rank'_lt (self : Std.UnionFind) (i : Fin (Std.UnionFind.size self)) : (Array.get self.arr i).parent ≠ ↑i → Std.UnionFind.rank self ↑i < Std.UnionFind.rank self (Array.get self.arr i).parent

noncomputable def Std.UnionFind.rankMax (self : Std.UnionFind) : Nat

Maximum rank of nodes in a union-find structure

Equations

• Std.UnionFind.rankMax self = Array.foldr (fun (x : Std.UFNode) => max x.rank) 0 self.arr (Array.size self.arr) + 1

theorem Std.UnionFind.rank'_lt_rankMax (self : Std.UnionFind) (i : Fin (Std.UnionFind.size self)) : (Array.get self.arr i).rank < Std.UnionFind.rankMax self

theorem Std.UnionFind.rank'_lt_rankMax.go {l : List Std.UFNode} {x : Std.UFNode} : x ∈ l → x.rank ≤ List.foldr (fun (x : Std.UFNode) => max x.rank) 0 l

theorem Std.UnionFind.rankD_lt_rankMax (self : Std.UnionFind) (i : Nat) : Std.UnionFind.rankD self.arr i < Std.UnionFind.rankMax self

theorem Std.UnionFind.lt_rankMax (self : Std.UnionFind) (i : Nat) : Std.UnionFind.rank self i < Std.UnionFind.rankMax self

theorem Std.UnionFind.push_rankD {i : Nat} (arr : Array Std.UFNode) : Std.UnionFind.rankD (Array.push arr { parent := Array.size arr, rank := 0 }) i = Std.UnionFind.rankD arr i

theorem Std.UnionFind.push_parentD {i : Nat} (arr : Array Std.UFNode) : Std.UnionFind.parentD (Array.push arr { parent := Array.size arr, rank := 0 }) i = Std.UnionFind.parentD arr i

def Std.UnionFind.push (self : Std.UnionFind) : Std.UnionFind

Add a new node to a union-find structure, unlinked with any other nodes

Equations

• Std.UnionFind.push self = { arr := Array.push self.arr { parent := Array.size self.arr, rank := 0 }, parentD_lt := ⋯, rankD_lt := ⋯ }

def Std.UnionFind.root (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) : Fin (Std.UnionFind.size self)

Root of a union-find node.

Equations

• Std.UnionFind.root self x = if h : (Array.get self.arr x).parent = ↑x then x else let_fun this := ⋯; Std.UnionFind.root self { val := (Array.get self.arr x).parent, isLt := ⋯ }

def Std.UnionFind.rootN {n : Nat} (self : Std.UnionFind) (x : Fin n) (h : n = Std.UnionFind.size self) : Fin n

Root of a union-find node.

Equations

• Std.UnionFind.rootN self x h = match n, h, x with | .(Std.UnionFind.size self), ⋯, x => Std.UnionFind.root self x

def Std.UnionFind.root! (self : Std.UnionFind) (x : Nat) : Nat

Root of a union-find node. Panics if index is out of bounds.

Equations

• Std.UnionFind.root! self x = if h : x < Std.UnionFind.size self then ↑(Std.UnionFind.root self { val := x, isLt := h }) else Std.UnionFind.panicWith x "index out of bounds"

def Std.UnionFind.rootD (self : Std.UnionFind) (x : Nat) : Nat

Root of a union-find node. Returns input if index is out of bounds.

Equations

• Std.UnionFind.rootD self x = if h : x < Std.UnionFind.size self then ↑(Std.UnionFind.root self { val := x, isLt := h }) else x

theorem Std.UnionFind.parent_root (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) : (Array.get self.arr (Std.UnionFind.root self x)).parent = ↑(Std.UnionFind.root self x)

theorem Std.UnionFind.parent_rootD (self : Std.UnionFind) (x : Nat) : Std.UnionFind.parent self (Std.UnionFind.rootD self x) = Std.UnionFind.rootD self x

theorem Std.UnionFind.rootD_parent (self : Std.UnionFind) (x : Nat) : Std.UnionFind.rootD self (Std.UnionFind.parent self x) = Std.UnionFind.rootD self x

theorem Std.UnionFind.rootD_lt {self : Std.UnionFind} {x : Nat} : Std.UnionFind.rootD self x < Std.UnionFind.size self ↔ x < Std.UnionFind.size self

theorem Std.UnionFind.rootD_eq_self {self : Std.UnionFind} {x : Nat} : Std.UnionFind.rootD self x = x ↔ Std.UnionFind.parent self x = x

theorem Std.UnionFind.rootD_rootD {self : Std.UnionFind} {x : Nat} : Std.UnionFind.rootD self (Std.UnionFind.rootD self x) = Std.UnionFind.rootD self x

theorem Std.UnionFind.rootD_ext {m1 : Std.UnionFind} {m2 : Std.UnionFind} (H : ∀ (x : Nat), Std.UnionFind.parent m1 x = Std.UnionFind.parent m2 x) {x : Nat} : Std.UnionFind.rootD m1 x = Std.UnionFind.rootD m2 x

theorem Std.UnionFind.le_rank_root {self : Std.UnionFind} {x : Nat} : Std.UnionFind.rank self x ≤ Std.UnionFind.rank self (Std.UnionFind.rootD self x)

theorem Std.UnionFind.lt_rank_root {self : Std.UnionFind} {x : Nat} : Std.UnionFind.rank self x < Std.UnionFind.rank self (Std.UnionFind.rootD self x) ↔ Std.UnionFind.parent self x ≠ x

structure Std.UnionFind.FindAux (n : Nat) : Type

Auxiliary data structure for find operation

• s : Array Std.UFNode

  Array of nodes

• root : Fin n

  Index of root node

• size_eq : Array.size self.s = n

  Size requirement

def Std.UnionFind.findAux (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) : Std.UnionFind.FindAux (Std.UnionFind.size self)

Auxiliary function for find operation

Equations

• One or more equations did not get rendered due to their size.

theorem Std.UnionFind.findAux_root {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} : (Std.UnionFind.findAux self x).root = Std.UnionFind.root self x

theorem Std.UnionFind.findAux_s {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} : (Std.UnionFind.findAux self x).s = if (Array.get self.arr x).parent = ↑x then self.arr else Array.modify (Std.UnionFind.findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun (s : Std.UFNode) => { parent := Std.UnionFind.rootD self ↑x, rank := s.rank }

theorem Std.UnionFind.rankD_findAux {i : Nat} {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} : Std.UnionFind.rankD (Std.UnionFind.findAux self x).s i = Std.UnionFind.rank self i

theorem Std.UnionFind.parentD_findAux {i : Nat} {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} : Std.UnionFind.parentD (Std.UnionFind.findAux self x).s i = if i = ↑x then Std.UnionFind.rootD self ↑x else Std.UnionFind.parentD (Std.UnionFind.findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

theorem Std.UnionFind.parentD_findAux_rootD {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} : Std.UnionFind.parentD (Std.UnionFind.findAux self x).s (Std.UnionFind.rootD self ↑x) = Std.UnionFind.rootD self ↑x

theorem Std.UnionFind.parentD_findAux_lt {i : Nat} {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} (h : i < Std.UnionFind.size self) : Std.UnionFind.parentD (Std.UnionFind.findAux self x).s i < Std.UnionFind.size self

theorem Std.UnionFind.parentD_findAux_or (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) (i : Nat) : Std.UnionFind.parentD (Std.UnionFind.findAux self x).s i = Std.UnionFind.rootD self i ∧ Std.UnionFind.rootD self i = Std.UnionFind.rootD self ↑x ∨ Std.UnionFind.parentD (Std.UnionFind.findAux self x).s i = Std.UnionFind.parent self i

theorem Std.UnionFind.lt_rankD_findAux {i : Nat} {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} : Std.UnionFind.parentD (Std.UnionFind.findAux self x).s i ≠ i → Std.UnionFind.rank self i < Std.UnionFind.rank self (Std.UnionFind.parentD (Std.UnionFind.findAux self x).s i)

def Std.UnionFind.find (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) : (s : Std.UnionFind) × { _root : Fin (Std.UnionFind.size s) // Std.UnionFind.size s = Std.UnionFind.size self }

Find root of a union-find node, updating the structure using path compression.

Equations

• Std.UnionFind.find self x = let r := Std.UnionFind.findAux self x; { fst := { arr := r.s, parentD_lt := ⋯, rankD_lt := ⋯ }, snd := { val := { val := ↑r.root, isLt := ⋯ }, property := ⋯ } }

def Std.UnionFind.findN {n : Nat} (self : Std.UnionFind) (x : Fin n) (h : n = Std.UnionFind.size self) : Std.UnionFind × Fin n

Find root of a union-find node, updating the structure using path compression.

Equations

• One or more equations did not get rendered due to their size.

def Std.UnionFind.find! (self : Std.UnionFind) (x : Nat) : Std.UnionFind × Nat

Find root of a union-find node, updating the structure using path compression. Panics if index is out of bounds.

Equations

• One or more equations did not get rendered due to their size.

def Std.UnionFind.findD (self : Std.UnionFind) (x : Nat) : Std.UnionFind × Nat

Find root of a union-find node, updating the structure using path compression. Returns inputs unchanged when index is out of bounds.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Std.UnionFind.find_size (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) : Std.UnionFind.size (Std.UnionFind.find self x).fst = Std.UnionFind.size self

@[simp]

theorem Std.UnionFind.find_root_2 (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) : ↑(Std.UnionFind.find self x).snd.val = Std.UnionFind.rootD self ↑x

@[simp]

theorem Std.UnionFind.find_parent_1 (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) : Std.UnionFind.parent (Std.UnionFind.find self x).fst ↑x = Std.UnionFind.rootD self ↑x

theorem Std.UnionFind.find_parent_or (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) (i : Nat) : Std.UnionFind.parent (Std.UnionFind.find self x).fst i = Std.UnionFind.rootD self i ∧ Std.UnionFind.rootD self i = Std.UnionFind.rootD self ↑x ∨ Std.UnionFind.parent (Std.UnionFind.find self x).fst i = Std.UnionFind.parent self i

@[simp]

theorem Std.UnionFind.find_root_1 (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) (i : Nat) : Std.UnionFind.rootD (Std.UnionFind.find self x).fst i = Std.UnionFind.rootD self i

def Std.UnionFind.linkAux (self : Array Std.UFNode) (x : Fin (Array.size self)) (y : Fin (Array.size self)) : Array Std.UFNode

Link two union-find nodes

Equations

• One or more equations did not get rendered due to their size.

theorem Std.UnionFind.setParentBump_rankD_lt {arr' : Array Std.UFNode} {arr : Array Std.UFNode} {x : Fin (Array.size arr)} {y : Fin (Array.size arr)} (hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y) (H : (Array.get arr x).rank ≤ (Array.get arr y).rank) {i : Nat} (rankD_lt : Std.UnionFind.parentD arr i ≠ i → Std.UnionFind.rankD arr i < Std.UnionFind.rankD arr (Std.UnionFind.parentD arr i)) (hP : Std.UnionFind.parentD arr' i = if ↑x = i then ↑y else Std.UnionFind.parentD arr i) (hR : ∀ {i : Nat}, Std.UnionFind.rankD arr' i = if ↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else Std.UnionFind.rankD arr i) : ¬Std.UnionFind.parentD arr' i = i → Std.UnionFind.rankD arr' i < Std.UnionFind.rankD arr' (Std.UnionFind.parentD arr' i)

theorem Std.UnionFind.setParent_rankD_lt {arr : Array Std.UFNode} {x : Fin (Array.size arr)} {y : Fin (Array.size arr)} (h : (Array.get arr x).rank < (Array.get arr y).rank) {i : Nat} (rankD_lt : Std.UnionFind.parentD arr i ≠ i → Std.UnionFind.rankD arr i < Std.UnionFind.rankD arr (Std.UnionFind.parentD arr i)) : let arr' := Array.set arr x { parent := ↑y, rank := (Array.get arr x).rank }; Std.UnionFind.parentD arr' i ≠ i → Std.UnionFind.rankD arr' i < Std.UnionFind.rankD arr' (Std.UnionFind.parentD arr' i)

@[simp]

theorem Std.UnionFind.linkAux_size {self : Array Std.UFNode} {x : Fin (Array.size self)} {y : Fin (Array.size self)} : Array.size (Std.UnionFind.linkAux self x y) = Array.size self

def Std.UnionFind.link (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) (y : Fin (Std.UnionFind.size self)) (yroot : Std.UnionFind.parent self ↑y = ↑y) : Std.UnionFind

Link a union-find node to a root node.

Equations

• Std.UnionFind.link self x y yroot = { arr := Std.UnionFind.linkAux self.arr x y, parentD_lt := ⋯, rankD_lt := ⋯ }

def Std.UnionFind.linkN {n : Nat} (self : Std.UnionFind) (x : Fin n) (y : Fin n) (yroot : Std.UnionFind.parent self ↑y = ↑y) (h : n = Std.UnionFind.size self) : Std.UnionFind

Link a union-find node to a root node.

Equations

• Std.UnionFind.linkN self x y yroot h = match n, h, x, y, yroot with | .(Std.UnionFind.size self), ⋯, x, y, yroot => Std.UnionFind.link self x y yroot

def Std.UnionFind.link! (self : Std.UnionFind) (x : Nat) (y : Nat) (yroot : Std.UnionFind.parent self y = y) : Std.UnionFind

Link a union-find node to a root node. Panics if either index is out of bounds.

Equations

• One or more equations did not get rendered due to their size.

def Std.UnionFind.union (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) (y : Fin (Std.UnionFind.size self)) : Std.UnionFind

Link two union-find nodes, uniting their respective classes.

Equations

• One or more equations did not get rendered due to their size.

def Std.UnionFind.unionN {n : Nat} (self : Std.UnionFind) (x : Fin n) (y : Fin n) (h : n = Std.UnionFind.size self) : Std.UnionFind

Link two union-find nodes, uniting their respective classes.

Equations

• Std.UnionFind.unionN self x y h = match n, h, x, y with | .(Std.UnionFind.size self), ⋯, x, y => Std.UnionFind.union self x y

def Std.UnionFind.union! (self : Std.UnionFind) (x : Nat) (y : Nat) : Std.UnionFind

Link two union-find nodes, uniting their respective classes. Panics if either index is out of bounds.

Equations

• One or more equations did not get rendered due to their size.

def Std.UnionFind.checkEquiv (self : Std.UnionFind) (x : Fin (Std.UnionFind.size self)) (y : Fin (Std.UnionFind.size self)) : Std.UnionFind × Bool

Check whether two union-find nodes are equivalent, updating structure using path compression.

Equations

• One or more equations did not get rendered due to their size.

def Std.UnionFind.checkEquivN {n : Nat} (self : Std.UnionFind) (x : Fin n) (y : Fin n) (h : n = Std.UnionFind.size self) : Std.UnionFind × Bool

Check whether two union-find nodes are equivalent, updating structure using path compression.

Equations

• Std.UnionFind.checkEquivN self x y h = match n, h, x, y with | .(Std.UnionFind.size self), ⋯, x, y => Std.UnionFind.checkEquiv self x y

def Std.UnionFind.checkEquiv! (self : Std.UnionFind) (x : Nat) (y : Nat) : Std.UnionFind × Bool

Check whether two union-find nodes are equivalent, updating structure using path compression. Panics if either index is out of bounds.

Equations

• One or more equations did not get rendered due to their size.

def Std.UnionFind.checkEquivD (self : Std.UnionFind) (x : Nat) (y : Nat) : Std.UnionFind × Bool

Check whether two union-find nodes are equivalent with path compression, returns x == y if either index is out of bounds

Equations

• Std.UnionFind.checkEquivD self x y = match Std.UnionFind.findD self x with | (s, x) => match Std.UnionFind.findD s y with | (s, y) => (s, x == y)

def Std.UnionFind.Equiv (self : Std.UnionFind) (a : Nat) (b : Nat) : Prop

Equivalence relation from a UnionFind structure

Equations

• Std.UnionFind.Equiv self a b = (Std.UnionFind.rootD self a = Std.UnionFind.rootD self b)