Skip to Content.
Sympa Menu

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

Subject: Ssreflect Users Discussion List

List archive

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


Chronological Thread 
  • From: Abhishek Kr Singh <>
  • To:
  • Subject: [ssreflect] Theory of Finite sets on infinite (Countable Domain)
  • Date: Wed, 22 Nov 2017 10:34:02 +0530
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:2ibjCBxBBokCBU7XCy+O+j09IxM/srCxBDY+r6Qd0u0SIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSip9iQfFBHyPhZdI//vX4/UlcW+keG04ZzaJQtS1xSnZrYnBR+2rB7Ru8peopEqEac3xRuB9nJCe+VNxW5rY0+UhT7z486x+Nho9CEG6KFpzNJJTaivJ/dwdrdfFjlza20=
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


Archive powered by MHonArc 2.6.18.

Top of Page