# Add function `map_kmap` that transforms the keys of a finite map.

This function `map_kmap f`

allows one to turn maps with keys `K1`

(e.g., `gmap K1 A`

) into maps with keys `K2`

(e.g., `gmap K2 A`

), where `f : K1 → K2`

.

Notes:

- The function
`f`

should be injective, otherwise`map_kmap f`

is ill-behaved. Consider`map_kmap (λ _, 0) {[ 0 := 10, 1 := 20 ]}`

. What's the result of that? Well, that depends on how the map is exactly represented (for`gmap`

that depends on how exactly the`Countable`

instances are defined). - There are tons of generalizations of this function possible, e.g., with functions
`f`

that go to`option K2`

so that elements can be dropped, etc (similar to`omap`

versus`fmap`

), or that could also take the values into account (similar to`imap`

versus`fmap`

). I think the version in this MR is useful because it enjoys nice lemmas. Maybe in the future we could define a generic version and define the one in this MR in terms of a more generic version. - Some of the lemmas hold without
`Inj`

(e.g.`lookup_map_kmap_None`

). I don't think there's a point in doing that because then I can no longer use the generic lemmas about`list_to_map`

, also`map_kmap f`

where`f`

is not injective is ill-behaved (as previously stated).

Thanks @jules for the suggestion and feedback.