The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Does anyone know of work on basic combinatorics in Coq or other proof 
assistants?

I'm talking about the combinatorics that university computer science 
students often learn early in their careers.  Classic examples include 
counting how many poker hands there are of particular kinds.  I see some 
substantially fancier stuff in the Coq contribs.  I have to admit, I 
haven't ventured into their code to see if they also do this simpler stuff.

I'd like to be able to ask bachelor's students to solve these basic 
set-size-calculating problems in Coq, with minimal manual proof effort, 
but rigorous mathematical guarantees.

Some of you may have seen a dead-on related master's thesis online by my 
former student Andrew Haven, which I am naturally aware of; I ask this 
question to find out if we missed any related work.

I'll be happy to receive responses privately, though I imagine others on 
the list will be interested, too.

Thanks!