update to mc 1.16.0

.github/workflows/docker-action.yml

@@ -19,6 +19,8 @@ jobs:
         image:
           - 'mathcomp/mathcomp:1.15.0-coq-8.15'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

coq-infotheo.opam

@@ -22,11 +22,11 @@ build: [
 install: [make "install"]
 depends: [
   "coq" { (>= "8.15" & < "8.17~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.14.0" & < "1.16~") | (= "dev") }
-  "coq-mathcomp-fingroup" { (>= "1.14.0" & < "1.16~") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "1.14.0" & < "1.16~") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "1.14.0" & < "1.16~") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "1.14.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-ssreflect" { (>= "1.14.0" & < "1.17~") | (= "dev") }
+  "coq-mathcomp-fingroup" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
+  "coq-mathcomp-algebra" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
+  "coq-mathcomp-solvable" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
+  "coq-mathcomp-field" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
   "coq-mathcomp-analysis" { (>= "0.5.4") & (< "0.7~")}
   "coq-hierarchy-builder" { >= "1.3.0" }
 ]

ecc_classic/bch.v

@@ -678,9 +678,9 @@ rewrite HM /fdcoor poly_rV_K //; last first.
   move: (ltn_modp ('X * rVpoly x') ('X^n - 1)).
   rewrite size_Xn_sub_1 // ltnS => ->.
   by rewrite monic_neq0 // monic_Xn_sub_1.
-rewrite !hornerE.
+rewrite !(hornerE,hornerXn(*TODO(rei): not necessary since mc1.16.0*)).
 move: (Hx i); rewrite /fdcoor => /eqP ->; rewrite mulr0 add0r.
-by rewrite hornerXn mxE exprAC a1 expr1n subrr mulr0.
+by rewrite mxE exprAC a1 expr1n subrr mulr0.
 Qed.
 
 End BCH_cyclic.

ecc_modern/ldpc_algo_proof.v

@@ -870,30 +870,28 @@ Proof.
 move: k t; refine (children_ind _).
 move=> k [id0 tag0  ch0 up0 down0] /= IH Hun.
 rewrite !(eq_sym id0).
-case: ifP => Hi1.
+case: ifPn => Hi1.
   rewrite -(eqP Hi1).
   rewrite size_flatten /shape.
   rewrite -map_comp.
-  rewrite (eq_map (f1:=size \o msg i1 i2 (Some i1))
-                  (f2:=pred1 i2 \o node_id)); last first.
+  rewrite (@eq_map _ _ (size \o msg i1 i2 (Some i1))
+                  (pred1 i2 \o node_id)); last first.
     move=> [id1 ? ? ? ?] /=.
-    rewrite eqxx.
-    rewrite (eq_sym id1).
-    by case: ifP.
-  rewrite !map_comp.
+    by rewrite eqxx (eq_sym id1); case: ifP.
+  rewrite 2!map_comp.
   rewrite -map_comp.
   rewrite count_sumn.
-  apply count_uniq_mem.
+  apply: count_uniq_mem.
   move /andP: Hun => [_ Hun].
   refine (subseq_uniq _ Hun).
-  by apply subseq_labels.
-case: ifP => Hi2.
+  exact: subseq_labels.
+case: ifPn => Hi2.
   move /andP: Hun => [_ Hun].
   rewrite -(eqP Hi2).
   rewrite size_flatten /shape.
   rewrite -map_comp.
-  rewrite (eq_map (f1:=size \o msg i1 i2 (Some i2))
-                  (f2:=pred1 i1 \o node_id)); last first.
+  rewrite (@eq_map _ _ (size \o msg i1 i2 (Some i2))
+                  (pred1 i1 \o node_id)); last first.
     move=> [id1 ? ? ? ?] /=.
     rewrite eqxx.
     rewrite (eq_sym id1).
@@ -903,9 +901,9 @@ case: ifP => Hi2.
   rewrite !map_comp.
   rewrite -map_comp.
   rewrite count_sumn.
-  apply count_uniq_mem.
+  apply: count_uniq_mem.
   refine (subseq_uniq _ Hun).
-  by apply subseq_labels.
+  exact: subseq_labels.
 rewrite (eq_map (msg_none_eq _ _)); first last.
     by rewrite Hi2.
   by rewrite Hi1.

ecc_modern/subgraph_partition.v

@@ -145,7 +145,7 @@ move: {Hac}(Hac [:: a, b & p']).
 rewrite /ucycle /cycle {3}[b :: p']lock /= -lock Hun Hab rcons_path Hp' Hla.
 rewrite (_ : a \notin b :: p'); last first.
   apply: contra Ha; rewrite !inE => /orP[/eqP ->|]; first by rewrite eqxx.
-  move/Hmem; rewrite inE => ->; by rewrite orbT.
+  by move/Hmem; rewrite ?inE(*TODO(rei): not necessary since mc1.16.0*) => ->; rewrite orbT.
 by destruct p' as [|p'1 p'2] => [//|/= /(_ isT)].
 Qed.
 
@@ -639,7 +639,7 @@ apply/andP; split.
       apply uniq_path_ucycle_extend_1 => //; first by rewrite symmetric_g.
       by move: Hl2; rewrite -cat_rcons rcons_cat cat_path => /andP[].
       by move: Hun2; rewrite -cat_cons -(cat1s n1) catA cat_uniq cats1 => /and3P[].
-    rewrite inE mem_cat mem_seq1 => /orP[|].
+    rewrite ?inE(*TODO(rei): not necessary since mc1.16.0*) mem_cat mem_seq1 => /orP[|].
       rewrite mem_rev => yl2.
       case/splitPr : yl1 => l11 l12 in Hl1 Hun1 Hp.
       case/splitPr : yl2 => l21 l22 in Hl2 Hun2 Hp.
@@ -715,7 +715,7 @@ case/orP => [ | yl1].
     by move: Hun2; rewrite -cat_cons -(cat1s n1) catA cat_uniq cats1 => /and3P[].
   rewrite inE.
   apply/negP; by rewrite (simple_neg simple_g).
-rewrite inE /= in_cons inE.
+rewrite ?inE /= ?in_cons ?inE(*TODO(rei): not necessary since mc1.16.0*).
 case/orP.
   move/eqP => ?; subst y.
   case/splitPr : yl1 => l11 l12 in Hl1 Hun1 Hp.

meta.yml

@@ -49,31 +49,35 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
+- version: '1.16.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.16.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev") }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev") }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev")  }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev")  }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev")  }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev")  }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam:

probability/convex.v

@@ -1531,7 +1531,7 @@ have ->: p.~ * q = (p.~ * q)%R by [].
 by rewrite pq_is_rs -/r -/s mulrC.
 Qed.
 
-HB.instance Definition _ (*lmodR_convType*) :=
+HB.instance Definition _ :=
   @isConvexSpace.Build E (Choice.class _) avg avg1 avgI avgC avgA.
 
 Lemma avgrE p (x y : E) : x <| p |> y = avg p x y. Proof. by []. Qed.
@@ -1796,7 +1796,7 @@ Import GRing.
 Let linear_is_affine: affine f.
 Proof. by move=>p x y; rewrite linearD 2!linearZZ. Qed.
 
-HB.instance Definition _ (*linear_affine*) := isAffine.Build _ _ _ linear_is_affine.
+HB.instance Definition _ := isAffine.Build _ _ _ linear_is_affine.
 
 End linear_affine.
 
@@ -1819,7 +1819,7 @@ Let avgA p q (d0 d1 d2 : R) :
   avg p d0 (avg q d1 d2) = avg [s_of p, q] (avg [r_of p, q] d0 d1) d2.
 Proof. by rewrite /avg convA. Qed.
 
-HB.instance Definition _ (*R_convMixin*) := @isConvexSpace.Build R
+HB.instance Definition _ := @isConvexSpace.Build R
   (Choice.class _) _ avg1 avgI avgC avgA.
 
 Lemma avgRE p (x y : R) : x <| p |> y = (p * x + p.~ * y)%R. Proof. by []. Qed.
@@ -1914,7 +1914,7 @@ move => *.
 apply FunctionalExtensionality.functional_extensionality_dep => a.
 exact/convA.
 Qed.
-HB.instance Definition _ (*depfunConvType*) := @isConvexSpace.Build _ (Choice.class _)
+HB.instance Definition _ := @isConvexSpace.Build _ (Choice.class _)
   _ avg1 avgI avgC avgA.
 End depfun_convex_space.
 
@@ -1933,7 +1933,7 @@ Let avgA p q (d0 d1 d2 : T) :
   avg p d0 (avg q d1 d2) = avg [s_of p, q] (avg [r_of p, q] d0 d1) d2.
 Proof. move => *; congr (pair _ _); by apply convA. Qed.
 
-HB.instance Definition _ (*pairConvType*) :=
+HB.instance Definition _ :=
   @isConvexSpace.Build T (Choice.class _) avg avg1 avgI avgC avgA.
 
 End pair_convex_space.