coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeff Terrell <jeff AT kc.com>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Simple Transformation
- Date: Sat, 21 Feb 2009 15:46:52 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] Simple Transformation, Jeff Terrell
- Re: [Coq-Club] Simple Transformation,
Matthew Brecknell
- Re: [Coq-Club] Simple Transformation, Jeff Terrell
- Re: [Coq-Club] Simple Transformation, Luke Palmer
- Re: [Coq-Club] Simple Transformation,
Matthew Brecknell
- Re: [Coq-Club] Simple Transformation,
Jeff Terrell
- Re: [Coq-Club] Simple Transformation, Adam Chlipala
- Re: [Coq-Club] Simple Transformation, Matthew Brecknell
- [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness,
Adam Chlipala
- Re: [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness, Adam Chlipala
- Re: [Coq-Club] Partial Witness, Jeff Terrell
- Re: [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness,
Adam Chlipala
- Re: [Coq-Club] Simple Transformation,
Jeff Terrell
- Re: [Coq-Club] Simple Transformation, Jeff Terrell
- Re: [Coq-Club] Simple Transformation,
Matthew Brecknell
Archive powered by MhonArc 2.6.16.