bernoulli probability measure

[affeldt-aist]

Motivation for this change

Bernoulli probability measure as defined in ~~PR #749~~ draft PR #912

Things done/to do

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md

• [x] added corresponding documentation in the headers

Compatibility with MathComp 2.0

• [ ] I added the label TODO: HB port to make sure someone ports this PR to the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

The new interval stuff may be cleaner here. And I am worried about legibility if we have to add these [measure of ] annotations to every term.

Note that the [measure of _] annotations are really here for compatibility with Coq 8.15.

[affeldt-aist]

One year ago this PR introduced the Bernoulli probability measure. The main problem pointed at in particular by @zstone1 was that the definition was not very readable. It was using {i01 R}. In essence, this has not changed: the new definition uses non-negative reals and a proof that they are smaller than one (similar business).

This update also defines the binomial distribution binomial_prob and the uniform distribution uniform_prob.

This update also defined "total" versions of the Bernoulli and binomial distributions: bernoulliT and binomial_probT. bernoulliT takes any real p and returns a dummy probability measure when p is not in [0,1], and similarly for binomial_probT so that for example bernoulliT satisifies:

Lemma bernoulliTE p U : 0 <= p <= 1 ->
  (bernoulliT p U = p%:E * \d_true U + (`1-p)%:E * \d_false U)%E.

which is close to the formulation that @zstone1 was expected in his first review comment.

We have been using all these distributions to verify a probabilistic program using https://github.com/math-comp/analysis/pull/912

I understand that @hoheinzollern has also been using the definition of the Bernoulli probability measure in his own work.

So, still not perfect but usable in practice, so what about merging it (possibly marking it as experimental)?

PS: Here is the only commit of the PR before update, for reference https://github.com/math-comp/analysis/pull/895/commits/87540b53429a3c9142d0dc1957934e1227b66d62

[affeldt-aist]

fyi: @proux01 @hoheinzollern (comments also welcomed if you have time)

[affeldt-aist]

I still have to move a few things around and to make the changelog and the doc but I think that it addresses the comments from the last meeting, mainly that the total versions are now the default and that the use of non-negative numbers and proofs that they are smaller than 1 are reduced to a minimal. Note that this code is actually a subset of PR #912 so it has been "tested".

[affeldt-aist]

@hoheinzollern @t6s the PR is now complete (with changelog and doc)