The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Dear Adam,

> 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 understand the notion of proof irrelevance, if that's what you mean.

> You are probably operating under the misconception that Coq is commonly 
> used to "extract programs from proofs."  Hardly anyone does this, in Coq 
> or any other system.  Rather, Coq is more like a rich programming 
> environment with a compilation toolchain by way of extraction to OCaml.

I was eventually hoping to extract an OCaml program to perform the 
transformation. I'm aware that Coq has 3 forms of existential quantification, 
and I'm also aware that the form that I'm using here, in what I loosely 
described as a specification (I forgot that this has a particular meaning in 
Coq), is not suitable for extraction.

> You could restate your problem with product types in place of 
> conjunction and sigma types in place of [exists], and then it would be 
> possible to use tactical proof search to build a real _program_, rather 
> than a purely mathematical _proof_, as you are doing now.

Thanks for the info.

> I'm sure I've used many terms and concepts in this message that you 
> aren't familiar with.  Thus, my meta-message is that you should read a 
> book on Coq, rather than jumping right into an implementation, where you 
> assume you already have the right intuitions to make do with the manual 
> alone.

I haven't jumped into anything. In fact, I've been studying the Coq'Art book for 
a while, in addition to books and papers on type theory - mainly Martin-Lof; 
it's a difficult subject to get into.

I'm really disappointed with the tone of your remarks. If your intention was to 
humiliate me, you have succeeded.

Regards,
Jeff.