Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm

Lukas Stevens, Rebecca Ghidini

Using Isabelle/HOL, we verify a union-find data structure with an explain operation due to Nieuwenhuis and Oliveras. We devise a simpler, more naive version of the explain operatio…