The Coq mailing list

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

Dear Matthieu,

many thanks for this answer. I am glad that to hear about the ongoing
improvements of the record projections. For now I try to rejig the 
sigma-types to fewer parameters. For instance, replacing

Definition doublesigT1 (A B:Set)(R: A -> B -> Set): Set:=
(sigT (fun x: A => (sigT (fun y: B => R x y)))).

by

Definition doublesigT2 (A B:Set)(R: A -> B -> Set): Set:=
(sigT (fun z: (prod A B) =>  R (fst z) (snd z))).

Best regards

   Erik

9 nov 2013 kl. 12:26 skrev Matthieu Sozeau:

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