Cleaning 20231122 (#107)

* rm sumR_ge0, big_ord1_eq, bigcap_const

* generalize big_tuple_ffun

* rm Rbigop.v, bigcap_ext

* etc.
---------

Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

_CoqProject

@@ -14,7 +14,6 @@ lib/ssr_ext.v
 lib/f2.v
 lib/ssralg_ext.v
 lib/bigop_ext.v
-lib/Rbigop.v
 lib/natbin.v
 lib/binary_entropy_function.v
 lib/num_occ.v

ecc_classic/decoding.v

@@ -5,7 +5,7 @@ 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 realType_ext Reals_ext ssr_ext ssralg_ext Rbigop f2 fdist.
+Require Import ssrR realType_ext Reals_ext ssr_ext ssralg_ext f2 fdist.
 Require Import proba.
 Require Import channel_code channel binary_symmetric_channel hamming pproba.
 

ecc_classic/hamming_code.v

@@ -4,7 +4,7 @@ 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 realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming.
-Require Import bigop_ext Rbigop fdist proba channel channel_code decoding.
+Require Import bigop_ext fdist proba channel channel_code decoding.
 Require Import binary_symmetric_channel.
 
 (******************************************************************************)

ecc_modern/checksum.v

@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix vector.
 Require Import Reals.
 Require Import ssralg_ext ssrR Reals_ext f2 fdist channel tanner linearcode.
-Require Import Rbigop pproba.
+Require Import pproba.
 
 (******************************************************************************)
 (*                         Checksum Operator                                  *)

ecc_modern/ldpc.v

@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix vector ssrnum.
 Require Import Reals Lra.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext num_occ bigop_ext Rbigop.
+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.
@@ -456,7 +456,7 @@ transitivity (
   \sum_(x = d [~ setT :\ n0]) \prod_(m0 in 'F n0)
     (W ``(y \# 'V(m0, n0) :\ n0 | x \# 'V(m0, n0) :\ n0) *
       \prod_(m1 in 'F(m0, n0)) (\delta ('V m1) x)%:R)).
-  apply eq_bigr => /= t Ht.
+  apply: eq_bigr => /= t Ht.
   rewrite [in X in _ = X]big_split /=; congr (_ * _).
   by apply DMC_sub_vec_Fnext.
 rewrite (@rmul_rsum_commute0 _ _ _ (Tanner.connected tanner)  (Tanner.acyclic tanner) d n0 _ y (fun m x y => W ``(x | y))) //.

ecc_modern/ldpc_algo.v

@@ -3,7 +3,7 @@
 Require Import Init.Wf Recdef Reals.
 From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext Rbigop f2 subgraph_partition tanner.
+Require Import ssrR Reals_ext f2 subgraph_partition tanner.
 Require Import fdist channel pproba linearcode ssralg_ext.
 Require Import tanner_partition summary ldpc checksum.
 

ecc_modern/ldpc_algo_proof.v

@@ -3,7 +3,7 @@
 Require Import Wf_nat Init.Wf Recdef Reals.
 From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext ssr_ext ssralg_ext bigop_ext Rbigop f2.
+Require Import ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2.
 Require Import fdist channel pproba linearcode subgraph_partition tanner.
 Require Import tanner_partition summary ldpc checksum ldpc_algo.
 

ecc_modern/summary.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg zmodp matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import ssr_ext ssralg_ext ssrR Rbigop f2.
+Require Import ssr_ext ssralg_ext ssrR f2.
 
 (******************************************************************************)
 (*                        The Summary Operator                                *)

ecc_modern/summary_tanner.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg zmodp matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import ssr_ext ssralg_ext ssrR Reals_ext Rbigop f2 summary.
+Require Import ssr_ext ssralg_ext ssrR Reals_ext f2 summary.
 Require Import subgraph_partition tanner tanner_partition fdist channel.
 Require Import checksum.
 

ecc_modern/tanner_partition.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix.
 From mathcomp Require Import Rstruct.
-Require Import ssr_ext subgraph_partition tanner f2 Rbigop.
+Require Import ssr_ext subgraph_partition tanner f2.
 
 (******************************************************************************)
 (*               Cover/partition properties of Tanner graphs                  *)
@@ -530,7 +530,7 @@ Qed.
 Local Open Scope R_scope.
 
 Lemma rprod_Fgraph_part_fnode g n0:
-  \prod_(m0 < m) g m0 = \prod_(m0 in 'F n0) \prod_(m1 in 'F(m0, n0)) g m1.
+  \prod_(m0 < m) g m0 = \prod_(m0 in 'F n0) \prod_(m1 in 'F(m0, n0)) g m1 :> Rdefinitions.R.
 Proof.
 transitivity (\prod_(m0 in [set: 'I_m]) g m0).
   apply eq_bigl => /= ?; by rewrite in_set.

information_theory/aep.v

@@ -1,11 +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 ssralg ssrnum matrix.
 From mathcomp Require boolp.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb Rbigop fdist proba.
-Require Import entropy.
+Require Import ssrR Reals_ext realType_ext ssr_ext bigop_ext ssralg_ext logb.
+Require Import fdist proba entropy.
 
 (******************************************************************************)
 (*              Asymptotic Equipartition Property (AEP)                       *)
@@ -140,12 +140,10 @@ apply/Pr_incl/subsetP => ta; rewrite 2!inE => /andP[H1].
 rewrite /sum_mlog_prod [`-- (`log _)]lock /= -lock /= /scalel_RV /log_RV /neg_RV.
 rewrite fdist_rVE.
 rewrite log_prodR_sumR_mlog //.
-have : forall x, 0 <= P x.
-  move=> x.
-  apply/RleP.
-  exact: FDist.ge0.
-move/prodR_gt0_inv; apply.
-by move: H1; rewrite fdist_rVE => /RltP.
+move=> i; apply/RltP.
+move: i; apply/prod_gt0_inv.
+  by move=> x; exact: FDist.ge0.
+by move: H1; rewrite fdist_rVE.
 Qed.
 
 End AEP.

information_theory/binary_symmetric_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            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum zmodp matrix lra.
-From mathcomp Require Import mathcomp_extra Rstruct classical_sets.
+From mathcomp Require Import mathcomp_extra classical_sets Rstruct reals.
 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 ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext.
+Require Import fdist entropy binary_entropy_function channel hamming channel_code.
 Require Import pproba.
 
 (******************************************************************************)
@@ -331,7 +331,7 @@ Lemma bsc_prob_prop (p : {prob R}) n : Prob.p p < 1 / 2 ->
   ((1 - Prob.p p) ^ (n - n2) * (Prob.p p) ^ n2 <= (1 - Prob.p p) ^ (n - n1) * (Prob.p p) ^ n1)%R.
 Proof.
 move=> p05 d1 d2 d1d2.
-case/boolP: (p == R0%:pr).
+case/boolP: (p == 0%:pr).
   move/eqP->; rewrite !coqRE; apply/RleP.
   rewrite probpK subr0 !expr1n !mul1r !expr0n.
   move: d1d2; case: d2; first by rewrite leqn0 => /andP [] ->.

information_theory/channel.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect all_algebra.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop fdist.
+Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist.
 Require Import proba entropy jfdist_cond.
 
 (******************************************************************************)
@@ -34,6 +34,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
+Import Num.Theory.
+
 Declare Scope channel_scope.
 Delimit Scope fdist_scope with channel.
 Local Open Scope channel_scope.
@@ -167,7 +169,7 @@ Local Open Scope ring_scope.
 Definition f := [ffun b : B => \sum_(a in A) W a b * P a].
 
 Let f0 (b : B) : (0 <= f b).
-Proof. by rewrite ffunE; apply/RleP; apply: sumR_ge0 => a _; exact: mulR_ge0. Qed.
+Proof. by rewrite ffunE; apply/RleP; apply/RleP/sumr_ge0 => a _; rewrite mulr_ge0. Qed.
 
 Let f1 : \sum_(b in B) f b = 1.
 Proof.

information_theory/channel_code.v

@@ -1,9 +1,9 @@
 (* 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 matrix.
+From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import Reals_ext ssrR logb Rbigop fdist proba channel.
+Require Import Reals_ext ssrR logb fdist proba channel.
 
 (******************************************************************************)
 (*                        Definition of a channel code                        *)
@@ -35,6 +35,8 @@ Local Open Scope proba_scope.
 Local Open Scope channel_scope.
 Local Open Scope R_scope.
 
+Import Num.Theory.
+
 Section code_definition.
 Variables (A B M : finType) (n : nat).
 
@@ -61,15 +63,15 @@ Local Notation "echa( W , c )" := (CodeErrRate W c) (at level 50).
 
 Lemma echa_ge0 (HM : (0 < #| M |)%nat) W (c : code) : 0 <= echa(W , c).
 Proof.
-apply mulR_ge0.
+apply/RleP/mulR_ge0.
 - apply divR_ge0; [exact/Rle_0_1| exact/ltR0n].
-- by apply: sumR_ge0 => ? _; exact: sumR_ge0.
+- by apply/RleP/sumr_ge0 => ? _; exact: sumr_ge0.
 Qed.
 
 Lemma echa_le1 (HM : (0 < #| M |)%nat) W (c : code) : echa(W , c) <= 1.
 Proof.
 rewrite /CodeErrRate div1R.
-apply (@leR_pmul2l (INR #|M|)); first exact/ltR0n.
+apply/RleP/ (@leR_pmul2l (INR #|M|)); first exact/ltR0n.
 rewrite mulRA mulRV ?INR_eq0' -?lt0n // mul1R -iter_addR -big_const.
 by apply: leR_sumR => m _; exact: Pr_1.
 Qed.
@@ -81,7 +83,7 @@ Local Notation "scha( W , C )" := (scha W C).
 Hypothesis Mnot0 : (0 < #|M|)%nat.
 
 Lemma scha_pos (W : `Ch(A, B)) (c : code) : 0 <= scha(W, c).
-Proof. rewrite /scha; rewrite subR_ge0; exact/echa_le1. Qed.
+Proof. by rewrite /scha; rewrite subr_ge0; exact/echa_le1. Qed.
 
 Lemma schaE (W : `Ch(A, B)) (c : code) :
   scha(W, c) = (1 / #|M|%:R *

information_theory/channel_coding_converse.v

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

information_theory/channel_coding_direct.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix perm.
 Require Import Reals Lra Classical.
 From mathcomp Require Import Rstruct classical_sets.
-Require Import ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext Rbigop.
+Require Import ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext.
 Require Import fdist proba entropy aep typ_seq joint_typ_seq channel.
 Require Import channel_code.
 
@@ -96,7 +96,7 @@ set x := \sum_(f <- _) _ in H.
 have : \sum_(f : encT A M n) Wght.d P f * epsilon <= x.
   rewrite /x; apply leR_sumRl => //= f _.
   - by apply leR_wpmul2l => //; exact/Rnot_lt_le/abs.
-  - by apply mulR_ge0 => //; exact/echa_ge0.
+  - by apply mulR_ge0 => //; exact/RleP/echa_ge0.
 apply/Rlt_not_le/(@ltR_leR_trans epsilon) => //.
 rewrite -big_distrl /= (FDist.f1 (Wght.d P)) mul1R.
 by apply/RleP; rewrite Order.POrderTheory.lexx.
@@ -367,7 +367,7 @@ transitivity (\sum_(v : 'rV[A]_n)
       move=> ? _; by rewrite -[in RHS]Hf !ffunE mxE.
   rewrite (_ : ord0 = nth ord0 (enum M) 0); last by rewrite enum_ordSl.
   rewrite -(big_tuple_ffun _ (fun f => \prod_(m : M) P `^ n (f m))
-    (fun r => fun yn => r *
+    (fun r yn => r *
       (\sum_(y in ~: [set y0 | prod_rV (yn, y0) \in `JTS P W n epsilon0])
       W ``(y | yn))) (\row_(i < n) a) ord0)%R.
   transitivity (\sum_(j : _)

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 realType_ext Reals_ext ssr_ext ssralg_ext logb Rbigop ln_facts.
+Require Import ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb ln_facts.
 Require Import num_occ fdist entropy channel divergence types jtypes.
 Require Import proba jfdist_cond.
 

information_theory/entropy.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect all_algebra fingroup perm matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext Rbigop bigop_ext.
+Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext.
 Require Import logb ln_facts fdist jfdist_cond proba binary_entropy_function.
 Require Import divergence.
 
@@ -69,7 +69,7 @@ Local Notation "'`H'" := (entropy).
 
 Lemma entropy_ge0 : 0 <= `H.
 Proof.
-rewrite /entropy big_morph_oppR; apply sumR_ge0 => i _.
+rewrite /entropy big_morph_oppR; apply/RleP/sumr_ge0 => i _; apply/RleP.
 have [->|Hi] := eqVneq (P i) 0; first by rewrite mul0R oppR0.
   (* NB: this step in a standard textbook would be handled as a consequence of lim x->0 x log x = 0 *)
 rewrite mulRC -mulNR; apply mulR_ge0 => //; apply: oppR_ge0.
@@ -261,17 +261,17 @@ Qed.
 
 Lemma cond_entropy1_ge0 a : 0 <= cond_entropy1 a.
 Proof.
-rewrite /cond_entropy1 big_morph_oppR; apply sumR_ge0 => b _; rewrite -mulRN.
+rewrite /cond_entropy1 big_morph_oppR; apply/RleP/sumr_ge0 => b _; rewrite -mulRN.
 have [->|H0] := eqVneq (\Pr_QP[[set b]|[set a]]) 0.
   by rewrite mul0R.
-apply mulR_ge0; [exact: jcPr_ge0|].
+apply/RleP/mulR_ge0; [exact: jcPr_ge0|].
 rewrite -oppR0 -(Log_1 2) /log leR_oppr oppRK.
 by apply Log_increasing_le => //; [rewrite jcPr_gt0 | exact: jcPr_le1].
 Qed.
 
 Lemma cond_entropy_ge0 : 0 <= cond_entropy.
 Proof.
-by apply sumR_ge0 => a _; apply mulR_ge0 => //; exact: cond_entropy1_ge0.
+by apply/RleP/sumr_ge0 => a _; apply/RleP/mulR_ge0 => //; exact: cond_entropy1_ge0.
 Qed.
 
 End conditional_entropy.
@@ -690,7 +690,7 @@ Qed.
 Lemma cdiv1_ge0 z : 0 <= cdiv1 z.
 Proof.
 have [z0|z0] := eqVneq (PQR`2 z) 0.
-  apply sumR_ge0 => -[a b] _.
+  apply/RleP/sumr_ge0 => -[a b] _; apply/RleP.
   by rewrite {1}/jcPr setX1 Pr_set1 (dom_by_fdist_snd _ z0) div0R mul0R.
 have Hc : (fdistX PQR)`1 z != 0 by rewrite fdistX1.
 have Hc1 : (fdistX (fdist_proj13 PQR))`1 z != 0.
@@ -797,7 +797,7 @@ Qed.
 (* 2.92 *)
 Lemma cond_mutual_info_ge0 : 0 <= cond_mutual_info PQR.
 Proof.
-rewrite cond_mutual_infoE2; apply sumR_ge0 => c _; apply mulR_ge0 => //.
+rewrite cond_mutual_infoE2; apply/RleP/sumr_ge0 => c _; apply/RleP/mulR_ge0 => //.
 exact: cdiv1_ge0.
 Qed.
 

information_theory/entropy_convex.v

@@ -3,10 +3,10 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
 From mathcomp Require boolp.
-From mathcomp Require Import mathcomp_extra Rstruct.
+From mathcomp Require Import mathcomp_extra Rstruct reals.
 Require Import Reals Ranalysis_ext Lra.
 Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext.
-Require Import Rbigop fdist jfdist_cond entropy convex binary_entropy_function.
+Require Import fdist jfdist_cond entropy convex binary_entropy_function.
 Require Import log_sum divergence.
 
 (******************************************************************************)
@@ -109,7 +109,7 @@ Definition uncurry_dom_pair U (f : {fdist A} -> {fdist A} -> U) (x : dom_pair) :
 
 Let avg := avg_dom_pair.
 
-Let avg1 x y : avg 1%coqR%:pr x y = x.
+Let avg1 x y : avg 1%:pr x y = x.
 Proof. by rewrite /avg; case x => x0 H /=; exact/boolp.eq_exist/conv1. Qed.
 
 Let avgI p x : avg p x x = x.
@@ -143,7 +143,7 @@ have [y2a0|y2a0] := eqVneq (y.2 a) 0.
     rewrite (_ : x.1 a = 0).
       by rewrite -!RmultE -!RplusE ?(mul0R,mulR0,addR0).
     exact/((dominatesP _ _).1 Hx).
-  have [p0|p0] := eqVneq p 0%coqR%:pr.
+  have [p0|p0] := eqVneq p 0%:pr.
     by rewrite p0 -!RmultE -!RplusE ?(mul0R,mulR0,addR0).
   apply/Req_le; rewrite -!RmultE -!RplusE mulRA ?(mulR0,addR0); congr (_ * _ * log _).
   simpl.
@@ -179,7 +179,7 @@ rewrite /= -!sumR_ord_setT !big_ord_recl !big_ord0 !addR0.
 rewrite /h /= !ffunE => /leR_trans; apply.
 rewrite !eqxx eq_sym (negbTE (neq_lift ord0 ord0)) -!mulRA; apply/Req_le.
 congr (_  + _ ).
-  have [->|t0] := eqVneq p 0%coqR%:pr; first by rewrite !mul0R.
+  have [->|t0] := eqVneq p 0%:pr; first by rewrite !mul0R.
   by congr (_ * (_ * log _)); field; split; exact/eqP.
 have [->|t1] := eqVneq (Prob.p p).~ 0; first by rewrite !mul0R.
 by congr (_ * (_ * log _)); field; split; exact/eqP.

information_theory/erasure_channel.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect all_algebra matrix.
 Require Import Reals.
 From mathcomp Require Import mathcomp_extra Rstruct.
-Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb Rbigop fdist.
+Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist.
 Require Import entropy binary_entropy_function channel hamming channel_code.
 
 (******************************************************************************)