ink

structure UFModel (n : ℕ) : Type

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

ink

def UFModel.empty : UFModel 0

Equations

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

ink

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.

ink

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

Equations

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

ink

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

Equations

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

ink

structure UFNode (α : Type u_1) : Type u_1

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

ink

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 => f (Array.get arr i)

ink

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

ink

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

ink

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) : f (Array.get arr { val := i, isLt := h₁ }) = m { val := i, isLt := h₂ }

ink

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)) : f (Array.get arr i) = m i

ink

theorem UFModel.Agrees.empty {α : Type u_1} {β : Sort u_2} {f : α → β} {g : Fin 0 → β} : UFModel.Agrees #[] f g

ink

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'

ink

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'

ink

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

Equations

• UFModel.Models arr m = ((UFModel.Agrees arr (fun x => x.parent) fun i => ↑(UFModel.parent m i)) ∧ UFModel.Agrees arr (fun x => x.rank) fun i => UFModel.rank m ↑i)

ink

theorem UFModel.Models.size_eq {α : Type u_1} {arr : Array (UFNode α)} {n : ℕ} {m : UFModel n} (H : UFModel.Models arr m) : n = Array.size arr

ink

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₂ })

ink

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)

ink

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

ink

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

ink

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))

ink

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)

ink

structure UnionFind (α : Type u_1) : Type u_1

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

ink

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

Equations

• UnionFind.size self = Array.size self.arr

ink

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

ink

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

Equations

• UnionFind.empty = { arr := #[], model := (_ : ∃ n m, UFModel.Models #[] m) }

ink

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

Equations

• UnionFind.mkEmpty c = { arr := Array.mkEmpty c, model := (_ : ∃ n m, UFModel.Models (Array.mkEmpty c) m) }

ink

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

Equations

• UnionFind.rank self i = if h : i < UnionFind.size self then (Array.get self.arr { val := i, isLt := h }).rank else 0

ink

def UnionFind.rankMaxAux {α : Type u_1} (self : UnionFind α) (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) }

ink

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

Equations

• UnionFind.rankMax self = ↑(UnionFind.rankMaxAux self (UnionFind.size self)) + 1

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

Equations

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

ink

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.

ink

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

Equations

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

ink

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) : UnionFind α

Equations

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

ink

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

Equations

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