diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index e6d37e90..37f5a8aa 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/coq-infotheo.opam b/coq-infotheo.opam index fc3d0327..1830231f 100644 --- a/coq-infotheo.opam +++ b/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" } ] diff --git a/ecc_classic/bch.v b/ecc_classic/bch.v index c4af88f7..2f35bdc0 100644 --- a/ecc_classic/bch.v +++ b/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. diff --git a/ecc_modern/ldpc_algo_proof.v b/ecc_modern/ldpc_algo_proof.v index 9dfd8cd8..36a31802 100644 --- a/ecc_modern/ldpc_algo_proof.v +++ b/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. diff --git a/ecc_modern/subgraph_partition.v b/ecc_modern/subgraph_partition.v index 386494af..9b73e855 100644 --- a/ecc_modern/subgraph_partition.v +++ b/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. diff --git a/meta.yml b/meta.yml index 2452c2be..e4b11d0a 100644 --- a/meta.yml +++ b/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: diff --git a/probability/convex.v b/probability/convex.v index 14a48d95..3627aaf4 100644 --- a/probability/convex.v +++ b/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.