The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

This sounds usefu but I did not understand how to use it in practice.

Suppose my proof is

....

refine ( constr _ _ ).

{ apply a1. exact b1. }

{ apply a2. exact b2. }

Defined.

How do I "abstract" the first argument of constr? 

V.




On Jun 15, 2014, at 11: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
>> 
>> 
>> 
>> --
>> 
>