coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Catalin Hritcu <catalin.hritcu AT gmail.com>
- To: Ruddy Hahn <ruddy.hahn AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Lists without repetition of occurrences
- Date: Wed, 24 Mar 2010 19:29:50 +0100
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=him/fjTPLym/i3IUeXhXuBXVLjTeSFwsdcXSP/7AKYxUoGlKhhUniNjpkbtziu8HG2 z7GU3vRLTGZ6oJq3E2NonFP/mXFnX9PiFwJJLaaGKZAUztdWK7pRMdf9Dx1cmanHnbiw eZ6RtXm/uLWLDTeE0eD8JdXP0wbpR0W5NVxnk=
Hi Ruddy,
Another solution would be to use normal lists, but to carry separate
proofs around that the list doesn't actually contain duplicates. The
standard library provides a NoDup predicate in the Lists module and
you can "add" it to a normal list type using Specif.sig. So you in
this case you would represent your snatlist type as {xs : list nat |
NoDup xs}. Carrying proofs around and constructing new ones from them
can be quite painful, but at least the type is easy to define this
way.
The other alternative I see would be again to use normal lists, and
call a "normalization" function that removes duplicate every time this
is needed. This would be needed for instance when checking if two
lists possibly containing duplicates represent the same set.
Cheers,
Catalin
PS: I'm a beginner to Coq myself and was faced with a similar problem
recently, so I would take my own advice with a big grain of salt :)
On Wed, Mar 24, 2010 at 4:45 PM, Ruddy Hahn
<ruddy.hahn AT gmail.com>
wrote:
> Hello,
> I am interested in representing lists of natural numbers without repetition
> of occurrences,
> using inductive types.
>
> Thus
> (1) The empty list is a list without repetition of occurrences.
> (2) If l is a list without repetition of occurrences, and if (n : nat) does
> not already
> occur in l, then (cons n l) is a list without repetition of
> occurrences
> An attempt at defining snatlist as an inductive type is as follows:
> (A snatlist is a list of natural numbers without repetition of occurrences.)
> Inductive snatlist : Set :=
> | snil : snatlist
> | scons : forall (n : nat) (l : snatlist), ~ (occur n l) -> snatlist
> with occur (n : nat) (l : snatlist) : Prop :=
> | ocHead : forall (n : nat) (l : snatlist) (p : ~ (occur n l)), occur n
> (scons n l p)
> | ocCons : forall (m : nat) (l : snatlist) (p: ~ (occur n l)),
> (occur m l) -> occur m (scons n l p)
> It does not work and yields error:
> (Error: Parameters should be syntactically the same for each inductive
> type.)
> How could one fix that ?
> Thanks a lot.
> R.
- [Coq-Club] Lists without repetition of occurrences, Ruddy Hahn
- Re: [Coq-Club] Lists without repetition of occurrences, Adam Chlipala
- Re: [Coq-Club] Lists without repetition of occurrences, Martijn Vermaat
- Re: [Coq-Club] Lists without repetition of occurrences, Catalin Hritcu
Archive powered by MhonArc 2.6.16.