The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You might be interested in a paper I wrote on designing a performant category theory library in Coq: http://people.csail.mit.edu/jgross/#category-coq-experience.

Very briefly, I'd suggest trying to flatten your nested sigma types into records, and, possibly, destructing them early in the proofs when you need to destruct them at all.  Moving to trunk with primitive projections (you'll have to define your own sigma types, though) may also solve the problems.  I'm happy to chat more about any bits of my paper (or any other performance issues you may run into).

-Jason

On Sun, Jun 15, 2014 at 10:00 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:

Le Sun, 15 Jun 2014 20:01:10 +0000,
Erik Palmgren <palmgren AT math.su.se> a écrit :

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

The "abstract" tactic can be quite helpful for this kind of things.

For instance, you can do something like:

Definition foo : bar.
Proof.
 <regular tactics for parts you want transparent>
 abstract (<opaque proof part>).
Defined.

This is especially useful in combination with the refine tactic.

Definition foo : {x : bar | P x}.
refine (existT P (f x) _).
abstract (my_tactic).
Defined.

>
> 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<UrlBlockedError.aspx>> 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<http://people.su.se/~epalm/coq/czf_and_setoids/CategoricalUniverse-test12.v>

> which is the actual development (it may require recompilation).
>
> Best regards
>
> Erik Palmgren
>
>
>
> --
>