Add set_omap to finite sets

Add omap-like function to finite sets, aka OCaml's filter_map operation.

I needed it to destruct a set of X + Y into a set of X and a set of Y.

Also add a few lemmas to reason about it.

changed the description

added 7 commits

• 12cc431c...0727c134 - 6 commits from branch iris:master
• accdd9ca - Merge branch 'master' into 'dorian/set_omap'

Compare with previous version

General question first: For your use case, you could also use set_bind cannot you?

The omap operation might be more convenient and this sounds like a useful MR.

Could we add a correspondence with mbind?

added 2 commits

• 466ffc8a - Add set_omap operation
• d9cd96a0 - CHANGELOG

Compare with previous version

added 1 commit

• 6f94a9dc - Minor tweaks.

Compare with previous version

I pushed some minor improvements, this MR looks good.

Please add the correspondence with mbind.

Also feel free to add (by YOURNAME) in the CHANGELOG so you receive the deserved credit :).

added 30 commits

• 6f94a9dc...32e33c9d - 25 commits from branch iris:master
• fa42a517 - Add set_omap operation
• d3f5750c - CHANGELOG
• dc113e38 - Minor tweaks.
• 83c2e50b - Compatibility with bind and map
• a1c6eb22 - Add name to CHANGELOG

Compare with previous version

added 1 commit

• 4578c166 - Add set_omap_filter

Compare with previous version

resolved all threads

added 1 commit

• 8a9095bb - Styling

Compare with previous version

added 2 commits

• 7994e7ce - Weaken `set_bind` lemmas to require `Set_` instead of `FinSet` for the resulting set.
• 4b826234 - More tweaks.

Compare with previous version

added 5 commits

• 69cbd5f4 - Add name to CHANGELOG
• 6c2e853c - Add set_omap_filter
• 8f0e1015 - Styling
• 5dbf0f40 - Weaken `set_bind` lemmas to require `Set_` instead of `FinSet` for the resulting set.
• 290723a3 - More tweaks.

Compare with previous version

@jung Any comments about this?

Hm, not really, seems to make sense. I wonder if there's any lemma relating this and the version on maps, perhaps through gset_to_gmap or set_to_map... but that seems too niche to be relevant.

I guess we could add such a lemma later, if there's need. Going to press merge then. Thank you!

added 28 commits

• 290723a3...504d165a - 20 commits from branch iris:master
• 17cac1d5 - Add set_omap operation
• 04aa97fc - CHANGELOG
• 12b0bd3a - Minor tweaks.
• d8b8610f - Compatibility with bind and map
• 62a5000b - Add set_omap_filter
• 0f9fda3d - Styling
• 13b83bd0 - Weaken `set_bind` lemmas to require `Set_` instead of `FinSet` for the resulting set.
• cf2ea0e7 - More tweaks.

Compare with previous version

added 11 commits

• cf2ea0e7...28d33f1f - 3 commits from branch iris:master
• 906a7bef - Add set_omap operation
• 3363cdfc - CHANGELOG
• 34a8ec0a - Minor tweaks.
• 3634203c - Compatibility with bind and map
• 01f80762 - Add set_omap_filter
• 86b802c5 - Styling
• 3a80961c - Weaken `set_bind` lemmas to require `Set_` instead of `FinSet` for the resulting set.
• 0f7f6619 - More tweaks.

Compare with previous version

enabled an automatic merge when the pipeline for 0f7f6619 succeeds

It appears I never pressed merge, so doing that now.

merged

mentioned in commit a1765eda