The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hi,

Enrico may add more informations about that but the main problem
"Proof using" addresses is section "discharging" mechanism.

When closing a section, each definition done within the section is
"discharged", which implies adding universal quantifications to its
type. The variables quantified are the section variables *occurring in
its body*.

Parallelisation means using lemmas's types whithout compiling them
first (postponing the proof checking, i.e. the building of the body
via tactics). For lemmas declared in sections we have to settle their
discharged types in absence of body, thus we have to rely on Proof
using annotations. The checking at Qed is there only to check that the
annotations are correct so that when using parallel compilation the
discharged types remain the same.

Hope it helps,

P.







2015-02-08 1:26 GMT+01:00 Jonathan Leivent 
<jonikelee AT gmail.com>:
>
> On 02/07/2015 04:55 PM, Jason Gross wrote:
>>
>> ..  If you want
>> to do this on the first run of the file, too, you must use [Proof using
>> <variables to be used in the proof>].
>>
>>
>
> I guess I don't understand the behavior of [Proof using]:  How is [Proof
> using] important to proof parallelism, if the [Proof using] declaration is
> only processed at Qed time (to determine if the proof obeyed the restriction
> or not, and to abstract over only the used variables)?  Was [Proof using]
> changed in 8.5 to do earlier processing?
>
> -- Jonathan
>