This library is an extension of mathematical component in order to support finite sets and finite maps on choicetypes (rather that finite types). This includes support for functions with finite support and multisets. The library also contains a generic order and set libary, which will be used to subsume notations for finite sets, eventually.

• Author(s):
  • Cyril Cohen (initial)
  • Kazuhiko Sakaguchi
• License: CeCILL-B
• Compatible Coq versions: Coq 8.16 to 8.18
• Additional dependencies:
  • MathComp ssreflect 2.0 to 2.1
• Coq namespace: mathcomp.finmap
• Related publication(s): none

The easiest way to install the latest released version of Finite maps is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-finmap

To instead build and install manually, do:

git clone https://github.com/math-comp/finmap.git
cd finmap
make   # or make -j <number-of-cores-on-your-machine> 
make install

The documentation is available in the header of the file.

This library will be integrated to the mathematical components library in the near future.

This library was developed independently but inspired from Pierre-Yves Strub's library, from Christian Doczkal's library and from Beta Ziliani's work (no reference provided so far).

Another alternative is Arthur Azevedo de Amorim extensional structures library.

Many thanks to Kazuhiko Sakaguchi (for the order library now moved to the main math-comp repository) and to various contributors