Cleaning 20231121

_CoqProject

@@ -24,7 +24,6 @@ lib/euclid.v
 lib/dft.v
 lib/vandermonde.v
 lib/classical_sets_ext.v
-lib/Rstruct_ext.v
 probability/fdist.v
 probability/proba.v
 probability/fsdist.v

ecc_classic/decoding.v

@@ -1,14 +1,13 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp ssrnum.
-From mathcomp Require Import matrix vector order.
-From mathcomp Require Import lra Rstruct reals.
+From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm.
+From mathcomp Require Import zmodp matrix vector order.
+From mathcomp Require Import lra mathcomp_extra Rstruct reals.
 From mathcomp Require ssrnum.
 Require Import Reals.
-Require Import ssrR Reals_ext ssr_ext ssralg_ext Rbigop f2 fdist proba.
-Require Import realType_ext.
+Require Import ssrR realType_ext Reals_ext ssr_ext ssralg_ext Rbigop f2 fdist.
+Require Import proba.
 Require Import channel_code channel binary_symmetric_channel hamming pproba.
-Require Import Rstruct_ext.
 
 (******************************************************************************)
 (*                      The variety of decoders                               *)
@@ -225,7 +224,7 @@ Variable enc : encT [finType of 'F_2] M n.
 Hypothesis compatible : cancel_on C enc discard.
 Variable P : {fdist 'rV['F_2]_n}.
 
-Lemma MD_implies_ML : p < 1/2 :> R-> MD_decoding [set cw in C] f ->
+Lemma MD_implies_ML : Prob.p p < 1/2 :> R-> MD_decoding [set cw in C] f ->
   (forall y, f y != None) -> ML_decoding W C f P.
 Proof.
 move=> p05 MD f_total y.
@@ -242,7 +241,7 @@ case: oc Hoc => [c|] Hc; last first.
 exists c; split; first by reflexivity.
 (* replace  W ``^ n (y | f c) with a closed formula because it is a BSC *)
 pose dH_y c := dH y c.
-pose g : nat -> R := fun d : nat => ((1 - p) ^ (n - d) * p ^ d)%R.
+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 _ _ _.
@@ -262,9 +261,9 @@ transitivity (\big[Order.max/0]_(c in C) (g (dH_y c))); last first.
 rewrite (@bigmaxR_bigmin_vec_helper _ _ _ _ _ _ _ _ _ _ codebook_not_empty) //.
 - by rewrite bigmaxRE; apply eq_bigl => /= i; rewrite inE.
 - by apply bsc_prob_prop.
-- move=> r; rewrite /g Prob_pE !coqRE.
+- move=> r; rewrite /g !coqRE.
   apply/RleP/mulr_ge0; apply/exprn_ge0; last exact/prob_ge0.
-  exact/RleP/onem_ge0/RleP/prob_le1.
+  exact/onem_ge0/prob_le1.
 - rewrite inE; move/subsetP: f_img; apply.
   rewrite inE; apply/existsP; by exists (receivable_rV y); apply/eqP.
 - by move=> ? _; rewrite /dH_y max_dH.

ecc_classic/hamming_code.v

@@ -3,8 +3,8 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix mxalgebra vector.
 From mathcomp Require Import Rstruct.
-Require Import ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext.
-Require Import Rbigop fdist proba channel channel_code decoding.
+Require Import realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming.
+Require Import bigop_ext Rbigop fdist proba channel channel_code decoding.
 Require Import binary_symmetric_channel.
 
 (******************************************************************************)
@@ -978,13 +978,13 @@ Local Open Scope R_scope.
 Lemma e_hamming m0 :
   e(W, hamming_channel_code) m0 =
   \sum_(e0 in [set e0 : 'rV['F_2]_n | (2 <= wH e0)%nat])
