Finite map composition

• Add a map_compose operator for finite map composition
• Add notation m ∘ₘ n for map_compose m n
• Add various lemmas to manipulate map composition

This is arguably a niche operator we might not want to include. If you think that is the case feel free to close without merging.

I'm submitting in case someone else would have a use for it, since this is now fairly complete (although it could use some compatibility lemmas with insert).

added 2 commits

• c2284444 - Remove extra parameter
• 32f3dba1 - Naming stuff

Compare with previous version

added 1 commit

• a99f68e9 - Forgot to name stuff

Compare with previous version

mentioned in merge request !505 (merged)

mentioned in merge request !506 (merged)

Thanks for the MR and sorry for being so late with a review/making a pass.

I committed some tweaks. Aside from minor things and proof refactoring, some noteworthy changes:

• Only add the relevant type classes to map_compose. Due to the unbundling FinMap gives many arguments, now you only get the required ones.
• Weaken some lemmas from Set_ to SemiSet. This became possible to due !505 (merged).
• Use =@{M A} instead of type casts where possible.
• Add map_compose_disjoint_r and rename your lemma into map_compose_disjoint_l. This corresponds to having two versions of the union lemma.
• Do not use Proper instances for monotonicity. We don't use this style elsewhere in std++ and things like Proper ((⊆) ==> (⊆)) (λ m, map_compose m n) are generally not infered automatically due to the lambda.
• Add map_compose_insert_{None,Some}, map_compose_delete, map_fmap_map_compose, map_omap_map_compose.
• Remove map_compose_filter_subseteq_{l,r}. This is just modus ponens of two monotonicity lemmas and I am not convinced this combination deserves its own lemma. If we go this way, there is at least a quadratic number of combinations that we can add.

added 179 commits

• a99f68e9...7f6df4fa - 176 commits from branch iris:master
• b9802e1e - Add finite map compose operation and lemmas
• 383c4535 - CHANGELOG and coqdoc
• 562726c1 - Tweaks.

Compare with previous version

This is arguably a niche operator [..]

Agree, but it's a reasonable operator so it makes sense to include it.

That said, if it's niche, does it deserve having a notation? An argument in favor is that we are already using ₘ notations for maps, so having ∘ₘ as well is unlikely to cause conflicts or problems in the future.

added 2 commits

• 21a6a7f5 - Tweak map_compose lemmas, definitions, proofs.
• abac9560 - Tests.

Compare with previous version

mentioned in commit iris@24c44378

mentioned in merge request iris!990 (merged)

added 1 commit

• b3de63c4 - Streamline `map_compose_as` lemmas.

Compare with previous version

resolved all threads

I think this is ready to me merged. @dlesbre can you check that I did not mess up anything by modifying this MR?

resolved all threads

Merging!

merged

mentioned in commit 6cb762da