(Finite, discrete) Probabilities in Coq?

I am looking for a development defining finite support (sub)-probability distribution on an arbitrary type (in particular without decidable equality).

Is there any up to date library for doing proof about this kind of basic probability theory in Coq ? I am aware of ALEA but it seems rather outdated (Coq 8.3).

1 Like

Maybe your best chance is to assume excluded-middle an use any of the libraries that work that way?

I think the most recently updated libraries with probability are Polaris and infotheo.

1 Like

Have a look at classical analysis in math-comp. It will be merged with infotheo. However, neither of them is constructive, as you seem to require.
There is also FCF.

The following is a relatively recent standalone library formalizing key parts of probability theory, extracted from the Polaris project:


Indeed I was reading Tassaroti’s PhD and I noticed this library; seems pretty close in purpose to what Pierre-Yves Strub and colleagues have, right?

Should an attempt to unify them happen?

For completenes, here is a development by Pierre-Yves Strub on probability and probabilistic programs building on MathComp Analysis (which already has definitions of distributions and similar concepts):

There is now also the following paper on constructing continuous distributions using the HoTT library:

The latest developments on probability in Coq are as follows.


The ALEA probability library was revived for Coq 8.11 and later:


The Ceramist project verified probabilistic data structures such as Bloom filters in an axiom-free way:

1 Like

Yes, I think some integration makes sense.
Perhaps also with the constructive work by @VincentSe (by adding LEM).