Equations
- UFModel.empty = { parent := fun (i : Fin 0) => i.elim0, rank := fun (x : ℕ) => 0, rank_lt := UFModel.empty.proof_1 }
Instances For
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 = arr.size
theorem
UFModel.Agrees.get_eq'
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{arr : Array α}
{m : Fin arr.size → β}
(H : UFModel.Agrees arr f m)
(i : Fin arr.size)
:
f (arr.get i) = m i
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 ⟨↑i, h⟩)
(hm₂ : ∀ (h : n < k), f x = m' ⟨n, h⟩)
:
UFModel.Agrees (arr.push 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 arr.size}
{x : α}
{m' : Fin n → β}
(hm₁ : ∀ (j : Fin n), ↑j ≠ ↑i → m' j = m j)
(hm₂ : ∀ (h : ↑i < n), f x = m' ⟨↑i, h⟩)
:
UFModel.Agrees (arr.set i x) f m'
Equations
- UFModel.Models arr m = ((UFModel.Agrees arr (fun (x : UFNode α) => x.parent) fun (i : Fin n) => ↑(m.parent i)) ∧ UFModel.Agrees arr (fun (x : UFNode α) => x.rank) fun (i : Fin n) => m.rank ↑i)
Instances For
theorem
UFModel.Models.size_eq
{α : Type u_1}
{arr : Array (UFNode α)}
{n : ℕ}
{m : UFModel n}
(H : UFModel.Models arr m)
:
n = arr.size
theorem
UFModel.Models.parent_eq'
{α : Type u_1}
{arr : Array (UFNode α)}
{m : UFModel arr.size}
(H : UFModel.Models arr m)
(i : Fin arr.size)
:
arr[↑i].parent = ↑(m.parent 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 (arr.push { parent := n, value := x, rank := 0 }) (m.push 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 : m.rank ↑i < m.rank ↑j)
(hi : ↑i < arr.size)
(x : UFNode α)
(hp : x.parent = ↑j)
(hrk : x.rank = arr[i].rank)
:
UFModel.Models (arr.set ⟨↑i, hi⟩ x) (m.setParent i j H)
theorem
UnionFind.model
{α : Type u_1}
(self : UnionFind α)
:
∃ (n : ℕ), ∃ (m : UFModel n), UFModel.Models self.arr m
theorem
UnionFind.model'
{α : Type u_1}
(self : UnionFind α)
:
∃ (m : UFModel self.arr.size), UFModel.Models self.arr m
Equations
- UnionFind.empty = { arr := #[], model := ⋯ }
Instances For
Equations
- UnionFind.mkEmpty c = { arr := Array.mkEmpty c, model := ⋯ }
Instances For
theorem
UnionFind.rank_eq
{α : Type u_1}
(self : UnionFind α)
{n : ℕ}
{m : UFModel n}
(H : UFModel.Models self.arr m)
{i : ℕ}
(h : i < self.size)
:
self.rank i = m.rank i
@[irreducible]
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- self.find x = match self.findAux x with | ⟨s, ⟨root, H⟩⟩ => let_fun this := ⋯; ⟨{ arr := s, model := ⋯ }, ⟨root, ⋯⟩⟩