Equivalence classes of a multiset

Stream: Is there code for X?

[Jesse Slater]

I am trying to break a multiset into a multiset (or finset) of multisets by an equivalence relation on elements.

def Multiset.classes
  (m : Multiset α) (op : α → α → Prop) (equiv : Equivalence op)
  : Multiset (Multiset α) := _

[Matt Diamond]

This could work, but I wouldn't be surprised if there's a better way:

import Mathlib.Data.Multiset.Powerset
import Mathlib.Data.Finset.Basic

def Multiset.classes {α : Type*} [DecidableEq α]
  (m : Multiset α) (op : α → α → Prop) [DecidableRel op] : Finset (Multiset α) :=
(m.powerset.filter (fun a => ∀ x ∈ a, ∀ y ∈ m, y ∈ a ↔ op x y)).toFinset

[Matt Diamond]

the proof of Equivalence op isn't needed for the definition of Multiset.classes but would be used to prove things about the result

[Jesse Slater]

I came up with this:

def Multiset.classes
  (m : Multiset α) (eq : α → α → Prop)
  [DecidableRel eq] [DecidableEq α] :=
  let x := m.powerset
  |>.filter (λ p => ∀ a ∈ p, ∀ b ∈ p, eq a b)
  x.filter (λ p => ∀ q ∈ x, p ≤ q → p = q)

[Jesse Slater]

I have to do a second filter to get rid of subsets, since I want the join of set of classes to be the original set

[Antoine Chambert-Loir]

This definition works, but if you had to compute that set, it would be inefficient: if the multiset m has nelements, you start by sifting out of its powerset, which has 2 ^ n elements.

[Eric Wieser]

I think it might be better to write the naive algorithm on List and show that when the relation is symmetric and transitive it is permutation invariant

[Eric Wieser]

Though I guess you could also use (m.map (Quot.mk r)).toFinset.map ⟨fun q => m.filter (Quot.mk . = q), sorry⟩ or similar