The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Dear Adam,

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?

> P.S.: Please don't include long proof interaction traces in future 
> messages.  Showing one proof sequent would be enough for me, and I 
> almost ignored your message because of how long it was.  (Others may 
> have different opinions, but I'm guessing that most agree on this.)

I'm sorry about this - I was just trying to provide some context.

Regards,
Jeff.