fixes #203

.github/workflows/docker-action.yml

@@ -17,8 +17,10 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.4.0-coq-8.20'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
+          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.1'
+          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0'
+          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

coq-infotheo.opam

@@ -21,8 +21,8 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.20" & < "9.2~") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") }
+  "coq" { (>= "9.0" & < "9.2~") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.7~") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
   "coq-mathcomp-solvable"

ecc_classic/linearcode.v

@@ -877,8 +877,7 @@ Coercion lcode_coercion (A B : finFieldType) (n : nat) (M : finType) (c : Lcode.
  let: Lcode.mk v _ _ _ := c in v.
 
 Section AboutCasts.
-
-Variable R : comRingType.
+Variable R : comPzRingType.
 
 Definition cast_cols {rows} {f : nat -> nat -> nat} {P : nat -> nat -> Type}
   (HPf : forall k n, P k n -> f k n = n) {k n} (HP : P k n) :

information_theory/channel.v

@@ -52,12 +52,12 @@ Reserved Notation "W '``(|' x ')'" (at level 1, x at next level).
 Reserved Notation "W '``(' y '|' x ')'" (at level 1, y, x at next level).
 Reserved Notation "'`O(' P , W )" (at level 0, P, W at next level,
   format "'`O(' P ,  W )").
-Reserved Notation "'`H(' P '`o' W )" (at level 10, P, W at next level,
+Reserved Notation "'`H(' P '`o' W )" (at level 0, P, W at next level,
   format "'`H(' P  '`o'  W )").
-Reserved Notation "`H( P , W )" (at level 10, P, W at next level,
+Reserved Notation "`H( P , W )" (at level 0, P, W at next level,
   format "`H( P ,  W )").
-Reserved Notation "`H( W | P )" (at level 10, W, P at next level).
-Reserved Notation "`I( P , W )" (at level 50, format "`I( P ,  W )").
+Reserved Notation "`H( W | P )" (at level 0, W, P at next level).
+Reserved Notation "`I( P , W )" (at level 0, format "`I( P ,  W )").
 
 (* TODO: generalize the channel notations to (R:realType) *)
 Notation "{ 'fdist' T }" := ((Rdefinitions.R).-fdist T) : fdist_scope.

information_theory/conditional_divergence.v

@@ -12,8 +12,7 @@ Require Import jfdist_cond.
 
 Reserved Notation "P '|-' V '<<' W" (at level 5, V, W at next level).
 Reserved Notation "P '|-' V '<<b' W" (at level 5, V, W at next level).
-Reserved Notation "'D(' V '||' W '|' P ')'"
-  (at level 50, V, W, P at next level).
+Reserved Notation "'D(' V '||' W '|' P ')'" (at level 50, V, W, P at next level).
 
 Set Implicit Arguments.
 Unset Strict Implicit.

information_theory/entropy.v

@@ -37,10 +37,10 @@ Unset Strict Implicit.
 Import Prenex Implicits.
 
 Reserved Notation "'`H'" (at level 0).
-Reserved Notation "`H( X , Y )" (at level 10, X, Y at next level,
+Reserved Notation "`H( X , Y )" (at level 0, X, Y at next level,
   format "`H( X ,  Y )").
-Reserved Notation "`H( Y | X )" (at level 10, Y, X at next level).
-Reserved Notation "`I( X ; Y )" (at level 50, format "`I( X ;  Y )").
+Reserved Notation "`H( Y | X )" (at level 0, Y, X at next level).
+Reserved Notation "`I( X ; Y )" (at level 0, format "`I( X ;  Y )").
 Reserved Notation "`H[ Y | X = a ]" (at level 0, Y, X, a at next level,
   format "`H[  Y  |  X  =  a  ]").
 

lib/derive_ext.v

@@ -2,8 +2,8 @@
 (* Copyright (C) 2025 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
 From mathcomp Require Import ring lra.
-From mathcomp Require Import unstable mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import set_interval.
+From mathcomp Require Import unstable mathcomp_extra boolp classical_sets.
+From mathcomp Require Import functions set_interval.
 From mathcomp Require Import reals topology normedtype.
 From mathcomp Require Import realfun derive exp.
 Require Import realType_ext ssralg_ext.
@@ -116,7 +116,8 @@ apply: (He `|e'|).
 - exact: ltW.
 Qed.
 
-Local Notation DQ f v a h := (h^-1 *: (f (h *: v + a) - f a)).
+Let DQ (R : numFieldType) (V W : normedModType R) (f : V -> W) v a h :=
+  (h^-1 *: (f (h *: v + a) - f a)).
 
 Let near_eq_difference_quotient (R : numFieldType) (V W : normedModType R)
   (f g : V -> W) (a v : V) :
@@ -143,7 +144,8 @@ have fg0: \forall h \near (0^')%classic, f (h *: v + a) = g (h *: v + a).
     rewrite opprD addrCA subrr addr0 normrN !normrZ !normr_id.
     rewrite mulrCA ltr_pMl// ?mulr_gt0// ?normr_gt0//.
     by rewrite [ltLHS](_ : 1 = 1%:R)// normr_nat ltr_nat.
-have:= fg0 => /filterS; apply=> h ->.
+have:= fg0 => /filterS.
+rewrite /DQ; apply=> h ->.
 move: fg.
 by rewrite -nbhs_nearE nbhsE=> -[] U [] oU Ua /(_ a Ua) ->.
 Qed.

lib/realType_ext.v

@@ -1,9 +1,9 @@
 (* infotheo: information theory and error-correcting codes in Rocq            *)
 (* Copyright (C) 2025 infotheo authors, license: LGPL-2.1-or-later            *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg archimedean ssrnum ssrint.
 From mathcomp Require Import reals normedtype sequences exp.
 From mathcomp Require Import unstable mathcomp_extra boolp interval_inference.
 From mathcomp Require Import ring lra.
 
 (**md**************************************************************************)
@@ -80,49 +80,50 @@
   (forall a, 0 < F a) -> 0 < \prod_(a : A) F a.
 Proof. by move=> F0; elim/big_ind : _ => // x y ? ?; exact: mulr_gt0. Qed.
 
+Notation "p '.~'" := (onem p). (* TODO: remove when dropping support for MCA < 1.15.0 *)
+
 (* PR to mathcomp_extra.v? *)
 Section onem.
 Variable R : realFieldType.
 Implicit Types r s : R.
 
-Lemma onem_le r s : (r <= s) = (`1-s <= `1-r).
+Lemma onem_le r s : (r <= s) = (s.~ <= r.~).
 Proof.
 apply/idP/idP => [|?]; first exact: lerB.
 by rewrite -(opprK r) lerNl -(lerD2l 1).
 Qed.
 
-Lemma onem_lt  r s : (r < s) = (`1-s < `1-r).
+Lemma onem_lt r s : (r < s) = (s.~ < r.~).
 Proof.
 apply/idP/idP => [rs|]; first by rewrite ler_ltB.
 by rewrite ltrBrDl addrCA -ltrBrDl subrr subr_lt0.
 Qed.
 
-Lemma onemE r : `1-r = 1 - r.  Proof. by []. Qed.
+Lemma onemE r : r.~ = 1 - r.  Proof. by []. Qed.
 
-Lemma onem_div r s : s != 0 -> `1-(r / s) = (s - r) / s.
+Lemma onem_div r s : s != 0 -> (r / s).~ = (s - r) / s.
 Proof. by rewrite !onemE => q0; rewrite mulrDl mulNr divff. Qed.
 
-Lemma onem_prob r : 0 <= r <= 1 -> 0 <= onem r <= 1.
+Lemma onem_prob r : 0 <= r <= 1 -> 0 <= r.~ <= 1.
 Proof.
 by move=> /andP[r0 r1]; apply/andP; split; [rewrite onem_ge0|rewrite onem_le1].
 Qed.
 
-Lemma onem_eq0 r : (`1-r = 0) <-> (r = 1).
+Lemma onem_eq0 r : (r.~ = 0) <-> (r = 1).
 Proof. by rewrite /onem; split => [/subr0_eq//|->]; rewrite subrr. Qed.
 
-Lemma onem_neq0 (r : R) : (`1-r != 0) <-> (r != 1).
+Lemma onem_neq0 (r : R) : (r.~ != 0) <-> (r != 1).
 Proof. by split; apply: contra => /eqP/onem_eq0/eqP. Qed.
 
-Lemma onem_eq1 r : `1-r = 1 <-> r = 0. Proof. rewrite onemE; lra. Qed.
+Lemma onem_eq1 r : r.~ = 1 <-> r = 0. Proof. rewrite onemE; lra. Qed.
 
-Lemma onem_oprob r : 0 < r < 1 -> 0 < `1-r < 1.
+Lemma onem_oprob r : 0 < r < 1 -> 0 < r.~ < 1.
 Proof. by move=> /andP [? ?]; apply/andP; rewrite onem_gt0 // onem_lt1. Qed.
 
-Lemma subr_onem r s : r - `1-s = r + s - 1.
+Lemma subr_onem r s : r - s.~ = r + s - 1.
 Proof. by rewrite /onem opprB addrA. Qed.
 
 End onem.
-Notation "p '.~'" := (onem p).
 
 Section about_the_pow_function.
 
@@ -305,9 +306,9 @@
 split => [/= pq1|[-> ->]]; last by rewrite mulr1.
 move: (oner_neq0 R); rewrite -{1}pq1 mulf_eq0 negb_or => /andP[p0 q0].
 have := prob_le1 p; rewrite le_eqVlt => /orP[/eqP p1|p1].
   by rewrite p1 mul1r in pq1; split; exact/val_inj.
 have := prob_le1 q; rewrite le_eqVlt => /orP[/eqP q1|q1].
   by rewrite q1 mulr1 in pq1; split; exact/val_inj.
 have {}p0 : 0 < p%:num by rewrite lt_neqAle ge0 eq_sym andbT.
 by move: p1; rewrite -[in X in X -> _]pq1 (ltr_pMr _ p0) ltNge (ltW q1).
 Qed.
@@ -315,16 +316,13 @@
 End prob_lemmas.
 
 Global Hint Resolve prob_ge0 : core.
 Global Hint Resolve prob_le1 : core.
 
 #[export] Hint Extern 0 (is_true (@Order.le ring_display _ _ _)) =>
   exact/prob_le1 : core.
 #[export] Hint Extern 0 (is_true (@Order.le ring_display _ _ _)) =>
   exact/prob_ge0 : core.
 
-Arguments prob0 {R}.
-Arguments prob1 {R}.
-
 Lemma prob_invn {R : realType} (m : nat) :
   0 <= ((1 + m)%:R^-1 : R) <= 1.
 Proof.
@@ -865,19 +863,3 @@
 Proof. by rewrite s_of_gt0// oprob_neq0. Qed.
 
 End oprob_lemmas2.
-
-Section i01_prob.
-Variable R : realType.
-
-#[deprecated(since="infotheo 0.9.7", note="{prob R} and {i01 R} are identical")]
-Definition i01_of_prob (p : {prob R}) : {i01 R} := p.
-#[deprecated(since="infotheo 0.9.7", note="{prob R} and {i01 R} are identical")]
-Definition prob_of_i01 (p : {i01 R}) : {prob R} := p.
-#[deprecated(since="infotheo 0.9.7", note="{prob R} and {i01 R} are identical")]
-Lemma i01_of_probK : cancel i01_of_prob prob_of_i01.
-Proof. by []. Qed.
-#[deprecated(since="infotheo 0.9.7", note="{prob R} and {i01 R} are identical")]
-Lemma prob_of_i01K : cancel prob_of_i01 i01_of_prob.
-Proof. by []. Qed.
-
-End i01_prob.

probability/convex.v

@@ -160,7 +160,7 @@ Reserved Notation "\ssum_ ( i < n ) F"
   (at level 41, F at level 41, i, n at level 50,
   format "'[' \ssum_ ( i  <  n ) '/  '  F ']'").
 Reserved Notation "{ 'affine' T '->' R }"
-  (at level 36, T, R at next level, format "{ 'affine'  T  '->'  R }").
+  (at level 0, T, R at next level, format "{ 'affine'  T  '->'  R }").
 Reserved Notation "p *: a" (at level 40).
 
 Declare Scope convex_scope.
@@ -2515,7 +2515,7 @@ HB.structure Definition ConvexFunction {R : realType} {d : Order.disp_t} (U : co
 Arguments convex_functionP {R d U V} s.
 
 Notation "{ 'convex' T '->' R }" :=
-  (ConvexFunction.type T R) (at level 36, T, R at next level,
+  (ConvexFunction.type T R) (at level 0, T, R at next level,
     format "{ 'convex'  T  '->'  R }") : convex_scope.
 
 Section convex_function_prop'.
@@ -2656,7 +2656,7 @@ HB.structure Definition ConcaveFunction {R : realType} {d : Order.disp_t}
 Arguments concave_functionP {R d U V} s.
 
 Notation "{ 'concave' T '->' R }" :=
-  (ConvexFunction.type T R) (at level 36, T, R at next level,
+  (ConvexFunction.type T R) (at level 0, T, R at next level,
     format "{ 'concave'  T  '->'  R }") : convex_scope.
 
 Section concave_function_prop.

probability/necset.v

@@ -80,16 +80,16 @@ Require Import realType_ext classical_sets_ext fdist fsdist convex.
 
 Declare Scope latt_scope.
 
-Reserved Notation "x %:ne" (at level 0, format "x %:ne").
+Reserved Notation "x %:ne" (at level 1, format "x %:ne").
 Reserved Notation "x <| p |>: Y" (format "x  <| p |>:  Y", at level 49).
 Reserved Notation "X :<| p |>: Y" (format "X  :<| p |>:  Y", at level 49).
 Reserved Notation "x [+] y" (format "x  [+]  y", at level 50).
 Reserved Notation "'|_|' f" (at level 36, f at level 36, format "|_|  f").
 Reserved Notation "{ 'necset' T }" (at level 0, format "{ 'necset'  T }").
 Reserved Notation "{ 'Biglub_morph' T '->' R }"
-  (at level 36, T, R at next level, format "{ 'Biglub_morph'  T  '->'  R }").
+  (at level 0, T, R at next level, format "{ 'Biglub_morph'  T  '->'  R }").
 Reserved Notation "{ 'Biglub_affine' T '->' R }"
-  (at level 36, T, R at next level, format "{ 'Biglub_affine'  T  '->'  R }").
+  (at level 0, T, R at next level, format "{ 'Biglub_affine'  T  '->'  R }").
 
 Set Implicit Arguments.
 Unset Strict Implicit.

probability/proba.v

@@ -97,7 +97,7 @@ Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln fdist.
 (*                                                                            *)
 (******************************************************************************)
 
-Reserved Notation "E `*T" (at level 40).
+Reserved Notation "E `*T" (at level 1).
 Reserved Notation "T`* F" (at level 40).
 Reserved Notation "{ 'RV' d -> T }" (at level 0, d, T at level 1,
   format "{ 'RV'  d  ->  T }").
@@ -119,19 +119,19 @@ Reserved Notation "X `+ Y" (at level 50).
 Reserved Notation "X `- Y" (at level 50).
 Reserved Notation "X '`+cst' m" (at level 50).
 Reserved Notation "X '`-cst' m" (at level 50).
-Reserved Notation "X '`^2' " (at level 49).
+Reserved Notation "X '`^2' " (at level 1).
 Reserved Notation "'`--' P" (at level 5).
 Reserved Notation "'`log' P" (at level 5).
 Reserved Notation "'[%' x , y , .. , z ']'" (at level 0,
   format "[%  x ,  y ,  .. ,  z ]").
 Reserved Notation "X '\=sum' Xs" (at level 50).
 Reserved Notation "'`E'" (at level 0).
 Reserved Notation "'`V'" (at level 0).
-Reserved Notation "`Pr_ P [ A | B ]" (at level 6, P, A, B at next level,
+Reserved Notation "`Pr_ P [ A | B ]" (at level 0, P, A, B at next level,
   format "`Pr_ P [ A  |  B ]").
-Reserved Notation "`Pr_[ A | B ]" (at level 6, A, B at next level,
+Reserved Notation "`Pr_[ A | B ]" (at level 0, A, B at next level,
   format "`Pr_[ A  |  B ]").
-Reserved Notation "`E_[ X | B ]" (at level 6, X, B at next level,
+Reserved Notation "`E_[ X | B ]" (at level 0, X, B at next level,
   format "`E_[ X  |  B ]").
 Reserved Notation "`Pr[ X = a | Y = b ]" (at level 0, X, Y, a, b at next level,
   format "`Pr[  X  =  a  |  Y  =  b  ]").
@@ -1492,7 +1492,7 @@ rewrite -!Ind_bigcap big_const.
   have [m ->] : exists m, (n.+1 - i)%nat = m.+1.
     by exists (n.+1 - i).-1; rewrite prednK // subn_gt0.
   rewrite iterSr iter_fix ?setIT ?setIid //.
-rewrite -Ind_cap -/Efull.
+rewrite -Ind_setI -/Efull.
 suff : \bigcap_(j0 in j) S j0 \subset Efull by move/setIidPr->.
 rewrite /Efull.
 pose i0 := odflt ord0 (pick (mem j)).
@@ -2703,7 +2703,7 @@ Let XY : {RV P -> (TA * TB)%type} := fun x => (X' x, Y' x).
 Lemma prod_dist_inde_RV : P |= X' _|_ Y'.
 Proof.
 apply/inde_RV_events => x y.
-rewrite (_ : [set _ | _ ] = finset (X @^-1 x) `*T); last first.
+rewrite (_ : [set _ | _ ] = (finset (X @^-1 x)) `*T); last first.
   by apply/setP => -[a b]; rewrite !inE.
 rewrite (_ : [set x | preim Y' (pred1 y) x] = T`* finset (Y @^-1 y)); last first.
   by apply/setP => -[a b]; rewrite !inE.
@@ -2738,7 +2738,7 @@ rewrite (_ : [set x0 | _] =
     finset (X @^-1 x) `* finset (Y @^-1 y))%set; last first.
   by apply/setP => -[a b]; rewrite !inE /= xpair_eqE.
 rewrite Pr_fdist_prod_of_rV
-    (_ : [set x0 | _] = finset (X @^-1 x) `*T); last first.
+    (_ : [set x0 | _] = (finset (X @^-1 x)) `*T); last first.
   by apply/setP => a; rewrite !inE.
 rewrite Pr_fdist_prod_of_rV1.
 rewrite (_ : [set x0 | _] = T`* finset (Y @^-1 y)); last first.