Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] Theory of Finite sets on infinite (Countable Domain)

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Theory of Finite sets on infinite (Countable Domain)


Chronological Thread 
  • From: Abhishek Kr Singh <>
  • To: Christian Doczkal <>
  • Cc:
  • Subject: Re: [ssreflect] Theory of Finite sets on infinite (Countable Domain)
  • Date: Wed, 22 Nov 2017 15:44:36 +0530
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:CV1XRxQWrKXfFmVn5swgVI3Sb9psv+yvbD5Q0YIujvd0So/mwa64ZRON2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnY6Uy/yPgttJ+nzBpWaz4Huj7jzqNXvZFBjhCC8eq9zJRP+gQLapMofhcM2IaYrywDVo3JOPehRznFrLFa7khDno8Oh+5gl/T4G6Nw78MsVeK/6fr84QL8QLy5uCGEz682j4RDJTQqU5nYfFHgRiDJHBgHE6FfxWZKn4XiyjfZ0xCTPZZ6+drszQzn3qv4zEBI=
Hi Christian and Pierre-Yves,

Thanks for the references. This seems to be exactly what I needed for my formalization. I will look into these links.

Thanks

On Wed, Nov 22, 2017 at 2:09 PM, Christian Doczkal <> wrote:
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>




--
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


Archive powered by MHonArc 2.6.18.

Top of Page