A Coq formalization of information theory and linear error correcting codes

Infotheo is a Coq library for reasoning about discrete probabilities, information theory, and linear error-correcting codes.

Meta

• Author(s):
  • Reynald Affeldt, AIST (initial)
  • Manabu Hagiwara, Chiba U. (previously AIST) (initial)
  • Jonas Senizergues, ENS Cachan (internship at AIST) (initial)
  • Jacques Garrigue, Nagoya U.
  • Kazuhiko Sakaguchi, Tsukuba U.
  • Taku Asai, Nagoya U. (M2)
  • Takafumi Saikawa, Nagoya U.
  • Naruomi Obata, Titech (M2)
• License: LGPL-2.1-or-later
• Compatible Coq versions: Coq 8.13
• Additional dependencies:
  • MathComp ssreflect 1.12
  • MathComp fingroup 1.12
  • MathComp algebra 1.12
  • MathComp solvable 1.12
  • MathComp field 1.12
  • MathComp analysis 0.3.6
• Coq namespace: infotheo
• Related publication(s):
  • Formal Adventures in Convex and Conical Spaces doi:10.1007/978-3-030-53518-6_2
  • A Library for Formalization of Linear Error-Correcting Codes doi:10.1007/s10817-019-09538-8
  • Reasoning with Conditional Probabilities and Joint Distributions in Coq doi:10.11309/jssst.37.3_79
  • Examples of formal proofs about data compression doi:10.23919/ISITA.2018.8664276
  • Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes
  • Formalization of error-correcting codes---from Hamming to modern coding theory doi:10.1007/978-3-319-22102-1_2
  • Formalization of Shannon’s Theorems doi:10.1007/s10817-013-9298-1

Building and installation instructions

The easiest way to install the latest released version of A Coq formalization of information theory and linear error correcting codes is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-infotheo

To instead build and install manually, do (using GNU make):

git clone https://github.com/affeldt-aist/infotheo.git
cd infotheo
make   # or make -j <number-of-cores-on-your-machine> 
make -C extraction tests
make install

Acknowledgments

Many thanks to several contributors (committers).

The principle of inclusion-exclusion is a contribution by Erik Martin-Dorel (University Toulouse III Paul Sabatier, IRIT research laboratory) (main theorem: Pr_bigcup_incl_excl; commit 956096859ed89325b2bb74033690ac882bbcd64e)

The variable-length source coding theorems are a contribution by Ryosuke Obi (Chiba U. (M2)) (commit a67da5e24eaaabb345d225a5bd0f5e86d35413a8) (with Manabu Hagiwara and Mitsuharu Yamamoto)

Commit 64814f529c1819684c4b8060d0779c24c6339041 was originally by Karl Palmskog

The formalization of modern coding theory is a collaboration with K. Kasai, S. Kuzuoka, R. Obi

Y. Takahashi collaborated to the formalization of linear error-correcting codes

This work was partially supported by a JSPS Grant-in-Aid for Scientific Research (Project Number: 25289118), a JSPS Grand-in-Aid for Scientific Research (Project Number: 18H03204)

Documentation

Each file is documented in its header.

Changes are documented in changelog.txt.

Installation with Windows 10

Installation of infotheo on Windows is less simple. See this page for instructions to install MathComp on Windows 10 (or this page for instructions in Japanese).

Once MathComp is installed (with opam), do opam install coq-infotheo or git clone git@github.com:affeldt-aist/infotheo.git; opam install .

Original License

Before version 0.2, infotheo was distributed under the terms of the GPL-3.0-or-later license.