The Coq mailing list

[Matthew Brecknell <coq-club AT brecknell.org>]

Jeff Terrell wrote:
> What I was trying to do was to come up with an example in which a witness 
> *couldn't* be constructed from constraints in the current goal, because I 
> was 
> keen to understand how to deal with such a situation. Unfortunately, I 
> messed up 
> the theorem and that led to some confusion; I'm sorry to everyone for that.

There's no substitute for understanding the thing you are attempting to
formalise. If you're unable to imagine what properties a witness must
satisfy, it's unlikely you'll be able to prove much of interest.

Having said that, some tactics do generate existential meta-variables to
be determined in a later proof step. (In particular, various tactics
beginning with 'e', for example eauto). I don't know whether you might
be able to use meta-variables in your proof. Perhaps someone else can
comment?

> Your theorem above tie things down quite nicely - many thanks for that. But 
> I 
> was also wondering (for curiosity sake more than anything else) whether <-> 
> could be replaced by ->, if the implicand constrained Y to be the smallest 
> possible list. If that were possible, (X p') wouldn't then be a witness.

You could write something like this (which is really just factoring out
the extra conjunction and quantification which Adam described):

Inductive shortest (A: Type) (P: list A -> Prop) : list A -> Prop :=
  | is_shortest: forall x, P x
    -> (forall y, P y -> length x <= length y)
    -> shortest A P x.

Implicit Arguments shortest [A].

Theorem T :
  forall l : list Process, exists m : list Package,
    forall p : Process, In p l -> exists a : Package,
      In a m /\
      PID p = AID a /\
      shortest
        (fun y => forall n, In n (X p) -> n > 0 -> In n y)
        (Y a).

I think this is actually stronger than the previous formulation, since
it also disallows duplicates. I've not attempted a proof, though I
imagine you would want to start with some lemmas relating shortest and
In.

Regards,
Matthew

PS - I apologise for my previous double-post. I initially sent it by
accident from a non-subscribed address, and falsely presumed it had been
dropped when it hadn't come through for a while. I realise now that it
was probably sitting in a queue for moderation.