coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mulhern <mulhern AT gmail.com>
- To: "Sean Wilson" <sean.wilson AT ed.ac.uk>, coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club]Representation question
- Date: Mon, 12 Mar 2007 19:02:29 -0600
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:in-reply-to:mime-version:content-type:references; b=qlTcgJslA2DQy9hUwNRKkiQ5Ls9DybWsEPPvHrvDdm+S195COhn3d/fhJ9nsebS2ZiQLBbfduHxRv28zgW0Nmi1k4CZi3rZgRT9arvep0d8vg9qpueyx4fRmDod216pRtNHReL3YwfzO0vdHWMZd4qE0rCGHAuODd3+bcSQUQ4o=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi!
I'ld use a list, because of the many library functions in existence for List. :)
But then I'ld think,"what if I want to do this":
Variable bound : nat.
Inductive mytype : Set :=
| Ground : mytype
| Cons : {x : list mytype | length x = bound} -> mytype
.
The Coq compiler will give me an error because of the non-strictly positive occurence of mytype in the second constructor.
Secretly, my inductive constructor actually is like this:
Inductive mytype : Set :=
| Ground : mytype
| Cons : {x : list mytype | length (A := mytype) x = bound} -> mytype
.
And it's that implicit occurence of mytype that is causing all the trouble.
If that happened, I'ld reexamine very closely my reasons for thinking I needed a bounded list in the first place. Perhaps I only really need to bound the computations I perform on an unbounded list. If that's the case, I don't need the sig type or any statements about the length of the list in the constructor. I can bound the computation in the induction principle, instead.
I tend to think that the sig type is more valuable in the statement of theorems which you intend to extract to functions than in the construction of inductive types.
- mulhern
On 3/5/07,
Sean Wilson <sean.wilson AT ed.ac.uk> wrote:
Hi,
Given the usual definition for lists indexed by length:
Inductive vect [A:Set] : nat -> Set :=
| nil : (vect A O)
| cons : (x:A)(n:nat)(vect A n)->(vect A (S n)).
Can anyone explain what the difference is between using terms of this type and
terms of type {x:list A | length = n}, particularly in the domain of writing
certified programs (e.g. in the specification of a head/tail/take/append
function)? When and why would you pick one representation over the other?
Thanks.
--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/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
- [Coq-Club]Representation question, Sean Wilson
- Re: [Coq-Club]Representation question (and what can Program do about it), Matthieu Sozeau
- Re: [Coq-Club]Representation question, mulhern
- Re: [Coq-Club]Representation question, Frederic Blanqui
- Re: [Coq-Club]Representation question,
roconnor
- Re: [Coq-Club]Representation question, Frederic Blanqui
Archive powered by MhonArc 2.6.16.