From 0aa8978666ea48c7d3fb2456bc6b9cb3524d53da Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 14 Dec 2020 02:43:33 +0900 Subject: [PATCH 1/2] compatibility with mathcomp-analysis.0.3.4 --- changelog.txt | 2 ++ lib/classical_sets_ext.v | 32 ++++------------- probability/convex_choice.v | 2 +- probability/necset.v | 72 ++++++++++++++++++------------------- 4 files changed, 45 insertions(+), 63 deletions(-) diff --git a/changelog.txt b/changelog.txt index 0fb7e7ec..d1288dd8 100644 --- a/changelog.txt +++ b/changelog.txt @@ -6,6 +6,8 @@ from 0.2 to 0.? + 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 ----------------- from 0.1.2 to 0.2 diff --git a/lib/classical_sets_ext.v b/lib/classical_sets_ext.v index a5e7430a..bf446e0d 100644 --- a/lib/classical_sets_ext.v +++ b/lib/classical_sets_ext.v @@ -17,15 +17,11 @@ Local Open Scope classical_set_scope. Lemma eq_imagel (f g : T -> U) A : (forall a, A a -> f a = g a) -> f @` A = g @` A. Proof. -by move=> H; apply eqEsubset=> a; +by move=> H; rewrite eqEsubset; split=> a; case => x Xx <-; [rewrite H | rewrite -H] => //; exists x. Qed. -(* TODO: useful? *) -Lemma set1_inj : injective (@set1 T). -Proof. by move=> a b; rewrite /set1 => /(congr1 (fun f => f a)) <-. Qed. - -Lemma image_subset (f : T -> U) A (Y : set U) : +Lemma subset_image (f : T -> U) A (Y : set U) : f @` A `<=` Y <-> forall a, A a -> Y (f a). Proof. split=> H. @@ -33,13 +29,6 @@ split=> H. - by move=> b [] a Xa <-; apply H. Qed. -Lemma fullimage_subset (f : T -> U) (Y : set U) : - f @` setT `<=` Y <-> forall t, Y (f t). -Proof. -rewrite (_ : (forall a, Y (f a)) <-> (forall a, setT a -> Y (f a))) ?image_subset //. -by firstorder. -Qed. - Lemma eq_bigcupr (P : set U) (X Y : U -> set T) : X =1 Y -> bigsetU P X = bigsetU P Y. Proof. by move/funext ->. Qed. @@ -51,29 +40,23 @@ Proof. by move=> -> /funext ->. Qed. Lemma bigcup_of_singleton (P : set U) (f : U -> T) : \bigcup_(x in P) [set f x] = f @` P. Proof. -apply eqEsubset=> a; +rewrite eqEsubset; split=> a; by [case=> i Pi ->; apply imageP | case=> i Pi <-; exists i]. Qed. -(* TODO: PR in progress in mathcomp-analysis *) -Lemma bigcup_set0 (X : U -> set T) : \bigcup_(i in set0) X i = set0. -Proof. by apply eqEsubset => a // [] //. Qed. - -Lemma bigcup_set1 (i : U) (X : U -> set T) : \bigcup_(i in [set i]) X i = X i. -Proof. apply eqEsubset => a; by [case=> j -> | exists i]. Qed. -(* TODO: end PR *) - Lemma bigcup_image V (P : set V) (f : V -> U) (X : U -> set T) : \bigcup_(x in f @` P) X x = \bigcup_(x in P) X (f x). Proof. -apply eqEsubset=> x. +rewrite eqEsubset; split=> x. - by case=> j [] i pi <- Xfix; exists i. - by case=> i Pi Xfix; exists (f i); first by exists i. Qed. Lemma bigcup_of_const (P : set U) (X : U -> set T) (i : U) : P i -> (forall j, P j -> X j = X i) -> \bigcup_(j in P) X j = X i. -Proof. move=> Pi H; apply eqEsubset=> a; by [case=> j /H -> | exists i]. Qed. +Proof. +move=> Pi H; rewrite eqEsubset; split=> a; by [case=> j /H -> | exists i]. +Qed. Lemma bigsubsetU (P : set U) (X : U -> set T) (Y : set T) : (forall i, P i -> X i `<=` Y) <-> bigsetU P X `<=` Y. @@ -95,7 +78,6 @@ End PR_to_classical_sets. Notation imageA := (deprecate imageA image_comp _) (only parsing). Notation image_idfun := (deprecate image_idfun image_id _) (only parsing). -(*Notation bigcup_set1 := (deprecate bigcup_set1 bigcup_of_singleton _) (only parsing).*) Notation bigcup0 := (deprecate bigcup0 bigcup_set0 _) (only parsing). Notation bigcup1 := (deprecate bigcup1 bigcup_set1 _) (only parsing). Notation bigcup_const := (deprecate bigcup_const bigcup_of_const _) (only parsing). diff --git a/probability/convex_choice.v b/probability/convex_choice.v index f7520a03..4952a8ee 100644 --- a/probability/convex_choice.v +++ b/probability/convex_choice.v @@ -1763,7 +1763,7 @@ Lemma hull_eqEsubset X Y : Proof. move/hull_monotone; rewrite hull_cset /= => H1. move/hull_monotone; rewrite hull_cset /= => H2. -exact/eqEsubset. +by rewrite eqEsubset. Qed. (* hull (X `|` hull Y) = hull (hull (X `|` Y)) = hull (x `|` y); diff --git a/probability/necset.v b/probability/necset.v index ec1a1cbf..cea04fdc 100644 --- a/probability/necset.v +++ b/probability/necset.v @@ -67,7 +67,8 @@ Section moveme. Local Open Scope classical_set_scope. Lemma setU_bigsetU T (I J : set T) : I `|` J = bigsetU [set I; J] idfun. Proof. -apply eqEsubset => x; [case=> Hx; by [exists I => //; left | exists J => //; right] |]. +rewrite eqEsubset;split => x. + by case=> ?; [exists I => //; left|exists J => //; right]. by case=> K [] -> Hx; [left | right]. Qed. End moveme. @@ -209,9 +210,10 @@ Proof. by case: X => X [] X0 /=; case: cid. Qed. Global Opaque neset_repr. Local Hint Resolve repr_in_neset : core. -Lemma image_const A B (X : neset A) (b : B) : - (fun _ => b) @` X = [set b]. -Proof. apply eqEsubset=> b'; [by case => ? _ -> | by move=> ?; eexists]. Qed. +Lemma image_const A B (X : neset A) (b : B) : (fun _ => b) @` X = [set b]. +Proof. +rewrite eqEsubset; split=> b'; [by case => ? _ -> | by move=> ?; eexists]. +Qed. Lemma neset_bigsetU_neq0 A B (X : neset A) (F : A -> neset B) : bigsetU X F != set0. Proof. by apply/bigcup_set0P; eexists; split => //; eexists. Qed. @@ -266,18 +268,18 @@ Lemma conv_setE p X Y : X :<| p |>: Y = \bigcup_(x in X) (x <| p |>: Y). Proof. by []. Qed. Lemma convC_set p X Y : X :<| p |>: Y = Y :<| p.~%:pr |>: X. Proof. -by apply eqEsubset=> u; case=> x Xx; rewrite conv_pt_setE => -[] y Yy <-; +by rewrite eqEsubset; split=> u; case=> x Xx; rewrite conv_pt_setE => -[] y Yy <-; exists y => //; rewrite conv_pt_setE; exists x => //; rewrite -convC. Qed. Lemma conv1_pt_set x (Y : neset L) : x <| 1%:pr |>: Y = [set x]. Proof. -apply eqEsubset => u; rewrite conv_pt_setE. +rewrite eqEsubset;split => u; rewrite conv_pt_setE. - by case => y _; rewrite conv1. - by move=> ->; eexists => //; rewrite conv1. Qed. Lemma conv0_pt_set x (Y : set L) : x <| 0%:pr |>: Y = Y. Proof. -apply eqEsubset => u; rewrite conv_pt_setE. +rewrite eqEsubset; split => u; rewrite conv_pt_setE. - by case=> y Yy <-; rewrite conv0. - by move=> Yu; exists u=> //; rewrite conv0. Qed. @@ -344,13 +346,11 @@ Proof. by move/conv_set_monotone=> YY' u [] p _ /YY' HY'; exists p. Qed. Lemma iter_monotone_conv_set (X : neset L) (m : nat) : forall n, (m <= n)%N -> iter_conv_set X m `<=` iter_conv_set X n. Proof. -elim: m. -- move=> n _. - case: n => // n. +elim: m => [n _|m IHm]. +- case: n => // n. rewrite iter0_conv_set iterS_conv_set. by exists 1%:pr => //; rewrite conv1_set. -- move=> m IHm. - case => // n /(IHm _) mn. +- case => // n /(IHm _) mn. rewrite iterS_conv_set=> a [] p _ H. exists p => //. by move: (@conv_set_monotone p X _ _ mn) => /(_ a); apply. @@ -374,12 +374,13 @@ move=> n IHn g d X. case/boolP: (X == set0); first by move/eqP => -> /(_ (g ord0)) H; apply False_ind; apply/H/imageP. move=> Xneq0 gX; set X' := NESet.Pack (NESet.Mixin Xneq0). -have gXi : forall i : 'I_n.+1, X (g i) by apply fullimage_subset. +have gXi : forall i : 'I_n.+1, X (g i). + by move=> i; move/subset_image : gX; apply. case/boolP: (d ord0 == 1). - move/eqP=> d01. suff : X (<|>_d g) by move/(@iter_conv_set_superset X' n.+1 (<|>_d g)). rewrite (convn_proj g d01). - by apply/gX/imageP. + exact/gX/imageP. - move=> d0n1; rewrite convnE //. exists (probfdist d ord0) => //. exists (g ord0) => //. @@ -387,30 +388,28 @@ case/boolP: (d ord0 == 1). exists (<|>_(DelFDist.d d0n1) (fun x : 'I_n => g (DelFDist.f ord0 x))) => //. apply IHn. move=> u [] i _ <-. - by apply/gX/imageP. + exact/gX/imageP. Qed. Lemma oplus_convC_set (X Y : set L) : oplus_conv_set X Y = oplus_conv_set Y X. Proof. suff H : forall X' Y', oplus_conv_set X' Y' `<=` oplus_conv_set Y' X' - by apply/eqEsubset/H. + by rewrite eqEsubset; split => // /H. move=> {X} {Y} X Y u [] p _. rewrite convC_set => H. -by exists p.~%:pr => //. +by exists p.~%:pr. Qed. Lemma convmm_cset (p : prob) (X : {convex_set L}) : X :<| p |>: X = X. Proof. -apply eqEsubset=> x. +rewrite eqEsubset; split=> x. - case => x0 Xx0; rewrite conv_pt_setE => -[] x1 Xx1 <-; rewrite -in_setE. by move/asboolP : (convex_setP X); rewrite in_setE; apply. - by move=> Xx; exists x=> //; rewrite conv_pt_setE; exists x=> //; rewrite convmm. Qed. Lemma oplus_convmm_cset (X : {convex_set L}) : oplus_conv_set X X = X. Proof. -apply eqEsubset => x. -- case=> p _. - by rewrite convmm_cset. -- move=> Xx. - exists 0%:pr => //. +rewrite eqEsubset; split => x. +- by case=> p _; rewrite convmm_cset. +- move=> Xx; exists 0%:pr => //. by rewrite convmm_cset. Qed. Lemma oplus_convmm_set_hull (X : set L) : @@ -418,11 +417,12 @@ Lemma oplus_convmm_set_hull (X : set L) : Proof. by rewrite oplus_convmm_cset. Qed. Lemma hull_iter_conv_set (X : set L) : hull X = \bigcup_(i in natset) iter_conv_set X i. Proof. -apply eqEsubset; first by move=> x [] n [] g [] d [] gX ->; exists n => //; apply Convn_iter_conv_set. +rewrite eqEsubset; split. + by move=> x [] n [] g [] d [] gX ->; exists n => //; apply Convn_iter_conv_set. apply bigsubsetU. elim => [_|n IHn _]; first exact/subset_hull. -have H : iter_conv_set X n.+1 `<=` oplus_conv_set X (hull X) - by apply/oplus_conv_set_monotone/IHn. +have H : iter_conv_set X n.+1 `<=` oplus_conv_set X (hull X). + exact/oplus_conv_set_monotone/IHn. apply (subset_trans H). rewrite oplus_convC_set. have : oplus_conv_set (hull X) X `<=` oplus_conv_set (hull X) (hull X). @@ -448,8 +448,6 @@ End convex_neset_lemmas. Notation "x <| p |>: Y" := (conv_pt_set p x Y) : convex_scope. Notation "X :<| p |>: Y" := (conv_set p X Y) : convex_scope. -(*Reserved Notation "'OP' s" (format "'OP' s", at level 6).*) - Module SemiCompleteSemiLattice. Section def. Local Open Scope classical_set_scope. @@ -504,7 +502,7 @@ Proof. by rewrite lub_op_bigsetU. Qed. Lemma nesetU_bigsetU T (I J : neset T) : (I `|` J)%:ne = (bigsetU [set I; J] idfun)%:ne. Proof. -apply/neset_ext => /=; apply eqEsubset => x. +apply/neset_ext => /=; rewrite eqEsubset; split => x. by case=> Hx; [exists I => //; left | exists J => //; right]. by case=> K [] -> Hx; [left | right]. Qed. @@ -975,7 +973,7 @@ Local Open Scope classical_set_scope. Lemma hull_necsetU (X Y : necset A) : hull (X `|` Y) = [set u | exists x, exists y, exists p, x \in X /\ y \in Y /\ u = x <| p |> y]. Proof. -apply eqEsubset => a. +rewrite eqEsubset; split => a. - case/hull_setU; try by apply/set0P/neset_neq0. move=> x xX [] y yY [] p ->; by exists x, y, p. - by case => x [] y [] p [] xX [] yY ->; apply mem_hull_setU; rewrite -in_setE. @@ -1024,7 +1022,7 @@ Definition conv p X Y : necset A := locked (NESet.Mixin (pre_conv_neq0 X Y p)))). Lemma conv1 X Y : conv 1%:pr X Y = X. Proof. -rewrite /conv; unlock; apply necset_ext => /=; apply/eqEsubset => a. +rewrite /conv; unlock; apply necset_ext => /=; rewrite eqEsubset; split => a. by case => x [] y [] xX [] yY ->; rewrite -in_setE conv1. case/set0P: (neset_neq0 Y) => y; rewrite -in_setE => yY. rewrite -in_setE => aX. @@ -1032,7 +1030,7 @@ by exists a, y; rewrite conv1. Qed. Lemma convmm p X : conv p X X = X. Proof. -rewrite/conv; unlock; apply necset_ext => /=; apply eqEsubset => a. +rewrite/conv; unlock; apply necset_ext => /=; rewrite eqEsubset; split => a. - case => x [] y [] xX [] yY ->. rewrite -in_setE; exact: mem_convex_set. - rewrite -in_setE => aX. @@ -1040,13 +1038,13 @@ rewrite/conv; unlock; apply necset_ext => /=; apply eqEsubset => a. Qed. Lemma convC p X Y : conv p X Y = conv p.~%:pr Y X. Proof. -by rewrite/conv; unlock; apply necset_ext => /=; apply eqEsubset => a; +by rewrite/conv; unlock; apply necset_ext => /=; rewrite eqEsubset; split => a; case => x [] y [] xX [] yY ->; exists y, x; [rewrite convC | rewrite -convC]. Qed. Lemma convA p q X Y Z : conv p X (conv q Y Z) = conv [s_of p, q] (conv [r_of p, q] X Y) Z. Proof. -rewrite/conv; unlock; apply/necset_ext => /=; apply eqEsubset => a; case => x []. +rewrite/conv; unlock; apply/necset_ext => /=; rewrite eqEsubset; split => a; case => x []. - move=> y [] xX []. rewrite in_setE => -[] y0 [] z0 [] y0Y [] z0Z -> ->. exists (x <| [r_of p, q] |> y0), z0. @@ -1068,7 +1066,7 @@ Lemma convE p (X Y : necset A) : conv p X Y = Proof. by rewrite/conv; unlock. Qed. Lemma conv_conv_set p X Y : conv p X Y = X :<| p |>: Y :> set A. Proof. -rewrite convE; apply eqEsubset=> u. +rewrite convE eqEsubset; split=> u. - by case=> x [] y; rewrite !in_setE; case=> Xx [] Yy ->; exists x => //; rewrite conv_pt_setE; exists y. - by case=> x Xx; rewrite conv_pt_setE => -[] y Yy <-; exists x, y; rewrite !in_setE. Qed. @@ -1136,7 +1134,7 @@ Lemma axiom (p : prob) (X : L) (I : neset L) : Proof. apply necset_ext => /=. rewrite -hull_cset necset_convType.conv_conv_set /= hull_conv_set_strr. -congr hull; apply eqEsubset=> u /=. +congr hull; rewrite eqEsubset; split=> u /=. - case=> x Xx [] y []Y IY Yy <-. exists (necset_convType.conv p X Y); first by exists Y. rewrite necset_convType.conv_conv_set. @@ -1256,7 +1254,7 @@ Proof. rewrite /lub_binary -[in LHS]lub_op_hull. congr (|_| _). apply neset_ext => /=. -apply eqEsubset=> i /=. +rewrite eqEsubset; split=> i /=. - move/set0P: (set1_neq0 x)=> Hx. move/set0P: (set1_neq0 y)=> Hy. move/(@hull_setU _ _ (necset1 x) (necset1 y) Hx Hy)=> [] a /asboolP ->. From 65cdc490b3ed5a4fc7d1f2f7a5445b106589be76 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 14 Dec 2020 17:19:47 +0900 Subject: [PATCH 2/2] use coq-templates to generate utility files --- .github/workflows/docker-action.yml | 32 ++++++ LICENSE.txt => LICENSE | 0 README.md | 121 ++++++++++++++++++++ README.org | 74 ------------ changelog.txt | 15 ++- coq-infotheo.opam | 48 ++++++++ dune | 7 ++ dune-project | 6 + index.md | 59 ++++++++++ infotheo_authors.txt | 25 ---- meta.yml | 170 ++++++++++++++++++++++++++++ opam | 44 ------- 12 files changed, 454 insertions(+), 147 deletions(-) create mode 100644 .github/workflows/docker-action.yml rename LICENSE.txt => LICENSE (100%) create mode 100644 README.md delete mode 100644 README.org create mode 100644 coq-infotheo.opam create mode 100644 dune create mode 100644 dune-project create mode 100644 index.md delete mode 100644 infotheo_authors.txt create mode 100644 meta.yml delete mode 100644 opam diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 00000000..4d71fc74 --- /dev/null +++ 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 b/LICENSE similarity index 100% rename from LICENSE.txt rename to LICENSE diff --git a/README.md b/README.md new file mode 100644 index 00000000..7415d81a --- /dev/null +++ b/README.md @@ -0,0 +1,121 @@ + +# 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 +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 git@github.com: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 deleted file mode 100644 index e6241a95..00000000 --- a/README.org +++ /dev/null @@ -1,74 +0,0 @@ -* infotheo - -[[https://travis-ci.com/affeldt-aist/infotheo][file:https://travis-ci.com/affeldt-aist/infotheo.svg?branch=master]] - -** Installation - - The preferred way to install infotheo is with opam because it takes - care of the dependencies with other libraries. If not already done, - add the repository for Coq libraries to opam and update: - -1. ~opam repo add coq-released https://coq.inria.fr/opam/released~ -2. ~opam update~ - -*** Last stable version: - -Version 0.2: -3. ~opam install coq-infotheo~ - -**** Requirements - -- [[https://coq.inria.fr][Coq]] 8.11 or 8.12 -- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.11.0 -- [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.3.2 - which requires - + [[https://github.com/math-comp/finmap][finmap]] 1.5.0 or greater - -All versions available from opam. - -*** Development version (git master): - -1. ~git clone git@github.com:affeldt-aist/infotheo.git~ -2. ~cd infotheo~ - -If opam is installed, do: - -3. ~opam install .~ - -If opam is not installed but if the requirements are met, do: - -3. ~make~ -4. ~make install~ - -*** About Windows 10 - -Installation of infotheo on Windows is less simple. -See [[https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org][this page]] for instructions to install MathComp on Windows 10 -(or [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html][this page]] 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 git@github.com: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 - 1. Install bigenough 1.0.0 ([[https://github.com/math-comp/bigenough][download]]) - 2. Install finmap 1.5.0 ([[https://github.com/math-comp/finmap][download]]) - 3. Install analysis 0.3.2 ([[https://github.com/math-comp/analysis][download]]) - + Install infotheo using ~coq_makefile~, ~make~, ~make install~ as explained above ([[https://github.com/affeldt-aist/infotheo][download]]) - -** License - -LGPL-2.1-or-later - -(Before version 0.2, infotheo was distributed under the terms of the -~GPL-3.0-or-later~ license.) - -** Authors - -See [[infotheo_authors.txt]] - -** References - -There are a few papers available [[https://staff.aist.go.jp/reynald.affeldt/shannon/][here]] that provide explanations and references. - diff --git a/changelog.txt b/changelog.txt index d1288dd8..f986a31f 100644 --- a/changelog.txt +++ b/changelog.txt @@ -3,11 +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 + + 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 new file mode 100644 index 00000000..11b87f04 --- /dev/null +++ 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 " +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 new file mode 100644 index 00000000..13f7a06a --- /dev/null +++ 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 new file mode 100644 index 00000000..f60d9a67 --- /dev/null +++ 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 new file mode 100644 index 00000000..f03a76bc --- /dev/null +++ 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: + - | + + + + + +--- + +
+View the project on GitHub +
+ +## 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) + diff --git a/infotheo_authors.txt b/infotheo_authors.txt deleted file mode 100644 index 30aed3c4..00000000 --- a/infotheo_authors.txt +++ /dev/null @@ -1,25 +0,0 @@ -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) - -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) - -Acknowledgments: -- 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) diff --git a/meta.yml b/meta.yml new file mode 100644 index 00000000..d9e1eb54 --- /dev/null +++ b/meta.yml @@ -0,0 +1,170 @@ +fullname: A Coq formalization of information theory and linear error correcting codes +shortname: infotheo +organization: affeldt-aist +opam_name: coq-infotheo +community: false +action: true +coqdoc: false + +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. +authors: +- name: Reynald Affeldt, AIST + initial: true +- name: Manabu Hagiwara, Chiba U. (previously AIST) + initial: true +- name: Jonas Senizergues, ENS Cachan (internship at AIST) + initial: true +- name: Jacques Garrigue, Nagoya U. + initial: false +- name: Kazuhiko Sakaguchi, Tsukuba U. + initial: false +- name: Taku Asai, Nagoya U. (M2) + initial: false +- name: Takafumi Saikawa, Nagoya U. + initial: false +- name: Naruomi Obata, Titech (M2) + initial: false + +opam-file-maintainer: Reynald Affeldt + +opam-file-version: dev + +license: + fullname: LGPL-2.1-or-later + identifier: LGPL-2.1-or-later + file: LICENSE + +supported_coq_versions: + text: Coq 8.11 to 8.12 + opam: '{ (>= "8.11" & < "8.13~") | (= "dev") }' + +tested_coq_opam_versions: +- version: '1.11.0-coq-8.11' + repo: 'mathcomp/mathcomp' +- version: '1.11.0-coq-8.12' + repo: 'mathcomp/mathcomp' + +dependencies: +- opam: + name: coq-mathcomp-ssreflect + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp ssreflect 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-fingroup + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp fingroup 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-algebra + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp algebra 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-solvable + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp solvable 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-field + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp field 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-analysis + version: '{ (= "0.3.4") }' + description: |- + [MathComp analysis 0.3.4](https://github.com/math-comp/analysis) +namespace: infotheo + +keywords: +- name: information theory +- name: probability +- name: error-correcting codes + +publications: +- pub_url: https://arxiv.org/abs/2004.12713 + pub_title: Formal Adventures in Convex and Conical Spaces + pub_doi: 10.1007/978-3-030-53518-6_2 +- pub_url: https://link.springer.com/article/10.1007/s10817-019-09538-8 + pub_title: A Library for Formalization of Linear Error-Correcting Codes + pub_doi: 10.1007/s10817-019-09538-8 +- pub_url: https://www.jstage.jst.go.jp/article/jssst/37/3/37_3_79/_article/-char/en + pub_title: Reasoning with Conditional Probabilities and Joint Distributions in Coq + pub_doi: 10.11309/jssst.37.3_79 +- pub_url: http://staff.aist.go.jp/reynald.affeldt/documents/compression-isita2018.pdf + pub_title: Examples of formal proofs about data compression + pub_doi: 10.23919/ISITA.2018.8664276 +- pub_url: http://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf + pub_title: Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes +- pub_url: http://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf + pub_title: Formalization of error-correcting codes---from Hamming to modern coding theory + pub_doi: 10.1007/978-3-319-22102-1_2 +- pub_url: https://link.springer.com/article/10.1007%2Fs10817-013-9298-1 + pub_title: Formalization of Shannon’s Theorems + pub_doi: 10.1007/s10817-013-9298-1 + +#make_target: [ +# [make "-j%{jobs}%" ] +# [make "-C" "extraction" "tests"] {with-test} +# ] + +documentation: |- + ## 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 git@github.com: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/opam b/opam deleted file mode 100644 index 34e99cc0..00000000 --- a/opam +++ /dev/null @@ -1,44 +0,0 @@ -opam-version: "2.0" -maintainer: "reynald.affeldt@aist.go.jp" -homepage: "https://github.com/affeldt-aist/infotheo" -bug-reports: "https://github.com/affeldt-aist/infotheo/issues" -dev-repo: "git+https://github.com/affeldt-aist/infotheo.git" -license: "LGPL-2.1-or-later" -authors: [ - "Reynald Affeldt" - "Manabu Hagiwara" - "Jonas Senizergues" - "Jacques Garrigue" - "Kazuhiko Sakaguchi" - "Taku Asai" - "Takafumi Saikawa" - "Naruomi Obata" - "Erik Martin-Dorel" - "Ryosuke Obi" - "Mitsuharu Yamamoto" -] -build: [ - [make "-j%{jobs}%"] - [make "-C" "extraction" "tests"] {with-test} -] -install: [ - [make "install"] -] -depends: [ - "coq" {>= "8.11" & < "8.13~"} - "coq-mathcomp-field" {>= "1.11" & < "1.12~"} - "coq-mathcomp-analysis" {>= "0.3.2" & < "0.3.3~"} -] -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. -""" -tags: [ - "category:Computer Science/Data Types and Data Structures" - "keyword: information theory" - "keyword: probability" - "keyword: error-correcting codes" - "logpath:infotheo" - "date:2020-10-13" -]