I am looking for data structure implementation or something that I can implement easily for Coq that provides extraction friendly/ search tree data structure that works with arbitrary keys. I assume I will have to implement equality function or hash functions for keys but I have no problem with that.

If no such implementation exist, I am also welcoming papers on describing efficient implementation for functional programming languages, that I can just implement.

how about fmapavl? https://github.com/coq/coq/blob/master/theories/FSets/FMapAVL.v

that is what I am looking for, thanks! (or I think so)

Search trees typically require total ordering on keys. I've recently ported a bunch of search structures from Isabelle to Coq/Ssreflect here: https://github.com/clayrat/fav-ssr

Last updated: Feb 09 2023 at 00:03 UTC