The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Dear Erik,

  I would suspect that the representation of record projections is the culprit
here. It's easy to check: Set Printing All in the goals where you're doing the
destruct and see if they're reasonably big or not. The type annotations of 
sigma
projections (and records with parameters) can result in exponentially larger 
fully explicit terms, hence longer abstractions/substitutions/retypechecking 
used in destruct. Qed/Defined re-typecheck these huge terms. 

  One solution is to replace sigmas with specific records (with no 
parameters) 
when possible. Another one is to use a more efficient representation of 
record 
projections, without parameters (part of my polyproj branch at 
github.com/mattam82/coq.git and soon to be merged with the trunk). If you 
want 
to try it out I can provide guidance.

Cheers,
-- Matthieu

On 8 nov. 2013, at 21:14, Erik Palmgren 
<palmgren AT math.su.se>
 wrote:

> 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
> 
> 
> 
>