test compatibility with Coq 8.19 (#112)

.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

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" }
 ]
 

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 *)

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

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.

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.
 

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 =

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:

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 ->.