-    (1 - p) ^ (n - wH e0) * p ^ wH e0.
+    (1 - Prob.p p) ^ (n - wH e0) * (Prob.p p) ^ wH e0.
 Proof.
 rewrite /ErrRateCond /Pr /=.
 transitivity (
   \sum_(a | a \in preimC (dec hamming_channel_code) m0)
     let d := dH ((enc hamming_channel_code) m0) a in
-    (1 - p) ^ (n - d) * p ^ d).
+    (1 - Prob.p p) ^ (n - d) * (Prob.p p) ^ d).
   apply eq_bigr => t Ht.
   rewrite dH_sym.
   rewrite -(DMC_BSC_prop p (enc hamming_channel_code) m0 t).
@@ -995,7 +995,7 @@ transitivity (
                            m1 != m0 else
                            true])
       (let d := dH ((enc hamming_channel_code) m0) a in
-       (1 - p) ^ (n - d) * p ^ d)).
+       (1 - Prob.p p) ^ (n - d) * (Prob.p p) ^ d)).
   apply eq_bigl => t /=.
   rewrite !inE.
   case_eq (dec hamming_channel_code t) => [m1 Hm1|]; last first.
@@ -1007,7 +1007,7 @@ set f := fun y => (y0 + y).
 Local Open Scope R_scope.
 transitivity (
   \sum_(y | f y \in [set e1 | (1 < wH e1)%nat])
-    (1 - p) ^ (n - wH (f y)) * p ^ wH (f y)).
+    (1 - Prob.p p) ^ (n - wH (f y)) * (Prob.p p) ^ wH (f y)).
   apply eq_big.
     move=> y.
     simpl in y, f, m0.
@@ -1043,9 +1043,9 @@ apply/esym/reindex.
 exists f; move=> /= x _; by rewrite /f addrA F2_addmx add0r.
 Qed.
 
-Lemma hamming_error_rate : p < 1/2 ->
+Lemma hamming_error_rate : Prob.p p < 1/2 ->
   echa(W, hamming_channel_code) =
-    1 - ((1 - p) ^ n) - INR n * p * ((1 - p) ^ (n - 1)).
+    1 - ((1 - Prob.p p) ^ n) - n%:R * (Prob.p p) * ((1 - Prob.p p) ^ (n - 1)).
 Proof.
 move=> p05.
 rewrite /CodeErrRate.
@@ -1062,7 +1062,7 @@ have -> : 1 / den * den = 1.
 rewrite mul1R.
 have toleft A B C D : A + C + D = B -> A = B - C - D by move => <-; ring.
 apply toleft.
