Ssreflect Users Discussion List

[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,
-- 
Cyril Cohen

On 21/04/2016 11:45, Felipe Cerqueira wrote:
> Hello,
> 
> I was trying to build a simple ListSet in ssreflect on top of seq, as
> opposed to using finsets (since they only work with fintypes).
> I'm used to working with seq, so it would be nice to have a "list that is
> uniq".
> I tried the following code:
> 
> Section SeqSet.
> 
>   Context {T: eqType}.
> 
>   Record set (T : eqType) :=
>   {
>     _set_seq :> seq T ;
>     _ : uniq _set_seq (* uniqueness property*)
>   }.
> 
>   Canonical Structure setSubType T := [subType for _set_seq T by set_rect 
> T].
>   Definition set_eqMixin T := [eqMixin of set T by <:].
>   Canonical Structure mySubType_eqType T := EqType (set T) (set_eqMixin T).
> 
> End SeqSet.
>  
> Even though the code above compiles, I'm not able to do the following:
> 
>   Variable s1: set nat.
>   Variable s2: set 'I_10.
> 
> The problem is that nat is the Type, not the eqType.
> I tried having a look at finset.v to see how it is done there, but there
> was something about
> Phantom that I didn't understand.
> 
> Is there an easy way to do this? What I've been doing so far is to use
> lists everywhere
> and add the hypothesis of uniqueness separately.
> 
> Thanks,
> Felipe