Partial labeled partition / Disjoint set map

Stream: Is there code for X?

[aron]

Hi :wave: I've been working on a data structure that I've found useful called DisjointSetMap, and I'm curious whether a) something like this already exists in Mathlib, and b) whether it would be a welcome contribution.

What it is: A DisjointSetMap k v is a finite collection of pairwise-disjoint nonempty Finset ks, each associated with a value of type v. Mathematically, it's a partial labeled partition: a partition of some finite subset of k where each equivalence class carries a label. Lookup is by element — given key : k, the map finds which partition contains key and returns the associated value.

How it relates to existing Mathlib structures:

• Finpartition partitions a specific finset with no values attached. This structure is a partial partition (doesn't need to cover a fixed set) and each part carries a value.
• AList/Finmap map individual keys to values. This maps sets of keys to shared values, with a disjointness invariant.
• IndexedPartition works with Set, not Finset, and has no separate value type.

API surface:

• empty, singleton, support, lookup, lookupPart
• insert (fresh singleton key), erase (remove entire partition containing a key)
• mapValues (apply a function to all values)
• insertMerging — the distinctive operation: insert a set of keys with a value, automatically merging with any overlapping existing partitions

Implementation: List-based (like AList), could be lifted to Multiset for extensional equality (like Finmap).

Full source: https://gist.github.com/Arrow7000/821b13c0bffe119cd13025610469a554

I'd appreciate any feedback on:

1. Does this already exist somewhere I haven't looked?
2. Would this be in scope for Mathlib? (I realize it's somewhat CS-flavored, but so are AList and Finmap.)
3. If so, any suggestions on naming? "Disjoint set map" is the CS name; mathematically it's probably closer to a "partial labeled partition" or "valued partial partition"?

Thanks :folded_hands:

[Kim Morrison]

Does it have a mathematical application? From what you've said so far I don't see it being in scope for Mathlib.

[aron]

Ok that makes sense. What about the stdlib? Possibly in a similar place to HashSet or HashMap?

It's sort of in an in-between place because it's not really a mathematical data structure, it's more geared towards programming. But unlike HashSet and HashMap it's not written for runtime efficiency but for ease of proving. Similarly to e.g. ALists. Is there a place for such data structures in the stdlib?

[Kim Morrison]

Is there any application?

[aron]

Well yeah it's a useful data structure
https://en.wikipedia.org/wiki/Disjoint-set_data_structure

[Bryan Gin-ge Chen]

I have not looked at your code yet, but based on your wiki link I think docs#Batteries.UnionFind might be related.