The Coq mailing list

[Erik Palmgren <palmgren AT math.su.se>]

Dear Coq users,

I have been working (together with Olov Wilander) on an implementation of categories of setoids with equality on objects. These are thus not the usual E-categories of setoids. It relies heavily on proof irrelevant families of setoids. Some of the constructions have turned remarkable slow to check in Coq.  For instance a 3000+ lines development (see below) took almost two hours to check on a modern laptop. The most time consuming steps are various destructs with patterns and the command Defined. Previously in this list, it has been pointed out that complicated destruct patterns can generate many cases, that may generate huge terms difficult to check. I can not really see that  in my example, that so many cases are generated. Perhaps it has instead something to do with the many type dependencies that arise.  If someone has a hint as to what makes this example so slow, I would be very grateful.

The example is

CategoricalUniverse.v

in 

http://people.su.se/~epalm/coq/czf_and_setoids/

(Accompanying paper: czf&setoids_rvsd.pdf in the same directory).

Erik Palmgren