# Documentation

Mathlib.Data.UnionFind

structure UFModel (n : ) :
• parent : Fin nFin n
• rank :
• rank_lt : ∀ (i : Fin n), ↑(parent i) irank i < rank ↑(parent i)
Instances For
Equations
def UFModel.push {n : } (m : ) (k : ) (le : n k) :
Equations
• One or more equations did not get rendered due to their size.
def UFModel.setParent {n : } (m : ) (x : Fin n) (y : Fin n) (h : UFModel.rank m x < UFModel.rank m y) :
Equations
• One or more equations did not get rendered due to their size.
def UFModel.setParentBump {n : } (m : ) (x : Fin n) (y : Fin n) (H : UFModel.rank m x UFModel.rank m y) (hroot : ↑() = y) :
Equations
• One or more equations did not get rendered due to their size.
structure UFNode (α : Type u_1) :
Type u_1
• parent :
• value : α
• rank :
Instances For
inductive UFModel.Agrees {α : Type u_1} {β : Sort u_2} (arr : ) (f : αβ) {n : } :
(Fin nβ) → Prop
Instances For
theorem UFModel.Agrees.mk' {α : Type u_1} {β : Sort u_2} {arr : } {f : αβ} {n : } {g : Fin nβ} (e : n = Array.size arr) (H : ∀ (i : ) (h₁ : i < Array.size arr) (h₂ : i < n), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }) :
theorem UFModel.Agrees.size_eq {α : Type u_1} {n : } {β : Sort u_2} {f : αβ} {arr : } {m : Fin nβ} (H : UFModel.Agrees arr f m) :
theorem UFModel.Agrees.get_eq {α : Type u_1} {β : Sort u_2} {f : αβ} {arr : } {n : } {m : Fin nβ} (H : UFModel.Agrees arr f m) (i : ) (h₁ : i < Array.size arr) (h₂ : i < n) :
f (Array.get arr { val := i, isLt := h₁ }) = m { val := i, isLt := h₂ }
theorem UFModel.Agrees.get_eq' {α : Type u_1} {β : Sort u_2} {f : αβ} {arr : } {m : Fin (Array.size arr)β} (H : UFModel.Agrees arr f m) (i : Fin (Array.size arr)) :
f (Array.get arr i) = m i
theorem UFModel.Agrees.empty {α : Type u_1} {β : Sort u_2} {f : αβ} {g : Fin 0β} :
theorem UFModel.Agrees.push {α : Type u_1} {β : Sort u_2} {f : αβ} {arr : } {n : } {m : Fin nβ} (H : UFModel.Agrees arr f m) (k : ) (hk : k = n + 1) (x : α) (m' : Fin kβ) (hm₁ : ∀ (i : Fin k) (h : i < n), m' i = m { val := i, isLt := h }) (hm₂ : ∀ (h : n < k), f x = m' { val := n, isLt := h }) :
theorem UFModel.Agrees.set {α : Type u_1} {β : Sort u_2} {f : αβ} {arr : } {n : } {m : Fin nβ} (H : UFModel.Agrees arr f m) {i : Fin (Array.size arr)} {x : α} {m' : Fin nβ} (hm₁ : ∀ (j : Fin n), j im' j = m j) (hm₂ : ∀ (h : i < n), f x = m' { val := i, isLt := h }) :
UFModel.Agrees (Array.set arr i x) f m'
def UFModel.Models {α : Type u_1} (arr : Array ()) {n : } (m : ) :
Equations
theorem UFModel.Models.size_eq {α : Type u_1} {arr : Array ()} {n : } {m : } (H : UFModel.Models arr m) :
theorem UFModel.Models.parent_eq {α : Type u_1} {arr : Array ()} {n : } {m : } (H : UFModel.Models arr m) (i : ) (h₁ : i < Array.size arr) (h₂ : i < n) :
arr[i].parent = ↑(UFModel.parent m { val := i, isLt := h₂ })
theorem UFModel.Models.parent_eq' {α : Type u_1} {arr : Array ()} {m : UFModel (Array.size arr)} (H : UFModel.Models arr m) (i : Fin (Array.size arr)) :
arr[i].parent = ↑()
theorem UFModel.Models.rank_eq {α : Type u_1} {arr : Array ()} {n : } {m : } (H : UFModel.Models arr m) (i : ) (h : i < Array.size arr) :
arr[i].rank =
theorem UFModel.Models.empty {α : Type u_1} :
theorem UFModel.Models.push {α : Type u_1} {arr : Array ()} {n : } {m : } (H : UFModel.Models arr m) (k : ) (hk : k = n + 1) (x : α) :
UFModel.Models (Array.push arr { parent := n, value := x, rank := 0 }) (UFModel.push m k (_ : n k))
theorem UFModel.Models.setParent {α : Type u_1} {arr : Array ()} {n : } {m : } (hm : UFModel.Models arr m) (i : Fin n) (j : Fin n) (H : UFModel.rank m i < UFModel.rank m j) (hi : i < Array.size arr) (x : ) (hp : x.parent = j) (hrk : x.rank = arr[i].rank) :
UFModel.Models (Array.set arr { val := i, isLt := hi } x) ()
structure UnionFind (α : Type u_1) :
Type u_1
Instances For
def UnionFind.size {α : Type u_1} (self : ) :
Equations
theorem UnionFind.model' {α : Type u_1} (self : ) :
m, UFModel.Models self.arr m
def UnionFind.empty {α : Type u_1} :
Equations
• UnionFind.empty = { arr := #[], model := (_ : n m, UFModel.Models #[] m) }
def UnionFind.mkEmpty {α : Type u_1} (c : ) :
Equations
• = { arr := , model := (_ : n m, ) }
def UnionFind.rank {α : Type u_1} (self : ) (i : ) :
Equations
def UnionFind.rankMaxAux {α : Type u_1} (self : ) (i : ) :
{ k // ∀ (j : ), j < i∀ (h : j < Array.size self.arr), (Array.get self.arr { val := j, isLt := h }).rank k }
Equations
• One or more equations did not get rendered due to their size.
• UnionFind.rankMaxAux self 0 = { val := 0, property := (_ : ∀ (a : ), a < 0∀ (a_2 : a < Array.size self.arr), (Array.get self.arr { val := a, isLt := a_2 }).rank 0) }
def UnionFind.rankMax {α : Type u_1} (self : ) :
Equations
theorem UnionFind.lt_rankMax' {α : Type u_1} (self : ) (i : Fin (UnionFind.size self)) :
(Array.get self.arr i).rank <
theorem UnionFind.lt_rankMax {α : Type u_1} (self : ) (i : ) :
theorem UnionFind.rank_eq {α : Type u_1} (self : ) {n : } {m : } (H : UFModel.Models self.arr m) {i : } (h : i < UnionFind.size self) :
theorem UnionFind.rank_lt {α : Type u_1} (self : ) {i : } (h : i < Array.size self.arr) :
self.arr[i].parent iUnionFind.rank self i < UnionFind.rank self self.arr[i].parent
theorem UnionFind.parent_lt {α : Type u_1} (self : ) (i : ) (h : i < Array.size self.arr) :
self.arr[i].parent < UnionFind.size self
def UnionFind.push {α : Type u_1} (self : ) (x : α) :
Equations
• One or more equations did not get rendered due to their size.
def UnionFind.findAux {α : Type u_1} (self : ) (x : Fin (UnionFind.size self)) :
(s : Array ()) ×' (root : Fin ()) ×' n m m', UFModel.Models self.arr m m'.rank = m.rank (hr, ↑(UFModel.parent m' { val := root, isLt := hr }) = root) UFModel.rank m x UFModel.rank m root
Equations
• One or more equations did not get rendered due to their size.
def UnionFind.find {α : Type u_1} (self : ) (x : Fin (UnionFind.size self)) :
(s : ) × (root : ) ×' (Array.get s.arr root).parent = root
Equations
• One or more equations did not get rendered due to their size.
def UnionFind.union {α : Type u_1} (self : ) (x : Fin (UnionFind.size self)) (y : Fin (UnionFind.size self)) :
Equations
• One or more equations did not get rendered due to their size.