The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Wed, 24 Mar 2010 19:29:50 +0100, Catalin Hritcu  
<catalin.hritcu AT gmail.com> a écrit:

> 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:

To represent sets of positive, I prefer to use a PositiveMap unit
(I have my own version of it, in which PositiveMap.equal a b = true => a =  
b).
It is mainly Patricia trees.

If you prefer to use nat, a funny way is to put "true" in the slot  
corresponding to the number;
the biggest being omitted.

So {3; 5; 8} is represented by
[false (*0*);
 false (*1*);
 false;
 true  (*3*);
 false;
 true;
 false;
 false
]
or even, define a:
Inductive natset :=
| Last: natset
| Add: natset -> natset
| Skip: natset -> natset.
(or use BinPos.positive which is isomorphic)

This makes a bijection from list bool to non-empty set.
Managing empty sets can be done with an "option (list bool)".

That seems stupid and inefficient, but in fact it is computationnaly  
faster for coq:
The previous structure:
 cons (S (S (S O))) (cons (S (S (S (S (S O)))))) (cons (S (S (S (S (S (S  
(S (S O)))))))) nil)
 23 constructors used
mine:
 Skip (Skip (Skip (Add (Skip (Add (Skip (Skip Last)))))))
 9 constructors used

adding/removing an element is also computationnaly faster, as you don't  
use the "nat_eq" function.

In fact, it is "Patricia stack" instead of "Patricia tree" and like  
Patricia trees, you can compress path
by using differences: {3; 5; 8} can be represented by: [3; 2 (*+3=5*); 3  
(*+5=8*)]
(and also like Patricia trees, you won't really gain in coq, as the  
constructors of the nodes we skip are just
replaced by the constructors of the positive expressing the differences)

So, to represent sets, lists with no duplicates are not ideal IMHO.
But if you need to keep the order in which you got them, that is another  
thing...

So to

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay