Ssreflect Users Discussion List

[Georges Gonthier <>]

  While the bigops library does allow for iteration over explicit sequences, 
most of the theory assumes the index type is finite because this simplifies 
the interface quite a bit. Any bigop can be rebased over a finType (namely, 
'I_something) by rewriting with big_nth and big_mkord. In your specific case, 
you may want to use the eq_big_term lemma to switch from indexing over s : 
seq (s.t. uniq s holds) to indexing over finset_of s. Similarly you could 
prove the equivalent of big_setU1 using the rot_to lemma without induction.
  Finally, when you'll have to resort to induction it will most likely be on 
the size of the set rather than its structural representation, so you should 
familiarize yourself with the ssreflect idioms for doing that.

   Cheers,
Georges

(CC'ing the ssreflect list again)

-----Original Message-----
From: Christian Doczkal [] 
Sent: 05 August 2010 12:21
To: Georges Gonthier
Subject: E: FSets with powerset operation

Dear Georges

Thanks a lot for the pointer. I guess in this case I can wait for the
release of ssreflect 1.3. Your powerset definition dramatically
simplifies my proof of the powerset axiom 

(X \in powerset Y = X subset Y) 

The only thing I'm still a little worried about with the choiceType
version is the use of big operators wich (as far as I can tell) work
only by coercing my fsets to seq. And the induction principle on the
seq's in the representation is useless, as I mentioned before. So how,
if not by induction would one go about proving any meaningful properties
of a definition like Union below?

Definition Union (P : {fset {fset T}}) : {fset T} := \big[@union T/empty]_(Y 
<- P) Y.

-- 
Regards
Christian

PS. sorry for the cut of mail I sent earlier.