From 76a65408698b3d382062cc5cff768f32632b68ce Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 30 May 2024 07:27:24 +0200 Subject: [PATCH] minor modifications - aligning code to the paper - upd code wrt last mathcomp-analysis - CI (add interval, etc.) --- .github/workflows/docker-action.yml | 1 - README.md | 5 +++- changelog.txt | 2 ++ coq-infotheo.opam | 6 ++-- information_theory/entropy.v | 9 ++---- information_theory/entropy_convex.v | 4 +-- information_theory/error_exponent.v | 6 ++-- information_theory/jtypes.v | 6 +--- information_theory/pproba.v | 27 ++++------------- information_theory/string_entropy.v | 2 +- information_theory/typ_seq.v | 3 +- lib/Reals_ext.v | 18 ++++++------ lib/logb.v | 5 +--- lib/ssrR.v | 15 +--------- meta.yml | 17 +++++++---- probability/convex.v | 10 +++---- probability/convex_stone.v | 12 ++++---- robust/weightedmean.v | 45 +++++++++++++++-------------- 18 files changed, 82 insertions(+), 111 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 0e80a934..edc24fd9 100644 --- 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 index 96e45c48..a97dc1cf 100644 --- 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 index d8816fb1..af074db5 100644 --- 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 index 1013b748..97f0969e 100644 --- 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 index 063186d9..6f4a9aba 100644 --- 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 index d4957147..b9df3c49 100644 --- 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 index 0bbf8dcb..71011ce7 100644 --- 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 index 41887e9d..1ed16f3d 100644 --- 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 index e01f2352..927744f1 100644 --- 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 index ec5c4877..b73daa92 100644 --- 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 index ba16be68..384cf5e5 100644 --- 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 index ec0fbb00..f6ad77d1 100644 --- 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 index d629e7fd..c04cd978 100644 --- 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 index 7304d8a7..394bd6c7 100644 --- 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 index 7d2ea5e7..9eb8a2dc 100644 --- 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 @@ -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 index 1e602740..4b826f92 100644 --- 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. diff --git a/probability/convex_stone.v b/probability/convex_stone.v index e4c28d35..e7711cfc 100644 --- a/probability/convex_stone.v +++ b/probability/convex_stone.v @@ -421,7 +421,7 @@ congr (_ <| _ |> _). (* TODO: lemma? *) apply val_inj => /=. rewrite /s /onem /= !(p_of_rsE,q_of_rsE) /= !(p_of_rsE,q_of_rsE) /= /onem. - rewrite -!RminusE -R1E -!RmultE -!RinvE'. + rewrite -!RminusE -R1E -!RmultE -!RinvE. field. rewrite subR_eq0 mulRC; apply/nesym/eqP. by rewrite RmultE -p_of_rsE. @@ -429,7 +429,7 @@ congr (_ <| _ |> _). apply val_inj => /=. rewrite -[in RHS](onemK (Prob.p p)); congr onem. rewrite q_of_rsE {1}p_of_rsE /= q_of_rsE p_of_rsE /= /onem. -rewrite -!RminusE -!R1E -!RmultE -!RinvE'. +rewrite -!RminusE -!R1E -!RmultE -!RinvE. field. split. rewrite subR_eq0; apply/nesym/eqP; by rewrite RmultE -p_of_rsE. @@ -706,7 +706,7 @@ congr (_ <| _ |> _). rewrite fdistI_permE permE /= p_of_rsE /= r_of_pqE /=. rewrite s_of_pqE /= /onem. rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. - rewrite -R1E -!RminusE -!RdivE'// -!RmultE. + rewrite -R1E -!RminusE -!RdivE// -!RmultE. set tmp1 := d _. set tmp2 := d _. field. @@ -719,8 +719,8 @@ congr (_ <| _ |> _). rewrite q_of_rsE /= !fdistI_permE p_of_rsE /= r_of_pqE /= s_of_pqE. rewrite /= /onem !permE /=. rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. - rewrite -[RHS]RdivE'. - rewrite -R1E -!RminusE -!RdivE' // -!RmultE. + rewrite -[RHS]RdivE. + rewrite -R1E -!RminusE -!RdivE // -!RmultE. set tmp1 := d _. set tmp2 := d _. field. @@ -834,7 +834,7 @@ apply val_inj => /=. rewrite !fdistI_permE !permE /= q_of_rsE /= p_of_rsE /=. rewrite (_ : Ordinal _ = ord_max); last exact/val_inj. rewrite onemK. -rewrite -!RdivE' //. +rewrite -!RdivE //. rewrite -!RminusE. rewrite {1 2}/Rdiv. rewrite -2!mulRA. diff --git a/robust/weightedmean.v b/robust/weightedmean.v index 4ae9e104..5631f330 100644 --- a/robust/weightedmean.v +++ b/robust/weightedmean.v @@ -803,7 +803,8 @@ apply (@le_trans _ _ ((1 - eps) * `V (WP.-RV X) * rewrite mulrC !mulrA (_ : 4 * 4 = 16); last lra. by rewrite -[leLHS]mulrA -[leRHS]mulrA ler_pM // mulr_ge0. by rewrite -sqrtrV // -sqrtrM // sqr_sqrtr. -by rewrite /bound_intermediate [leRHS]mulrC (mulrC (1-eps)) !coqRE (_ : 2%coqR = 2)// !mulrA. +rewrite /bound_intermediate [leRHS]mulrC (mulrC (1 - eps)). +by rewrite ?coqRE !mulrA. Qed. Lemma bound_evar_ineq_S : @@ -839,7 +840,7 @@ apply (@le_trans _ _ ((1 - eps) * - apply: ler_pM=> //. apply: addr_ge0; first lra. rewrite mulr_ge0//. exact: sqr_ge0. - apply: lerD => //. apply: ler_pM=> //; first exact: sqr_ge0. - by move: low_eps; rewrite !coqRE (_ : 2%coqR = 2)//; lra. + by move: low_eps; rewrite 2?coqRE 2?(_ : 2%coqR = 2)//; lra. rewrite lerXn2r // ?nnegrE ?addr_ge0 //?invr_ge0 ?mulr_ge0 // ?sqrtr_ge0 //. rewrite lerD ?lerXn2r // ?nnegrE ?addr_ge0 //?invr_ge0 ?mulr_ge0 // ?sqrtr_ge0 //. rewrite ?lef_pV2 ?posrE ?mulr_gt0 // ?sqrtr_gt0 //; last by move: eps_max01; lra. @@ -1051,14 +1052,14 @@ Variables (U : finType) (P : {fdist U}) (X : {RV P -> R}). Local Obligation Tactic := idtac. -Lemma filter1D_arg_decreasing (C : nneg_finfun U) (var : R) : - 0 <= var -> is01 C -> +Lemma filter1D_arg_decreasing (C : nneg_finfun U) (v : R) : + 0 <= v -> is01 C -> forall PC0 : Weighted.total P C != 0, let WP := wgt PC0 in - forall K : Rleb (`V (WP.-RV X)) (16 * var) <> true, + forall K : Rleb (`V (WP.-RV X)) (16 * v) <> true, (#|0.-support (update X PC0)| < #|0.-support C|)%coq_nat. Proof. -rewrite/Weighted.total=> var_ge0 C01 PCneq0 /negP/RlebP/RleP. +rewrite/Weighted.total=> v_ge0 C01 PCneq0 /negP/RlebP/RleP. rewrite -ltNge !coqRE=> evar16. apply/ssrnat.ltP/proper_card/properP; split. apply/subsetP => u; rewrite !supportE /update_ffun ffunE. @@ -1082,24 +1083,24 @@ rewrite /update_ffun supportE ffunE negbK ifF. by rewrite (negbTE sq_dev_max_neq0)/=; exact/negbTE. Qed. -Function filter1D_rec var (var_ge0 : 0 <= var) +Function filter1D_rec v (v_ge0 : 0 <= v) (C : nneg_finfun U) (C01 : is01 C) (PC0 : Weighted.total P C != 0) {measure (fun C => #| 0.-support C |) C} := let WP := wgt PC0 in - if `V (WP.-RV X) <=? 16 * var is left _ then + if `V (WP.-RV X) <=? 16 * v is left _ then Some (`E (WP.-RV X)) else let C' := update X PC0 in if Weighted.total P C' !=? 0 is left PC0' then - filter1D_rec var_ge0 (is01_update X PC0 C01) PC0' + filter1D_rec v_ge0 (is01_update X PC0 C01) PC0' else None. Proof. -rewrite/Weighted.total=> var var_ge0 C C01 PC0 evar16 h2 h3 _. -exact: (filter1D_arg_decreasing var_ge0). +rewrite/Weighted.total=> v v_ge0 C C01 PC0 evar16 h2 h3 _. +exact: (filter1D_arg_decreasing v_ge0). Qed. -Definition filter1D var (var_ge0 : 0 <= var) := filter1D_rec var_ge0 (@C1_is01 U) (PC1_neq0 P). +Definition filter1D v (v_ge0 : 0 <= v) := filter1D_rec v_ge0 (@C1_is01 U) (PC1_neq0 P). End filter1D. @@ -1111,18 +1112,19 @@ Local Open Scope ring_scope. Variables (U : finType) (P : {fdist U}) (X : {RV P -> R}) (S : {set U}). Local Notation cplt_S := (~: S). Local Notation eps := (Pr P cplt_S). -Hypotheses (low_eps : eps <= eps_max). +Hypothesis low_eps : eps <= eps_max. (* Let mu := `E_[X | S]. *) -(* Let var := `V_[X | S]. *) -Let var_ge0 := cvariance_ge0' X S. +(* Let v := `V_[X | S]. *) +Let v_ge0 := cvariance_ge0' X S. Let eps0 : 0 <= eps. Proof. exact/RleP/Pr_ge0. Qed. Functional Scheme filter1D_rec_ind := Induction for filter1D_rec Sort Prop. Lemma filter1D_correct : - if filter1D X var_ge0 is Some mu_hat - then `| `E_[X | S] - mu_hat | <= Num.sqrt (`V_[X | S] * (2 * eps) / (2 - eps)) + - Num.sqrt (16 * `V_[X | S] * (2 * eps) / (1 - eps)) + let v := `V_[X | S] in + if @filter1D U P X v v_ge0 is Some mu_hat + then `| `E_[X | S] - mu_hat | <= Num.sqrt (v * (2 * eps) / (2 - eps)) + + Num.sqrt (16 * v * (2 * eps) / (1 - eps)) else false. Proof. have sixteenE: 16%coqR = 16 by rewrite /16%coqR -INR_IPR /= coqRE. @@ -1151,13 +1153,12 @@ apply filter1D_rec_ind => //=. rewrite /invariant. under eq_bigr do rewrite mulrDl mulNr PC0' subr0 mul1r. under [in leRHS]eq_bigr do rewrite mulrDl mulNr PC0' subr0 mul1r. - rewrite -/eps -/(Pr P S) pr_S. - have->: false <-> False :> Prop by []. + rewrite -/eps -/(Pr P S) pr_S boolp.falseE. apply/negP; rewrite -ltNge. by rewrite -mulrA gtr_pMr; move: low_eps; lra. Qed. -Corollary filter1D_converges : filter1D X var_ge0 != None. -Proof. by move: filter1D_correct; case: (filter1D X var_ge0). Qed. +Corollary filter1D_converges : @filter1D U P X `V_[X | S] v_ge0 != None. +Proof. by move: filter1D_correct => /=; case: (filter1D X v_ge0). Qed. End filter1D_correct.