Documentation

Batteries.Data.UnionFind.Lemmas

@[simp]
theorem Batteries.UnionFind.arr_push {m : Batteries.UnionFind} :
m.push.arr = m.arr.push { parent := m.arr.size, rank := 0 }
@[simp]
theorem Batteries.UnionFind.parentD_push {a : Nat} {arr : Array Batteries.UFNode} :
Batteries.UnionFind.parentD (arr.push { parent := arr.size, rank := 0 }) a = Batteries.UnionFind.parentD arr a
@[simp]
theorem Batteries.UnionFind.parent_push {a : Nat} {m : Batteries.UnionFind} :
m.push.parent a = m.parent a
@[simp]
theorem Batteries.UnionFind.rankD_push {a : Nat} {arr : Array Batteries.UFNode} :
Batteries.UnionFind.rankD (arr.push { parent := arr.size, rank := 0 }) a = Batteries.UnionFind.rankD arr a
@[simp]
theorem Batteries.UnionFind.rank_push {a : Nat} {m : Batteries.UnionFind} :
m.push.rank a = m.rank a
@[simp]
theorem Batteries.UnionFind.rankMax_push {m : Batteries.UnionFind} :
m.push.rankMax = m.rankMax
@[simp]
theorem Batteries.UnionFind.root_push {x : Nat} {self : Batteries.UnionFind} :
self.push.rootD x = self.rootD x
theorem Batteries.UnionFind.parentD_linkAux {i : Nat} {self : Array Batteries.UFNode} {x : Fin self.size} {y : Fin self.size} :
Batteries.UnionFind.parentD (Batteries.UnionFind.linkAux self x y) i = if x = y then Batteries.UnionFind.parentD self i else if (self.get y).rank < (self.get x).rank then if y = i then x else Batteries.UnionFind.parentD self i else if x = i then y else Batteries.UnionFind.parentD self i
@[irreducible]
theorem Batteries.UnionFind.root_link.go {self : Batteries.UnionFind} {x : Fin self.size} {y : Fin self.size} (xroot : self.parent x = x) (yroot : self.parent y = y) {m : Batteries.UnionFind} (hm : ∀ (i : Nat), m.parent i = if y = i then x else self.parent i) (i : Nat) :
m.rootD i = if self.rootD i = x self.rootD i = y then x else self.rootD i
theorem Batteries.UnionFind.Equiv.rfl {self : Batteries.UnionFind} {a : Nat} :
self.Equiv a a
theorem Batteries.UnionFind.Equiv.symm {self : Batteries.UnionFind} {a : Nat} {b : Nat} :
self.Equiv a bself.Equiv b a
theorem Batteries.UnionFind.Equiv.trans {self : Batteries.UnionFind} {a : Nat} {b : Nat} {c : Nat} :
self.Equiv a bself.Equiv b cself.Equiv a c
@[simp]
@[simp]
theorem Batteries.UnionFind.equiv_push {a : Nat} {b : Nat} {self : Batteries.UnionFind} :
self.push.Equiv a b self.Equiv a b
@[simp]
theorem Batteries.UnionFind.equiv_rootD {self : Batteries.UnionFind} {a : Nat} :
self.Equiv (self.rootD a) a
@[simp]
theorem Batteries.UnionFind.equiv_rootD_l {self : Batteries.UnionFind} {a : Nat} {b : Nat} :
self.Equiv (self.rootD a) b self.Equiv a b
@[simp]
theorem Batteries.UnionFind.equiv_rootD_r {self : Batteries.UnionFind} {a : Nat} {b : Nat} :
self.Equiv a (self.rootD b) self.Equiv a b
theorem Batteries.UnionFind.equiv_find {a : Nat} {b : Nat} {self : Batteries.UnionFind} {x : Fin self.size} :
(self.find x).fst.Equiv a b self.Equiv a b
theorem Batteries.UnionFind.equiv_union {a : Nat} {b : Nat} {self : Batteries.UnionFind} {x : Fin self.size} {y : Fin self.size} :
(self.union x y).Equiv a b self.Equiv a b self.Equiv a x self.Equiv (↑y) b self.Equiv a y self.Equiv (↑x) b