Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Simple Transformation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simple Transformation


chronological Thread 

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







Archive powered by MhonArc 2.6.16.

Top of Page