The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Sun, Feb 08, 2015 at 01:58:07AM +0100, Pierre Courtieu wrote:
> 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.

That's all exact, thanks!

Bottom line, if one has no Section he can ignore Proof using.

Other 2 little services are provided by Proof using.
1) If you end the proof with Admitted, hence you don't give a complete body,
   with Proof using you can still tell Coq what to discharge.
2) Proof using declarations are checked by Coq.
   I've seen mathematical proofs where the methmatician had such a messy
   context that he was helping the reader by saying "this lemma hods
   under this part of the curret section-global set of hyps".  Proof
   using, together with Collection, should help you model this sentence
   faithfully.

Best,
-- 
Enrico Tassi