Replace extructures with finmap

[MarkusKL]

This issue is about replacing the dependecy extructures with finmap

In my attempt to do so I have made the following observations:

• Advantage: finmap is based on choiceType rather than ordType, which would simplify this codebase
• Advantage: finmap follows the development of math-comp more closely.
• Incompatibility: unionm (extructures) is left-biased while + (finmap) is right-biased.
• Missing: I have not been able to find suitable replacements for the following operations
  • mapm used to define package linking.
  • mapim used to define the identity module
  • mkfmap with notation [fmap ... ] used to generate a finmap from a list of key-value pairs.
  • A theory of permutations to be used by nomninal definitions.

[spitters]

@CohenCyril, @arthuraa Do you have any input on this? Should these lemmas be moved/ported to finmap?
arthuraa/extructures#22

We can probably also upstream any utility libraries we create around this.
e.g. from #65

[arthuraa]

I have started porting some extructures definitions to finmap. Some features (e.g. the bias of unionm) might not make it, but maybe we could release a compatibility wrapper if there is interest.

I am drafting a standalone version of the permutation module of extructures as a separate library based on finmap.

[spitters]

@MarkusKL Maybe you can give an overview here of your additions to finmap.

[CohenCyril]

There is also this development from 10 years ago: https://github.com/lewer/nominal-coq (joint work by @mattam82, @lewer and myself) that I started updating to mathcomp 2 in january, which contains some theory of finite permutations in a choiceType and nominal (choice)Types. I did not have time to finish the update to mathcomp 2 yet.

[spitters]

Thanks @CohenCyril .
FYI, we're trying to integrate @MarkusKL nominal-SSProve into the main repo.
Maybe there's a possibility to refactor more to be inline with your work?
github.com/MarkusKL/nominal-ssprove/blob/master/theories/Nominal.v

There's also work by @annenkov on using nominal sets in Rocq:
https://github.com/annenkov/stlcnorm
https://dannenkov.me/papers/nominal_slides.pdf

[arthuraa]

FYI, I have ported the permutation library of extructures to use finmap:

https://github.com/arthuraa/finperm

[spitters]

@CohenCyril What are the plans on nominal Rocq. Will it be moved to Rocq community? We can probably integrate @MarkusKL code into a joint library.

[MarkusKL]

This header introduces the extra fmap definitions:
https://github.com/SSProve/ssprove/blob/main/theories/Crypt/package/fmap_extra.v#L13
They are defined in Prop to not require EqDec on the values of the map.

My work on nominals is to be included here over the next week: #82
Originating from nominal-ssprove.

[spitters]

@CohenCyril Nominal SSProve has now been merged. Would it make sense to move the general nominal part to a more general place?

[spitters]

@MarkusKL what is the status of this, now that nominal has been merged?

[MarkusKL]

The issues is still relevant since SSProve is still based on extructures.