Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Partial Witness

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Partial Witness


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page