The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

I don't really see any advantage in using ListSet. Either just stick
to List or use actual MSets. I enclose a version which uses lists
which does not repeat elements of a set (although it repeats sets).
What exactly are your demands? If you tell us what you want to use
this for, we can probably tell you how to avoid using it.

With kind regards,

Andrej

2011/11/9 左樱 
<phoebezz AT 163.com>:
> Hi guys:
>    Thank you  very much for all your guidance.
>    I read something about list combination in Caml and rewrote the function
> 'comb' in coq. But I found it didn't meet my demand.
>    So I try to wrote another function 'combList' and tested it successfully.
> However, I think my definition of 'combList' is too complex that I used
> another 3 auxiliary function in the definition. It troubles me a lot when I
> try to prove some lemmas relates to it .  So can you help me to simplify
> 'combList'?  Thanks!
>     The related codes are in the attachment .
>
> Best,
> Phoebe
>
>
>
>
>
> -------- Forwarding messages --------
> From: "左樱" 
> <phoebezz AT 163.com>
> Date: 2011-11-06 21:47:43
> To: 
> coq-club AT inria.fr
> Subject: How to define combination in coq
> Hi guys,
>           I'm trying to define a function to compute the combination of
> sets, which pick an element from every set and combine into another set. Let
> ci be the number of element in set i .The total number of elements in result
> set will be
>   Πci  (0<i<n)
> for example
>  Definition  sets :={{"a","b"},{"c","d"},{"e"}}
>   combination (sets)  =
> {{“a”,"c","e"},{"a","d","e"},{“b”,"c","e"},{"b","d","e"}}
> Can you give me some guidance about the definition of combination function?
> Thank you very much.
>
>
>
>

Attachment: combine.v
Description: Binary data