Add images (codomains) to finite maps

Simple axiomatization of finite map images (also called codomains). This is strongly inspired by the implementation of dom.

It doesn't contain nearly as much lemmas though, mainly because results on the image are generally much weaker than those on the domain, so just using the definition seems simple then providing overly complex lemmas.

Disclaimers: I'm not exactly an expert in Coq but eager to learn more. If you find that my coding style and proofs are ugly, inefficient, impractical or not in keeping with recommended guidelines feel free to let me know.

added 1 commit

• 30bd65d3 - Fix pipeline

Compare with previous version

added 1 commit

• 84201b32 - Actually managed to run coq with -mangle-names

Compare with previous version

Thanks for the merge request! This looks like a sensible operator to have and the MR provides a good start. Some general comments for a first round:

• I don't think we need an interface FinMapImg. The main reason we have such an interface for the domain is that you can give a specific instance for a concrete map implementation. For example, for gmap you can compute the domain as a gset in linear time. For the image, I don't think there's a smart way to compute it. You just need to do a linear number of insertions into a set. Hence I think FinMapImg should be removed, and fin_map_img should be in fin_maps.v where all the image lemmas concern that instance.
• I think having an operational type class Img still makes sense. It allows us to define instances also for other types for which the notion of an image makes sense.
• Style: Please use unicode symbols (λ/→/∧ instead of fun/->/∧).
• Style: Please try to put spaces around the :s.
• Style: See https://gitlab.mpi-sws.org/iris/iris/-/wikis/style-guide (this reminds me, we probably should make that style guide more prominent somewhere :))

added 4 commits

• 9b358d9c - Change styling
• 5a25ecbc - Add link to style guide
• a82173fe - Remove FinMapImg
• 8e31834c - More union lemmas

Compare with previous version

added 2 commits

• 003d1c7c - Revert "Add link to style guide"
• bdcbb33f - Various small improvements

Compare with previous version

added 1 commit

• e629b5f8 - Remove gmap Instance

Compare with previous version

added 1 commit

• f3cadb68 - Proof styling

Compare with previous version

added 14 commits

• f3cadb68...2d8ccea3 - 13 commits from branch iris:master
• 5ecc2e07 - Merge branch 'master' into 'dorian/fin-map-img'

Compare with previous version

added 1 commit

• 59f59ae5 - Simplify diff

Compare with previous version

added 6 commits

• 59f59ae5...edeef15e - 5 commits from branch iris:master
• 16bb306e - Merge branch 'master' into 'dorian/fin-map-img'

Compare with previous version