-rewrite -addRA -(hamming_01 n p) //.
+rewrite -addRA -(hamming_01 n (Prob.p p)) //.
 rewrite -big_union //.
   rewrite (_ : _ :|: _ = [set: 'rV_n]).
     by apply binomial_theorem.

ecc_modern/ldpc.v

@@ -8,7 +8,6 @@ Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext num_occ bigop_ext
 Require Import fdist channel pproba f2 linearcode subgraph_partition tanner.
 Require Import tanner_partition hamming binary_symmetric_channel decoding.
 Require Import channel_code summary checksum summary_tanner.
-Require Import Rstruct_ext.
 
 (******************************************************************************)
 (*                   LDPC Codes and Sum-Product Decoding                      *)

information_theory/binary_symmetric_channel.v

@@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra Rstruct classical_sets.
 Require Import Reals Lra.
 Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext Rbigop fdist.
 Require Import entropy binary_entropy_function channel hamming channel_code.
-Require Import pproba Rstruct_ext.
+Require Import pproba.
 
 (******************************************************************************)
 (*                Capacity of the binary symmetric channel                    *)
@@ -76,15 +76,12 @@ rewrite /log LogM; last 2 first.
   move/eqP in H1.
   have [+ _] := fdist_gt0 P a.
   by move/(_ H1) => /RltP.
-  case/andP: p_01' => ? ?.
-  apply/Reals_ext.onem_gt0.
-  by apply/RltP.
+  by case/andP: p_01' => ? ?; exact/RltP/onem_gt0.
 rewrite /log LogM; last 2 first.
   move/eqP in H1.
   have [+ _] := fdist_gt0 P a.
   by move/(_ H1) => /RltP.
-  case/andP: p_01' => ? ?.
-  by apply/RltP.
+  by case/andP: p_01' => ? ?; exact/RltP.
 case: (Req_EM_T (P b) 0) => H2.
   rewrite H2 !(mul0R, mulR0, addR0, add0R).
   move: (FDist.f1 P); rewrite Set2sumE /= -/a -/b.
@@ -96,15 +93,12 @@ rewrite /log LogM; last 2 first.
   move/eqP in H2.
   have [+ _] := fdist_gt0 P b.
   by move/(_ H2) => /RltP.
-  case/andP: p_01' => ? ?.
-  by apply/RltP.
+  by case/andP: p_01' => ? ?; exact/RltP.
 rewrite /log LogM; last 2 first.
   move/eqP in H2.
   have [+ _] := fdist_gt0 P b.
   by move/(_ H2) => /RltP.
-  case/andP: p_01' => ? ?.
-  apply/Reals_ext.onem_gt0.
-  by apply/RltP.
+  by case/andP: p_01' => ? ?; exact/RltP/onem_gt0.
 rewrite /log.
 rewrite -!RmultE.
 rewrite /onem -RminusE (_ : 1%mcR = 1)//.
@@ -291,11 +285,11 @@ Variables (M : finType) (n : nat) (f : encT [finType of 'F_2] M n).
 Local Open Scope vec_ext_scope.
 
 Lemma DMC_BSC_prop m y : let d := dH y (f m) in
-  W ``(y | f m) = ((1 - p) ^ (n - d) * p ^ d)%R.
+  W ``(y | f m) = ((1 - Prob.p p) ^ (n - d) * Prob.p p ^ d)%R.
 Proof.
 move=> d; rewrite DMCE.
-transitivity ((\prod_(i < n | (f m) ``_ i == y ``_ i) (1 - p)) *
-              (\prod_(i < n | (f m) ``_ i != y ``_ i) p))%R.
+transitivity ((\prod_(i < n | (f m) ``_ i == y ``_ i) (1 - Prob.p p)) *
+              (\prod_(i < n | (f m) ``_ i != y ``_ i) Prob.p p))%R.
   rewrite (bigID [pred i | (f m) ``_ i == y ``_ i]) /=; congr (_ * _).
     by apply eq_bigr => // i /eqP ->; rewrite /BSC.c fdist_binaryxx.
   apply eq_bigr => //= i /negbTE Hyi; by rewrite /BSC.c fdist_binaryE eq_sym Hyi.
@@ -332,11 +326,10 @@ apply: exprn_ege1.
 by rewrite ler_pdivlMr // mul1r.
 Qed.
 
-Lemma bsc_prob_prop p n : p%:pp < 1 / 2 ->
+Lemma bsc_prob_prop (p : {prob R}) n : Prob.p p < 1 / 2 ->
   forall n1 n2 : nat, (n1 <= n2 <= n)%nat ->
-  ((1 - p) ^ (n - n2) * p ^ n2 <= (1 - p) ^ (n - n1) * p ^ n1)%R.
+  ((1 - Prob.p p) ^ (n - n2) * (Prob.p p) ^ n2 <= (1 - Prob.p p) ^ (n - n1) * (Prob.p p) ^ n1)%R.
 Proof.
-rewrite Prob_pE.
 move=> p05 d1 d2 d1d2.
 case/boolP: (p == R0%:pr).
   move/eqP->; rewrite !coqRE; apply/RleP.

information_theory/conditional_divergence.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg finset matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext ssr_ext ssralg_ext logb Rbigop ln_facts.
+Require Import ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb Rbigop ln_facts.
 Require Import num_occ fdist entropy channel divergence types jtypes.
 Require Import proba jfdist_cond.
 

information_theory/entropy.v

@@ -1,10 +1,11 @@
-(* infotheo: information theory and error-correcting codes in Coq               *)
-(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later              *)
+(* infotheo: information theory and error-correcting codes in Coq             *)
+(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect all_algebra fingroup perm matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext ssr_ext ssralg_ext Rbigop bigop_ext logb ln_facts.
-Require Import fdist jfdist_cond proba binary_entropy_function divergence.
+Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext Rbigop bigop_ext.
+Require Import logb ln_facts fdist jfdist_cond proba binary_entropy_function.
+Require Import divergence.
 
 (******************************************************************************)
 (*                Chapter 2 of Elements of Information Theory                 *)
@@ -114,7 +115,7 @@ by rewrite -INRE; apply/ltR0n.
 Qed.
 
 Lemma entropy_H2 (card_A : #|A| = 2%nat) (p : {prob R}) :
-  H2 p = entropy (fdist_binary card_A p (Set2.a card_A)).
+  H2 (Prob.p p) = entropy (fdist_binary card_A p (Set2.a card_A)).
 Proof.
 rewrite /H2 /entropy Set2sumE /= fdist_binaryxx !fdist_binaryE.
 by rewrite eq_sym (negbTE (Set2.a_neq_b _)) oppRD addRC.

information_theory/entropy_convex.v

@@ -156,7 +156,7 @@ have [x2a0|x2a0] := eqVneq (x.2 a) 0.
   simpl.
   by field; split; exact/eqP.
 set h : {fdist A} -> {fdist A} -> {ffun 'I_2 -> R} := fun p1 p2 => [ffun i =>
-  [eta (fun=> 0) with ord0 |-> p * p1 a, lift ord0 ord0 |-> (Prob.p p).~ * p2 a] i].
+  [eta (fun=> 0) with ord0 |-> Prob.p p * p1 a, lift ord0 ord0 |-> (Prob.p p).~ * p2 a] i].
 have hdom : h x.1 y.1 `<< h x.2 y.2.
   apply/dominatesP => i; rewrite /h /= !ffunE; case: ifPn => _.
     by rewrite mulR_eq0 => -[->|/eqP]; [rewrite mul0R | rewrite (negbTE x2a0)].
@@ -208,7 +208,7 @@ Proof.
 apply RNconcave_function => p q t; rewrite /convex_function_at.
 rewrite !(entropy_log_div _ cardApredS) /= /leconv /= [in X in _ <= X]avgRE.
 rewrite oppRD oppRK 2!mulRN mulRDr mulRN mulRDr mulRN oppRD oppRK oppRD oppRK.
-rewrite addRCA !addRA -2!mulRN -mulRDl (addRC _ t).
+rewrite addRCA !addRA -2!mulRN -mulRDl (addRC _ (Prob.p t)).
 rewrite !RplusE onemKC mul1R -!RplusE -addRA leR_add2l.
 have := convex_relative_entropy t (dom_by_uniform p cardApredS)
                                   (dom_by_uniform q cardApredS).
@@ -375,9 +375,9 @@ rewrite 2!big_distrr -big_split /=; apply eq_bigr => a _.
 rewrite !fdistX2 !fdist_fstE !mulRN -oppRD; congr (- _).
 rewrite !big_distrr -big_split /=; apply eq_bigr => b _.
 rewrite !big_distrl !big_distrr -big_split /=; apply eq_bigr => b0 _.
-rewrite !fdist_prodE /= fdist_convE /= !(mulRA t) !(mulRA (Prob.p t).~).
+rewrite !fdist_prodE /= fdist_convE /= !(mulRA (Prob.p t)) !(mulRA (Prob.p t).~).
 rewrite -!(RmultE,RplusE).
-have [Hp|/eqP Hp] := eqVneq (t * p a) 0.
+have [Hp|/eqP Hp] := eqVneq (Prob.p t * p a) 0.
   rewrite Hp ?(add0R,mul0R).
   have [->|/eqP Hq] := eqVneq ((Prob.p t).~ * q a) 0.
     by rewrite ?(mul0R).

information_theory/erasure_channel.v

@@ -1,10 +1,10 @@
-(* infotheo: information theory and error-correcting codes in Coq              *)
-(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later             *)
+(* infotheo: information theory and error-correcting codes in Coq             *)
+(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect all_algebra matrix.
 Require Import Reals.
-From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb Rbigop fdist entropy.
-Require Import binary_entropy_function channel hamming channel_code.
+From mathcomp Require Import mathcomp_extra Rstruct.
+Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb Rbigop fdist.
+Require Import entropy binary_entropy_function channel hamming channel_code.
 
 (******************************************************************************)
 (*                     Definition of erasure channel                          *)
@@ -41,8 +41,8 @@ rewrite /f ffunE.
 case: b => [a'|]; last first.
   by case: p_01 => /RleP.
 case: ifP => _ //.
-case: p_01 => ? ?//.
-by apply/RleP/onem_ge0.
+case: p_01 => ? ? //.
+exact/onem_ge0/RleP.
 Qed.
 
 Lemma f1 (a : A) : \sum_(a' : {:option A}) f a a' = 1.
@@ -54,10 +54,10 @@ apply/eqP; rewrite psumr_eq0/=; last first.
  - rewrite /f; case => [a'|]; last by case: p_01.
   rewrite ffunE.
   case: ifPn => [_ _|//].
-  by case: p_01 => ? ?; apply/RleP/onem_ge0.
+  by case: p_01 => ? ?; apply/onem_ge0/RleP.
 - apply/allP; case => //= a' aa'; rewrite ffunE; case: ifPn => // /eqP ?.
     subst a'.
-    move: aa'; by rewrite eqxx.
+    by move: aa'; rewrite eqxx.
   by rewrite eqxx implybT.
 Qed.
 

information_theory/error_exponent.v

@@ -2,12 +2,10 @@
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 Require Import Reals Lra.
-From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext Ranalysis_ext logb ln_facts Rbigop fdist entropy.
-From mathcomp Require Import reals.
-Require Import realType_ext Rstruct_ext.
-Require Import channel_code channel divergence conditional_divergence.
-Require Import variation_dist pinsker.
+From mathcomp Require Import Rstruct reals.
+Require Import ssrR realType_ext Reals_ext Ranalysis_ext logb ln_facts Rbigop.
+Require Import fdist entropy channel_code channel divergence.
+Require Import conditional_divergence variation_dist pinsker.
 
 (******************************************************************************)
 (*                         Error exponent bound                               *)

information_theory/string_entropy.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext Rstruct_ext realType_ext ssr_ext ssralg_ext logb.
+Require Import ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb.
 Require Import Rbigop fdist entropy convex ln_facts jensen num_occ.
 
 (******************************************************************************)

information_theory/success_decode_bound.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Rstruct_ext Reals_ext ssr_ext ssralg_ext logb Rbigop fdist entropy.
+Require Import ssrR Reals_ext ssr_ext ssralg_ext logb Rbigop fdist entropy.
 Require Import ln_facts num_occ types jtypes divergence conditional_divergence.
 Require Import entropy channel_code channel.
 

lib/Rbigop.v

@@ -492,6 +492,21 @@ Qed.
 Local Close Scope vec_ext_scope.
 Local Close Scope ring_scope.
 
+Lemma bigmaxRE (I : Type) (r : seq I) (P : pred I) (F : I -> R) :
+  \rmax_(i <- r | P i) F i = \big[Order.max/0]_(i <- r | P i) F i.
+Proof.
+rewrite /Rmax /Order.max/=.
+congr BigOp.bigop.
+apply: boolp.funext=> i /=.
+congr BigBody.
+apply: boolp.funext=> x /=.
+apply: boolp.funext=> y /=.
+rewrite lt_neqAle.
+case: (Rle_dec x y); move/RleP;
+  first by case/boolP: (x == y) => /= [/eqP -> | _ ->].
+by move/negPf->; rewrite andbF.
+Qed.
+
 Section bigmaxR.
 
 Variables (A : eqType) (F : A -> R) (s : seq A).