- rank_lt : ∀ (i : Fin n), ↑(UFModel.parent s i) ≠ ↑i → UFModel.rank s ↑i < UFModel.rank s ↑(UFModel.parent s i)
Instances For
def
UFModel.setParent
{n : ℕ}
(m : UFModel n)
(x : Fin n)
(y : Fin n)
(h : UFModel.rank m ↑x < UFModel.rank m ↑y)
:
UFModel n
Instances For
def
UFModel.setParentBump
{n : ℕ}
(m : UFModel n)
(x : Fin n)
(y : Fin n)
(H : UFModel.rank m ↑x ≤ UFModel.rank m ↑y)
(hroot : ↑(UFModel.parent m y) = ↑y)
:
UFModel n
Instances For
theorem
UFModel.Agrees.mk'
{α : Type u_1}
{β : Sort u_2}
{arr : Array α}
{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₂ })
:
UFModel.Agrees arr f g
theorem
UFModel.Agrees.size_eq
{α : Type u_1}
{n : ℕ}
{β : Sort u_2}
{f : α → β}
{arr : Array α}
{m : Fin n → β}
(H : UFModel.Agrees arr f m)
:
n = Array.size arr
theorem
UFModel.Agrees.get_eq
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{arr : Array α}
{n : ℕ}
{m : Fin n → β}
(H : UFModel.Agrees arr f m)
(i : ℕ)
(h₁ : i < Array.size arr)
(h₂ : i < n)
:
theorem
UFModel.Agrees.get_eq'
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{arr : Array α}
{m : Fin (Array.size arr) → β}
(H : UFModel.Agrees arr f m)
(i : Fin (Array.size arr))
:
theorem
UFModel.Agrees.empty
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{g : Fin 0 → β}
:
UFModel.Agrees #[] f g
theorem
UFModel.Agrees.push
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{arr : Array α}
{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 })
:
UFModel.Agrees (Array.push arr x) f m'
theorem
UFModel.Agrees.set
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{arr : Array α}
{n : ℕ}
{m : Fin n → β}
(H : UFModel.Agrees arr f m)
{i : Fin (Array.size arr)}
{x : α}
{m' : Fin n → β}
(hm₁ : ∀ (j : Fin n), ↑j ≠ ↑i → m' j = m j)
(hm₂ : ∀ (h : ↑i < n), f x = m' { val := ↑i, isLt := h })
:
UFModel.Agrees (Array.set arr i x) f m'
theorem
UFModel.Models.size_eq
{α : Type u_1}
{arr : Array (UFNode α)}
{n : ℕ}
{m : UFModel n}
(H : UFModel.Models arr m)
:
n = Array.size arr
theorem
UFModel.Models.parent_eq
{α : Type u_1}
{arr : Array (UFNode α)}
{n : ℕ}
{m : UFModel n}
(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 (UFNode α)}
{m : UFModel (Array.size arr)}
(H : UFModel.Models arr m)
(i : Fin (Array.size arr))
:
arr[↑i].parent = ↑(UFModel.parent m i)
theorem
UFModel.Models.rank_eq
{α : Type u_1}
{arr : Array (UFNode α)}
{n : ℕ}
{m : UFModel n}
(H : UFModel.Models arr m)
(i : ℕ)
(h : i < Array.size arr)
:
arr[i].rank = UFModel.rank m i
theorem
UFModel.Models.push
{α : Type u_1}
{arr : Array (UFNode α)}
{n : ℕ}
{m : UFModel n}
(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 (UFNode α)}
{n : ℕ}
{m : UFModel n}
(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 : UFNode α)
(hp : x.parent = ↑j)
(hrk : x.rank = arr[i].rank)
:
UFModel.Models (Array.set arr { val := ↑i, isLt := hi } x) (UFModel.setParent m i j H)
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) }
Instances For
theorem
UnionFind.lt_rankMax'
{α : Type u_1}
(self : UnionFind α)
(i : Fin (UnionFind.size self))
:
(Array.get self.arr i).rank < UnionFind.rankMax self
theorem
UnionFind.lt_rankMax
{α : Type u_1}
(self : UnionFind α)
(i : ℕ)
:
UnionFind.rank self i < UnionFind.rankMax self
theorem
UnionFind.rank_eq
{α : Type u_1}
(self : UnionFind α)
{n : ℕ}
{m : UFModel n}
(H : UFModel.Models self.arr m)
{i : ℕ}
(h : i < UnionFind.size self)
:
UnionFind.rank self i = UFModel.rank m i
theorem
UnionFind.rank_lt
{α : Type u_1}
(self : UnionFind α)
{i : ℕ}
(h : i < Array.size self.arr)
:
self.arr[i].parent ≠ i → UnionFind.rank self i < UnionFind.rank self self.arr[i].parent
theorem
UnionFind.parent_lt
{α : Type u_1}
(self : UnionFind α)
(i : ℕ)
(h : i < Array.size self.arr)
:
self.arr[i].parent < UnionFind.size self
def
UnionFind.findAux
{α : Type u_1}
(self : UnionFind α)
(x : Fin (UnionFind.size self))
:
(s : Array (UFNode α)) ×'
(root : Fin (Array.size s)) ×'
∃ n m m',
UFModel.Models self.arr m ∧ UFModel.Models s 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.
Instances For
def
UnionFind.find
{α : Type u_1}
(self : UnionFind α)
(x : Fin (UnionFind.size self))
:
(s : UnionFind α) ×
(root : Fin (UnionFind.size s)) ×' UnionFind.size s = UnionFind.size self ∧ (Array.get s.arr root).parent = ↑root
Instances For
def
UnionFind.link
{α : Type u_1}
(self : UnionFind α)
(x : Fin (UnionFind.size self))
(y : Fin (UnionFind.size self))
(yroot : (Array.get self.arr y).parent = ↑y)
:
Instances For
def
UnionFind.union
{α : Type u_1}
(self : UnionFind α)
(x : Fin (UnionFind.size self))
(y : Fin (UnionFind.size self))
: