Small enhancement proposal: add a function that combines mapi and map2 in Coq.FSets.FMapInterface

[dnjansen]

Description of the problem

I am using (map2 f m1 m2) to combine two finite maps m1 and m2 into one, but in function f I would like to get access to the current key as well, not only to the values in m1 and m2. I suggest to add a function with signature

mapi2 : (key -> option elt -> option elt' -> option elt'') -> t elt -> t elt' -> t elt''

mapi2 should satisfy the following properties (adapted from the specification of map2 in Coq.FSets.FMapInterface):

Parameter mapi2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
    (x:key)(f:key -> option elt->option elt'->option elt''),
    In x m \/ In x m' ->
    exists y:key, E.Eq y x /\ find x (mapi2 f m m') = f y (find x m) (find x m').

Parameter mapi2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
    (x:key)(f:option elt->option elt'->option elt''),
    In x (mapi2 f m m') -> In x m \/ In x m'.

I think that mapi2 can be implemented by copying the definition of map2 in Coq.FSets.FMapLists with minimal changes.

Coq Version

8.18.0

[palmskog]

@dnjansen FMap and the FSets modules are considered legacy code at this point. We are developing a successor of FMap called MMap in Coq-community: https://github.com/coq-community/coq-mmaps

Maybe you would consider proposing your changes to that project instead? The process would be much more lightweight, and the MMaps package is slated for inclusion in the Coq Platform: coq/platform#307

[dnjansen]

Thank you for your answer. I can see that MMap already provides the functionality I requested as a function merge. I suggest to close the issue.