The Coq mailing list

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

Many thanks to Matthieu, Bas and Vladimir, for the hints how to improve proof performance. The suggested separation of data and proofs (for setoids and categories) seems to have speeded up the first part of the proof, but slowed down the final part, probably since further levels of records/existentials were introduced.  In total a slightly worse runtime: from 34 min 40 sec to 34 min 50 sec on the Mac Book Air I am using. I guess the main problem is what Matthieu describes below. In general I would like to end all proofs with "Defined", since I may need the constructions of the proofs later.

Best regards

Erik

---

Från: matthieu.sozeau AT gmail.com [matthieu.sozeau AT gmail.com] för Matthieu Sozeau [matthieu.sozeau AT inria.fr]
Skickat: den 15 juni 2014 12:12
Till: coq-club AT inria.fr
Ämne: [Coq-Club] Slow iterated sigmas

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

--