From efadbb0c94154c6a7a3804bf48c4ad32084be16a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 2 Feb 2024 17:16:28 +0900 Subject: [PATCH] test compatibility with Coq 8.19 --- .github/workflows/docker-action.yml | 1 + coq-infotheo.opam | 4 ++-- ecc_classic/decoding.v | 7 ++----- ecc_classic/hamming_code.v | 3 +-- ecc_modern/degree_profile.v | 2 +- information_theory/string_entropy.v | 2 +- lib/bigop_ext.v | 2 +- meta.yml | 6 ++++-- probability/convex_equiv.v | 4 ++-- 9 files changed, 15 insertions(+), 16 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index fba646be..a2a581e6 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -23,6 +23,7 @@ jobs: - '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' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/coq-infotheo.opam b/coq-infotheo.opam index 08ab81ac..98e18bac 100644 --- a/coq-infotheo.opam +++ b/coq-infotheo.opam @@ -21,14 +21,14 @@ build: [ ] install: [make "install"] depends: [ - "coq" { (>= "8.17" & < "8.19~") | (= "dev") } + "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-hierarchy-builder" { = "1.5.0" } + "coq-hierarchy-builder" { >= "1.5.0" } "coq-mathcomp-algebra-tactics" { = "1.1.1" } ] diff --git a/ecc_classic/decoding.v b/ecc_classic/decoding.v index 1155b050..01d1c89c 100644 --- a/ecc_classic/decoding.v +++ b/ecc_classic/decoding.v @@ -244,17 +244,14 @@ pose dH_y c := dH y c. pose g : nat -> R := fun d : nat => ((1 - Prob.p p) ^ (n - d) * (Prob.p p) ^ d)%R. have -> : W ``(y | c) = g (dH_y c). move: (DMC_BSC_prop p enc (discard c) y). - set cast_card := eq_ind_r _ _ _. - rewrite (_ : cast_card = card_F2) //. - clear cast_card. + rewrite [X in BSC.c X _](_ : _ = card_F2) //. rewrite -/W compatible //. move/subsetP : f_img; apply. by rewrite inE; apply/existsP; exists (receivable_rV y); apply/eqP. transitivity (\big[Order.max/0]_(c in C) (g (dH_y c))); last first. apply eq_bigr => /= c' Hc'. move: (DMC_BSC_prop p enc (discard c') y). - set cast_card := eq_ind_r _ _ _. - rewrite (_ : cast_card = card_F2) //. + rewrite [X in BSC.c X _](_ : _ = card_F2) //. by rewrite -/W compatible. (* the function maxed over is decreasing so we may look for its minimizer, which is given by minimum distance decoding *) diff --git a/ecc_classic/hamming_code.v b/ecc_classic/hamming_code.v index 5fed669c..3cafee7e 100644 --- a/ecc_classic/hamming_code.v +++ b/ecc_classic/hamming_code.v @@ -988,8 +988,7 @@ transitivity ( apply eq_bigr => t Ht. rewrite dH_sym. rewrite -(DMC_BSC_prop p (enc hamming_channel_code) m0 t). - set x := eq_ind_r _ _ _. - rewrite (_ : x = card_F2) //; by apply eq_irrelevance. + by rewrite [X in BSC.c X _](_ : _ = card_F2). transitivity ( \sum_(a|a \in [set tb | if dec hamming_channel_code tb is Some m1 then m1 != m0 else diff --git a/ecc_modern/degree_profile.v b/ecc_modern/degree_profile.v index 4bbb7d70..5167a9ff 100644 --- a/ecc_modern/degree_profile.v +++ b/ecc_modern/degree_profile.v @@ -1829,7 +1829,7 @@ case: (lastP p) Hp Hl => /=. by rewrite eqxx /= sp_in_step_edom step_edges_sp_ep eqxx. move=> {}p x' Hp Hl. rewrite last_rcons in Hl. -elimtype False; move: Hp. +exfalso; move: Hp. rewrite (eqP Hl) rcons_path /graph_rel => /andP [_] /=. case: (last (x,b1) p) => [] [|] a b. by destruct b. diff --git a/information_theory/string_entropy.v b/information_theory/string_entropy.v index 85a61e94..bb57752e 100644 --- a/information_theory/string_entropy.v +++ b/information_theory/string_entropy.v @@ -115,7 +115,7 @@ Lemma mulnRdep_nz x y (Hx : x != O) : mulnRdep x y = x * y Hx. Proof. rewrite /mulnRdep /=. destruct boolP. - by elimtype False; rewrite i in Hx. + by exfalso; rewrite i in Hx. do 2!f_equal; apply eq_irrelevance. Qed. diff --git a/lib/bigop_ext.v b/lib/bigop_ext.v index 5aabf601..9530e74b 100644 --- a/lib/bigop_ext.v +++ b/lib/bigop_ext.v @@ -227,7 +227,7 @@ rewrite bigU //. have -> : h @^-1: (B :\: [set h x | x in I]) = set0. apply/setP/subset_eqP/andP; rewrite sub0set; split => //. apply/subsetP=> i; rewrite !inE; case/andP. - move/imsetP=> H _; elimtype False; apply H. + move/imsetP=> H _; rewrite boolp.falseE; apply: H. by exists i; rewrite ?inE. rewrite big_set0 Monoid.mulm1. have -> : \big[aop/idx]_(x in B :\: [set h x | x in I]) \big[aop/idx]_(i | h i == x) F i = diff --git a/meta.yml b/meta.yml index 5edabcfa..f456a6af 100644 --- a/meta.yml +++ b/meta.yml @@ -42,7 +42,7 @@ nix: true supported_coq_versions: text: Coq 8.17 - opam: '{ (>= "8.17" & < "8.19~") | (= "dev") }' + opam: '{ (>= "8.17" & < "8.20~") | (= "dev") }' tested_coq_opam_versions: - version: '1.17.0-coq-8.17' @@ -57,6 +57,8 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '1.19.0-coq-8.18' repo: 'mathcomp/mathcomp' +- version: '1.19.0-coq-8.19' + repo: 'mathcomp/mathcomp' dependencies: - opam: @@ -91,7 +93,7 @@ dependencies: [MathComp analysis](https://github.com/math-comp/analysis) - opam: name: coq-hierarchy-builder - version: '{ = "1.5.0" }' + version: '{ >= "1.5.0" }' description: |- [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) - opam: diff --git a/probability/convex_equiv.v b/probability/convex_equiv.v index 2779138c..01ebc90a 100644 --- a/probability/convex_equiv.v +++ b/probability/convex_equiv.v @@ -199,7 +199,7 @@ Lemma axmap : ax_map T. Proof. move=> n m u d g. have -> : fdistmap u d = fdist_convn d (fun i : 'I_m => fdist1 (u i)). - by apply fdist_ext => i; rewrite /fdistmap fdistbindE. + by apply: fdist_ext => /= i; rewrite /fdistmap/= fdistbindE// fdist_convnE. rewrite -axbary. by congr (<&>_ _ _); apply funext => i /=; rewrite axproj. Qed. @@ -554,7 +554,7 @@ Lemma axinjmap : ax_inj_map T. Proof. move=> n m u d g Hu. have -> : fdistmap u d = fdist_convn d (fun i : 'I_m => fdist1 (u i)). - by apply fdist_ext => i; rewrite /fdistmap fdistbindE. + by apply fdist_ext => i; rewrite /fdistmap fdistbindE// fdist_convnE. rewrite -axbarypart. - congr (<&>_ _ _); apply funext => j /=; symmetry; apply axidem => i. by rewrite supp_fdist1 inE => /eqP ->.