Hello,

we are trying to use coq-proba (https://github.com/jtassarotti/coq-proba) but it seems that distributions (`distrib`

) cannot take into account a Setoid equality. Is this true? More precisely when reasoning on a `distrib A`

one cannot use setoid `rewrite`

.

you will probably have to open an issue in the repo or email the author, I don't think we have proba users here...

Hi I was not aware of `coq-proba`

until now, I wonder how it compares to https://github.com/affeldt-aist/infotheo and https://github.com/math-comp/analysis/blob/master/theories/altreals/distr.v which cover discrete probability theory

CC @Reynald Affeldt @Pierre-Yves Strub @Joseph Tassarotti

there is a thread here which does some (shallow) comparisons of these libraries: https://coq.discourse.group/t/finite-discrete-probabilities-in-coq/166

One aspect is the monad that mixes nondeterminism and probabilistic choice, whether you want to take idempotence into account or not (see https://arxiv.org/abs/2003.09993 and https://dl.acm.org/doi/10.1145/3290377).

Thanks for the infos!

Cyril Cohen said:

Hi I was not aware of

`coq-proba`

until now, I wonder how it compares to https://github.com/affeldt-aist/infotheo and https://github.com/math-comp/analysis/blob/master/theories/altreals/distr.v which cover discrete probability theory

CC Reynald Affeldt Pierre-Yves Strub Joseph Tassarotti

Me neither. Anway, i still have to make `distr.v`

an actual library :/

Proba is derived from the work in this paper: https://iris-project.org/pdfs/2019-popl-polaris-final.pdf

Ok. the library seems pretty advanced

i'm not maintaining `distr.v`

anymore, but i should put it in a repo. for tracability

Am I to understand that the only people tackling continuous probability distributions are these folk?

I believe the work based on coquelicot does it too, but based on classical maths.

I think coq-proba has also a notion of continuous probabilities. @Joseph Tassarotti may confirm.

Yes, coq-proba is essentially a collection of whatever I needed for my dissertation work (or felt like formalizing during my phd), so it's got a bit of unusual variety (e.g. the non-determinism monads for my POPL 2019 paper, stuff about proving tail bounds related to my ITP 2018 paper, etc). There is support for continuous probabilities and basic measure theory/lebesgue integration. However, that only handles finite measures. Subsequently, there has been work on more general measures/integration theory from math-comp groups and by Sylvie Boldo and her collaborators, extending coquelicot.

Last updated: Dec 05 2023 at 05:01 UTC