The Coq mailing list

[��ӣ <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

  ¦°c_{i  (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