Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

bernoulli probability measure #895

Merged
merged 4 commits into from
May 27, 2024
Merged

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Apr 12, 2023

Motivation for this change

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

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • 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 affeldt-aist added enhancement ✨ This issue/PR is about adding new features enhancing the library TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. labels Apr 12, 2023
@affeldt-aist affeldt-aist added this to the 0.6.2 milestone Apr 12, 2023
Copy link
Contributor

@zstone1 zstone1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

theories/measure.v Outdated Show resolved Hide resolved
Variables (R : realType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R).
Local Open Scope ring_scope.

Definition bernoulli : set _ -> \bar R := measure_add
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a lot of text for what would be p 1_true + (1-p) 1_false on paper. It took me ~3 minutes to read, which is maybe an indictment of my own reading comprehension. But still, I would love to make this definition clean, and handle the measure stuff on the next line. Is there a way to do this?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You are totally right. It is time to make this happen. I turn this PR into a draft and work on this ASAP.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Part of the problem is to have the + notation for non-negative measures. Wouldn't it be better to wait for the isZsemimodule interface that comes with MathComp 2.0?

@affeldt-aist affeldt-aist marked this pull request as draft April 16, 2023 04:53
@affeldt-aist
Copy link
Member Author

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 affeldt-aist modified the milestones: 0.6.2, 0.6.3 Apr 16, 2023
@affeldt-aist affeldt-aist force-pushed the bernoulli branch 3 times, most recently from 5296b6a to 87540b5 Compare April 26, 2023 10:27
Variables (R : realType) (p : {i01 R}).

Definition bernoulli : set _ -> \bar R := measure_add
(mscale (NngNum (itv_ge0 p)) (dirac true))
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To hide NngNum (itv_ge0 p) I was hoping to turn p%:inum into an instance of non-negative number so as to use p%:inum%:nng instead (which is not much more readable but a bit more in the spirit). The following addition to itv.v is not enough:

Section tmp.
Context {T : numDomainType}.

Lemma i01_snum_subproof (p : {i01 T}) : Signed.spec 0%R ?=0 >=0 (Itv.r p).
Proof. by rewrite /=. Qed.

Canonical i01_snum (x : {i01 T}) := Signed.mk (i01_snum_subproof x).
End tmp.

Obviously, I am missing something. @proux01

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, I would also have expected it to work, I reduced it to the following minimal example

Section Example.
Variable R : realDomainType.

Check erefl : @eq R 0 (Signed.r _).  (* correctly infers zero_snum *)
Check erefl : @eq R (Signed.r _) 0.  (* same *)

Variable x : {i01 R}.

Check erefl : @eq R (Signed.r _) (Itv.r x).  (* correctly infers i01_snum *)
Fail Check erefl : @eq R (Itv.r x) (Signed.r _).  (* why? I would also have expected the same result *)

and unfortunately the phantom behind %:sgn hence %:nng seems closer to the second failing case.

@CohenCyril would you have an idea of what's happening?

Anyhow, all this advocates for the project of merging signed and itv in the future.

@affeldt-aist affeldt-aist modified the milestones: 0.6.3, 0.6.4 Jun 20, 2023
@affeldt-aist affeldt-aist modified the milestones: 0.6.4, 0.6.5 Jul 31, 2023
@affeldt-aist affeldt-aist modified the milestones: 0.6.5, 0.6.6 Sep 27, 2023
@affeldt-aist affeldt-aist modified the milestones: 0.6.6, 0.6.7 Nov 10, 2023
@affeldt-aist affeldt-aist modified the milestones: 0.6.7, 0.6.8 Jan 7, 2024
@affeldt-aist affeldt-aist modified the milestones: 0.7.0, 1.0.0 Jan 17, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.0.0, 1.1.0 Jan 24, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.1.0, 1.2.0 Mar 14, 2024
@affeldt-aist affeldt-aist removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Apr 10, 2024
@affeldt-aist
Copy link
Member Author

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 #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 87540b5

@affeldt-aist affeldt-aist requested a review from t6s April 10, 2024 07:53
@affeldt-aist affeldt-aist marked this pull request as ready for review April 10, 2024 07:53
@affeldt-aist
Copy link
Member Author

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

@affeldt-aist
Copy link
Member Author

affeldt-aist commented May 8, 2024

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 affeldt-aist requested review from hoheinzollern and t6s and removed request for t6s May 8, 2024 15:41
@affeldt-aist
Copy link
Member Author

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

theories/measure.v Outdated Show resolved Hide resolved
Copy link
Member

@t6s t6s left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me and ready to be merged, leaving two points to future PRs:

  1. Lemmas around measurable_fun_bool should be refactored. This should be easy and I have already prepared a branch to be PRed.
  2. Bernoulli is an instance of amore generic finitely-supported probability measure, which in turn an instance of adiscrete probability measure. This should be put in a hierarchy.

Co-authored-by: Takafumi Saikawa <[email protected]>
Copy link
Collaborator

@hoheinzollern hoheinzollern left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me.

@affeldt-aist affeldt-aist merged commit e00d6f7 into math-comp:master May 27, 2024
16 checks passed
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this pull request Jun 20, 2024
* bernoulli, binomial, uniform distr

Co-authored-by: Takafumi Saikawa <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants