The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello Adam,

I am not sure if this is what you are looking for, but there is a bit of 
basic combinatorics in the SSReflect library. You may in particular want 
to have a look at the file binomial.v : 
http://ssr2.msr-inria.inria.fr/~jenkins/current/binomial.html

This file contains definitions and proofs around binomial coefficients, 
Pascal triangle,... It also includes combinatorial characterizations of 
the binomials, like the fact that 'C(n,k) represents the number of 
subsets of cardinal k in a set of cardinal n:

Lemma card_draws T k : #|[set A : {set T} | #|A| == k]| = 'C(#|T|, k).

While this is probably not enough for what you want (especially if you 
are looking for some automation), it may be an interesting basis or 
related work. More generally, it shows one way to deal with finite sets 
and counting arguments in Coq proofs.

Maxime.

On 12/03/2013 05:10 PM, Adam Chlipala wrote:
> 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!