adapt smc_useful_tools to mc2 (#1)

* port to MC2 (affeldt-aist#116)


---------

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

* changelog

* fix

* lemma 3.1

* cleaning

* Lemma 3.2

* Lemma 3.3 in a new file probability/smc.v

* WIP: try to prove Lemma 3.4

* WIP: lemma 3.4

* WIP: try prob + uniform dist

* pXY_unif

* comments

* mc2

---------

Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Co-authored-by: Greg Weng <greg.weng@mercari.com>
Co-authored-by: weng-chenghui <144981080+weng-chenghui@users.noreply.github.com>

.github/workflows/docker-action.yml

@@ -17,13 +17,9 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.19.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.19.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.19.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -31,7 +31,7 @@ information theory, and linear error-correcting codes.
   - Takafumi Saikawa, Nagoya U.
   - Naruomi Obata, Titech (M2)
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.17
+- Compatible Coq versions: Coq 8.17--8.19
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

changelog.txt

@@ -1,3 +1,15 @@
+-------------------
+from 0.6.1 to 0.7.0
+-------------------
+
+Port to MathComp 2
+
+-------------------
+from 0.6.0 to 0.6.1
+-------------------
+
+compatibility release
+
 -------------------
 from 0.5.2 to 0.6.0
 -------------------

coq-infotheo.opam

@@ -22,14 +22,14 @@ build: [
 install: [make "install"]
 depends: [
   "coq" { (>= "8.17" & < "8.20~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.16.0" & < "1.20.0") | (= "dev") }
-  "coq-mathcomp-fingroup" { (>= "1.16.0" & < "1.20.0") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "1.16.0" & < "1.20.0") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "1.16.0" & < "1.20.0") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "1.16.0" & < "1.20.0") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "0.6.6") & (< "0.8~")}
+  "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
+  "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev")  }
+  "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev")  }
+  "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev")  }
+  "coq-mathcomp-field" { (>= "2.2.0") | (= "dev")  }
+  "coq-mathcomp-analysis" { (>= "1.0.0") }
   "coq-hierarchy-builder" { >= "1.5.0" }
-  "coq-mathcomp-algebra-tactics" { = "1.1.1" }
+  "coq-mathcomp-algebra-tactics" { >= "1.2.0" }
 ]
 
 tags: [

ecc_classic/alternant.v

@@ -54,7 +54,7 @@ Section injection_into_extension_field.
 
 Variables (F0 : finFieldType) (F1 : fieldExtType F0).
 
-Definition ext_inj : {rmorphism F0 -> F1} := @GRing.in_alg_rmorphism F0 F1.
+Definition ext_inj : {rmorphism F0 -> F1} := @GRing.in_alg F1.
 
 Definition ext_inj_tmp : {rmorphism F0 -> (FinFieldExtType F1)} := ext_inj.
 

ecc_classic/bch.v

@@ -158,7 +158,7 @@ Section BCH_def.
 Variables (n : nat) (m : nat).
 
 Definition code (a : 'rV_n) t :=
-  Rcode.t (@GF2_of_F2_rmorphism m) (kernel (PCM a t)).
+  Rcode.t (@GF2_of_F2 m) (kernel (PCM a t)).
 
 End BCH_def.
 

ecc_classic/cyclic_code.v

@@ -122,10 +122,12 @@ Lemma rcs'_rcs (R : idomainType) n (x : 'rV[R]_n.+1) : rcs' x = rcs x.
 Proof.
 rewrite /rcs' /rcs; apply/rowP => i; rewrite !mxE.
 case: ifPn => [/eqP -> |i0].
-  congr (x _ _); apply val_inj => /=.
-  by rewrite PermDef.fun_of_permE ffunE /= inordK.
+  congr (x _ _).
+  rewrite /rcs_perm/= unlock/= ffunE eqxx.
+  apply/val_inj => /=.
+  by rewrite inordK.
 congr (x _ _); apply val_inj => /=.
-rewrite PermDef.fun_of_permE ffunE /= inordK.
+rewrite unlock ffunE /= inordK.
   by rewrite (negPf i0) inordK // (ltn_trans _ (ltn_ord i)) // prednK // lt0n.
 by rewrite (ltn_trans _ (ltn_ord i)) // prednK // lt0n.
 Qed.
@@ -138,7 +140,7 @@ rewrite coef_add_poly coefXM coefCM coef_add_poly coefXn 2!coef_opp_poly coefC.
 case: ifPn => [/eqP ->|i0]; last rewrite subr0.
   rewrite 2!add0r mulrN1 coef_rVpoly /=.
   case: insubP => //= j _ j0.
-  rewrite mxE PermDef.fun_of_permE ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _).
+  rewrite mxE unlock ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _).
   by apply val_inj => /=; rewrite inordK.
 case/boolP : (i == n.+1) => [/eqP ->|in0].
   rewrite mulr1 2!coef_rVpoly /=.
