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).
Maybe your best chance is to assume excluded-middle an use any of the libraries that work that way?
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:
Yes, I think some integration makes sense.
Perhaps also with the constructive work by @VincentSe (by adding LEM).