The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

What about another kind of trade-off? You can use different (But provably equivalent) implementations of the same data structure. 

While proving take an lightweight inefficient version. When extracting take the heavyweight-but-squashed-at-extctraction version.

You need a way to switch from one implementation to another. Either with modules (MSet and co are extremely versatile in this aspect) or maybe use the parametricity plugin?

Best 

P

Le jeu. 14 mai 2020 à 19:55, Hugo Herbelin <Hugo.Herbelin AT inria.fr> a écrit :

For the record, Pierre Letouzey (main author of the FSets/FMaps
library with Jean-Christophe Filliātre) has precisely updated last
week his "M" version of FMaps (https://github.com/letouzey/coq-mmaps),
with the plan to release it soon as an opam package.

Best,

Hugo

On Thu, May 14, 2020 at 12:46:38PM -0400, Andrew Appel wrote:
> The MSets interface of the Coq standard library factors the program from the
> proof, and may solve the problem that's being discussed here.
> It was intended as a replacement for FSets and FMaps.
> There had been a plan to make MMaps also (finite maps instead of sets), but
> unfortunately I don't think that was ever done.
>
> There are efficient implementations of MSets for AVL trees and Red-Black trees
> in the standard library.
>