Variant of FMap where get samples randomly

[chdoc]

This is a theory I created for the CV2EC project. It is still quite drafty, but I would be happy to get some feedback.

In particular I would be interested to hear what people think of the overloading of membership (e.g. x \in m and (x,y) \in m)

[fdupress]

I have trouble seeing how this is used. Is this meant to capture CV's find semantics?

I have absolutely no objection to the \in notation—entirely appropriate for a relation. But perhaps opting for a canonical variable name that better reflects the relational (rather than map-like) nature of the mathematical object would be better?

Also, it might be worth having operators that inject maps as relations and projects relations as sets of maps?
These may be useful, for example, when relating one game that uses a proper map to a game that uses a relational map. (Only build those if you see a use case.)

[chdoc]

I have trouble seeing how this is used. Is this meant to capture CV's find semantics?

Indeed, this was I developed to convert a proof that was carried out using fmap to one that captures CV's find semantics. The goal was to stay as compatible as possible too fmap, regarding both the syntax of programs and the names of lemmas.

I have absolutely no objection to the \in notation—entirely appropriate for a relation.

The point is more that lemmas use both the newly defined \in notation as well as the \in notation for lists inherited from the implementation of the rmap type.

[strub]

This PR is still marked as "draft". What should we do with it?

[fdupress]

Is it used anywhere? If yes, and that somewhere is currently maintained, we should probably have at least one release with it. If no, I still do not understand what it does (or if what it does is something we want) and am not willing to push it forward.

[strub]

Hi @chdoc. The theory seems to be pretty ad-hoc and bound to CV2EC. Not sure whether we should integrate it in the standard library.

[chdoc]

I found it useful when dealing with the sampling semantics of CV. So yes, in that respect it is ad-hoc and bound to CV. If you don't think this is generally useful, feel free to close this.

[strub]

Let's keep it in the cv2ec repo. Thank you.