Equiv instance for multisets

The default Equiv instance for multiset is a bit strange. I would expect it to coincide with (extensional) equality, but it is actually equality of the underlying sets, due to the collection_equiv instance.

Because of this I had to employ somewhat of a hack for defining RA structure on gmultiset.

closed via commit 42a87a40

Fixed, thanks for the report.

I have to say I am not too happy about the "default" Equiv instances for maps and collections, that you just get whenever you have a Lookup or ElemOf respectively.

However, by lack of alternative, and since it's not really an issue, I decided not to care.

Oh, and when you are done with it, please make an Iris MR for the multiset RA :).

However, by lack of alternative, and since it's not really an issue, I decided not to care.

Fair enough :)

Oh, and when you are done with it, please make an Iris MR for the multiset RA :).

So, what do you think of this Local Instance way of forcing Leibniz equality?

Just to be clear, https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/commit/42a87a40bf9da5794bbde639943aaf1fc2c979c7 fixed this issue.

The thing I still not like is that there are overlapping Equiv instances for some types. E.g. for gmultiset there is the one that's introduced in https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/commit/42a87a40bf9da5794bbde639943aaf1fc2c979c7, and the "default" one. By means of priorities we do get the proper one, but in other cases, it may lead to unnecessary backtracking.