The Coq mailing list

[Luke Palmer <lrpalmer AT gmail.com>]

On Sat, Feb 21, 2009 at 8:46 AM, Jeff Terrell <jeff AT kc.com> wrote:

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.

Well, trying to prove anything significant without using lemmas is setting yourself up for a lot of pain.  You can restrict yourself to a very small set of tactics, but you will need to modularize your proofs.  Those simple rules may be enough, but as Matthew suggests, you should first prove lemmas about lists, map, and in, until the actual thing you are trying to prove is a trivial consequence of those.

It's actually not that hard to start from scratch, if you like doing that to learn.  For example:

Fixpoint map A B (f : A->B) (l : list A) :=
    match l with
    | nil => nil
    | x :: xs => f x :: map A B f xs
    end.

Then your proof can begin:

intro l.
exists (map _ _ p2p l).

And as you continue the proof, you will see what lemmas you need.

Luke
 

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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club