The Coq mailing list

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

Thanks for this advice. I will probably use it in the next extension. Anyway 
I managed to improve the proof by introducing many explicit subsidiary 
lemmas, so the checking time went down from 34 minutes to under 3 minutes! 
Quite reasonable performance. It seems that the exponential behavior of 
iterated sigmas could be beaten this way, in this case anyway.

Best regards

Erik
________________________________________
Från: AUGER Cédric 
[sedrikov AT gmail.com]
Skickat: den 15 juni 2014 23:00
Till: 
coq-club AT inria.fr
Kopia: Erik Palmgren
Ämne: Re: [Coq-Club] Slow iterated sigmas

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