The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Erik,

  Apart from Vladimir's answer about separating "data" and proofs, there is a known problem of representation when using projections of sigma types and parametrized records that you might be experiencing. Each projection takes all the parameters as arguments, and in nested/iterated cases this can lead to a blowup in proof-term size and type checking time. You can check that this happens using Set Printing All, the actual proof term should be much much larger than what you see if implicit arguments are hidden. The next version (and current trunk) will have support for a more economical representation that solves that problem.
-- Matthieu

On Saturday, June 14, 2014, Erik Palmgren <palmgren AT math.su.se> wrote:

Here is a remark I made some time ago. I am getting, what I think, absurdly slow 

response from Coq when checking proofs involving many iterated sigmas or records.

There was some improvement when upgrading from 8.3 to 8.4, and rearranging some sigma-constructions,

but it is still too hard for the quite modest complexity I am considering.  

I am using an alternative development of setoids, since I want to

the truth-values of equality to be in Set rather than in the Coq-standard Prop. The goal

of the development is to construct a category of setoids closed under the various 

categorical constructions as pullbacks, pushouts and internal products etc. I see no principal

difficulties in this, but the implementation in Coq has turned to be quite frustrating, because of

the slowness of checking proofs. So far just proving closure for pullbacks, has required machine times

of up to an hour.

Does anyone have an idea for how to improve performance?

The URL 

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

contains CategoricalUniverse-test12.v which is the actual development (it may require recompilation).

Best regards

Erik Palmgren

--