structure UFModel (n : ℕ) : Type

• parent : Fin n → Fin n
• rank : ℕ → ℕ
• rank_lt : ∀ (i : Fin n), ↑(self.parent i) ≠ ↑i → self.rank ↑i < self.rank ↑(self.parent i)

theorem UFModel.rank_lt {n : ℕ} (self : UFModel n) (i : Fin n) : ↑(self.parent i) ≠ ↑i → self.rank ↑i < self.rank ↑(self.parent i)

def UFModel.empty : UFModel 0

Equations

• UFModel.empty = { parent := fun (i : Fin 0) => i.elim0, rank := fun (x : ℕ) => 0, rank_lt := UFModel.empty.proof_1 }

def UFModel.push {n : ℕ} (m : UFModel n) (k : ℕ) (le : n ≤ k) : UFModel k

Equations

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

def UFModel.setParent {n : ℕ} (m : UFModel n) (x : Fin n) (y : Fin n) (h : m.rank ↑x < m.rank ↑y) : UFModel n

Equations

• m.setParent x y h = { parent := fun (i : Fin n) => if ↑x = ↑i then y else m.parent i, rank := m.rank, rank_lt := ⋯ }

def UFModel.setParentBump {n : ℕ} (m : UFModel n) (x : Fin n) (y : Fin n) (H : m.rank ↑x ≤ m.rank ↑y) (hroot : ↑(m.parent y) = ↑y) : UFModel n

Equations

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

structure UFNode (α : Type u_1) : Type u_1

• parent : ℕ
• value : α
• rank : ℕ

inductive UFModel.Agrees {α : Type u_1} {β : Sort u_2} (arr : Array α) (f : α → β) {n : ℕ} : (Fin n → β) → Prop

• mk: ∀ {α : Type u_1} {β : Sort u_2} {arr : Array α} {f : α → β}, UFModel.Agrees arr f fun (i : Fin arr.size) => f (arr.get i)

theorem UFModel.Agrees.mk' {α : Type u_1} {β : Sort u_2} {arr : Array α} {f : α → β} {n : ℕ} {g : Fin n → β} (e : n = arr.size) (H : ∀ (i : ℕ) (h₁ : i < arr.size) (h₂ : i < n), f (arr.get ⟨i, h₁⟩) = g ⟨i, 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 = arr.size

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 < arr.size) (h₂ : i < n) : f (arr.get ⟨i, h₁⟩) = m ⟨i, h₂⟩

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'

def UFModel.Models {α : Type u_1} (arr : Array (UFNode α)) {n : ℕ} (m : UFModel n) : Prop

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)

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 α)} {n : ℕ} {m : UFModel n} (H : UFModel.Models arr m) (i : ℕ) (h₁ : i < arr.size) (h₂ : i < n) : arr[i].parent = ↑(m.parent ⟨i, h₂⟩)

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.rank_eq {α : Type u_1} {arr : Array (UFNode α)} {n : ℕ} {m : UFModel n} (H : UFModel.Models arr m) (i : ℕ) (h : i < arr.size) : arr[i].rank = m.rank i

theorem UFModel.Models.empty {α : Type u_1} : UFModel.Models #[] UFModel.empty

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)

structure UnionFind (α : Type u_1) : Type u_1

• arr : Array (UFNode α)
• model : ∃ (n : ℕ), ∃ (m : UFModel n), UFModel.Models self.arr m

theorem UnionFind.model {α : Type u_1} (self : UnionFind α) : ∃ (n : ℕ), ∃ (m : UFModel n), UFModel.Models self.arr m

def UnionFind.size {α : Type u_1} (self : UnionFind α) : ℕ

Equations

• self.size = self.arr.size

theorem UnionFind.model' {α : Type u_1} (self : UnionFind α) : ∃ (m : UFModel self.arr.size), UFModel.Models self.arr m

def UnionFind.empty {α : Type u_1} : UnionFind α

