coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <herbelin AT pauillac.inria.fr>
- To: Adam Chlipala <adamc AT hcoop.net>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Partial Witness
- Date: Mon, 2 Mar 2009 22:31:17 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Mon, Mar 02, 2009 at 10:26:32AM -0500, Adam Chlipala wrote:
> Hugo Herbelin wrote:
> >> You are proving a theorem whose type belongs to [Prop]. That means the
> >> proof really is a proof, and every proof is equivalent computationally.
> >> There is never any reason to prefer any proof to another, putting aside
> >> issues of how difficult different proof strategies are to code.
> >>
> >
> > I would not be so peremptory. If the common view is indeed to "think"
> > proofs as computationally irrelevant, this is not enforced by the
> > logic of Coq and "proof-relevant" models remain available. Moreover,
> > even if a logic is proof-irrelevant, this does not mean that the
> > computational content of the proofs cannot be observed and
> > manipulated at the meta-level. See e.g. Alexandre Miquel's
> > realizability and extraction for Prop which supports classical
> > reasoning and, even, proof-irrelevance (at the logical level).
>
> Still, I believe that, for someone _new_ to Coq and not interested in
> pondering metatheory, thinking about [Prop] non-irrelevantly is most
> likely to lead only to misleading intuitions. There is a substantial
> amount of talk out there about "extracting programs from proofs," and I
> feel that a lot of newcomers to Coq end up confused because they assume
> that this is how Coq is usually used.
I agree on the irrelevance of presenting Prop non-irrelevant when
teaching Coq. About "extracting programs from proofs", I like to
explain this feature because it is remarkable and it emphasizes the
fundamental identity between proofs and programs. But I don't insist
on using it because I consider that it is more "natural" to write
programs "as programs", allowing for a better control of the exact
code and a better separation between the computational content and the
properties of the program. About writing programs using tactics, I
know people that like to proceed this way. Maybe it is a kind of
snobism but I don't care, as most of the time they know what they are
doing. I agree that confusion (or ideology) regarding Coq having to be
used along the extraction-from-proof paradigm is not to be encouraged.
> > In any case, let's keep this list friendly!
>
> OK, I feel I need to step in briefly to make one thing clear, since I
> don't want the reputation of a crotchety ogre who breakfasts on the
> bones of newbies: I see no point during this thread where anyone was
> unfriendly. I think we have an issue of miscommunication across
> cultures and conventions of expression. I'm going to try to learn from
> this to avoid writing things that bother people in the future, but I
> hope you can take my word for it that I wasn't trying to be anything but
> friendly and helpful at any point.
Adam, I believe you. I know your enthusiasm and your contribution to
our community.
Hugo
- Re: [Coq-Club] Partial Witness, Roman Beslik
- <Possible follow-ups>
- Re: [Coq-Club] Partial Witness, Matthew Brecknell
- Re: [Coq-Club] Partial Witness,
Matthew Brecknell
- Re: [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness,
Adam Chlipala
- Re: [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness, Adam Chlipala
- Re: [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness, Matthew Brecknell
- Re: [Coq-Club] Partial Witness,
Adam Chlipala
- Re: [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness,
Hugo Herbelin
- Re: [Coq-Club] Partial Witness,
Adam Chlipala
- Re: [Coq-Club] Partial Witness, Hugo Herbelin
- Re: [Coq-Club] Partial Witness,
Adam Chlipala
Archive powered by MhonArc 2.6.16.