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
- [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments, Jason Gross, 02/07/2015
- Re: [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments, Jonathan Leivent, 02/08/2015
- Re: [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments, Pierre Courtieu, 02/08/2015
- Re: [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments, Jonathan Leivent, 02/08/2015
- Re: [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments, Enrico Tassi, 02/08/2015
- Re: [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments, Pierre Courtieu, 02/08/2015
- Re: [Coq-Club] Announcement: Tool for enabling better Coq 8.5 parallization on existing Coq developments, Jonathan Leivent, 02/08/2015
Archive powered by MHonArc 2.6.18.