minor modifications

- aligning code to the paper - upd code wrt last mathcomp-analysis - CI (add interval, etc.)
affeldt-aist · Jun 14, 2024 · e9d5413 · e9d5413
1 parent c222fb8
commit e9d5413
Show file tree

Hide file tree

Showing 18 changed files with 82 additions and 111 deletions.
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/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
@@ -312,8 +312,8 @@ Definition divRnnm n m := n%:R / (n + m)%:R.
 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.
@@ -336,8 +336,8 @@ Canonical probinvn (n : nat) :=
 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.
@@ -459,7 +459,7 @@ rewrite r_of_pqE; apply/andP; split.
   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.
@@ -556,15 +556,15 @@ Canonical divRposxxy (x y : Rpos) :=
 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.
 
@@ -626,7 +626,7 @@ Lemma r_of_Rpos_probA (p q r : Rpos) :
   (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/logb.v b/lib/logb.v
@@ -170,10 +170,7 @@ Proof.
 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
@@ -638,26 +638,13 @@ Proof. by move=> xo y0; apply/Rinv_lt_contravar/mulR_gt0. Qed.
 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.

diff --git a/meta.yml b/meta.yml
@@ -28,6 +28,8 @@ authors:
   initial: false
 - name: Naruomi Obata, Titech (M2)
   initial: false
+- name: Alessandro Bruni, IT-University of Copenhagen
+  initial: false
 
 opam-file-maintainer: Reynald Affeldt <reynald.affeldt@aist.go.jp>
 
@@ -41,12 +43,10 @@ license:
 nix: true
 
 supported_coq_versions:
-  text: Coq 8.17--8.19
-  opam: '{ (>= "8.17" & < "8.20~") | (= "dev") }'
+  text: Coq 8.18--8.19
+  opam: '{ (>= "8.18" & < "8.20~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'
@@ -80,7 +80,7 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.0.0") }'
+    version: '{ (>= "1.2.0") }'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:
@@ -93,6 +93,11 @@ dependencies:
     version: '{ >= "1.2.0" }'
   description: |-
     MathComp algebra tactics
+- opam:
+    name: coq-interval
+    version: '{ >= "4.10.0"}'
+  description:
+    A Coq tactic for proving bounds
 
 namespace: infotheo
 
@@ -104,7 +109,7 @@ keywords:
 
 publications:
 - pub_url: https://dl.acm.org/doi/abs/10.1145/3479394.3479412
-  pub_title: Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation
+  pub_title: "Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation"
   pub_doi: 10.1145/3479394.3479412
 - pub_url: https://arxiv.org/abs/2004.12713
   pub_title: Formal Adventures in Convex and Conical Spaces

diff --git a/probability/convex.v b/probability/convex.v
@@ -521,7 +521,7 @@ Let addptC' : commutative addpt.
 Proof.
 move=> [r x|] [q y|] //=; congr (_ *: _); first by apply: val_inj; rewrite /= addRC.
 rewrite convC; congr (_ <| _ |> _); apply/val_inj => /=.
-by rewrite RdivE' RplusE onem_divRxxy.
+by rewrite RdivE RplusE onem_divRxxy.
 Qed.
 
 Let addptA' : associative addpt.
@@ -1724,8 +1724,8 @@ Proof. by move=> x /=; rewrite scale1r. Qed.
 Lemma scaler_addpt : {morph scaler : x y / addpt x y >-> x + y}.
 Proof.
 move=> [p x|] [q y|] /=; rewrite ?(add0r,addr0) //.
-rewrite avgrE /divRposxxy /= RdivE' onem_div; last exact: Rpos_neq0.
-rewrite -!RmultE -!RinvE' -!(mulRC (/ _)%coqR) scalerDr !scalerA !mulrA.
+rewrite avgrE /divRposxxy /= RdivE onem_div; last exact: Rpos_neq0.
+rewrite -!RmultE -!RinvE -!(mulRC (/ _)%coqR) scalerDr !scalerA !mulrA.
 have ->: (p + q)%coqR * (/ (p + q))%coqR = 1 by apply mulRV; last by apply Rpos_neq0.
 by rewrite !mul1r (addRC p) addrK.
 Qed.
@@ -1995,8 +1995,8 @@ Proof. by move=> x /=; rewrite mul1R. Qed.
 Lemma scaleR_addpt : {morph scaleR : x y / addpt x y >-> (x + y)%coqR}.
 Proof.
 move=> [p x|] [q y|] /=; rewrite ?(add0R,addR0) //.
-rewrite avgRE /avg /divRposxxy /= RdivE' onem_div /Rdiv; last exact: Rpos_neq0.
-rewrite -!RmultE -!RinvE' -!(mulRC (/ _)%coqR) mulRDr !mulRA mulRV; last exact: Rpos_neq0.
+rewrite avgRE /avg /divRposxxy /= RdivE onem_div /Rdiv; last exact: Rpos_neq0.
+rewrite -!RmultE -!RinvE -!(mulRC (/ _)%coqR) mulRDr !mulRA mulRV; last exact: Rpos_neq0.
 by rewrite !mul1R (addRC p) addrK.
 Qed.