The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

In my experience using several definitions (e.g. for a group to have the "group_carrier", "group_data", then "group_axioms" consisting of "group_assoc", "group_unit", "group_inverse" all of these being separate definitions, then "group" consisting of "group_data" and "group_axioms") makes things much much faster since Coq does not unfold the internal definitions unless necessary.

V.

On Jun 14, 2014, at 8:31 PM, 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