Ssreflect Users Discussion List

[Felipe Cerqueira <>]

Hi Christian, Hi Cyril,

Thanks for the links.
I think in my formalization I haven't compared two sets for equality so far.
There's a specific list (set) where I need to count or \sum over the 
elements
that satisfy some property. To prove tight bounds I need to know there 
aren't duplicates.

But I'll have a look at the libraries. They seem quite useful.

Felipe

On 4/21/16 4:48 PM, Christian Doczkal wrote:
> Hello Felipe,
>
> I know of three implementation of finite sets as quotients on seq. Maybe
> one of them fulfills your needs:
>
> 1. A simple prototype implementation by Pierre-Yves Strub
> https://github.com/strub/ssrmisc
>
> 2. A finite set library developed by myself (fset.v) :
> https://redmine.ps.uni-saarland.de/projects/completness-and-decidability-for-modal-logics_project/repository/comp-dec-modal-libs
>
> 3. The Cyril's Library mentioned below.
>
> Regards
> Christian
>
> Am 21.04.2016 um 16:43 schrieb Cyril:
> > Dear Felipe,
> > uniq asserts that the list contains no duplicates, but in order to
> > guarantee the canonicity of the list representing your set, you need a
> > little bit more than that, namely the choice of a canonical representative
> > for the list of elements, either by sorting them or by using a choice 
> > function.
> > I have been developing such a library here:
> >   https://github.com/Barbichu/finmap
> > I'm working on a new revision at the time which will mainly solve some
> > inconsistency with the "comprehension" notations.
> > Best regards,