Merge pull request #20 from affeldt-aist/compatibility_analysis_034

Compatibility analysis 034
affeldt-aist · Dec 15, 2020 · 864db9a · 864db9a
2 parents 8bdf8b5 + 65cdc49
commit 864db9a
Show file tree

Hide file tree

Showing 15 changed files with 498 additions and 209 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -0,0 +1,32 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp:1.11.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-infotheo.opam'
+          custom_image: ${{ matrix.image }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/LICENSE.txt → LICENSE b/LICENSE.txt → LICENSE
diff --git a/README.md b/README.md
@@ -0,0 +1,121 @@
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
+# A Coq formalization of information theory and linear error correcting codes
+
+[![Docker CI][docker-action-shield]][docker-action-link]
+
+[docker-action-shield]: https://github.com/affeldt-aist/infotheo/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/affeldt-aist/infotheo/actions?query=workflow:"Docker%20CI"
+
+
+
+
+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](LICENSE)
+- Compatible Coq versions: Coq 8.11 to 8.12
+- Additional dependencies:
+  - [MathComp ssreflect 1.11](https://math-comp.github.io)
+  - [MathComp fingroup 1.11](https://math-comp.github.io)
+  - [MathComp algebra 1.11](https://math-comp.github.io)
+  - [MathComp solvable 1.11](https://math-comp.github.io)
+  - [MathComp field 1.11](https://math-comp.github.io)
+  - [MathComp analysis 0.3.4](https://github.com/math-comp/analysis)
+- Coq namespace: `infotheo`
+- Related publication(s):
+  - [Formal Adventures in Convex and Conical Spaces](https://arxiv.org/abs/2004.12713) doi:[10.1007/978-3-030-53518-6_2](https://doi.org/10.1007/978-3-030-53518-6_2)
+  - [A Library for Formalization of Linear Error-Correcting Codes](https://link.springer.com/article/10.1007/s10817-019-09538-8) doi:[10.1007/s10817-019-09538-8](https://doi.org/10.1007/s10817-019-09538-8)
+  - [Reasoning with Conditional Probabilities and Joint Distributions in Coq](https://www.jstage.jst.go.jp/article/jssst/37/3/37_3_79/_article/-char/en) doi:[10.11309/jssst.37.3_79](https://doi.org/10.11309/jssst.37.3_79)
+  - [Examples of formal proofs about data compression](http://staff.aist.go.jp/reynald.affeldt/documents/compression-isita2018.pdf) doi:[10.23919/ISITA.2018.8664276](https://doi.org/10.23919/ISITA.2018.8664276)
+  - [Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes](http://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf) 
+  - [Formalization of error-correcting codes---from Hamming to modern coding theory](http://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf) doi:[10.1007/978-3-319-22102-1_2](https://doi.org/10.1007/978-3-319-22102-1_2)
+  - [Formalization of Shannon’s Theorems](https://link.springer.com/article/10.1007%2Fs10817-013-9298-1) doi:[10.1007/s10817-013-9298-1](https://doi.org/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](https://opam.ocaml.org/doc/Install.html):
+
+```shell
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam install coq-infotheo
+```
+
+To instead build and install manually, do:
+
+``` shell
+git clone https://github.com/affeldt-aist/infotheo.git
+cd infotheo
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+
+## Acknowledgments
+
+Many thanks to [various contributors](https://github.com/affeldt-aist/infotheo/graphs/contributors)
+
+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](changelog.txt).
+
+## Installation with Windows 10 (TODO: update)
+
+Installation of infotheo on Windows is less simple.
+See [this page](https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org)
+for instructions to install MathComp on Windows 10
+(or [this page](https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html) for instructions in Japanese).
+Once MathComp is installed, two options:
+
+1. You have installed MathComp with opam.
+   Then do:
+   `opam install coq-infotheo` or `git clone [email protected]:affeldt-aist/infotheo.git; opam install .`
+
+2. You have installed MathComp using unzip, untar, cd, make, make install.
+   Then do:
+   - Install MathComp-Analysis using unzip, untar, cd, make, make install
+     + Install bigenough 1.0.0 [download](https://github.com/math-comp/bigenough)
+     + Install finmap 1.5.0 [download](https://github.com/math-comp/finmap)
+     + Install analysis 0.3.2 [download](https://github.com/math-comp/analysis)
+   - Install infotheo using `coq_makefile`, `make`, `make install` as explained above
+     [download](https://github.com/affeldt-aist/infotheo)
+
+## Original License
+
+Before version 0.2, infotheo was distributed under the terms of the
+`GPL-3.0-or-later` license.
diff --git a/README.org b/README.org
diff --git a/changelog.txt b/changelog.txt
@@ -3,9 +3,18 @@ from 0.2 to 0.?
 ---------------
 
 - changed:
- + in ssrZ.v:
-   * Z_of_nat_le -> leZ_nat, Z_of_nat_lt -> ltZ_nat
-   * Z<=nat -> %:Z
+  + in ssrZ.v:
+    * Z_of_nat_le -> leZ_nat, Z_of_nat_lt -> ltZ_nat
+    * Z<=nat -> %:Z
+- removed:
+  + in classical_sets_ext:
+    set1_inj
+- renamed:
+  + in classical_sets_ext.v: 
+    image_subset -> subset_image
+- remove:
+  + in classical_sets_ext.v:
+    fullimage_subset
 
 -----------------
 from 0.1.2 to 0.2

diff --git a/coq-infotheo.opam b/coq-infotheo.opam
@@ -0,0 +1,48 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "Reynald Affeldt <[email protected]>"
+version: "dev"
+
+homepage: "https://github.com/affeldt-aist/infotheo"
+dev-repo: "git+https://github.com/affeldt-aist/infotheo.git"
+bug-reports: "https://github.com/affeldt-aist/infotheo/issues"
+license: "LGPL-2.1-or-later"
+
+synopsis: "Discrete probabilities and information theory for Coq"
+description: """
+Infotheo is a Coq library for reasoning about discrete probabilities,
+information theory, and linear error-correcting codes."""
+
+build: [
+    [make "-j%{jobs}%" ]
+    [make "-C" "extraction" "tests"] {with-test}
+  ]
+install: [make "install"]
+depends: [
+  "coq" { (>= "8.11" & < "8.13~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") }
+  "coq-mathcomp-fingroup" { (>= "1.11.0" & < "1.12~") }
+  "coq-mathcomp-algebra" { (>= "1.11.0" & < "1.12~") }
+  "coq-mathcomp-solvable" { (>= "1.11.0" & < "1.12~") }
+  "coq-mathcomp-field" { (>= "1.11.0" & < "1.12~") }
+  "coq-mathcomp-analysis" { (= "0.3.4") }
+]
+
+tags: [
+  "keyword:information theory"
+  "keyword:probability"
+  "keyword:error-correcting codes"
+  "logpath:infotheo"
+]
+authors: [
+  "Reynald Affeldt, AIST"
+  "Manabu Hagiwara, Chiba U. (previously AIST)"
+  "Jonas Senizergues, ENS Cachan (internship at AIST)"
+  "Jacques Garrigue, Nagoya U."
+  "Kazuhiko Sakaguchi, Tsukuba U."
+  "Taku Asai, Nagoya U. (M2)"
+  "Takafumi Saikawa, Nagoya U."
+  "Naruomi Obata, Titech (M2)"
+]
diff --git a/dune b/dune
@@ -0,0 +1,7 @@
+; This file was generated from `meta.yml`, please do not edit manually.
+; Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+(coq.theory
+ (name infotheo)
+ (package coq-infotheo)
+ (synopsis "Discrete probabilities and information theory for Coq"))
diff --git a/dune-project b/dune-project
@@ -0,0 +1,6 @@
+; This file was generated from `meta.yml`, please do not edit manually.
+; Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+(lang dune 2.5)
+(using coq 0.2)
+(name infotheo)
diff --git a/index.md b/index.md
@@ -0,0 +1,59 @@
+---
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+title: A Coq formalization of information theory and linear error correcting codes
+lang: en
+header-includes:
+  - |
+    <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
+    <style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
+    <style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
+    <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
+    <style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
+---
+
+<div style="text-align:left"><img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
+<a href="https://github.com/affeldt-aist/infotheo">View the project on GitHub</a>
+<img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"></div>
+
+## About
+
+Welcome to the A Coq formalization of information theory and linear error correcting codes project website!
+
+Infotheo is a Coq library for reasoning about discrete probabilities,
+information theory, and linear error-correcting codes.
+
+This is an open source project, licensed under the LGPL-2.1-or-later.
+
+## Get the code
+
+The current stable release of A Coq formalization of information theory and linear error correcting codes can be [downloaded from GitHub](https://github.com/affeldt-aist/infotheo/releases).
+
+## Documentation
+
+
+Related publications, if any, are listed below.
+
+- [Formal Adventures in Convex and Conical Spaces](https://arxiv.org/abs/2004.12713) doi:[10.1007/978-3-030-53518-6_2](https://doi.org/10.1007/978-3-030-53518-6_2)
+- [A Library for Formalization of Linear Error-Correcting Codes](https://link.springer.com/article/10.1007/s10817-019-09538-8) doi:[10.1007/s10817-019-09538-8](https://doi.org/10.1007/s10817-019-09538-8)
+- [Reasoning with Conditional Probabilities and Joint Distributions in Coq](https://www.jstage.jst.go.jp/article/jssst/37/3/37_3_79/_article/-char/en) doi:[10.11309/jssst.37.3_79](https://doi.org/10.11309/jssst.37.3_79)
+- [Examples of formal proofs about data compression](http://staff.aist.go.jp/reynald.affeldt/documents/compression-isita2018.pdf) doi:[10.23919/ISITA.2018.8664276](https://doi.org/10.23919/ISITA.2018.8664276)
+- [Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes](http://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf) 
+- [Formalization of error-correcting codes---from Hamming to modern coding theory](http://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf) doi:[10.1007/978-3-319-22102-1_2](https://doi.org/10.1007/978-3-319-22102-1_2)
+- [Formalization of Shannon’s Theorems](https://link.springer.com/article/10.1007%2Fs10817-013-9298-1) doi:[10.1007/s10817-013-9298-1](https://doi.org/10.1007/s10817-013-9298-1)
+
+## Help and contact
+
+- Report issues on [GitHub](https://github.com/affeldt-aist/infotheo/issues)
+
+## Authors and contributors
+
+- Reynald Affeldt, AIST
+- Manabu Hagiwara, Chiba U. (previously AIST)
+- Jonas Senizergues, ENS Cachan (internship at AIST)
+- Jacques Garrigue, Nagoya U.
+- Kazuhiko Sakaguchi, Tsukuba U.
+- Taku Asai, Nagoya U. (M2)
+- Takafumi Saikawa, Nagoya U.
+- Naruomi Obata, Titech (M2)
+