The Coq mailing list

[Petar Maksimovic <petar.maksimovic AT gmail.com>]

Hi Michael,

I think in the end I'll have to go with a duplication-free list type,
and try to use just the noDup fact and not implement the entire fmap
interface. I'm afraid I don't have the resources (time, mostly) at the
moment for porting stdlib in the way you suggested.

Thanks, cheers,
Petar

On 1 October 2015 at 16:30, Soegtrop, Michael
<michael.soegtrop AT intel.com>
 wrote:
> Dear Petar,
>
> in this case it might be easier to use a set type or duplication free list 
> type. In my experience it is much more pain to carry along the witnesses in 
> dependent types than to use types which have the desired properties by 
> construction.
>
> Unfortunately the set types in the standard library are implemented with 
> modules and are not first class polymorphic, but if lists are performance 
> wise ok as set representation for you, it is easy to define. If not, I 
> would be interested to work together on porting relevant standard libraries 
> (tree based sets) to type class based first class polymorphic 
> implementations.
>
> Best regards,
>
> Michael
>
>
> -----Original Message-----
> From: 
> coq-club-request AT inria.fr
>  
> [mailto:coq-club-request AT inria.fr]
>  On Behalf Of Petar Maksimovic
> Sent: Thursday, October 01, 2015 4:14 PM
> To: 
> coq-club AT inria.fr
> Subject: Re: [Coq-Club] Records and Inductive definitions
>
> Thanks Pierre-Marie and Epiphanie,
>
> Vectors would work if my example hadn't been somewhat under-illustrative. 
> What I would really like is
>
> Record list_noDup (T : Type) := {lT :> list T; cond: noDup lT}.
>
> Inductive T : Type :=
>  | T_main : list_noDup T -> T.
>
> but for that I think I'll need some sort of workaround.
>
> Cheers,
> Petar
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
> Chairperson of the Supervisory Board: Tiffany Doon Silva
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928