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
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-probauntil 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: Feb 06 2023 at 00:03 UTC