search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

use topology.fct_comRingType for RVs #67

Open t6s opened 3 years ago

t6s commented 3 years ago

This is an experiment to switch algebraic operations on random variables to the generic ones on ringType.

Some lemmas in proba.v, aep.v, typ_seq.v needed rather big modifications, while the proofs in other files could be accommodated just by changing rewrite /sq_RV /comp_RV to rewrite sq_RV_pow2.

t6s commented 3 years ago

One concern is that I could not use generic lemmas not so much I originally expected. I am afraid that the usefulness of the ring structure needs to be more clearly shown for this draft to be turned into a proper PR.

t6s commented 3 years ago

Oops, inv is indeed wrong. I have renamed it E_opp_RV. (I would rather keep neg for boolean negation.)

affeldt-aist commented 3 years ago

Could you put some information in the changelog? (At least about the potentially breaking changes.) In any case, good to see things get little bit tidier. Thanks!

t6s commented 3 years ago

I have noticed that this change imports the axiom of choice in proba.v, which I expect cause some controversy. I am now changing my mind to define the ring structure in a separate file and let a user import it when needed.

hoheinzollern commented 10 months ago

This is useful to have in robustmean, could you revive this and put it in the next release?

t6s commented 10 months ago

This is useful to have in robustmean, could you revive this and put it in the next release?

Let's do it! I think I can look at this after completing the current batch of cleaning in infotheo (removal of R).

I am afraid a release including this work will not be that quick, since completing it will require some experiments to settle some design choices.

Uses in robustmean will help this process, and so I suggest using a development branch for a while, not waiting for a release.

t6s commented 10 months ago

The proper way for RVs to behave like fct_ringType will be to definene them in the hierarchy, inheriting definitions from functions.v.

I would really like to use HB for such an extension. What is the current status of the compatibility between infotheo and HB-based analysis? @affeldt-aist

affeldt-aist commented 10 months ago

I didn't try but according to https://hal.science/hal-04225130/document (see page 2) and since we are not building any deep hierarchy using canonicals in infotheo (indeed we are now using HB for convex and scaled convex) this should almost be transparent (unless we try to get rid of our ordered structure, in which case there is a bit of work but maybe not much). Once this is done in a branch of infotheo, we just need to compile against this branch.

affeldt-aist commented 10 months ago

I am not saying that we should do it asap though, on the contrary, considering practical aspects, it is maybe more reasonable to clean up infotheo for robustmean as much as possible first and then do the port once MathComp-Analysis 1.0 is released (the plan is January 2024, beginning of the month at the latest).