The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Hi all,
I do need for setting my workbench a concept of finite map (and thus finite 
set)
where keys K have the following good properties:

  i have functions beq:K->K->bool , blt K->K ->bool
  such that
    k1=k2<->true=beq k1 k2
  and
   false=blt k1 k2->false=blt k2 k1->false beq k1 k2->False

while values of the map provide only the beq function.

Of course It should be possible to define a finite map such that
  there exists a function beq for maps with the same properties,
  where two maps are equal if maps the same keys in the same values.

One possible implementation is to use an ordered list of key,value.
May there are better solution, i have seen lots of solution where
sets/maps are represented as functions.
  but, is in this way possible to syntetize such beq function without
adding extra axioms to coq?
Moreover I think an induction principle over such maps will be very
useful, and it requires to not forgot the fact that we are referring
always to *finite* maps.


Can someone suggest me how to proceed?
Is there a librariy already implementing something similar?

Thanks
Marco.