Documentation

Mathlib.Data.UnionFind

structure UFModel (n : ) :
  • parent : Fin nFin n
  • rank :
  • rank_lt : ∀ (i : Fin n), ↑(parent i) irank i < rank ↑(parent i)
Instances For
    Equations
    def UFModel.push {n : } (m : UFModel n) (k : ) (le : n 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 : UFModel.rank m x < UFModel.rank m y) :
    Equations
    • One or more equations did not get rendered due to their size.
    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) :
    Equations
    • One or more equations did not get rendered due to their size.
    structure UFNode (α : Type u_1) :
    Type u_1
    • parent :
    • value : α
    • rank :
    Instances For
      inductive UFModel.Agrees {α : Type u_1} {β : Sort u_2} (arr : Array α) (f : αβ) {n : } :
      (Fin nβ) → Prop
      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₂ }) :
        theorem UFModel.Agrees.size_eq {α : Type u_1} {n : } {β : Sort u_2} {f : αβ} {arr : Array α} {m : Fin nβ} (H : UFModel.Agrees arr f m) :
        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₂ }
        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
        theorem UFModel.Agrees.empty {α : Type u_1} {β : Sort u_2} {f : αβ} {g : Fin 0β} :
        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 }) :
        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 im' j = m j) (hm₂ : ∀ (h : i < n), f x = m' { val := i, isLt := h }) :
        UFModel.Agrees (Array.set arr i x) f m'
        def UFModel.Models {α : Type u_1} (arr : Array (UFNode α)) {n : } (m : UFModel n) :
        Equations
        theorem UFModel.Models.size_eq {α : Type u_1} {arr : Array (UFNode α)} {n : } {m : UFModel n} (H : UFModel.Models arr m) :
        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)
        structure UnionFind (α : Type u_1) :
        Type u_1
        Instances For
          def UnionFind.size {α : Type u_1} (self : UnionFind α) :
          Equations
          theorem UnionFind.model' {α : Type u_1} (self : UnionFind α) :
          m, UFModel.Models self.arr m
          def UnionFind.empty {α : Type u_1} :
          Equations
          • UnionFind.empty = { arr := #[], model := (_ : n m, UFModel.Models #[] m) }
          def UnionFind.mkEmpty {α : Type u_1} (c : ) :
          Equations
          def UnionFind.rank {α : Type u_1} (self : UnionFind α) (i : ) :
          Equations
          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) }
          def UnionFind.rankMax {α : Type u_1} (self : UnionFind α) :
          Equations
          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 : ) :
          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) :
          theorem UnionFind.rank_lt {α : Type u_1} (self : UnionFind α) {i : } (h : i < Array.size self.arr) :
          self.arr[i].parent iUnionFind.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.push {α : Type u_1} (self : UnionFind α) (x : α) :
          Equations
          • One or more equations did not get rendered due to their size.
          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.
          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.
          def UnionFind.union {α : Type u_1} (self : UnionFind α) (x : Fin (UnionFind.size self)) (y : Fin (UnionFind.size self)) :
          Equations
          • One or more equations did not get rendered due to their size.