Multisets

[oskgo]

No description provided.

[oskgo]

There is still work to be done (moving helper lemmas to the right theories and cleanup), but I'd like some feedback on the interface.

I provide two interfaces; one through fmaps to positive integers, which more directly models the fundamental multiplicity operator, mult. The other interface goes through lists, since there is a lot of support for equality up to permutation of lists already, but some operators are much more difficult to define with lists than with fmaps, such as diff `|` and `&`.

@fdupress mentioned that you might want to give some feedback, @strub?

One thing that might be possible to improve is the humongous proof of offmap_mult, which glues the two interfaces together.

[fdupress]

@strub , I suggested that Oskar split the contributions to each standard library as a separate file to ease review, but just realised that github's UI does not really help with that. Is it better to split off the stdlib contributions as a separate PR altogether?

Some comments from the offline discussion he and I had:

• This should be defined as a Quotient, but this can't be done because that does not support parametric quotients. (In the same way that the subtype theory does not support subtypes of parametric types.)
• It looked like there could be opportunities to move mset_ind ahead of tofmap and simplify some of the proof, but that now looks wrong.

A couple more comments incoming straight in line.