The Coq mailing list

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

Jeff Terrell wrote:
> Hello Everyone,
> 
> I'm new to Coq and would appreciate some help in finding a proof term for
> 
> forall l : list Process,
>     exists m : list Package,
>        forall p : Process,
>           In p l -> exists a : Package,
>              In a m /\
>              PID p = AID a.
> 
> where
> 
> Record Process : Set := {PID : nat}.
> Record Package : Set := {AID : nat}.

Welcome!

The easiest way to prove this theorem is with a trivial mapping from
Process to Package:

Definition p2p (p: Process) : Package := Build_Package (PID p).

This mapping provides the proof of existence of a Package, given a
Process. You've used this mapping implicitly at one point in your proof
attempt; however, it helps to make it explicit.

To obtain the corresponding mapping over lists (and the corresponding
proof of existence), use the "map" function from the List library. To
complete the proof, there is no need for an explicit induction. Instead,
make use of a lemma (also from the List library) which relates the "map"
function to the "In" predicate.

One final comment: when you see something like "In p nil" in the list of
hypotheses, you know something is up. A false hypothesis can immediately
prove anything, so there is no need to even look at the conclusion!

Regards,
Matthew