The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Terrell wrote:
> Adam Chlipala wrote:
> > Jeff Terrell wrote:
> > > 1 subgoal
> > >
> > >   p' : Process
> > >   l : list Process
> > >   mw : list Package
> > >   H : forall p : Process,
> > >       In p l ->
> > >       exists a : Package,
> > >         In a mw /\
> > >         PID p = AID a /\ (forall n : nat, In n (X p) -> n > 0 -> In 
> > > n (Y a))
> > >   ============================
> > >    exists m : list Package,
> > >      forall p : Process,
> > >      In p (p' :: l) ->
> > >      exists a : Package,
> > >        In a m /\
> > >        PID p = AID a /\ (forall n : nat, In n (X p) -> n > 0 -> In n 
> > > (Y a))
> > >
> > > T < exists (Build_Package (PID p') ??????? :: mw).
> >
> > Don't you just want to put [(X p')] in the blank?  I can't spot 
> > anything tricky going on here.
>
> Unless the specification is wrong, the intention was for Y to contain 
> a subset of the numbers in X, so that (X p') *wouldn't* be a valid 
> witness for Y. What am I missing?

It's more than your specification being wrong: your understanding of 
what a specification is is wrong. ;-)  (But, putting that aside, you 
"specification" is "wrong" relative to your stated intentions, in the 
sense that the inner existential witness need not include any filtering 
and may even add new list elements, as long as every old element is kept.)

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.

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.

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.

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.