@@ -148,7 +150,7 @@ case/boolP : (i == n.+1) => [/eqP ->|in0].
 rewrite mulr0 2!coef_rVpoly; case: insubP => /= [j|].
   rewrite ltnS => in0' ji; case: insubP => /= [k _ ki|].
     apply/eqP; rewrite subr_eq0; apply/eqP.
-    rewrite mxE PermDef.fun_of_permE ffunE -val_eqE /= ki (negPf i0) -ji; congr (x _ _).
+    rewrite mxE unlock ffunE -val_eqE /= ki (negPf i0) -ji; congr (x _ _).
     apply/val_inj => /=; by rewrite inordK.
   rewrite ltnS -ltnNge => n0i; exfalso.
   rewrite -ltnS prednK // in in0'; last by rewrite lt0n.
@@ -234,20 +236,20 @@ rewrite (reindex_onto (@rcs_perm n) (perm_inv (@rcs_perm n))) /=; last first.
   move=> i1 _; by rewrite permKV.
 rewrite (eq_bigl xpredT); last by move=> i1; rewrite permK eqxx.
 apply eq_bigr => i1 _.
-rewrite coef_rVpoly PermDef.fun_of_permE ffunE.
+rewrite coef_rVpoly unlock ffunE.
 case: ifPn => [/eqP ->|].
   case: insubP => [j _ jn0|]; last by rewrite ltnS leqnn.
   rewrite /= in jn0.
   rewrite coef_rVpoly; case: insubP => // k _ k0.
   rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly.
-  rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE k0 /= expr0 mulr1.
+  rewrite coef_rVpoly_ord mxE unlock ffunE -val_eqE k0 /= expr0 mulr1.
   by rewrite exprAC an1 expr1n mulr1; congr (x _ _); apply val_inj => /=.
 case: insubP => /= [j|].
   rewrite ltnS => i1n0 ji1 i10; rewrite coef_rVpoly.
   case: insubP => /= [k|].
     rewrite ltnS => i1n0' ki1.
     rewrite mxE rcs_poly_rcs ?rVpolyK; last by rewrite size_poly.
-    rewrite coef_rVpoly_ord mxE PermDef.fun_of_permE ffunE -val_eqE [val k]/= ki1 val_eqE (negPf i10).
+    rewrite coef_rVpoly_ord mxE unlock ffunE -val_eqE [val k]/= ki1 val_eqE (negPf i10).
     rewrite inordK; last by rewrite ltnW // ltnS prednK // lt0n.
     rewrite prednK // ?lt0n //; congr (x _ _ * _).
     by apply/val_inj.

ecc_classic/decoding.v

