Multiset set notation

This MR adds a notation {[ x1 ;+ .. ;+ xn ]} for {{ x1 ]} ⊎ .. ⊎ {{ xn ]}.

Todo:

• bikeshed about notation
• port tests in !231 (merged) to new notation

Fixes #100 (closed)

This fixes #100 (closed)

I added that to the MR description so GitLab picks it up.

changed the description

It also removes weird notations {[ x1, x2 ]} for {[ (x1,x2) ]} that date back to the time we used the singleton class with a product for maps (there's now singletonM).

That sounds like a potentially breaking change that I'd prefer to land separately.

In terms of the new notation, I guess the obvious alternative would be ⊎{[ x1 ; .. x2 ]}. Though there is some risk that this is interpreted as doing a union of the xs instead of doing a union of singletons.

That sounds like a potentially breaking change that I'd prefer to land separately.

I can split up this MR

In terms of the new notation, I guess the obvious alternative would be ⊎{[ x1 ; .. x2 ]}. Though there is some risk that this is interpreted as doing a union of the xs instead of doing a union of singletons.

I don't like that, because with the space after the ⊎, it has a very different meaning. Also terms like X ⊎ ⊎{[ x1; x2 ]} look like typos :)

I can split up this MR

That would be good.

To continue the bikeshed (not because I dislike your proposal but just to explore the design space a bit), what about changing the ; instead? e.g. {[ x1 ;+ .. ;+ x2 ]}.

I quite like that suggestion! That also avoids the issue that if we ever overload + we don't end up with weird stuff like X + +{[ x1 ; x2 ]}

added 3 commits

• 877b0f4a...6d001c9d - 2 commits from branch master
• 8c7aff83 - Add notation for `singleton` with `disj_union`.

Compare with previous version

changed the description

Btw, the MR title seems wrong? This is not a singleton notation, it is a set literal notation.

changed title from Multiset singleton notation to Multiset set notation

added 16 commits

• 8c7aff83...dd04c27a - 13 commits from branch master
• 6e1f9a26 - Add notation for `singleton` with `disj_union`.
• 5d8dd980 - Ralf's suggested singleton notation.
• 3165a4c5 - Use new set notation for multisets in tests.

Compare with previous version

I updated this MR using Ralf's suggested notation, which I do too like better.

I also use the notation in the tests.

changed the description

marked the checklist item bikeshed about notation as completed

marked the checklist item port tests in !231 (merged) to new notation as completed

Would ;+; be better? (Not sure, just throwing it out there.)

That's yet another option...

I am not sure. It's more symmetric, but it's one keystroke more.

What are your thoughts?

I don't have a strong opinion either way -- "more symmetric, but it's one keystroke more", as you said. ;)

What about doing a quick poll on Mattermost so solicit feedback?

We asked on Mattermost, and the opinions were:

• @lepigre Use {[+ x1 ; .. ; xn +]}.
• @robbertkrebbers: Problem: what about the singleton, then there's both {[ x ]} and {[+ x +]} which parse to the same term, namely singleton x. Pretty printing will then always give {[ x ]}.
• @lepigre / @Blaisorblade: Use special type class for multiset singleton.

We already have SingletonM for maps, so we could have SingletonMS for sets. Then there would be no longer a Singleton instance for multisets, making {[ x1; ...; xn ]} on multisets no longer type check.

Not having Singleton for multisets, also has the consequence that we can no longer have Set_ instances for multisets, which "fixes" #98 (closed) and #87 (closed).

Not having Singleton for multisets, also has the consequence that we can no longer have Set_ instances for multisets, which "fixes" #98 (closed) and #87 (closed).

It certainly doesn't fix #98 (closed) since we'd still not have a lemma for x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y... that issue says that currently Set_ is already not satisfied for multisets so in fact I am confused by your statement saying "no longer".

making {[ x1; ...; xn ]} on multisets no longer type check

That sounds good, actually -- it prevents people from accidentally using the wrong notation.

It certainly doesn't fix #98 (closed) since we'd still not have a lemma for x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y... that issue says that currently Set_ is already not satisfied for multisets so in fact I am confused by your statement saying "no longer".

Oh, I meant no longer have SemiSet. This "fixes" it in the way that we consistently have no overloaded set lemmas for multisets. This might be a good thing, since the ones from sets give you the wrong ⊆ (if that appears in the statement).

It also means we need to have multiset copies of all of these lemmas.

I don't think that's a big problem. The majority of the lemmas in sets.v have to do with set inclusion (⊆, ⊂) or set equality (≡), both of which are the wrong notion for multisets (#87 (closed)). There aren't that many lemmas that just involve ∈, especially if you exclude those that involve ∩ or ∖, which currently do not work for multisets either (#98 (closed)).

Fair.