Drop use of experimental_reals (mathcomp-analysis)

[MarkusKL]

Motivation: Currently, the definitions and lemmas about sub-distributions are drawn from the sub-package experimental_reals from mathcomp-analysis. The theory relies on some admitted interchange_psum theorem while newer mathcomp-analysis theories based on Lebesgue integral are admitless.

Preliminary work here: https://github.com/MarkusKL/ssprove/tree/giry-experiments
Which depends on work in: math-comp/analysis#1608

[spitters]

It would be great to move away from the experimental reals.

[spitters]

Talking to @alejandroag, his Giry monad may be more complex than what we need.
Perhaps it is better to port the existing formalization of distributions to the std reals.

[MarkusKL]

Porting which parts, the experimental_reals code? And to this this and related theories? An important and hard result that we rely on is the swapping of abs. convergent sums/integrals. Is is already somewhere in the Stdlib?

[spitters]

I understand that the "experimental reals" are deprecated in MC. So, I guess there is a porting effort in MCA.
@affeldt-aist, @hoheinzollern could you enlighten us about the plans, and the status of the porting effort?

[affeldt-aist]

What is in the experimental_reals subdirectory and opam package has been there from the first release of MathComp-Analysis, is used by its main developer @strub, and as of today the plan is to keep it that way. It is in a subdirectory to better identify its wip status and because a different approach was judged more comfortable to develop generic measure theory. The need to complete experimental_reals and to uniformize the development has been identified (math-comp/analysis#255) but unfortunately nobody has found the time to work on it.
I think that the only problem is to find out how to sort it out: should it be a bridge or a port? A concrete use-case could provide an answer and then it is a matter of focusing and helping each other for a week or two.

[strub]

A few months ago (if not less), I asked for pulling out the distr library so that I can maintain it (I think that nearly of the contents of this file has been written by myself) and do the changes that I need for my own projects. Killing the 2 admits should be easy - I already proved them in EasyCrypt a few years ago. The idea has been rejected because of the ssprove dependency.

So I am proposing it a second time: I am ok with distr being pulled out of mathcomp-analysis. If so, I'll create a separate package that will contains distr & local dependencies, that will be admit-free & that will be maintained (because I need it and I don't have any incentive to move to a new library, this one is working well for all my needs). Of course, it will require mathcomp-analysis as a dependency.

The transition could be smooth: all the stakeholders are in this thread and we should be able to synchronize.

[affeldt-aist]

I am happy to help with whatever solution that can help you (@strub and SSProve) moving forward!

[MarkusKL]

I am happy to make the necessary updates to SSProve, and I think that it would be great to get rid of the admitted lemmas this way. I also know of some lemmas (such as distr_ext) that should be pushed upstream to the new package.

It is good to hear that psum_interchange is actually provable. I have been back and forth on that point.

[spitters]

Thanks @affeldt-aist @strub that clarifies the situation and gives a good way forward.

@alejandroag how do your plans with the Giry monad compare with the plans of @strub ?

[spitters]

Just to clarify, we would like to continue to use the discrete probabilities (distr) in SSProve, but with @MarkusKL we would sleep better if the admitted lemmas were proven. Which encoding of the reals to use is less important for us, as long as it fits with the long-term plans of MCA.