@@ -114,7 +114,7 @@ Section maximum_likelihood_decoding.
 
 Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
 Variables (n : nat) (C : {vspace 'rV[A]_n}).
-Variable f : decT B [finType of 'rV[A]_n] n.
+Variable f : decT B ('rV[A]_n) n.
 Variable P : {fdist 'rV[A]_n}.
 
 Local Open Scope reals_ext_scope.
@@ -130,8 +130,8 @@ Section maximum_likelihood_decoding_prop.
 
 Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
 Variables (n : nat) (C : {vspace 'rV[A]_n}).
-Variable repair : decT B [finType of 'rV[A]_n] n.
-Let P := fdist_uniform_supp real_realType (vspace_not_empty C).
+Variable repair : decT B ('rV[A]_n) n.
+Let P := fdist_uniform_supp R (vspace_not_empty C).
 Hypothesis ML_dec : ML_decoding W C repair P.
 
 Local Open Scope channel_code_scope.
@@ -216,11 +216,11 @@ Let card_F2 : #| 'F_2 | = 2%nat. Proof. by rewrite card_Fp. Qed.
 Let W := BSC.c card_F2 p.
 
 Variables (n : nat) (C : {vspace 'rV['F_2]_n}).
-Variable f : repairT [finType of 'F_2] [finType of 'F_2] n.
+Variable f : repairT 'F_2 'F_2 n.
 Variable f_img : oimg f \subset C.
 Variable M : finType.
-Variable discard : discardT [finType of 'F_2] n M.
-Variable enc : encT [finType of 'F_2] M n.
+Variable discard : discardT 'F_2 n M.
+Variable enc : encT 'F_2 M n.
 Hypothesis compatible : cancel_on C enc discard.
 Variable P : {fdist 'rV['F_2]_n}.
 
@@ -273,7 +273,7 @@ Section MAP_decoding.
 
 Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
 Variables (n : nat) (C : {vspace 'rV[A]_n}).
-Variable dec : decT B [finType of 'rV[A]_n] n.
+Variable dec : decT B ('rV[A]_n) n.
 Variable P : {fdist 'rV[A]_n}.
 
 Definition MAP_decoding := forall y : P.-receivable W,
@@ -286,9 +286,9 @@ Section MAP_decoding_prop.
 
 Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
 Variables (n : nat) (C : {vspace 'rV[A]_n}).
-Variable dec : decT B [finType of 'rV[A]_n] n.
+Variable dec : decT B ('rV[A]_n) n.
 Variable dec_img : oimg dec \subset C.
-Let P := fdist_uniform_supp real_realType (vspace_not_empty C).
+Let P := fdist_uniform_supp R (vspace_not_empty C).
 
 Lemma MAP_implies_ML : MAP_decoding W C dec P -> ML_decoding W C dec P.
 Proof.
@@ -332,13 +332,13 @@ End MAP_decoding_prop.
 
 Section MPM_decoding.
 (* in the special case of a binary code... *)
-Variable W : `Ch('F_2, [finType of 'F_2]).
+Variable W : `Ch('F_2, 'F_2).
 Variable n : nat.
 Variable C : {vspace 'rV['F_2]_n}.
 Hypothesis C_not_empty : (0 < #|[set cw in C]|)%nat.
 Variable m : nat.
-Variable enc : encT [finFieldType of 'F_2] [finType of 'rV['F_2]_(n - m)] n.
-Variable dec : decT [finFieldType of 'F_2] [finType of 'rV['F_2]_(n - m)] n.
+Variable enc : encT 'F_2 'rV['F_2]_(n - m) n.
+Variable dec : decT 'F_2 'rV['F_2]_(n - m) n.
 
 Local Open Scope vec_ext_scope.
 

ecc_classic/grs.v

@@ -72,7 +72,7 @@ Qed.
 
 Definition syndromep r y := \poly_(l < r) (syndrome_coord l y).
 
-Lemma syndomepE r y :
+Lemma syndromepE r y :
   syndromep r y = \sum_(i in supp y)
      (y ``_ i * b ``_ i)%:P * (\sum_(l < r) (a ``_ i ^+ l)%:P * 'X^l).
 Proof.
@@ -221,11 +221,14 @@ case/boolP : (r == O) => r0.
   rewrite -scalerAl mulrC mul_polyC; congr (_ *: (_ *: _)).
   apply eq_bigl => k; by rewrite in_setD1 andbC.
 rewrite /GRS_mod big_distrl /= /Omega /erreval -big_split /=.
-rewrite GRS.syndomepE big_distrr /=.
+rewrite GRS.syndromepE big_distrr /=.
 apply eq_bigr => i iy.
 rewrite -3!scalerAl -scalerA -scalerDr.
 rewrite polyCM -!mulrA mulrCA !mulrA mul_polyC -!scalerAl; congr (_ *: _).
-rewrite /Sigma /errloc (bigD1 i) //= mulrC -!mulrA mulrBl mul1r.
+rewrite /Sigma /errloc.
+rewrite (bigD1 i) //=.
+rewrite (mulrC (1 - a ``_ i *: 'X)).
+rewrite -!mulrA mulrBl mul1r.
 set x := (X in _ * X = _).
 rewrite (_ : x = (b ``_ i)%:P * (1 - (a ``_ i ^+ r)%:P * 'X^r)); last first.
   rewrite /x mulrCA -mulrBr big_distrr /= -sumrB.
@@ -241,7 +244,7 @@ rewrite (_ : x = (b ``_ i)%:P * (1 - (a ``_ i ^+ r)%:P * 'X^r)); last first.
     rewrite -!scalerAl mulrCA -exprS !scalerAl; congr (_ * _).
     by rewrite -mul_polyC -polyCM -exprS.
   by rewrite -mulrCA -scalerAl -exprS 2!mul_polyC scalerA -exprSr.
-rewrite mulrA mulrBr mulr1 mulrC -mul_polyC; congr (_ * _ + _).
+rewrite [in LHS]mulrA mulrBr mulr1 mulrC -mul_polyC; congr (_ * _ + _).
  apply/eq_bigl => j; by rewrite in_setD1 andbC.
 rewrite -mulNr !mulrA; congr (_ * _).
 by rewrite -mulNr -mulrA mulrC -!mulrA.