fixes #203 (#208)

* fixes #203

Author: affeldt-aist

.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

@@ -878,8 +878,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

@@ -53,12 +53,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.
 Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)

information_theory/entropy.v

@@ -38,10 +38,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.
@@ -117,7 +117,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) :
@@ -144,7 +145,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

@@ -81,49 +81,50 @@ Lemma prodr_gt0 (R : numDomainType) (A : finType) (F : A -> R) :
   (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.
 
@@ -323,9 +324,6 @@ Global Hint Resolve 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.
@@ -866,19 +864,3 @@ Lemma s_of_gt0_oprob p q : 0 < [s_of (OProb.p p), (OProb.p q)]%:num.
 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.
@@ -2516,7 +2516,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'.
@@ -2657,7 +2657,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.
 Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)