Documentation

Mathlib.Data.UnionFind

structure UFModel (n : ) :
  • parent : Fin nFin n
  • rank :
  • rank_lt : ∀ (i : Fin n), (self.parent i) iself.rank i < self.rank (self.parent i)
Instances For
    Equations
    Instances For
      def UFModel.push {n : } (m : UFModel n) (k : ) (le : n k) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def UFModel.setParent {n : } (m : UFModel n) (x : Fin n) (y : Fin n) (h : m.rank x < m.rank y) :
        Equations
        • UFModel.setParent m x y h = { parent := fun (i : Fin n) => if x = i then y else m.parent i, rank := m.rank, rank_lt := }
        Instances For
          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) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            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
                • One or more equations did not get rendered due to their size.
                Instances For
                  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 = (m.parent { 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 = (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 < Array.size arr) :
                  arr[i].rank = m.rank 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 )
                  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 < 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
                    Instances For
                      theorem UnionFind.model' {α : Type u_1} (self : UnionFind α) :
                      ∃ (m : UFModel (Array.size self.arr)), UFModel.Models self.arr m
                      def UnionFind.empty {α : Type u_1} :
                      Equations
                      • UnionFind.empty = { arr := #[], model := }
                      Instances For
                        def UnionFind.mkEmpty {α : Type u_1} (c : ) :
                        Equations
                        Instances For
                          def UnionFind.rank {α : Type u_1} (self : UnionFind α) (i : ) :
                          Equations
                          Instances For
                            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 := }
                            Instances For
                              def UnionFind.rankMax {α : Type u_1} (self : UnionFind α) :
                              Equations
                              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 : ) :
                                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 = m.rank i
                                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
                                Instances For
                                  def UnionFind.findAux {α : Type u_1} (self : UnionFind α) (x : Fin (UnionFind.size self)) :
                                  (s : Array (UFNode α)) ×' (root : Fin (Array.size s)) ×' ∃ (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 { val := root, isLt := hr }) = root) m.rank x m.rank 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
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      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.
                                      Instances For