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

new lemmas for infotheo #64

Closed hoheinzollern closed 4 months ago

hoheinzollern commented 3 years ago

Dear infotheo authors, I want to point out that my co-authors and I have a paper on the formalization of bounds on the trimmed mean algorithm that uses infotheo. It has been accepted at PPDP this year (https://ppdp2021.github.io/#accepted, the paper is called "Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation", soon to be available) and you can find the source code of the formalization here: https://github.com/ieva-itu/robustmean/blob/main/robustmean.v

We are thankful for the all the development of probability theory that we used in our paper, and we think you might appreciate some lemmas that should belong to infotheo more than our development. As we are all novice Coq programmers and not used to the mathcomp style, I'd appreciate if you could take a look at the code and see whether you're interested in integrating it here, and maybe help us match the style of the infotheo package. This is also why I'm not making a pull request yet.

affeldt-aist commented 3 years ago

Congratulations! I'm looking forward to reading your paper. We are interesting in integrating it and I am willing to spend time on it. Maybe the easiest way is to PR so that we can exchange about the code.

hoheinzollern commented 3 years ago

Sounds great, and thanks for the offer! I'll mention here my colleagues @ieva-itu and @carstenschuermann so they are in the loop. We'll start a pull request soon.

t6s commented 3 years ago

@hoheinzollern I can help modifying the proof script into a more mathcomp-ish style. Do you prefer such a change?

hoheinzollern commented 3 years ago

That would be very appreciated, of course I'd like to learn in the process if possible :) Could we do this together?

affeldt-aist commented 4 months ago

Lemmas made their way into master with commit https://github.com/affeldt-aist/infotheo/commit/45c68bd43c9ae1c7ead5e7c7fd80c23ec72b700f