Documentation

Batteries.Data.UnionFind.Basic

Union-find node type

  • parent : Nat

    Parent of node

  • rank : Nat

    Rank of node

Instances For
    def Batteries.UnionFind.panicWith {α : Type u_1} (v : α) (msg : String) :
    α

    Panic with return value

    Equations
    Instances For
      @[simp]
      theorem Batteries.UnionFind.panicWith_eq {α : Type u_1} (v : α) (msg : String) :

      Parent of a union-find node, defaults to self when the node is a root

      Equations
      Instances For

        Rank of a union-find node, defaults to 0 when the node is a root

        Equations
        Instances For
          theorem Batteries.UnionFind.parentD_eq {arr : Array Batteries.UFNode} {i : Fin arr.size} :
          Batteries.UnionFind.parentD arr i = (arr.get i).parent
          theorem Batteries.UnionFind.parentD_eq' {arr : Array Batteries.UFNode} {i : Nat} (h : i < arr.size) :
          Batteries.UnionFind.parentD arr i = (arr.get i, h).parent
          theorem Batteries.UnionFind.rankD_eq {arr : Array Batteries.UFNode} {i : Fin arr.size} :
          Batteries.UnionFind.rankD arr i = (arr.get i).rank
          theorem Batteries.UnionFind.rankD_eq' {arr : Array Batteries.UFNode} {i : Nat} (h : i < arr.size) :
          Batteries.UnionFind.rankD arr i = (arr.get i, h).rank
          theorem Batteries.UnionFind.parentD_set {arr : Array Batteries.UFNode} {x : Fin arr.size} {v : Batteries.UFNode} {i : Nat} :
          Batteries.UnionFind.parentD (arr.set x v) i = if x = i then v.parent else Batteries.UnionFind.parentD arr i
          theorem Batteries.UnionFind.rankD_set {arr : Array Batteries.UFNode} {x : Fin arr.size} {v : Batteries.UFNode} {i : Nat} :
          Batteries.UnionFind.rankD (arr.set x v) i = if x = i then v.rank else Batteries.UnionFind.rankD arr i

          Union-find data structure #

          The UnionFind structure is an implementation of disjoint-set data structure that uses path compression to make the primary operations run in amortized nearly linear time. The nodes of a UnionFind structure s are natural numbers smaller than s.size. The structure associates with a canonical representative from its equivalence class. The structure can be extended using the push operation and equivalence classes can be updated using the union operation.

          The main operations for UnionFind are:

          • empty/mkEmpty are used to create a new empty structure.
          • size returns the size of the data structure.
          • push adds a new node to a structure, unlinked to any other node.
          • union links two nodes of the data structure, joining their equivalence classes, and performs path compression.
          • find returns the canonical representative of a node and updates the data structure using path compression.
          • root returns the canonical representative of a node without altering the data structure.
          • checkEquiv checks whether two nodes have the same canonical representative and updates the structure using path compression.

          Most use cases should prefer find over root to benefit from the speedup from path-compression.

          The main operations use Fin s.size to represent nodes of the union-find structure. Some alternatives are provided:

          The noncomputable relation UnionFind.Equiv is provided to use the equivalence relation from a UnionFind structure in the context of proofs.

          Instances For
            theorem Batteries.UnionFind.parentD_lt (self : Batteries.UnionFind) {i : Nat} :
            i < self.arr.sizeBatteries.UnionFind.parentD self.arr i < self.arr.size

            Validity for parent nodes

            @[reducible, inline]

            Size of union-find structure.

            Equations
            • self.size = self.arr.size
            Instances For

              Create an empty union-find structure with specific capacity

              Equations
              Instances For
                @[reducible, inline]

                Parent of union-find node

                Equations
                Instances For
                  theorem Batteries.UnionFind.parent'_lt (self : Batteries.UnionFind) (i : Fin self.size) :
                  (self.arr.get i).parent < self.size
                  theorem Batteries.UnionFind.parent_lt (self : Batteries.UnionFind) (i : Nat) :
                  self.parent i < self.size i < self.size
                  @[reducible, inline]

                  Rank of union-find node

                  Equations
                  Instances For
                    theorem Batteries.UnionFind.rank_lt {self : Batteries.UnionFind} {i : Nat} :
                    self.parent i iself.rank i < self.rank (self.parent i)
                    theorem Batteries.UnionFind.rank'_lt (self : Batteries.UnionFind) (i : Fin self.size) :
                    (self.arr.get i).parent iself.rank i < self.rank (self.arr.get i).parent

                    Maximum rank of nodes in a union-find structure

                    Equations
                    Instances For
                      theorem Batteries.UnionFind.rank'_lt_rankMax (self : Batteries.UnionFind) (i : Fin self.size) :
                      (self.arr.get i).rank < self.rankMax
                      theorem Batteries.UnionFind.lt_rankMax (self : Batteries.UnionFind) (i : Nat) :
                      self.rank i < self.rankMax
                      theorem Batteries.UnionFind.push_rankD {i : Nat} (arr : Array Batteries.UFNode) :
                      Batteries.UnionFind.rankD (arr.push { parent := arr.size, rank := 0 }) i = Batteries.UnionFind.rankD arr i
                      theorem Batteries.UnionFind.push_parentD {i : Nat} (arr : Array Batteries.UFNode) :
                      Batteries.UnionFind.parentD (arr.push { parent := arr.size, rank := 0 }) i = Batteries.UnionFind.parentD arr i

                      Add a new node to a union-find structure, unlinked with any other nodes

                      Equations
                      • self.push = { arr := self.arr.push { parent := self.arr.size, rank := 0 }, parentD_lt := , rankD_lt := }
                      Instances For
                        @[irreducible]
                        def Batteries.UnionFind.root (self : Batteries.UnionFind) (x : Fin self.size) :
                        Fin self.size

                        Root of a union-find node.

                        Equations
                        • self.root x = if h : (self.arr.get x).parent = x then x else let_fun this := ; self.root (self.arr.get x).parent,
                        Instances For
                          def Batteries.UnionFind.rootN {n : Nat} (self : Batteries.UnionFind) (x : Fin n) (h : n = self.size) :
                          Fin n

                          Root of a union-find node.

                          Equations
                          • self.rootN x_2 = self.root x_2
                          Instances For

                            Root of a union-find node. Panics if index is out of bounds.

                            Equations
                            Instances For

                              Root of a union-find node. Returns input if index is out of bounds.

                              Equations
                              • self.rootD x = if h : x < self.size then (self.root x, h) else x
                              Instances For
                                @[irreducible]
                                theorem Batteries.UnionFind.parent_root (self : Batteries.UnionFind) (x : Fin self.size) :
                                (self.arr.get (self.root x)).parent = (self.root x)
                                theorem Batteries.UnionFind.parent_rootD (self : Batteries.UnionFind) (x : Nat) :
                                self.parent (self.rootD x) = self.rootD x
                                theorem Batteries.UnionFind.rootD_parent (self : Batteries.UnionFind) (x : Nat) :
                                self.rootD (self.parent x) = self.rootD x
                                theorem Batteries.UnionFind.rootD_lt {self : Batteries.UnionFind} {x : Nat} :
                                self.rootD x < self.size x < self.size
                                theorem Batteries.UnionFind.rootD_eq_self {self : Batteries.UnionFind} {x : Nat} :
                                self.rootD x = x self.parent x = x
                                theorem Batteries.UnionFind.rootD_rootD {self : Batteries.UnionFind} {x : Nat} :
                                self.rootD (self.rootD x) = self.rootD x
                                @[irreducible]
                                theorem Batteries.UnionFind.rootD_ext {m1 : Batteries.UnionFind} {m2 : Batteries.UnionFind} (H : ∀ (x : Nat), m1.parent x = m2.parent x) {x : Nat} :
                                m1.rootD x = m2.rootD x
                                @[irreducible]
                                theorem Batteries.UnionFind.le_rank_root {self : Batteries.UnionFind} {x : Nat} :
                                self.rank x self.rank (self.rootD x)
                                theorem Batteries.UnionFind.lt_rank_root {self : Batteries.UnionFind} {x : Nat} :
                                self.rank x < self.rank (self.rootD x) self.parent x x

                                Auxiliary data structure for find operation

                                Instances For

                                  Size requirement

                                  @[irreducible]

                                  Auxiliary function for find operation

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[irreducible]
                                    theorem Batteries.UnionFind.findAux_root {self : Batteries.UnionFind} {x : Fin self.size} :
                                    (self.findAux x).root = self.root x
                                    theorem Batteries.UnionFind.findAux_s {self : Batteries.UnionFind} {x : Fin self.size} :
                                    (self.findAux x).s = if (self.arr.get x).parent = x then self.arr else (self.findAux (self.arr.get x).parent, ).s.modify x fun (s : Batteries.UFNode) => { parent := self.rootD x, rank := s.rank }
                                    @[irreducible]
                                    theorem Batteries.UnionFind.rankD_findAux {i : Nat} {self : Batteries.UnionFind} {x : Fin self.size} :
                                    Batteries.UnionFind.rankD (self.findAux x).s i = self.rank i
                                    theorem Batteries.UnionFind.parentD_findAux {i : Nat} {self : Batteries.UnionFind} {x : Fin self.size} :
                                    Batteries.UnionFind.parentD (self.findAux x).s i = if i = x then self.rootD x else Batteries.UnionFind.parentD (self.findAux (self.arr.get x).parent, ).s i
                                    @[irreducible]
                                    theorem Batteries.UnionFind.parentD_findAux_rootD {self : Batteries.UnionFind} {x : Fin self.size} :
                                    Batteries.UnionFind.parentD (self.findAux x).s (self.rootD x) = self.rootD x
                                    @[irreducible]
                                    theorem Batteries.UnionFind.parentD_findAux_lt {i : Nat} {self : Batteries.UnionFind} {x : Fin self.size} (h : i < self.size) :
                                    Batteries.UnionFind.parentD (self.findAux x).s i < self.size
                                    @[irreducible]
                                    theorem Batteries.UnionFind.parentD_findAux_or (self : Batteries.UnionFind) (x : Fin self.size) (i : Nat) :
                                    Batteries.UnionFind.parentD (self.findAux x).s i = self.rootD i self.rootD i = self.rootD x Batteries.UnionFind.parentD (self.findAux x).s i = self.parent i
                                    @[irreducible]
                                    theorem Batteries.UnionFind.lt_rankD_findAux {i : Nat} {self : Batteries.UnionFind} {x : Fin self.size} :
                                    Batteries.UnionFind.parentD (self.findAux x).s i iself.rank i < self.rank (Batteries.UnionFind.parentD (self.findAux x).s i)
                                    def Batteries.UnionFind.find (self : Batteries.UnionFind) (x : Fin self.size) :
                                    (s : Batteries.UnionFind) × { _root : Fin s.size // s.size = self.size }

                                    Find root of a union-find node, updating the structure using path compression.

                                    Equations
                                    • self.find x = { arr := (self.findAux x).s, parentD_lt := , rankD_lt := }, (self.findAux x).root, ,
                                    Instances For
                                      def Batteries.UnionFind.findN {n : Nat} (self : Batteries.UnionFind) (x : Fin n) (h : n = self.size) :

                                      Find root of a union-find node, updating the structure using path compression.

                                      Equations
                                      • self.findN x_2 = match self.find x_2 with | s, r, h => (s, Fin.cast h r)
                                      Instances For

                                        Find root of a union-find node, updating the structure using path compression. Panics if index is out of bounds.

                                        Equations
                                        • self.find! x = if h : x < self.size then match self.find x, h with | s, r, property => (s, r) else Batteries.UnionFind.panicWith (self, x) "index out of bounds"
                                        Instances For

                                          Find root of a union-find node, updating the structure using path compression. Returns inputs unchanged when index is out of bounds.

                                          Equations
                                          • self.findD x = if h : x < self.size then match self.find x, h with | s, r, property => (s, r) else (self, x)
                                          Instances For
                                            @[simp]
                                            theorem Batteries.UnionFind.find_size (self : Batteries.UnionFind) (x : Fin self.size) :
                                            (self.find x).fst.size = self.size
                                            @[simp]
                                            theorem Batteries.UnionFind.find_root_2 (self : Batteries.UnionFind) (x : Fin self.size) :
                                            (self.find x).snd.val = self.rootD x
                                            @[simp]
                                            theorem Batteries.UnionFind.find_parent_1 (self : Batteries.UnionFind) (x : Fin self.size) :
                                            (self.find x).fst.parent x = self.rootD x
                                            theorem Batteries.UnionFind.find_parent_or (self : Batteries.UnionFind) (x : Fin self.size) (i : Nat) :
                                            (self.find x).fst.parent i = self.rootD i self.rootD i = self.rootD x (self.find x).fst.parent i = self.parent i
                                            @[simp, irreducible]
                                            theorem Batteries.UnionFind.find_root_1 (self : Batteries.UnionFind) (x : Fin self.size) (i : Nat) :
                                            (self.find x).fst.rootD i = self.rootD i
                                            def Batteries.UnionFind.linkAux (self : Array Batteries.UFNode) (x : Fin self.size) (y : Fin self.size) :

                                            Link two union-find nodes

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem Batteries.UnionFind.setParentBump_rankD_lt {arr' : Array Batteries.UFNode} {arr : Array Batteries.UFNode} {x : Fin arr.size} {y : Fin arr.size} (hroot : (arr.get x).rank < (arr.get y).rank (arr.get y).parent = y) (H : (arr.get x).rank (arr.get y).rank) {i : Nat} (rankD_lt : Batteries.UnionFind.parentD arr i iBatteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i)) (hP : Batteries.UnionFind.parentD arr' i = if x = i then y else Batteries.UnionFind.parentD arr i) (hR : ∀ {i : Nat}, Batteries.UnionFind.rankD arr' i = if y = i (arr.get x).rank = (arr.get y).rank then (arr.get y).rank + 1 else Batteries.UnionFind.rankD arr i) :
                                              theorem Batteries.UnionFind.setParent_rankD_lt {arr : Array Batteries.UFNode} {x : Fin arr.size} {y : Fin arr.size} (h : (arr.get x).rank < (arr.get y).rank) {i : Nat} (rankD_lt : Batteries.UnionFind.parentD arr i iBatteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i)) :
                                              let arr' := arr.set x { parent := y, rank := (arr.get x).rank }; Batteries.UnionFind.parentD arr' i iBatteries.UnionFind.rankD arr' i < Batteries.UnionFind.rankD arr' (Batteries.UnionFind.parentD arr' i)
                                              @[simp]
                                              theorem Batteries.UnionFind.linkAux_size {self : Array Batteries.UFNode} {x : Fin self.size} {y : Fin self.size} :
                                              (Batteries.UnionFind.linkAux self x y).size = self.size
                                              def Batteries.UnionFind.linkN {n : Nat} (self : Batteries.UnionFind) (x : Fin n) (y : Fin n) (yroot : self.parent y = y) (h : n = self.size) :

                                              Link a union-find node to a root node.

                                              Equations
                                              • self.linkN x_2 y_2 yroot_2 = self.link x_2 y_2 yroot_2
                                              Instances For
                                                def Batteries.UnionFind.link! (self : Batteries.UnionFind) (x : Nat) (y : Nat) (yroot : self.parent y = y) :

                                                Link a union-find node to a root node. Panics if either index is out of bounds.

                                                Equations
                                                Instances For
                                                  def Batteries.UnionFind.union (self : Batteries.UnionFind) (x : Fin self.size) (y : Fin self.size) :

                                                  Link two union-find nodes, uniting their respective classes.

                                                  Equations
                                                  • self.union x y = match self.find x with | self₁, rx, ex => let_fun hy := ; match eq : self₁.find y, hy with | self₂, ry, ey => self₂.link rx, ry
                                                  Instances For
                                                    def Batteries.UnionFind.unionN {n : Nat} (self : Batteries.UnionFind) (x : Fin n) (y : Fin n) (h : n = self.size) :

                                                    Link two union-find nodes, uniting their respective classes.

                                                    Equations
                                                    • self.unionN x_2 y_2 = self.union x_2 y_2
                                                    Instances For

                                                      Link two union-find nodes, uniting their respective classes. Panics if either index is out of bounds.

                                                      Equations
                                                      Instances For

                                                        Check whether two union-find nodes are equivalent, updating structure using path compression.

                                                        Equations
                                                        • self.checkEquiv x y = match self.find x with | s, r₁, isLt, h => match s.find (y) with | s_1, r₂, isLt, property => (s_1, r₁ == r₂)
                                                        Instances For
                                                          def Batteries.UnionFind.checkEquivN {n : Nat} (self : Batteries.UnionFind) (x : Fin n) (y : Fin n) (h : n = self.size) :

                                                          Check whether two union-find nodes are equivalent, updating structure using path compression.

                                                          Equations
                                                          • self.checkEquivN x_2 y_2 = self.checkEquiv x_2 y_2
                                                          Instances For

                                                            Check whether two union-find nodes are equivalent, updating structure using path compression. Panics if either index is out of bounds.

                                                            Equations
                                                            Instances For

                                                              Check whether two union-find nodes are equivalent with path compression, returns x == y if either index is out of bounds

                                                              Equations
                                                              • self.checkEquivD x y = match self.findD x with | (s, x) => match s.findD y with | (s, y) => (s, x == y)
                                                              Instances For

                                                                Equivalence relation from a UnionFind structure

                                                                Equations
                                                                • self.Equiv a b = (self.rootD a = self.rootD b)
                                                                Instances For