Stream: Coq users

Topic: coq-proba


view this post on Zulip Pierre Courtieu (Jan 06 2022 at 14:00):

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.

view this post on Zulip Karl Palmskog (Jan 07 2022 at 16:15):

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

view this post on Zulip Cyril Cohen (Jan 07 2022 at 18:09):

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

view this post on Zulip Karl Palmskog (Jan 07 2022 at 22:22):

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

view this post on Zulip Reynald Affeldt (Jan 08 2022 at 01:49):

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).

view this post on Zulip Pierre Courtieu (Jan 08 2022 at 09:15):

Thanks for the infos!

view this post on Zulip Pierre-Yves Strub (Jan 13 2022 at 12:05):

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 :/

view this post on Zulip Karl Palmskog (Jan 13 2022 at 12:07):

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

view this post on Zulip Pierre-Yves Strub (Jan 13 2022 at 12:07):

Ok. the library seems pretty advanced

view this post on Zulip Pierre-Yves Strub (Jan 13 2022 at 12:08):

i'm not maintaining distr.v anymore, but i should put it in a repo. for tracability

view this post on Zulip Quinn (Jan 14 2022 at 04:44):

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

view this post on Zulip Bas Spitters (Jan 18 2022 at 17:11):

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

view this post on Zulip Pierre Courtieu (Jan 18 2022 at 17:44):

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

view this post on Zulip Joseph Tassarotti (Jan 18 2022 at 22:36):

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