Ssreflect Users Discussion List

On Tue, 3 Aug 2010, Christian Doczkal wrote:

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

(choose P) is presumably an idempotent operation. I think you should just 
be able to behead the list and then apply (choose (perm_Eq elems)) to the 
tail of the list to get a finite set for the tail.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''