affeldt-aist · affeldt-aist · Jun 14, 2024 · May 30, 2024 · May 30, 2024 · May 30, 2024
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,7 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
           - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
       fail-fast: false

diff --git a/README.md b/README.md
@@ -30,8 +30,9 @@ information theory, and linear error-correcting codes.
   - Taku Asai, Nagoya U. (M2)
   - Takafumi Saikawa, Nagoya U.
   - Naruomi Obata, Titech (M2)
+  - Alessandro Bruni, IT-University of Copenhagen
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.17--8.19
+- Compatible Coq versions: Coq 8.18--8.19
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
@@ -41,8 +42,10 @@ information theory, and linear error-correcting codes.
   - [MathComp analysis](https://github.com/math-comp/analysis)
   - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder)
   - MathComp algebra tactics
+  - A Coq tactic for proving bounds
 - Coq namespace: `infotheo`
 - Related publication(s):
+  - [Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation](https://dl.acm.org/doi/abs/10.1145/3479394.3479412) doi:[10.1145/3479394.3479412](https://doi.org/10.1145/3479394.3479412)
   - [Formal Adventures in Convex and Conical Spaces](https://arxiv.org/abs/2004.12713) doi:[10.1007/978-3-030-53518-6_2](https://doi.org/10.1007/978-3-030-53518-6_2)
   - [A Library for Formalization of Linear Error-Correcting Codes](https://link.springer.com/article/10.1007/s10817-019-09538-8) doi:[10.1007/s10817-019-09538-8](https://doi.org/10.1007/s10817-019-09538-8)
   - [Reasoning with Conditional Probabilities and Joint Distributions in Coq](https://www.jstage.jst.go.jp/article/jssst/37/3/37_3_79/_article/-char/en) doi:[10.11309/jssst.37.3_79](https://doi.org/10.11309/jssst.37.3_79)

diff --git a/_CoqProject b/_CoqProject
@@ -89,6 +89,8 @@ ecc_modern/ldpc_erasure.v
 ecc_modern/max_subset.v
 ecc_modern/stopping_set.v
 ecc_modern/degree_profile.v
+robust/robustmean.v
+robust/weightedmean.v
 toy_examples/expected_value_variance.v
 toy_examples/expected_value_variance_ordn.v
 toy_examples/expected_value_variance_tuple.v

diff --git a/changelog.txt b/changelog.txt
@@ -1,3 +1,5 @@
+removed RinvE' and RdivE' (replaced by RinvE and RdivE in mathcomp)
+
 -------------------
 from 0.7.0 to 0.7.1
 -------------------

diff --git a/coq-infotheo.opam b/coq-infotheo.opam
@@ -21,15 +21,16 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.17" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-field" { (>= "2.2.0") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "1.0.0") }
+  "coq-mathcomp-analysis" { (>= "1.2.0") }
   "coq-hierarchy-builder" { >= "1.5.0" }
   "coq-mathcomp-algebra-tactics" { >= "1.2.0" }
+  "coq-interval" { >= "4.10.0"}
 ]
 
 tags: [
@@ -48,4 +49,5 @@ authors: [
   "Taku Asai, Nagoya U. (M2)"
   "Takafumi Saikawa, Nagoya U."
   "Naruomi Obata, Titech (M2)"
+  "Alessandro Bruni, IT-University of Copenhagen"
 ]
diff --git a/information_theory/entropy.v b/information_theory/entropy.v
@@ -107,8 +107,7 @@ Lemma entropy_uniform n (An1 : #|A| = n.+1) :
 Proof.
 rewrite /entropy.
 under eq_bigr do rewrite fdist_uniformE.
-rewrite big_const iter_addR mulRA RmultE -RinvE; last first.
-  by rewrite An1 -INRE INR_eq0'.
+rewrite big_const iter_addR mulRA RmultE -RinvE.
 rewrite INRE mulRV; last by rewrite An1 -INRE INR_eq0'.
 rewrite -RmultE mul1R logV ?oppRK//; rewrite An1.
 by rewrite -INRE; apply/ltR0n.
@@ -133,14 +132,12 @@ transitivity (\sum_(a|a \in A) P a * log (P a) +
   case/boolP : (P a == 0) => [/eqP ->|H0]; first by rewrite !mul0R.
   congr (_ * _); rewrite logDiv ?addR_opp //.
     by apply/RltP; rewrite -fdist_gt0.
-  rewrite fdist_uniformE.
-  rewrite -RinvE; last by rewrite An1 -INRE INR_eq0'.
+  rewrite fdist_uniformE -RinvE.
   apply/invR_gt0; rewrite An1 -INRE.
   exact/ltR0n.
 under [in X in _ + X]eq_bigr do rewrite fdist_uniformE.
 rewrite -[in X in _ + X = _]big_distrl /= FDist.f1 mul1R.
-rewrite addRC /entropy /log.
-  rewrite -RinvE; last by rewrite An1 -INRE INR_eq0'.
+rewrite addRC /entropy /log -RinvE.
 by rewrite LogV ?oppRK ?subR_opp // An1 ?INRE// -INRE; exact/ltR0n.
 Qed.
 

diff --git a/information_theory/entropy_convex.v b/information_theory/entropy_convex.v
@@ -64,9 +64,7 @@ have H a : p a * log (p a / u a) = RHS a.
     change (p a * log (p a / / #|A|%:R)) with (p a * log (p a * / / #|A|%:R)).
     have H0 : 0 < #|A|%:R by rewrite An1 ltR0n.
     have /eqP H1 : #|A|%:R <> 0 by apply/eqP/gtR_eqF.
-    rewrite -RinvE ?An1; last first.
-      by rewrite -INRE// INR_eq0'.
-    rewrite /Rdiv invRK// logM //; last first.
+    rewrite -RinvE An1 /Rdiv invRK// logM //; last first.
       by rewrite -INRE ltR0n.
     rewrite mulRDr -INRE.
     rewrite -An1.

diff --git a/information_theory/error_exponent.v b/information_theory/error_exponent.v
@@ -51,10 +51,10 @@ apply pow2_Rle_inv; [ exact: sqrt_pos | exact/ltRW/exp_pos | ].
 rewrite [in X in X <= _]/= mulR1 sqrt_sqrt; last first.
   apply mulR_ge0; [lra | exact: cdiv_ge0].
 apply/RleP; rewrite -(@ler_pM2r _ (/ 2)); last first.
-  by rewrite RinvE' invr_gt0// (_ : 2%coqR = 2%:R)// INRE ltr0n.
-rewrite RmultE -mulrA mulrCA RinvE' (_ : 2%coqR = 2%:R)// INRE.
+  by rewrite RinvE invr_gt0// (_ : 2%coqR = 2%:R)// INRE ltr0n.
+rewrite RmultE -mulrA mulrCA RinvE (_ : 2%coqR = 2%:R)// INRE.
 rewrite mulfV ?mulr1 ?gt_eqF//.
-by apply/RleP; rewrite -RdivE'.
+by apply/RleP; rewrite -RdivE.
 Qed.
 
 Local Open Scope variation_distance_scope.

diff --git a/information_theory/jtypes.v b/information_theory/jtypes.v
@@ -134,11 +134,7 @@ rewrite /=.
 under eq_bigr do rewrite ffunE.
 case/boolP : (\sum_(b1 in B) (f a b1) == O)%nat => Hcase.
 - by rewrite /Rle big_const iter_addR mulRV // INR_eq0' -lt0n.
-- under eq_bigr.
-    move=> b bB.
-    rewrite RdivE//; last first.
-      by rewrite INR_eq0'.
-    over.
+- under eq_bigr=> b bB do rewrite RdivE.
   rewrite big_morph_natRD /Rdiv.
   rewrite -big_distrl /=.
   rewrite GRing.mulfV//.

diff --git a/information_theory/pproba.v b/information_theory/pproba.v
@@ -111,8 +111,7 @@ Proof. by apply/sumr_ge0 => x _; exact: mulr_ge0. Qed.
 
 Let f0 x : 0 <= f x.
 Proof.
-rewrite ffunE; apply/RleP; rewrite -RdivE//; last first.
-  by rewrite /den -receivable_propE receivableP.
+rewrite ffunE; apply/RleP; rewrite -RdivE.
 apply: divR_ge0; first exact: mulR_ge0.
 apply/RltP; rewrite lt0r {1}/den -receivable_propE receivableP.
 exact/fdist_post_prob_den_ge0.
@@ -121,9 +120,7 @@ Qed.
 Let f1 : \sum_(x in 'rV_n) f x = 1.
 Proof.
 under eq_bigr do rewrite ffunE /=.
-rewrite -big_distrl /= -RmultE mulRC.
-rewrite -RinvE; last first.
-  by rewrite -receivable_propE receivableP.
+rewrite -big_distrl /= -RmultE mulRC -RinvE.
 by rewrite mulVR // -receivable_propE receivableP.
 Qed.
 
@@ -142,10 +139,7 @@ Variables (A B : finType) (W : `Ch(A, B)) (n : nat) (P : {fdist 'rV[A]_n}).
 Lemma post_probE (x : 'rV[A]_n) (y : P.-receivable W) :
   P `^^ W (x | y) = \Pr_(P `X (W ``^ n))[ [set x] | [set receivable_rV y]].
 Proof.
-rewrite fdist_post_probE /jcPr setX1 2!Pr_set1 fdist_prodE /=.
-rewrite -RdivE; last first.
-  rewrite -receivable_propE.
-  by case: y.
+rewrite fdist_post_probE /jcPr setX1 2!Pr_set1 fdist_prodE /= -RdivE.
 congr (_ / _).
 by rewrite fdist_sndE /=; apply eq_bigr => x' _; rewrite fdist_prodE /= -RmultE mulRC.
 Qed.
@@ -174,14 +168,8 @@ Lemma post_prob_uniformT (x : 'rV[A]_n) : x \in C -> (`U HC) `^^ W (x | y) = K *
 Proof.
 move=> Ht.
 have C0 : INR #|C| != 0 by rewrite INR_eq0' -lt0n.
-rewrite fdist_post_probE fdist_uniform_supp_in //.
-rewrite -RinvE; last first.
-  by rewrite -INRE.
-rewrite -!RmultE mulRC.
-rewrite -RinvE; last first.
-  rewrite -receivable_propE.
-  by case: y.
-rewrite mulRA.
+rewrite fdist_post_probE fdist_uniform_supp_in // -RinvE.
+rewrite -!RmultE mulRC -RinvE mulRA.
 congr (_ * _).
 rewrite /den fdist_uniform_supp_restrict.
 rewrite -invRM//.
@@ -228,10 +216,7 @@ Proof.
 under eq_bigr do rewrite /f' fdist_post_probE /Rdiv.
 rewrite -big_distrl /= mulR_eq0 => -[/eqP|].
 - by apply/negP; rewrite -receivable_propE receivableP.
-- rewrite -RinvE//; last first.
-    rewrite -receivable_propE.
-    by case: y.
-- by apply/invR_neq0/eqP; rewrite -receivable_propE receivableP.
+- by rewrite -RinvE; apply/invR_neq0/eqP; rewrite -receivable_propE receivableP.
 Qed.
 
 Let f (i : 'I_n) := [ffun a =>  marginal_post_prob_den * \sum_(t in 'rV_n | t ``_ i == a) f' t].

diff --git a/information_theory/string_entropy.v b/information_theory/string_entropy.v
@@ -266,7 +266,7 @@ Definition hoH (k : nat) := / n%:R *
 Lemma hoH_decr (k : nat) : hoH k.+1 <= hoH k.
 Proof.
 rewrite /hoH; apply/RleP; rewrite ler_pM2l//; last first.
-  by rewrite INRE RinvE' invr_gt0// ltr0n lt0n.
+  by rewrite INRE RinvE invr_gt0// ltr0n lt0n.
 (* TODO *)
 Abort.
 

diff --git a/information_theory/typ_seq.v b/information_theory/typ_seq.v
@@ -159,8 +159,7 @@ have -> : Pr P `^ n.+1 (~: p) =
         move/RleP: LHS => /ltRNge/(@Log_increasing 2 _ _ Rlt_1_2 H1).
         rewrite /exp2 ExpK // mulRC mulRN -mulNR -ltR_pdivr_mulr; last exact/ltR0n.
         rewrite /Rdiv mulRC ltR_oppr => /RltP; rewrite -ltrBrDl => LHS.
-        rewrite div1r// mulNr -RinvE//; last by rewrite gt_eqF// ltr0n.
-        rewrite ger0_norm// -INRE//.
+        rewrite div1r// mulNr -RinvE ger0_norm// -INRE//.
         by move/RltP : LHS; move/(ltR_trans He)/ltRW/RleP.
       + move: LHS; rewrite leNgt negbK => LHS.
         apply/orP; right; apply/andP; split.

diff --git a/lib/Reals_ext.v b/lib/Reals_ext.v
@@ -246,6 +246,46 @@
 HB.instance Definition _ := [Equality of nneg_finfun by <:].
 End nneg_finfun.
 
+
+Section nneg_finfun. (* Reals_ext.v *)
+Local Open Scope R_scope.
+
+Lemma nneg_finfun_ge0 (I : finType) (f : nneg_finfun I) i : (0 <= f i)%mcR.
+Proof. by case: f => /= f /forallP /(_ i). Qed.
+
+Lemma nneg_finfun_le0 (I : finType) (F : nneg_finfun I) i :
+  (F i == 0) = (F i <= 0)%mcR.
+Proof.
+apply/idP/idP => [/eqP -> //|].
+case: F => F /= /forallP /(_ i).
+by rewrite eq_le coqRE => -> ->.
+Qed.
+
+Fail Check F : pos_fun _. (* Why no coercion pos_ffun >-> pos_fun? *)
+
+Lemma pos_ffun_bigmaxR0P (I : finType) (r : seq I) (P : pred I) (F : nneg_finfun I) :
+  reflect (forall i : I, i \in r -> P i -> F i = 0)
+          (\rmax_(i <- r | P i) F i == 0).
+Proof.
+apply: (iffP idP) => [/eqP H i ir Pi|H].
+- apply/eqP; rewrite nneg_finfun_le0 -coqRE -H.
+  rewrite -big_filter; apply/RleP; apply: leR_bigmaxR.
+  by rewrite mem_filter ir Pi.
+- rewrite -big_filter big_seq.
+  under eq_bigr=> i do rewrite mem_filter=> /andP [] /[swap] /(H i) /[apply] ->.
+  by rewrite -big_seq big_const_seq iter_fix // maxRR.
+Qed.
+
+Lemma nnegP (U : finType) (C : {ffun U -> R}) :
+  (forall u : U, 0 <= C u) -> [forall a, (0 <= C a)%mcR].
+Proof. by move=> h; apply/forallP => u; apply/RleP. Qed.
+
+Definition Cpos_fun (U : finType) (C : nneg_finfun U)
+    (h : forall u : U, 0 <= C u) : nneg_finfun U :=
+  mkNNFinfun (nnegP h).
+
+End nneg_finfun.
+
 Record nneg_fun (T : Type) := mkNNFun {
   nneg_f :> T -> R ;
   nneg_f_ge0 : forall a, 0 <= nneg_f a }.
@@ -259,7 +299,7 @@
 Proof.
 have [/RleP ? /RleP ?] : (0 <= / IZR (Zpos p) <= 1)%coqR.
  split; first exact/Rlt_le/Rinv_0_lt_compat/IZR_lt/Pos2Z.is_pos.
  rewrite -[X in (_ <= X)%coqR]Rinv_1; apply Rle_Rinv => //.
  - exact/IZR_lt/Pos2Z.is_pos.
  - exact/IZR_le/Pos2Z.pos_le_pos/Pos.le_1_l.
 exact/andP.
@@ -272,8 +312,8 @@
 Lemma prob_divRnnm_subproof n m : (R0 <= divRnnm n m <= R1)%O.
 Proof.
 apply/andP; split.
-  by rewrite /divRnnm RdivE' divr_ge0// INRE ler0n.
-rewrite /divRnnm RdivE' !INRE.
+  by rewrite /divRnnm RdivE divr_ge0// INRE ler0n.
+rewrite /divRnnm RdivE !INRE.
 have [/eqP ->|n0] := boolP (n == O).
   by rewrite mul0r ler01.
 rewrite ler_pdivrMr// ?ltr0n ?addn_gt0; last first.
@@ -296,8 +336,8 @@
 Lemma prob_invp_subproof (p : {prob R}) : (0 <= 1 / (1 + Prob.p p) <= 1)%O.
 Proof.
 apply/andP; split.
-  by rewrite RdivE' mul1r invr_ge0 ?addr_ge0.
-rewrite RdivE' mul1r invf_le1//.
+  by rewrite RdivE mul1r invr_ge0 ?addr_ge0.
+rewrite RdivE mul1r invf_le1//.
   by rewrite lerDl.
 rewrite (@lt_le_trans _ _ 1)//.
 by rewrite lerDl.
@@ -419,7 +459,7 @@
   have := OProb.O1 (oprobcplt (oprobmulR (oprobcplt p) (oprobcplt q))).
   by move/andP=> [] /=.
 apply/RltP.
-rewrite -RdivE'.
+rewrite -RdivE.
 rewrite ltR_pdivr_mulr ?mul1R; last by apply/(oprob_gt0).
 rewrite ltR_neqAle; split; last exact/RleP/ge_s_of.
 rewrite s_of_pqE; apply/eqP/ltR_eqF.
@@ -516,15 +556,15 @@
 Lemma divRposxxyC r q : divRposxxy q r = (Prob.p (divRposxxy r q)).~%:pr.
 Proof.
 apply val_inj => /=; rewrite [in RHS]addRC.
-rewrite [in RHS]RdivE' onem_div// ?addrK//.
-  by rewrite RplusE RdivE'.
+rewrite [in RHS]RdivE onem_div// ?addrK//.
+  by rewrite RplusE RdivE.
 exact: Rpos_neq0.
 Qed.
 
 Lemma onem_divRxxy (r q : Rpos) : (rpos_coercion r / (rpos_coercion r + q)).~ = q / (q + r).
 Proof.
 rewrite /onem; apply/eqP; rewrite subr_eq.
-rewrite !RplusE (addrC (r : R)) RdivE' -mulrDl divff//.
+rewrite !RplusE (addrC (r : R)) RdivE -mulrDl divff//.
 by rewrite gtR_eqF//; apply: addR_gt0.
 Qed.
 
@@ -586,7 +626,7 @@
   (p / (p + q))%:pos%:pr.
 Proof.
 apply/val_inj; rewrite /= r_of_pqE s_of_pqE /onem /=.
-rewrite -!RminusE -R1E -!RmultE -!RinvE'.
+rewrite -!RminusE -R1E -!RmultE -!RinvE.
 field.
 do 3 (split; first exact/eqP/Rpos_neq0).
 rewrite (addRC p (q + r)) addRK {4}[in q + r]addRC addRK.

diff --git a/lib/bigop_ext.v b/lib/bigop_ext.v
@@ -1,6 +1,6 @@
 (* 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 Import all_ssreflect ssralg ssrnum matrix lra.
 Require Import (*ssrR Reals_ext*) logb ssr_ext ssralg_ext.
 
 (******************************************************************************)
@@ -605,3 +605,19 @@ apply: ler_suml=> // i; rewrite andb_orl andbN orbF; last by case/andP.
 by move=> /[dup] /F0 /[swap] -> /[!andTb] /[!negbK].
 Qed.
 End num.
+
+Section real.
+Local Open Scope ring_scope.
+Variables (R : realDomainType) (I : Type) (r : seq I).
+
+Lemma fsumr_gt0 (U : eqType) (F : U -> R) (s : seq U) :
+  0 < \sum_(i <- s) F i -> exists2 i, i \in s & 0 < F i.
+Proof.
+elim: s => [|h t ih]; first by rewrite big_nil ltxx.
+rewrite big_cons.
+have H : forall x y : R, 0 < x + y -> 0 < x \/ 0 < y by move=> x y; lra.
+move/H => [Fh0|]; first by exists h => //; rewrite mem_head.
+by move/ih => [u ut Fu0]; exists u => //; rewrite inE ut orbT.
+Qed.
+
+End real.
diff --git a/lib/logb.v b/lib/logb.v
@@ -92,7 +92,7 @@
 rewrite mulRC mulRA mulRC; congr (_ * _).
 rewrite factS natRM invRM ?INR_eq0' //; last by rewrite -lt0n fact_gt0.
 by rewrite mulRC mulRA mulRV ?mul1R // INR_eq0'.
 Qed.

 Let exp_dev_gt0 : forall n r, 0 < r -> 0 < exp_dev n r.
 Proof.
@@ -170,10 +170,7 @@
 move=> n1 x0 xy.
 apply leR_wpmul2r.
   apply/RleP.
-  rewrite RinvE//; last first.
-    rewrite gtR_eqF//.
-    exact/ln_pos.
-  by rewrite invr_ge0; exact/ltW/RltP/ln_pos.
+  by rewrite RinvE invr_ge0; exact/ltW/RltP/ln_pos.
 exact: ln_increasing_le.
 Qed.
 

diff --git a/lib/ssrR.v b/lib/ssrR.v
@@ -489,7 +489,7 @@
 Proof. by rewrite -{1}(addR0 x) ltR_add2l. Qed.

 Lemma subR_gt0 x y : (0 < y - x) <-> (x < y).
 Proof. by split; [exact: Rminus_gt_0_lt | exact: Rlt_Rminus]. Qed.
 Lemma subR_lt0 x y : (y - x < 0) <-> (y < x).
 Proof. by split; [exact: Rminus_lt | exact: Rlt_minus]. Qed.
 Lemma subR_ge0 x y : (0 <= y - x) <-> (x <= y).
@@ -638,26 +638,13 @@
 Lemma divRE x y : x / y = x * / y. Proof. by []. Qed.
 
 Delimit Scope R_scope with coqR.
-(* NB: this lemma depends on the internals of Rinv and Rinvx *)
-(* TODO: this really needs to be pushed to MathComp-Analysis *)
-Lemma RinvE' (x : R) : (/ x)%coqR = (x^-1)%mcR.
-Proof.
-have [-> | ] := eqVneq x 0%coqR; last exact: RinvE.
-rewrite /GRing.inv /GRing.mul /= /Rinvx eqxx /=.
-rewrite RinvImpl.Rinv_def.
-case: (Req_appart_dec 0 R0) => //.
-by move=> /[dup] -[] => /RltP; rewrite Order.POrderTheory.ltxx.
-Qed.
-
-Lemma RdivE' (x y : R) : (x / y)%coqR = (x / y)%mcR.
-Proof. by rewrite divRE RinvE'. Qed.
 
 Lemma R1E : 1%coqR = 1%mcR. Proof. by []. Qed.
 Lemma R0E : 0%coqR = 0%mcR. Proof. by []. Qed.
 
 Definition coqRE :=
   (R0E, R1E, INRE,
-    RinvE', RoppE, RdivE', RminusE, RplusE, RmultE, RpowE).
+    RinvE, RoppE, RdivE, RminusE, RplusE, RmultE, RpowE).
 
 Definition divRR (x : R) : x != 0 -> x / x = 1.
 Proof. by move=> x0; rewrite /Rdiv Rinv_r //; exact/eqP. Qed.