The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Dear Matthew,

Thanks for your comments.

The proposition is actually part of a much larger specification, in which each 
process contains a list of A, and each A contains a list of B and so on. In all, 
there are 4 nested levels of list recursion.

As a newcomer to type theory as well as Coq, I'd really prefer to stick to using 
tactics with which I can easily identify, e.g. forall, exist, ->, /\, \/ 
introduction and elimination rules, and list recursion.

So, at the risk of making myself unpopular, how would you prove the theorem 
using tactics like intro, exists, elim, split and so on. I think if I can see 
how to solve this simple problem by these means, it will help me to solve the 
more complex problem.

Many thanks.

Regards,
Jeff.

Matthew Brecknell wrote:
> 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