Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments


Chronological Thread 
  • From: Enrico Tassi <enrico.tassi AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments
  • Date: Sun, 8 Feb 2015 11:05:15 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page