Merge pull request #80 from affeldt-aist/compat_mathcomp_1150

compatibility with mc 1.15.0

.github/workflows/docker-action.yml

@@ -21,6 +21,8 @@ jobs:
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-8.14'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -98,11 +98,11 @@ Each file is documented in its header.
 
 Changes are documented in [changelog.txt](changelog.txt).
 
-## Installation with Windows 10
+## Installation with Windows 10 & 11
 
 Installation of infotheo on Windows is less simple.
 See [this page](https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org)
-for instructions to install MathComp on Windows 10
+for instructions to install MathComp on Windows 10 & 11
 (or [this page](https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html) for instructions in Japanese).
 
 Once MathComp is installed (with opam), do

changelog.txt

@@ -1,3 +1,8 @@
+-------------------
+from 0.3.7 to 0.3.8
+-------------------
+compatibility release
+
 -------------------
 from 0.3.6 to 0.3.7
 -------------------

coq-infotheo.opam

@@ -22,12 +22,12 @@ build: [
 install: [make "install"]
 depends: [
   "coq" { (>= "8.14" & < "8.16~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev") }
-  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "0.4.0") & (< "0.6~")}
+  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") }
+  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-field" { (>= "1.13.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-analysis" { (>= "0.5.3") & (< "0.6~")}
 ]
 
 tags: [

ecc_classic/hamming_code.v

@@ -115,7 +115,7 @@ apply rV_of_nat_neq0 => //.
 by rewrite -(addn1 i) addnC -ltn_subRL subn1 -Hamming.len_dim.
 Qed.
 
-Lemma no_weight_2_cw x : wH x = 2 -> syndrome H x <> 0.
+Lemma no_weight_2_cw x : wH x = 2%N -> syndrome H x <> 0.
 Proof.
 move=> /wH_2[i [j [Hij [Hi [Hj Hk]]]]].
 rewrite /syndrome mulmx_sum_col (bigID (pred1 i)) /= big_pred1_eq /=.
@@ -211,14 +211,14 @@ rewrite memv_ker lfunE /= weight_3_cw eqxx /=.
 apply/eqP/rV_of_nat_neq0 => //; [exact: rev7_neq0 | exact: rev7_ub (Hamming.two_len _)].
 Qed.
 
-Lemma hamming_min_dist : min_dist hamming_not_trivial = 3.
+Lemma hamming_min_dist : min_dist hamming_not_trivial = 3%N.
 Proof.
 move: (min_dist_is_min hamming_not_trivial) => Hforall.
 move: (min_dist_achieved hamming_not_trivial) => Hexists.
 move: (min_dist_neq0) => H3.
-suff : min_dist hamming_not_trivial <> 1%nat /\
-       min_dist hamming_not_trivial <> 2 /\
-       min_dist hamming_not_trivial <= 3.
+suff : min_dist hamming_not_trivial <> 1%N /\
+       min_dist hamming_not_trivial <> 2%N /\
+       min_dist hamming_not_trivial <= 3%N.
   move : H3.
   move/(_ _ _ _ hamming_not_trivial).
   destruct (min_dist hamming_not_trivial) as [|p]=> //.
@@ -235,7 +235,7 @@ split => [min2 | ].
   rewrite min2 => /no_weight_2_cw; apply.
   move: Hc; by rewrite memv_ker lfunE /= => /eqP.
 move: (Hforall (rV_of_nat n (7 * 2 ^ (n - 3)))).
-have -> : wH (rV_of_nat n (7 * 2 ^ (n - 3))) = 3.
+have -> : wH (rV_of_nat n (7 * 2 ^ (n - 3))) = 3%N.
   by rewrite -wH_7_rev7 ?Hamming.two_len // wH_7 // Hamming.two_len.
 apply; first by rewrite memv_ker lfun_simp /= weight_3_cw.
 apply/eqP/rV_of_nat_neq0; [exact: rev7_neq0 | exact: rev7_ub (Hamming.two_len _)].
@@ -965,7 +965,7 @@ Section hamming_code_error_rate.
 Variable M : finType.
 Hypothesis M_not_0 : 0 < #|M|.
 Variable p : prob.
-Let card_F2 : #| 'F_2 | = 2. by rewrite card_Fp. Qed.
+Let card_F2 : #| 'F_2 | = 2%N. by rewrite card_Fp. Qed.
 Let W := BSC.c card_F2 p.
 
 Variable m' : nat.

ecc_classic/poly_decoding.v

@@ -48,7 +48,7 @@ Qed.
 
 (* TODO: useful? *)
 Lemma size_one_minus_X (R : idomainType) (a : R) (a0 : a != 0) :
-  size (1 - a *: 'X) = 2.
+  size (1 - a *: 'X) = 2%N.
 Proof.
 rewrite addrC size_addl.
   by rewrite size_opp size_scale ?size_polyX // expf_neq0.

ecc_modern/ldpc_erasure.v

@@ -75,7 +75,7 @@ Qed.
 Definition letter_pickle (l : letter) :=
   match l with
   | Bit a => if a == (Zp0 : 'F_2) then O else 1%N
-  | Star => 2
+  | Star => 2%N
   | Blank => 3%N
   end.
 

ecc_modern/stopping_set.v

@@ -129,7 +129,7 @@ case/orP: {Hs1}(Hp _ (Hs1 m0)) => [|{Hp}Hs1].
   move=> Hs1; rewrite cards_eq0 => /eqP Hs2; apply/orP; right.
   by rewrite setIUl Hs2 set0U.
 apply/orP; right.
-by rewrite setIUl cardsU -(addn0 2) -addnBA ?leq_add // subset_leq_card // subsetIr.
+by rewrite setIUl cardsU -(addn0 2%N) -addnBA ?leq_add // subset_leq_card // subsetIr.
 Qed.
 
 Lemma stopsetE_help (s : {set 'I_n}) m0 n0 :

information_theory/binary_symmetric_channel.v

@@ -176,14 +176,16 @@ have has_sup_E : has_sup E.
   rewrite addRC -leR_subl_addr subRR.
   by rewrite (entropy_H2 card_A (Prob.mk_ (ltR2W p_01'))); exact/entropy_ge0.
 apply eqR_le; split.
-  apply real_sup_is_lub => // x [d _ dx].
+  apply/RleP.
+  have [_ /(_ (1 - H2 p))] := Rsup_isLub (0 : R) has_sup_E.
+  apply => x [d _ dx]; apply/RleP.
   suff : `H(d `o BSC.c card_A p_01) <= 1.
     move: (@IPW _ card_A d _ p_01') => ?.
     by unfold p_01 in *; lra.
   exact: H_out_max.
 move: (@IPW _ card_A (Uniform.d card_A) _ p_01').
 rewrite H_out_binary_uniform => <-.
-by apply/RleP/(@real_sup_ub) => //;exists (Uniform.d card_A).
+by apply/RleP/Rsup_ub => //=; exists (Uniform.d card_A).
 Qed.
 
 End bsc_capacity_theorem.

information_theory/channel.v

@@ -380,4 +380,4 @@ From mathcomp Require Import classical_sets.
 Local Open Scope classical_set_scope.
 
 Definition capacity (A B : finType) (W : `Ch(A, B)) :=
-  real_sup [set `I(P, W) | P in @setT (fdist A)].
+  reals.sup [set `I(P, W) | P in @setT (fdist A)].

information_theory/channel_coding_direct.v

@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix perm.
 Require Import Reals Lra Classical.
-From mathcomp Require Import Rstruct.
+From mathcomp Require Import Rstruct classical_sets.
 Require Import ssrZ ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop.
 Require Import fdist proba entropy aep typ_seq joint_typ_seq channel.
 Require Import channel_code.
@@ -134,7 +134,7 @@ rewrite wght_o_PI; congr (_ * _).
 rewrite /ErrRateCond /= (_ : (o_PI m m' g) m = g m'); last by rewrite ffunE tpermL.
 congr Pr; apply/setP => tb /=.
 rewrite 2!inE.
-apply/negbLR. rewrite in_setC negbK.
+apply/negbLR. rewrite finset.in_setC negbK.
 apply/idP/idP.
 - rewrite {1}/PHI' {1}/jtdec.
   rewrite ffunE.
@@ -653,25 +653,25 @@ apply/idP/idP.
 - rewrite /PHI' /jtdec ffunE.
   case: (pickP _) => [m2 Hm2 | Hm2].
   + move/eqP => m2m0.
-    rewrite in_setU in_setC {1}/Cal_E {1}/cal_E inE; apply/orP; left.
+    rewrite finset.in_setU finset.in_setC {1}/Cal_E {1}/cal_E inE; apply/orP; left.
     case/andP : Hm2 => _ /forallP/(_ ord0)/implyP; apply.
     by move/eqP in m2m0; apply: contra m2m0 => /eqP <-.
   + move=> _.
-    rewrite in_setU.
+    rewrite finset.in_setU.
     move/negbT : {Hm2}(Hm2 ord0).
     rewrite negb_and.
     case/orP => Hm2.
-    * by rewrite in_setC {1}/Cal_E {1}/cal_E inE Hm2.
+    * by rewrite finset.in_setC {1}/Cal_E {1}/cal_E inE Hm2.
     * apply/orP; right.
       apply/negPn.
       move: Hm2; apply contra => Hm2.
       apply/forallP => m_; apply/implyP => m_m0.
       apply: contra Hm2 => Hm2.
       apply/bigcupP; exists m_ => //; by rewrite /Cal_E /cal_E inE.
-- rewrite in_setU ffunE.
+- rewrite finset.in_setU ffunE.
   case: (pickP _) => [m2 Hm2|//].
   case/orP.
-  + rewrite in_setC /cal_E inE => Hy.
+  + rewrite finset.in_setC /cal_E inE => Hy.
     apply/eqP => -[m20].
     by case/andP : Hm2; rewrite m20 (negbTE Hy).
   + case/bigcupP => m Hm; rewrite /cal_E 2!inE => m_tb.
@@ -757,13 +757,13 @@ have -> : lhs = (#| M |.-1%:R * Pr ((P `^ n) `x ((`O(P , W)) `^ n)) [set x | pro
     Pr ((P `^ n) `x ((`O( P , W )) `^ n)) [set x | prod_rV x \in `JTS P W n epsilon0])%R; last first.
     rewrite big_const /= iter_addR; congr (_%:R * _)%R.
     rewrite card_ord /=.
-    transitivity (#| setT :\ (@ord0 k)|).
-      move: (cardsD1 (@ord0 k) setT) => /=.
+    transitivity (#| finset.setT :\ (@ord0 k)|).
+      move: (cardsD1 (@ord0 k) finset.setT) => /=.
       rewrite !cardsT !card_ord inE /= add1n.
       case=> H1; by rewrite {1}H1.
     rewrite cardsE.
     apply eq_card => m_.
-    by rewrite -!topredE /= !in_set andbC.
+    by rewrite -!topredE /= !finset.in_set andbC.
   by apply eq_big => //; exact: second_summand.
 rewrite card_ord /=.
 apply (@leR_ltR_trans (epsilon0 + k%:R *
@@ -827,10 +827,13 @@ have [P HP] : exists P : fdist A, r < `I(P, W).
     move/not_ex_all_not in abs.
     move=> P; exact/Rnot_lt_le/abs.
   have ? : capacity W <= r.
-    apply Rstruct.real_sup_is_lub.
+    apply/RleP.
+    have : has_sup [set `I(P, W) | P in [set: fdist A]].
       case: set_of_I_nonempty => [x [P H1]]; split; first by exists x, P.
       by exists (rate r) => _ [Q _ <-]; exact/Rstruct.RleP/abs.
-    by move=> x [P _ <-{x}]; exact: abs.
+    move=> /(@Rsup_isLub 0 [set `I(P, W) | P in [set: fdist A]])[_].
+    apply.
+    by move=> x [P _ <-{x}]; exact/RleP/abs.
   lra.
 have [epsilon0 Hepsilon0] : exists epsilon0,
   0 < epsilon0 /\ epsilon0 < epsilon / 2 /\ epsilon0 < (`I(P, W) - r) / 4.

information_theory/error_exponent.v

@@ -165,7 +165,7 @@ have : `I(P, V) <= capacity W + / ln 2 * (#|B|%:R + #|A|%:R * #|B|%:R) *
                                (- xlnx (sqrt (2 * D(V || W | P)))).
   apply (@leR_trans (`I(P, W) + / ln 2 * (#|B|%:R + #|A|%:R * #|B|%:R) *
                                - xlnx (sqrt (2 * D(V || W | P))))); last first.
-    apply/leR_add2r/Rstruct.RleP/Rstruct.real_sup_ub; last by exists P.
+    apply/leR_add2r/Rstruct.RleP/Rstruct.Rsup_ub; last by exists P.
     split; first by exists (`I(P, W)), P.
     case: set_of_I_has_ubound => y Hy.
     by exists y => _ [Q _ <-]; apply Hy; exists Q.

lib/ssralg_ext.v

@@ -500,7 +500,7 @@ Qed.
 
 End about_row_vectors_on_prime_fields.
 
-Lemma sum_char2 (F : fieldType) (_ : 2 \in [char F]) k (f : 'I_k -> F) :
+Lemma sum_char2 (F : fieldType) (_ : 2%N \in [char F]) k (f : 'I_k -> F) :
   (\sum_(i < k) (f i)) ^+ 2 = \sum_(i < k) (f i) ^+ 2.
 Proof.
 elim/big_ind2 : _ => [|x1 x2 y1 y2 <- <-|//] /=; first by rewrite expr0n.

meta.yml

@@ -53,36 +53,40 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev")  }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev")  }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev")  }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev")  }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev")  }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "0.4.0") & (< "0.6~")}'
+    version: '{ (>= "0.5.3") & (< "0.6~")}'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 namespace: infotheo
@@ -171,11 +175,11 @@ documentation: |-
 
   Changes are documented in [changelog.txt](changelog.txt).
   
-  ## Installation with Windows 10
+  ## Installation with Windows 10 & 11
 
   Installation of infotheo on Windows is less simple.
   See [this page](https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org)
-  for instructions to install MathComp on Windows 10
+  for instructions to install MathComp on Windows 10 & 11
   (or [this page](https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html) for instructions in Japanese).
 
   Once MathComp is installed (with opam), do