Kruskal's Algorithm & DSU

Stream: batteries

[Ayush Priyadarshi]

I was trying to implement(not prove) the Kruskal's algorithm using DSU
I found UnionFind in batteries
I am not sure how to evaluate the find function given an array and an index.

/-- Find root of a union-find node, updating the structure using path compression. -/
def find (self : UnionFind) (x : Fin self.size) :
    (s : UnionFind) × {_root : Fin s.size // s.size = self.size} :=
  let r := self.findAux x
  { 1.arr := r.s
    2.1.val := r.root
    1.parentD_lt := fun h => by
      simp only [Array.length_toList, FindAux.size_eq] at *
      exact parentD_findAux_lt h
    1.rankD_lt := fun h => by rw [rankD_findAux, rankD_findAux]; exact lt_rankD_findAux h
    2.1.isLt := show _ < r.s.size by rw [r.size_eq]; exact r.root.2
    2.2 := by simp [size, r.size_eq] }

Below is how I evaluated the parentD function

def exampleUF : Array Batteries.UFNode :=
  Array.mk [⟨0, 1⟩, ⟨0, 0⟩, ⟨2, 1⟩, ⟨2, 0⟩]

#eval Batteries.UnionFind.parentD UnionFind.exampleUF 0  -- → 0

Also how does it check whether the array i gave satisfies the properties of UFNode

[Mario Carneiro]

The intended use of UnionFind is to use the functions on it (empty, push, union, find) to create elements of the type; these functions preserve the UFNode properties, as proved in the UnionFind.Basic and UnionFind.Lemmas files.

[Mario Carneiro]

You shouldn't construct a UnionFind object directly from an array unless you feel like proving the invariant yourself

[Mario Carneiro]

It is possible to decide the invariant but no decision procedure was provided because that's not the intended use case