extensional trie map for positive

[palmskog]

WIP based on rocq-prover/rocq#17044.

[palmskog]

Hi @andres-erbsen, would you be interested in collaborating on getting the extensional trie from rocq-prover/rocq#17044 implemented for the MMap interface? In this PR, I adapted the code from your PR based on the PositiveMap we already have here.

Some questions I have been pondering:

• how does one implement the binders function for the trie?
• how does one expose the extensionality in the best way in the TrieMapAdditionalFacts module?

Any hints or help appreciated.

[andres-erbsen]

Thank you for getting started at the integration here and reminding me that this is on my todo list still. I think bindings could be implemented like values and extensionality could be exposed by defining Equal as Logic.eq.

[palmskog]

OK, I will take a stab at bindings using the values approach. However, for the Equal thing, unfortunately Interface.v defines Equal as something more general that we can't change if we want to implement the module type.