coq-community / coq-mmaps Goto Github PK

We would like to have a lemma relating fold and add, as is done for FMap here.

The background for why such a result is useful can be found in section 8 of this paper.

I'd love to use these maps in an experiment of mine, but it doesn't compile with recent enough versions of Coq:

File "./Facts.v", line 1752, characters 2-6:
Error:  (in proof not_empty_has_binding): Attempt to save an incomplete proof

With 8.11.2 I get

File "./Facts.v", line 1829, characters 34-55:
Error: No product even after head-reduction.

Are there plans to modernize this library?

The project is currently lacking locality annotations, like the following:

#[export] Instance Equal_equiv {elt} : Equivalence (@Equal elt).

This prevents compatibility with current Coq master. One will have to go through and annotate every Instance/Hint.

Even though the project is WIP, we may want to do a release/tag on GitHub, so that we can have an opam package for regular users as part of the released Coq opam repo. Is that OK with you @letouzey? And should we use a "regular" version number 1.0 or something that better signals WIP status?

The paper Efficient Extensional Binary Trees by Appel and Leroy and its accompanying Coq sources describe the following efficient trees which could implement the MMaps interface:

• binary tries, using a canonical first-order representation; another minimalistic implementation here
• binary Patricia trees from section 12.3 of Functional algorithms, verified! by T. Nipkow et al. Not extensional.
• trie data structure with sparse, 256-degree nodes that branch on the next character of the string.