Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Lists without repetition of occurrences

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lists without repetition of occurrences


chronological Thread 
  • 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.




Archive powered by MhonArc 2.6.16.

Top of Page