dfinsupp vs finsupp implementation

Stream: general

[Eric Wieser]

Does anyone know why dfinsupp is implemented as a quotient over a struct with a multiset but finsupp uses a finset? Did they originally use the same implementation at some point in the past? It would be great to capture the reason in an "implementation notes" section

[Chris Hughes]

Nothing more than the tastes of the people who defined them I think. It shouldn't make much difference because the implementation should be invisible. They never used the same implementation, finsupp came first and had to be generalised.

[Yury G. Kudryashov]

With the quotient you don't need decidable_eq in many cases.

[Yury G. Kudryashov]

BTW, it is possible to define dfinsupp without any finsets as the quotient of free_add_monoid (Σ i, β i) by the docs#add_con Inf {c | (∀ (i : α) (b₁ b₂ : β i), c [⟨i, b₁⟩, ⟨i, b₂⟩] [⟨i, b₁ + b₂⟩]) ∧ ∀ i, c [⟨i, 0⟩] 0}

[Yury G. Kudryashov]

This way we get the universal property for free.

[Eric Wieser]

Right, I thought this might be motivated by decidable equality

[Eric Wieser]

I added some implementation notes about this in #15554 (although the definition has changed slightly since this thread was created)