compatibility with Coq 8.20 (#131)

* compatibility with Coq 8.20

.github/workflows/docker-action.yml

@@ -17,8 +17,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -32,7 +32,7 @@ information theory, and linear error-correcting codes.
   - Naruomi Obata, Titech (M2)
   - Alessandro Bruni, IT-University of Copenhagen
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.18--8.19
+- Compatible Coq versions: Coq 8.19--8.20
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

changelog.txt

@@ -1,4 +1,6 @@
-
+-------------------
+from 0.7.2 to 0.7.3
+-------------------
 
 - lemma `conv_pt_cset_is_convex` changed into a `Let`
 

coq-infotheo.opam

@@ -21,13 +21,13 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.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") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "1.2.0") }
+  "coq-mathcomp-analysis" { (>= "1.5.0") }
   "coq-hierarchy-builder" { >= "1.5.0" }
   "coq-mathcomp-algebra-tactics" { >= "1.2.0" }
   "coq-interval" { >= "4.10.0"}

information_theory/jtypes.v

@@ -654,13 +654,13 @@ Local Open Scope nat_scope.
 Definition type_of_row (a : A) (Ha : N(a | ta) != 0) : P_ N(a | ta) ( B ).
 pose f := [ffun b => Ordinal (ctyp_element_ub Hrow_num_occ Hta a b)].
 pose d := [ffun b => ((f b)%:R / N(a | ta)%:R)%R].
-have d0 : forall b, (0 <= d b)%mcR.
+assert (d0 : forall b, (0 <= d b)%mcR).
   move=> b.
   apply/RleP.
   rewrite /d /= ffunE.
   apply mulR_ge0; first exact/leR0n.
   apply/invR_ge0/ltR0n; by rewrite lt0n.
-have d1 : (\sum_(b : B) d b)%R = 1%R.
+assert (d1 : (\sum_(b : B) d b)%R = 1%R).
   under eq_bigr do rewrite ffunE /=.
   rewrite -big_distrl /= -big_morph_natRD.
   set lhs := \sum_i _.
@@ -1240,17 +1240,17 @@ Hypothesis Bnot0 : (0 < #|B|)%nat.
 
 Definition num_co_occ_jtype (ta : n.-tuple A) (tb : n.-tuple B) : P_ n (A , B).
 set f := [ffun a => [ffun b => Ordinal (num_co_occ_ub a b ta tb)]].
-have Hf : \sum_(a in A) \sum_(b in B) f a b == n.
+assert (Hf : \sum_(a in A) \sum_(b in B) f a b == n).
   rewrite /f.
   apply/eqP.
   transitivity (\sum_a \sum_b N(a, b|ta, tb)); last by rewrite num_co_occ_sum.
   apply eq_big => a //= _.
   apply eq_big => b //= _.
   by rewrite 2!ffunE.
-have Htmp' : (forall a b,
+assert (Htmp' : (forall a b,
         (chan_of_jtype Anot0 Bnot0 f) a b =
         (let ln := (\sum_(b0 in B) (f a) b0)%nat in
-         if ln == O then / #|B|%:R else (((f a) b)%:R / ln%:R))%R).
+         if ln == O then / #|B|%:R else (((f a) b)%:R / ln%:R))%R)).
   by move=> a b; rewrite ffunE.
 exact (@JType.mk _ _ _ (chan_of_jtype Anot0 Bnot0 f) f Hf Htmp').
 Defined.

information_theory/types.v

@@ -90,10 +90,10 @@ Definition type_of_tuple (A : finType) n (ta : n.+1.-tuple A) : P_ n.+1 ( A ).
 set f := [ffun a => N(a | ta)%:R / n.+1%:R].
 assert (H1 : forall a, (0%mcR <= f a)%mcR).
   move=> a; rewrite ffunE; apply/RleP/divR_ge0; by [apply leR0n | apply ltR0n].
-have H2 : \sum_(a in A) f a = 1%R.
+assert (H2 : \sum_(a in A) f a = 1%R).
   under eq_bigr do rewrite ffunE /=.
   by rewrite -big_distrl /= -big_morph_natRD sum_num_occ_alt mulRV // INR_eq0'.
-have H : forall a, (N(a | ta) < n.+2)%nat.
+assert (H : forall a, (N(a | ta) < n.+2)%nat).
   move=> a; rewrite ltnS; by apply num_occ_leq_n.
 refine (@type.mkType _ n.+1 (FDist.make H1 H2)
   [ffun a => @Ordinal n.+2 (N(a | ta)) (H a)] _).
@@ -141,22 +141,22 @@ Qed.
 Definition fdist_of_ffun (A : finType) n (f : {ffun A -> 'I_n.+2})
   (Hf : (\sum_(a in A) f a)%nat == n.+1) : {fdist A}.
 set pf := [ffun a : A => INR (f a) / INR n.+1].
-have H : (\sum_(a in A) pf a)%mcR = 1 :> R.
+assert (pf_ge0 : forall a, (0 <= pf a)%mcR).
+  move=> a; apply/RleP.
+  rewrite /pf/= ffunE; apply: divR_ge0 => //.
+    apply/RleP.
+    rewrite INRE.
+    by rewrite Num.Theory.ler0n.
+  apply/RltP.
+  rewrite INRE.
+  by rewrite Num.Theory.ltr0n.
+assert (H : (\sum_(a in A) pf a)%mcR = 1 :> R).
   rewrite /pf; under eq_bigr do rewrite ffunE /=.
   rewrite /Rdiv -big_distrl /= -big_morph_natRD.
   move/eqP : Hf => ->.
   rewrite -RmultE.
   by rewrite mulRV// INR_eq0'.
-apply: (FDist.make _ H).
-move=> a.
-apply/RleP.
-rewrite /pf/= ffunE; apply: divR_ge0 => //.
-  apply/RleP.
-  rewrite INRE.
-  by rewrite Num.Theory.ler0n.
-apply/RltP.
-rewrite INRE.
-by rewrite Num.Theory.ltr0n.
+exact: (FDist.make pf_ge0 H).
 Defined.
 
 Lemma fdist_of_ffun_prop (A : finType) n (f : {ffun A -> 'I_n.+2})

meta.yml

@@ -43,14 +43,14 @@ license:
 nix: true
 
 supported_coq_versions:
-  text: Coq 8.18--8.19
-  opam: '{ (>= "8.18" & < "8.20~") | (= "dev") }'
+  text: Coq 8.19--8.20
+  opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
@@ -80,7 +80,7 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.2.0") }'
+    version: '{ (>= "1.5.0") }'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:

probability/convex_equiv.v

@@ -295,10 +295,13 @@ Module B := NaryToBin(A).
 Module EA := Equiv2(A).
 Import A B.
 
-Let equiv_convn n (d : {fdist 'I_n}) (g : 'I_n -> A.T) : <&>_d g = <|>_d g.
+#[local]
+Definition equiv_convn n (d : {fdist 'I_n}) (g : 'I_n -> A.T) :
+  <&>_d g = <|>_d g.
 Proof. by []. Qed.
 
-Let T' := NaryConv_sort__canonical__convex_ConvexSpace.
+#[local]
+Definition T' := NaryConv_sort__canonical__convex_ConvexSpace.
 
 Lemma equiv_conv p (a b : C.T) : a <| p |> b = a <& p &> b.
 Proof.

robust/weightedmean.v

@@ -407,7 +407,7 @@ by move=> *; exact/sq_dev_ge0.
 Qed.
 
 Lemma sq_dev_max_ge0 : 0 <= sq_dev_max.
-Proof. by rewrite /sq_dev_max; apply/topology.bigmax_geP; left. Qed.
+Proof. by rewrite /sq_dev_max; apply/boolp.bigmax_geP; left. Qed.
 
 Lemma sq_dev_max_ge u : C u != 0 -> sq_dev u <= sq_dev_max.
 Proof. by move=> Cu0; rewrite /sq_dev_max; apply/le_bigmax_cond. Qed.