The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

   Dear all,

  Recently I've started using FSets and FMaps in Coq, which are a very nice translations of ocaml sets and maps. Just like their ocaml counterparts, they require an order on the underlying datatypes used in a set/map. However, the big difference is that as long as we need just an orbitrary order (which is often the case when using sets or maps) in ocaml one gets this for free (by means of the polymorphic compare), whereas in Coq one needs to provide the order (along with some proofs of its properties) and this can be a very daunting task indeed. Use of appropriate tacticals can make it slightly less cumbersome but still I did not come up with a way to do this that would not require an amount of typing proportional to the number of constructors of the datatype; and if the number of constructors is getting large... In principle I do not see a fundamental reason why such an order could not be derived automatically (at least if we restrict to non-dependant types). Hence my question: can one do better than just to code such orders by hand? Any thoughts appreciated...

   Best wishes,
   Adam Koprowski

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================