Equations

• UnionFind.empty = { arr := #[], model := ⋯ }

def UnionFind.mkEmpty {α : Type u_1} (c : ℕ) : UnionFind α

Equations

• UnionFind.mkEmpty c = { arr := Array.mkEmpty c, model := ⋯ }

def UnionFind.rank {α : Type u_1} (self : UnionFind α) (i : ℕ) : ℕ

Equations

• self.rank i = if h : i < self.size then (self.arr.get ⟨i, h⟩).rank else 0

def UnionFind.rankMaxAux {α : Type u_1} (self : UnionFind α) (i : ℕ) : { k : ℕ // ∀ (j : ℕ), j < i → ∀ (h : j < self.arr.size), (self.arr.get ⟨j, h⟩).rank ≤ k }

Equations

• self.rankMaxAux 0 = ⟨0, ⋯⟩
• self.rankMaxAux i.succ = match self.rankMaxAux i with | ⟨k, H⟩ => ⟨max k (if h : i < self.arr.size then (self.arr.get ⟨i, h⟩).rank else 0), ⋯⟩

def UnionFind.rankMax {α : Type u_1} (self : UnionFind α) : ℕ

Equations

• self.rankMax = (self.rankMaxAux self.size).val + 1

theorem UnionFind.lt_rankMax' {α : Type u_1} (self : UnionFind α) (i : Fin self.size) : (self.arr.get i).rank < self.rankMax

theorem UnionFind.lt_rankMax {α : Type u_1} (self : UnionFind α) (i : ℕ) : self.rank i < self.rankMax

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

theorem UnionFind.rank_lt {α : Type u_1} (self : UnionFind α) {i : ℕ} (h : i < self.arr.size) : self.arr[i].parent ≠ i → self.rank i < self.rank self.arr[i].parent

theorem UnionFind.parent_lt {α : Type u_1} (self : UnionFind α) (i : ℕ) (h : i < self.arr.size) : self.arr[i].parent < self.size

def UnionFind.push {α : Type u_1} (self : UnionFind α) (x : α) : UnionFind α

Equations

• self.push x = { arr := self.arr.push { parent := self.arr.size, value := x, rank := 0 }, model := ⋯ }

@[irreducible]

def UnionFind.findAux {α : Type u_1} (self : UnionFind α) (x : Fin self.size) : (s : Array (UFNode α)) ×' (root : Fin s.size) ×' ∃ (n : ℕ), ∃ (m : UFModel n), ∃ (m' : UFModel n), UFModel.Models self.arr m ∧ UFModel.Models s m' ∧ m'.rank = m.rank ∧ (∃ (hr : ↑root < n), ↑(m'.parent ⟨↑root, hr⟩) = ↑root) ∧ m.rank ↑x ≤ m.rank ↑root

Equations

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

def UnionFind.find {α : Type u_1} (self : UnionFind α) (x : Fin self.size) : (s : UnionFind α) × (root : Fin s.size) ×' s.size = self.size ∧ (s.arr.get root).parent = ↑root

Equations

• self.find x = match self.findAux x with | ⟨s, ⟨root, H⟩⟩ => let_fun this := ⋯; ⟨{ arr := s, model := ⋯ }, ⟨root, ⋯⟩⟩

def UnionFind.link {α : Type u_1} (self : UnionFind α) (x : Fin self.size) (y : Fin self.size) (yroot : (self.arr.get y).parent = ↑y) : UnionFind α

Equations

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

def UnionFind.union {α : Type u_1} (self : UnionFind α) (x : Fin self.size) (y : Fin self.size) : UnionFind α

Equations

• self.union x y = match self.find x with | ⟨self₁, ⟨rx, ⋯⟩⟩ => match self₁.find ⟨↑y, ⋯⟩ with | ⟨self₂, ⟨ry, ⋯⟩⟩ => self₂.link ⟨↑rx, ⋯⟩ ry hry