Ssreflect Users Discussion List

[Christian Doczkal <>]

Hi, 

in fact, there are several such libraries. I developed one such library [1], 
so did Pierre-Yves
Strub. The most extensive library today is probably the one by Cyrill Cohen 
[2] (also includes links to the other libraries). 

I guess the only thing in my library that might not yet be in [2] are 
operators for least and greatest fixpoints for monotone and bounded functions 
from sets to sets. If you need that, please drop me a line.

Best,
Christian

[1] 
https://redmine.ps.uni-saarland.de/projects/completness-and-decidability-for-modal-logics_project/repository/comp-dec-modal-libs
[2] https://github.com/math-comp/finmap 


On 11/22/2017 06:04 AM, Abhishek Kr Singh wrote:
> Hi, 
> 
> I am working on the formalisation of some results on finite structures 
> (graphs and posets). I was trying to explore the possibility of using 
> ssreflect library.  
> All the structures which I want to talk about in the proofs are finite. 
> However, in the very beginning I cannot assume the elements of my sets from 
> finType. 
> For example, I want to start reasoning with a finite simple graph where in 
> the middle of the proof the nodes of the graphs are replaced with cliques 
> of different sizes. Therefore the finite set type from ssreflect seems to 
> be a little more restrictive. I cannot assume in the beginning all the 
> vertices of the graph are from some finType.  
>  Is there some work which builds a finite set  library (common results on 
> finite sets) starting from the countable type in ssreflect ?
>  
> 
> -- 
> Thanks and Regards.
> *
> *Abhishek Kr. Singh,
> Research Scholar,STCS, TIFR Mumbai.
> Homepage:  http://www.tcs.tifr.res.in/~abhishek/
> 
>  http://www.tcs.tifr.res.in/people/abhishek-singh
> <http://www.tcs.tifr.res.in/people/students>