Ssreflect Users Discussion List

[Georges Gonthier <>]

  I assume you have a function that injects seq T into finset T (say, 
finset_of) ? then you only need to enumerate all sublists of a given list, 
which you can do combinatorialy as you did before with the sorted lists (the 
uniq predicate gives you the property you obtained via sorted, that any item 
does not reappear later on).
   You can also go for a slightly more abstract approach, like using the 
standard enumeration of all n-tuples of Booleans along with the mask function 
to get the sublists, i.e., something like
  powerset s := let e := elems s in let mT := (size e).-tuple bool in
                finset_of (map (fun m : mT => finset_of (mask m e)) (enum mT))
should work, and you should get most of the properties you need from the 
library. Note that you can show that the argument to both calls of finset_of 
satisfy the uniq predicate, so you will easily be able to show that powerset 
s has 2 ^ size (elems s) elements.

  Georges

-----Original Message-----
From: Christian Doczkal [] 
Sent: 03 August 2010 17:12
To: 
Subject: RE: FSets with powerset operation

Hello

> More specifically, you should use the Choice interface, because it is
> more directly suited to your purposes, and is more general and more
> widely available than the Countable interface 

> there’s a little theory of that developed by Cyril Cohen in quotient.v
> (but this is still experimental work-in-progress).

Is this available somewhere

> In your case this would amount to representing finite sets with
> something like
> 
>       Record { elems : seq T ; _ : uniq elems; elems == choose (perm_eq 
> elems) elems }
> 
> with T : choiceType.

Unfortunately?, I already had developed the theory up to the powerset
construction using sorted/contType. I just tried to port this to
choiceType wich worked nicely except for the definition of powerset.

My definition of powerset uses recursion on the sorted list and
therefore relies on the fact that the representation invariant is
preserved unter behead.

So how could one go about defining the powerset with this
representation.

-- 
Regards
Christian