less warnings, CI

.github/workflows/docker-action.yml

@@ -17,13 +17,12 @@ 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.0.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.1.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)

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.0.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" & < "1.20.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/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,7 +130,7 @@ 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.
+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.
 
@@ -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,7 +286,7 @@ 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 R (vspace_not_empty C).
 
@@ -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/hamming_code.v

@@ -59,7 +59,7 @@ Let n := (2 ^ m.-1).-1.*2.+1.
 
 Definition PCM := \matrix_(i < m, j < n) (cV_of_nat m j.+1 i 0).
 
-Definition code : Lcode0.t [finFieldType of 'F_2] n := kernel PCM.
+Definition code : Lcode0.t 'F_2 n := kernel PCM.
 
 End hamming_code_definition.
 
@@ -602,7 +602,7 @@ Definition GEN' : 'M_(n - m, n) :=
   castmx (erefl, subnK (Hamming.dim_len m')) (row_mx 1%:M (- CSM)^T).
 
 Program Definition GEN'' : 'M_(n - m, n) :=
-  @Syslcode.GEN [finFieldType of 'F_2] _ _ _ (castmx (_, erefl (n - m)%nat) CSM).
+  @Syslcode.GEN 'F_2 _ _ _ (castmx (_, erefl (n - m)%nat) CSM).
 Next Obligation. exact: leq_subr. Qed.
 Next Obligation. by rewrite (subnBA _ (Hamming.dim_len m')) addnC addnK. Qed.
 
@@ -676,7 +676,7 @@ Definition mx_discard : 'M['F_2]_(n - m, n) :=
 (*   castmx _ (@Syslcode.DIS _ _ _ _).*)
 
 Definition mx_discard' : 'M_(n - m, n) :=
-  @Syslcode.DIS [finFieldType of 'F_2] _ _ (leq_subr _ _).
+  @Syslcode.DIS 'F_2 _ _ (leq_subr _ _).
 
 Lemma mx_discardE : mx_discard = mx_discard'.
 Proof.
@@ -842,7 +842,7 @@ apply/eqP => /=; rewrite ffunE /syndrome.
 by rewrite trmx_mul trmxK -mulmxA -(trmxK GEN) -trmx_mul PCM_GEN trmx0 mulmx0.
 Qed.
 
-Lemma enc_img_is_code : (enc channel_code) @: [finType of 'rV_(n - m)] \subset Hamming.code m.
+Lemma enc_img_is_code : (enc channel_code) @: 'rV_(n - m) \subset Hamming.code m.
 Proof.
 apply/subsetP => /= t /imsetP[/= x _] ->.
 by rewrite mem_kernel_syndrome0 (syndrome_enc x).
@@ -866,7 +866,7 @@ Variable r' : nat.
 Let r := r'.+2.
 Let n := Hamming.len r'.
 
-Definition lcode : Lcode.t [finFieldType of 'F_2] [finFieldType of 'F_2] n _ :=
+Definition lcode : Lcode.t 'F_2 'F_2 n _ :=
   @Lcode.mk _ _ _ _ _
     (Encoder.mk (@Hamming'.encode_inj r') (@Hamming'.enc_img_is_code r'))
     (Decoder.mk (@hamming_repair_img r') (@Hamming'.discard r')) (@Hamming'.enc_discard_is_id r').

ecc_classic/linearcode.v

@@ -489,7 +489,7 @@ End minimum_distance.
 
 Section not_trivial_binary_codes.
 
-Variable (n : nat) (C : Lcode0.t [finFieldType of 'F_2] n).
+Variable (n : nat) (C : Lcode0.t 'F_2 n).
 
 Hypothesis C_not_trivial : not_trivial C.
 
@@ -658,7 +658,7 @@ Section hamming_bound.
 
 Definition ball q n x r := [set y : 'rV['F_q]_n | dH x y <= r].
 
-Lemma min_dist_ball_disjoint n q (C : Lcode0.t [finFieldType of 'F_q] n)
+Lemma min_dist_ball_disjoint n q (C : Lcode0.t 'F_q n)
   (C_not_trivial : not_trivial C) t :
   min_dist C_not_trivial = t.*2.+1 ->
   forall x y, x \in C -> y \in C -> x != y -> ball x t :&: ball y t = set0.
@@ -671,7 +671,7 @@ move: (min_dist_prop C_not_trivial xC yC xy).
 rewrite Hmin => /(leq_ltn_trans xyt); by rewrite ltnn.
 Qed.
 
-Lemma ball_disjoint_min_dist_lb n q (C : Lcode0.t [finFieldType of 'F_q] n)
+Lemma ball_disjoint_min_dist_lb n q (C : Lcode0.t 'F_q n)
   (C_not_trivial : not_trivial C) t :
   (forall x y, x \in C -> y \in C -> x != y -> ball x t :&: ball y t = set0) ->
   forall x : 'rV_n, x \in C -> x != 0 -> t.*2 < wH x
@@ -741,7 +741,7 @@ apply eq_bigr => i _.
 rewrite card_sphere // (leq_trans _ rn) //; move: (ltn_ord i); by rewrite ltnS.
 Qed.
 
-Lemma hamming_bound q n (C : Lcode0.t [finFieldType of 'F_q] n)
+Lemma hamming_bound q n (C : Lcode0.t 'F_q n)
   (C_not_trivial : not_trivial C) t (tn : t <= n) : prime q ->
   min_dist C_not_trivial = t.*2.+1 -> #| C | * card_ball q n t <= q^n.
 Proof.
@@ -774,7 +774,7 @@ rewrite big_imset /=; last first.
 move=> <-; apply subset_leq_card; apply/subsetP => x; by rewrite inE.
 Qed.
 
-Definition perfect n q (C : Lcode0.t [finFieldType of 'F_q] n)
+Definition perfect n q (C : Lcode0.t 'F_q n)
   (C_not_trivial : not_trivial C) :=
   exists r, min_dist C_not_trivial = r.*2.+1 /\ (#| C | * card_ball q n r = q^n)%N.
 
@@ -859,7 +859,7 @@ Section lcode_prop.
 
 Variables (A B : finFieldType) (n : nat).
 
-Lemma dimlen (k : nat) (C : t A B n [finType of 'rV[A]_k]) : 1 < #|A| -> k <= n.
+Lemma dimlen (k : nat) (C : t A B n 'rV[A]_k) : 1 < #|A| -> k <= n.
 Proof.
 move=> F1.
 case : C =>  cws [] /= f.
@@ -1018,7 +1018,7 @@ Qed.
 Lemma H_G_T : 'H *m 'G ^T = 0.
 Proof. by rewrite -trmx0 -G_H_T trmx_mul trmxK. Qed.
 
-Definition encode : encT F [finType of 'rV[F]_k] n := [ffun x => x *m 'G].
+Definition encode : encT F 'rV[F]_k n := [ffun x => x *m 'G].
 
 Lemma encode_inj : injective encode.
 Proof.
@@ -1036,11 +1036,11 @@ Definition DIS : 'M[F]_(k, n) := castmx (erefl, subnKC dimlen) (row_mx 1%:M 0).
 
 Local Notation "'D" := DIS.
 
-Definition discard : discardT F n [finType of 'rV_k] := [ffun x => x *m 'D^T].
+Definition discard : discardT F n 'rV_k := [ffun x => x *m 'D^T].
 
 Definition t (repair : repairT F F n)
              (repair_img : oimg repair \subset kernel 'H)
-             (H : cancel_on (kernel 'H) encode discard) : Lcode.t F F n [finType of 'rV[F]_k].
+             (H : cancel_on (kernel 'H) encode discard) : Lcode.t F F n 'rV[F]_k.
 apply: (@Lcode.mk _ _ _ _ (kernel 'H)
          (Encoder.mk encode_inj _)
          (Decoder.mk repair_img discard)

ecc_classic/repcode.v

@@ -183,7 +183,7 @@ Section minimum_distance_decoding.
 
 Variable r : nat.
 (* we assume a repair function *)
-Variable f : repairT [finType of 'F_2] [finType of 'F_2] r.+1.
+Variable f : repairT 'F_2 'F_2 r.+1.
 Hypothesis Hf : oimg f \subset Rep.code r.
 Let RepLcode := Rep.Lcode_wo_repair Hf.
 
@@ -236,7 +236,7 @@ Definition majority_vote r (s : seq 'F_2) : option 'rV['F_2]_r :=
   else if (r./2 == cnt) && ~~ odd r then None
   else Some 0.
 
-Definition repair r : repairT [finFieldType of 'F_2] [finFieldType of 'F_2] r.+1 :=
+Definition repair r : repairT 'F_2 'F_2 r.+1 :=
   [ffun l => majority_vote r.+1 (tuple_of_row l)].
 
 Lemma repair_odd (r : nat) (Hr : odd r.+1) x : @repair r x != None.

ecc_modern/degree_profile.v

@@ -444,7 +444,7 @@ HB.instance Definition _ n l := @isFinite.Build (fintree n l) _ (@fintree_enumP
 
 Local Open Scope fdist_scope.
 
-Definition ensemble {K : numDomainType} n l := @FDist.t K [finType of (@fintree n l)].
+Definition ensemble {K : numDomainType} n l := @FDist.t K (@fintree n l).
 
 End ensemble.
 

information_theory/entropy.v

@@ -1337,7 +1337,7 @@ have H2 : cond_entropy (fdistA (fdistAC Q)) = cond_entropy (fdist_prod_of_rV P).
            cond_entropy1 (fdistA Q) (a1, a2))%R) /=.
   apply eq_bigr => v _.
 (* TODO: lemma yyy *)
-  rewrite (@reindex_onto _ _ _ [finType of 'rV[A]_n'] [finType of 'rV[A]_(n' - i)]
+  rewrite (@reindex_onto _ _ _ 'rV[A]_n' 'rV[A]_(n' - i)
     (fun w => (castmx (erefl 1%nat, subnKC (ltnS' (ltn_ord i))) (row_mx v w)))
     (@row_drop A _ i)) /=; last first.
     move=> w wv; apply/rowP => j.

information_theory/shannon_fano.v

@@ -57,7 +57,7 @@ Let a : A. by move/card_gt0P: (fdist_card_neq0 P) => /sigW [i]. Qed.
 
 Variable t' : nat.
 Let t := t'.+2.
-Let T := [finType of 'I_t].
+Let T := 'I_t.
 Variable (f : Encoding.t A T).
 
 Let sizes := [seq (size \o f) a| a in A].
@@ -107,7 +107,7 @@ Section shannon_fano_suboptimal.
 Variables (A : finType) (P : {fdist A}).
 Hypothesis Pr_pos : forall s, P s != 0.
 
-Let T := [finType of 'I_2].
+Let T := 'I_2.
 Variable f : Encoding.t A T.
 
 Local Open Scope entropy_scope.
@@ -150,7 +150,7 @@ Variables (A : finType) (P : {fdist A}).
 Variable (t' : nat).
 Let n := #|A|.-1.+1.
 Let t := t'.+2.
-Let T := [finType of 'I_t].
+Let T := 'I_t.
 Variable l : seq nat.
 Hypothesis l_n : size l = n.
 Hypothesis sorted_l : sorted leq l.

information_theory/typ_seq.v

@@ -220,7 +220,7 @@ rewrite Heq Pr_set0 in H.
 lra.
 Qed.
 
-Definition TS_0 (H : aep_bound P epsilon <= n.+1%:R) : [finType of 'rV[A]_n.+1].
+Definition TS_0 (H : aep_bound P epsilon <= n.+1%:R) : 'rV[A]_n.+1.
 apply (@enum_val _ (pred_of_set (`TS P n.+1 epsilon))).
 have -> : #| `TS P n.+1 epsilon| = #| `TS P n.+1 epsilon|.-1.+1.
   rewrite prednK //.

lib/Reals_ext.v

@@ -298,9 +298,9 @@ Proof.
 apply/andP; split.
   by rewrite RdivE' mul1r invr_ge0 ?addr_ge0.
 rewrite RdivE' mul1r invf_le1//.
-  by rewrite ler_addl.
+  by rewrite lerDl.
 rewrite (@lt_le_trans _ _ 1)//.
-by rewrite ler_addl.
+by rewrite lerDl.
 Qed.
 
 Definition Prob_invp (p : {prob R}) := Prob.mk (prob_invp_subproof p).

lib/bigop_ext.v

@@ -92,7 +92,7 @@ under eq_bigr=> i.
   over.
 rewrite bigA_distr_bigA big_mkord (partition_big
   (fun i : {ffun I -> bool} => inord #|[set x | i x]|)
-  (fun j : [finType of 'I_#|I|.+1] => true)) //=.
+  (fun j : 'I_#|I|.+1 => true)) //=.
 { eapply eq_big =>// i _.
   rewrite (reindex (fun s : {set I} => [ffun x => x \in s])); last first.
   { apply: onW_bij.

lib/dft.v

@@ -131,8 +131,8 @@ Proof. by rewrite /fdcoor linearZ /= hornerZ. Qed.
 Lemma fdcoorE y i : y ^`_ i = \sum_(j < n) (y ``_ j) * (u ``_ i) ^+ j.
 Proof.
 rewrite /fdcoor horner_poly; apply eq_bigr => j _; rewrite insubT //= => jn.
-rewrite /sub/=(_ : Ordinal jn = j) //.
-by apply/val_inj.
+rewrite /Sub/= (_ : Ordinal jn = j) //.
+exact/val_inj.
 Qed.
 
 End frequency_domain_coordinates.

lib/hamming.v

@@ -192,7 +192,7 @@ Qed.
 
 Section wH_num_occ_bitstring.
 
-Lemma wH_col_1 n (i : 'I_n) : @wH [fieldType of 'F_2] _ (col i 1%:M)^T = 1%N.
+Lemma wH_col_1 n (i : 'I_n) : @wH 'F_2 _ (col i 1%:M)^T = 1%N.
 Proof.
 rewrite wH_sum (bigD1 i) //= !mxE eqxx /= add1n (eq_bigr (fun=> O)).
 by rewrite big_const iter_addn mul0n.