The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

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.