The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Terrell wrote:
> Dear Matthew,
>
> Matthew Brecknell wrote:
> > Reading between the lines, I'm wondering if you might actually have
> > meant to write this:
> >
> > 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 /\
> >     forall n : nat,
> >       In n (X p) /\ n > 0 <-> In n (Y a).
>
> 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.

Do you have some convention in mind for doing such constraining with an 
implication?  I've never seen such a feature in logic or math, on paper 
or on a computer.  You could certainly do it with an extra conjunction 
and universally-quantified fact, though.