From 96329e987f96f691b33f35025f2e4b5408e956a2 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 12 Oct 2023 16:02:55 +0200 Subject: [PATCH 1/2] Remove 1.17.0 deprecations --- .github/workflows/docker-action.yml | 27 ++--- README.md | 14 +-- coq-mathcomp-apery.opam | 14 +-- meta.yml | 68 ++++--------- theories/a_props.v | 64 ++++++------ theories/bigopz.v | 34 +++---- theories/binomialz.v | 2 +- theories/extra_cauchyreals.v | 24 ++--- theories/extra_mathcomp.v | 26 ++--- theories/floor.v | 18 ++-- theories/hanson.v | 147 ++++++++++++++-------------- theories/hanson_elem_analysis.v | 42 ++++---- theories/hanson_elem_arith.v | 6 +- theories/harmonic_numbers.v | 5 +- theories/multinomial.v | 2 +- theories/ops_for_s.v | 10 +- theories/punk.v | 12 +-- theories/rat_of_Z.v | 2 +- theories/reduce_order.v | 4 +- theories/s_props.v | 14 +-- theories/z3irrational.v | 46 ++++----- theories/z3seq_props.v | 10 +- 22 files changed, 270 insertions(+), 321 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 05a08be..f6fbfde 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,34 +17,19 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.12.0-coq-8.13' - - 'mathcomp/mathcomp:1.12.0-coq-8.14' - - 'mathcomp/mathcomp:1.13.0-coq-8.13' - - 'mathcomp/mathcomp:1.13.0-coq-8.14' - - 'mathcomp/mathcomp:1.13.0-coq-8.15' - - 'mathcomp/mathcomp:1.14.0-coq-8.13' - - 'mathcomp/mathcomp:1.14.0-coq-8.14' - - 'mathcomp/mathcomp:1.14.0-coq-8.15' - - 'mathcomp/mathcomp:1.15.0-coq-8.13' - - 'mathcomp/mathcomp:1.15.0-coq-8.14' - - 'mathcomp/mathcomp:1.15.0-coq-8.15' - - 'mathcomp/mathcomp:1.15.0-coq-8.16' - - 'mathcomp/mathcomp:1.16.0-coq-8.13' - - 'mathcomp/mathcomp:1.16.0-coq-8.14' - - 'mathcomp/mathcomp:1.16.0-coq-8.15' - - 'mathcomp/mathcomp:1.16.0-coq-8.16' - - 'mathcomp/mathcomp:1.16.0-coq-8.17' - - 'mathcomp/mathcomp-dev:coq-8.16' - - 'mathcomp/mathcomp-dev:coq-8.17' - - 'mathcomp/mathcomp-dev:coq-dev' + - 'mathcomp/mathcomp:1.17.0-coq-8.15' + - 'mathcomp/mathcomp:1.17.0-coq-8.16' + - 'mathcomp/mathcomp:1.17.0-coq-8.17' + - 'mathcomp/mathcomp:1.17.0-coq-8.18' fail-fast: false steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - uses: coq-community/docker-coq-action@v1 with: opam_file: 'coq-mathcomp-apery.opam' custom_image: ${{ matrix.image }} + # See also: # https://github.com/coq-community/docker-coq-action#readme # https://github.com/erikmd/docker-coq-github-action-demo diff --git a/README.md b/README.md index 30dcae1..ebd26b2 100644 --- a/README.md +++ b/README.md @@ -41,16 +41,16 @@ remains the sole trusted code base. - Assia Mahboubi ([**@amahboubi**](https://github.com/amahboubi)) - Kazuhiko Sakaguchi ([**@pi8027**](https://github.com/pi8027)) - License: [CeCILL-C](LICENSE) -- Compatible Coq versions: 8.13 or later +- Compatible Coq versions: 8.15 or later - Additional dependencies: - - [MathComp ssreflect 1.12 or later](https://math-comp.github.io) + - [MathComp ssreflect 1.17 or later](https://math-comp.github.io) - [MathComp algebra](https://math-comp.github.io) - [MathComp field](https://math-comp.github.io) - - [CoqEAL 1.0.5 or later](https://github.com/coq-community/coqeal) - - [MathComp real closed fields 1.1.2 or later](https://github.com/math-comp/real-closed) - - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough) - - [Mczify](https://github.com/math-comp/mczify) 1.2.0 or later - - [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 0.2.0 or later + - [CoqEAL 1.1.3 or later](https://github.com/coq-community/coqeal) + - [MathComp real closed fields 1.1.4 or later](https://github.com/math-comp/real-closed) + - [MathComp bigenough 1.0.1 or later](https://github.com/math-comp/bigenough) + - [Mczify](https://github.com/math-comp/mczify) 1.3.0 or later + - [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.0.0 or later - Coq namespace: `mathcomp.apery` - Related publication(s): - [A Formal Proof of the Irrationality of ΞΆ(3)](https://arxiv.org/abs/1912.06611) diff --git a/coq-mathcomp-apery.opam b/coq-mathcomp-apery.opam index 15e9890..242b50f 100644 --- a/coq-mathcomp-apery.opam +++ b/coq-mathcomp-apery.opam @@ -23,15 +23,15 @@ remains the sole trusted code base.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {(>= "8.13" & < "8.18~") | (= "dev")} - "coq-mathcomp-ssreflect" {(>= "1.12" & < "1.17~") | (= "dev")} + "coq" {(>= "8.15" & < "8.19~") | (= "dev")} + "coq-mathcomp-ssreflect" {>= "1.17" & < "1.18~"} "coq-mathcomp-algebra" "coq-mathcomp-field" - "coq-coqeal" {>= "1.0.5"} - "coq-mathcomp-real-closed" {>= "1.1.2"} - "coq-mathcomp-bigenough" {>= "1.0.0"} - "coq-mathcomp-zify" {>= "1.2.0"} - "coq-mathcomp-algebra-tactics" {>= "0.2.0"} + "coq-coqeal" {>= "1.1.3" & < "2~"} + "coq-mathcomp-real-closed" {>= "1.1.4" & < "2~"} + "coq-mathcomp-bigenough" {>= "1.0.1"} + "coq-mathcomp-zify" {>= "1.3.0" & < "1.14~"} + "coq-mathcomp-algebra-tactics" {>= "1.0.0" & < "1.2~"} ] tags: [ diff --git a/meta.yml b/meta.yml index 2edb37f..df43ac6 100644 --- a/meta.yml +++ b/meta.yml @@ -51,57 +51,25 @@ license: identifier: CECILL-C supported_coq_versions: - text: 8.13 or later - opam: '{(>= "8.13" & < "8.18~") | (= "dev")}' + text: 8.15 or later + opam: '{(>= "8.15" & < "8.19~") | (= "dev")}' tested_coq_opam_versions: -- version: '1.12.0-coq-8.13' +- version: '1.17.0-coq-8.15' repo: 'mathcomp/mathcomp' -- version: '1.12.0-coq-8.14' +- version: '1.17.0-coq-8.16' repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.13' +- version: '1.17.0-coq-8.17' repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.14' +- version: '1.17.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.15' - repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.13' - repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.14' - repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.15' - repo: 'mathcomp/mathcomp' -- version: '1.15.0-coq-8.13' - repo: 'mathcomp/mathcomp' -- version: '1.15.0-coq-8.14' - repo: 'mathcomp/mathcomp' -- version: '1.15.0-coq-8.15' - repo: 'mathcomp/mathcomp' -- version: '1.15.0-coq-8.16' - repo: 'mathcomp/mathcomp' -- version: '1.16.0-coq-8.13' - repo: 'mathcomp/mathcomp' -- version: '1.16.0-coq-8.14' - repo: 'mathcomp/mathcomp' -- version: '1.16.0-coq-8.15' - repo: 'mathcomp/mathcomp' -- version: '1.16.0-coq-8.16' - repo: 'mathcomp/mathcomp' -- version: '1.16.0-coq-8.17' - repo: 'mathcomp/mathcomp' -- version: 'coq-8.16' - repo: 'mathcomp/mathcomp-dev' -- version: 'coq-8.17' - repo: 'mathcomp/mathcomp-dev' -- version: 'coq-dev' - repo: 'mathcomp/mathcomp-dev' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{(>= "1.12" & < "1.17~") | (= "dev")}' + version: '{>= "1.17" & < "1.18~"}' description: |- - [MathComp ssreflect 1.12 or later](https://math-comp.github.io) + [MathComp ssreflect 1.17 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra description: |- @@ -112,29 +80,29 @@ dependencies: [MathComp field](https://math-comp.github.io) - opam: name: coq-coqeal - version: '{>= "1.0.5"}' + version: '{>= "1.1.3" & < "2~"}' description: |- - [CoqEAL 1.0.5 or later](https://github.com/coq-community/coqeal) + [CoqEAL 1.1.3 or later](https://github.com/coq-community/coqeal) - opam: name: coq-mathcomp-real-closed - version: '{>= "1.1.2"}' + version: '{>= "1.1.4" & < "2~"}' description: |- - [MathComp real closed fields 1.1.2 or later](https://github.com/math-comp/real-closed) + [MathComp real closed fields 1.1.4 or later](https://github.com/math-comp/real-closed) - opam: name: coq-mathcomp-bigenough - version: '{>= "1.0.0"}' + version: '{>= "1.0.1"}' description: |- - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough) + [MathComp bigenough 1.0.1 or later](https://github.com/math-comp/bigenough) - opam: name: coq-mathcomp-zify - version: '{>= "1.2.0"}' + version: '{>= "1.3.0" & < "1.14~"}' description: |- - [Mczify](https://github.com/math-comp/mczify) 1.2.0 or later + [Mczify](https://github.com/math-comp/mczify) 1.3.0 or later - opam: name: coq-mathcomp-algebra-tactics - version: '{>= "0.2.0"}' + version: '{>= "1.0.0" & < "1.2~"}' description: |- - [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 0.2.0 or later + [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.0.0 or later namespace: mathcomp.apery diff --git a/theories/a_props.v b/theories/a_props.v index cd28576..b117265 100644 --- a/theories/a_props.v +++ b/theories/a_props.v @@ -34,7 +34,7 @@ Proof. by apply: rpred_sum => ?; rewrite rpred_zify. Qed. Fact lt_0_a (k : int) : 0 <= k -> 0 < a k. Proof. move=> h0k; rewrite /a big_int_recl /=; last lia. -apply: ltr_paddr; last exact: lt_0_c. +apply: ltr_wpDr; last exact: lt_0_c. by rewrite big_int_cond sumr_ge0 => // i ?; apply/ltW/lt_0_c; lia. Qed. @@ -51,7 +51,7 @@ Proof. move=> lenm. have [le0n | ltn0] := lerP 0 n; last by rewrite {1}/a big_geqz ?le_0_a; lia. have leSnSm : n + 1 <= m + 1 by lia. -rewrite /a (big_cat_int _ _ _ _ leSnSm) //=; apply: ler_paddr=> //; last first. +rewrite /a (big_cat_int _ _ _ _ leSnSm) //=; apply: ler_wpDr=> //; last first. rewrite [X in X <= _]big_int_cond [X in _ <= X]big_int_cond /=. apply: ler_sum => i; rewrite andbT => /andP [hi hin]; apply: c_incr; lia. rewrite big_int_cond; apply: sumr_ge0 => i; rewrite andbT => /andP [hni hmi]. @@ -74,8 +74,8 @@ Proof. by rewrite /rho a3_eq a2_eq. Qed. Fact le_1_rho (i : int) : 0 <= i -> 1 <= rho i. Proof. -move=> lei0; rewrite /rho ler_pdivl_mulr; last exact: lt_0_a. -by rewrite mul1r; apply: a_incr; rewrite ler_paddr. +move=> lei0; rewrite /rho ler_pdivlMr; last exact: lt_0_a. +by rewrite mul1r; apply: a_incr; rewrite ler_wpDr. Qed. Fact lt_0_rho (i : int) : 0 <= i -> 0 < rho i. @@ -97,12 +97,12 @@ Definition beta (x : rat) : rat := ((x + rat_of_Z 1) / (x + rat_of_Z 2)) ^+ 3. (* END TODO *) Fact lt_0_beta (x : rat) : 0 <= x -> 0 < beta x. -Proof. by move=> le0i; apply/exprn_gt0/divr_gt0; apply/ltr_paddl. Qed. +Proof. by move=> le0i; apply/exprn_gt0/divr_gt0; apply/ltr_wpDl. Qed. Fact lt_beta_1 (x : rat) : 0 <= x -> beta x < 1. Proof. move=> le0i; rewrite /beta expr_lte1 //; last by apply/divr_ge0; apply/addr_ge0. -by rewrite ltr_pdivr_mulr ?ltr_paddl // mul1r ltr_add2l lt_rat_of_Z. +by rewrite ltr_pdivrMr ?ltr_wpDl // mul1r ltrD2l lt_rat_of_Z. Qed. (* TODO : FIX/MOVE *) @@ -115,21 +115,21 @@ Definition alpha (x : rat) := Fact lt_2_alphaN (x : rat) : 0 <= x -> rat_of_Z 2 < alpha x. Proof. move=> le0i; rewrite /alpha. -have npos : 0 < x + rat_of_Z 2 by apply: ltr_paddl; rewrite ?ler0z. -rewrite ltr_pdivl_mulr; last by apply: exprn_gt0. +have npos : 0 < x + rat_of_Z 2 by apply: ltr_wpDl; rewrite ?ler0z. +rewrite ltr_pdivlMr; last by apply: exprn_gt0. have trans: rat_of_Z 2 * (x + rat_of_Z 2) ^+ 3 <= rat_of_Z 2 * (x + rat_of_Z 2) ^+ 2 * (rat_of_Z 2 * x + rat_of_Z 3). - rewrite [_ ^+ 3]exprSr mulrA ler_wpmul2l //. + rewrite [_ ^+ 3]exprSr mulrA ler_wpM2l //. by rewrite mulr_ge0 // exprn_ge0 // addr_ge0. - by apply: ler_add (ler_pemull _ _) _ => //; ring_lia. + by apply: lerD (ler_peMl _ _) _ => //; ring_lia. apply: le_lt_trans trans _. suff trans : rat_of_Z 2 * (x + rat_of_Z 2) ^+ 2 < rat_of_Z 17 * x ^ 2 + rat_of_Z 51 * x + rat_of_Z 39. - by rewrite ltr_pmul2r // ltr_paddl // mulr_ge0. -rewrite -exprnP sqrrD !mulrDr; apply: ler_lt_add; last first. + by rewrite ltr_pM2r // ltr_wpDl // mulr_ge0. +rewrite -exprnP sqrrD !mulrDr; apply: ler_ltD; last first. by rewrite [_ < _]refines_eq. -apply: ler_add; first by rewrite ler_wpmul2r ?exprn_ge0 // [_ <= _]refines_eq. -by rewrite [x * _]mulrC mulrA -mulrDl ler_wpmul2r // [_ <= _]refines_eq. +apply: lerD; first by rewrite ler_wpM2r ?exprn_ge0 // [_ <= _]refines_eq. +by rewrite [x * _]mulrC mulrA -mulrDl ler_wpM2r // [_ <= _]refines_eq. Qed. @@ -143,7 +143,7 @@ move=> le0i; rewrite -subr_ge0; set rhs := (X in 0 <= X). have -> : rhs = (rat_of_Z 51 * x ^+ 4 + rat_of_Z 456 * x ^+ 3 + rat_of_Z 1497 * x ^+ 2 + rat_of_Z 2136 * x + rat_of_Z 1121) / ((x + rat_of_Z 3) ^+ 3 * (x + rat_of_Z 2) ^+ 3). - by rewrite /rhs /alpha; field; rewrite !lt0r_neq0 // ltr_paddl. + by rewrite /rhs /alpha; field; rewrite !lt0r_neq0 // ltr_wpDl. by rewrite divr_ge0 ?addr_ge0 // mulr_ge0 // exprn_ge0 // addr_ge0. Qed. @@ -154,7 +154,7 @@ Fact lt_0_delta (x : rat) : 0 <= x -> 0 < delta x. Proof. move=> le0x; rewrite /delta subr_gt0. have /lt_trans -> //: rat_of_Z 4 * beta x < rat_of_Z 4. - by rewrite gtr_pmulr // lt_beta_1. + by rewrite gtr_pMr // lt_beta_1. have -> : rat_of_Z 4 = rat_of_Z 2 ^+ 2 by ring. rewrite -subr_gt0 subr_sqr mulr_gt0 //. rewrite subr_gt0; exact: lt_2_alphaN. @@ -173,7 +173,7 @@ have -> : rhs = (rat_of_Z 3456 * x ^ 10 + rat_of_Z 77550 * x ^ 9 + rat_of_Z 8307151) / ((x + rat_of_Z 3) ^ 6 * (x + rat_of_Z 2) ^ 6). rewrite {}/rhs /delta /alpha /beta. - by field; rewrite !lt0r_neq0 // ltr_paddl. + by field; rewrite !lt0r_neq0 // ltr_wpDl. by rewrite divr_ge0 ?addr_ge0 // mulr_ge0 // exprn_ge0 // addr_ge0. Qed. @@ -265,37 +265,37 @@ suff rho_in_Iyx i (le2i : 2%:~R <= i) : yp i <= QtoR (rho i) <= xp i. by have /andP[yr rx] := rho_in_Iyx _ le2k; apply: hr_p_pos. have lt_0_xp j : 0 <= j -> 0 < xp j. move=> le0j; rewrite /xp; apply: divr_gt0. - exact/ltr_paddr/lt_Ralpha_0/le0j/sqrtr_ge0. + exact/ltr_wpDr/lt_Ralpha_0/le0j/sqrtr_ge0. by rewrite RealAlg.ltr_to_alg. have le_1_xp j (le0j : 0 <= j) : 1 <= xp j. - rewrite /xp lter_pdivl_mulr ?mul1r; last by rewrite RealAlg.ltr_to_alg. + rewrite /xp lter_pdivlMr ?mul1r; last by rewrite RealAlg.ltr_to_alg. have trans : QtoR (rat_of_Z 2) <= Ralpha j%:Q. by apply: ltW; rewrite RealAlg.ltr_to_alg lt_2_alphaN // ler0z. - apply: le_trans trans _; rewrite ler_addl; exact: sqrtr_ge0. + apply: le_trans trans _; rewrite lerDl; exact: sqrtr_ge0. have le_yp_1 j : 2%:~R <= j -> yp j <= 1. move=> le2j. have le0j : 0 <= j by apply: le_trans le2j; rewrite le0z_nat. have -> : yp j = Rbeta j%:Q / xp j. by rewrite -xyp // mulrAC mulfV ?mul1r //; apply/lt0r_neq0/lt_0_xp. - rewrite ler_pdivr_mulr ?lt_0_xp // mul1r. + rewrite ler_pdivrMr ?lt_0_xp // mul1r. by apply/le_trans/le_1_xp/le0j/ltW/lt_Rbeta_1. have hr_incr j x y : 0 <= j -> 0 < x -> x <= y -> hr j x <= hr j y. move=> le0j lt0x lexy; rewrite -subr_ge0 /hr addrAC [- (Ralpha _ - _)]opprD. rewrite opprK addrA addrN add0r -mulrBr; apply: mulr_ge0. by rewrite RealAlg.ler_to_alg; apply/ltW/lt_0_beta; rewrite ler0z. - by rewrite subr_ge0 lef_pinv // posrE //; apply: lt_le_trans lexy. + by rewrite subr_ge0 lef_pV2 // posrE //; apply: lt_le_trans lexy. suff rho_in_I1x : 1 <= QtoR (rho i) <= xp i. by case/andP: rho_in_I1x => h1 ->; rewrite andbT; exact/le_trans/h1/le_yp_1. suff lerx : QtoR (rho i) <= xp i. by rewrite [X in X && _]RealAlg.ler_to_alg le_1_rho //=; apply: le_trans le2i. suff im_hr j x : 0 <= j -> 0 < x -> x <= xp j -> hr j x <= xp (j + 1). have base_case : QtoR (rho 2) <= xp 2. - rewrite /xp ler_pdivl_mulr; last by rewrite RealAlg.ltr_to_alg. - rewrite -ler_subl_addl; set lhs := (X in X <= _). + rewrite /xp ler_pdivlMr; last by rewrite RealAlg.ltr_to_alg. + rewrite -lerBlDl; set lhs := (X in X <= _). have [le_lhs_0 | lt_0_lhs] := ler0P lhs. exact/le_trans/sqrtr_ge0/le_lhs_0. rewrite -[lhs]gtr0_norm // -sqrtr_sqr; apply: ler_wsqrtr; rewrite /lhs. - rewrite -rmorphM /Ralpha -rmorphB -rmorphX /deltap RealAlg.ler_to_alg. + rewrite -rmorphM /Ralpha -rmorphB -rmorphXn /deltap RealAlg.ler_to_alg. have ->: 2%:~R = rat_of_Z 2 by rewrite rat_of_ZEdef. by rewrite /delta rho2_eq /alpha [_ <= _]refines_eq; vm_compute. case: i le2i; last by discriminate. @@ -315,9 +315,9 @@ have -> : hr j (xp j) = xp j. by rewrite fac_p // subrr mul0r oppr0. move=> h; apply: le_trans h _. suff xp_incr : xp j <= xp (j + 1) by []. -rewrite /xp ler_pmul2r; last first. +rewrite /xp ler_pM2r; last first. by rewrite invr_gt0 RealAlg.ltr_to_alg. -apply: ler_add. +apply: lerD. by rewrite RealAlg.ler_to_alg rmorphD /=; apply: alpha_incr; rewrite ler0z. rewrite ler_sqrt; last by try apply/ltW; apply/deltap_pos/addr_ge0. by rewrite /deltap RealAlg.ler_to_alg rmorphD; apply: delta_incr; rewrite ler0z. @@ -366,14 +366,14 @@ Proof. move=> lt1i ltiNrho. rewrite /Ka; set Ka' := (X in a 1 * X * _ <_). suff : Ka' * 33%:Q ^ i < a i / a 1. - rewrite [in X in X -> _]ltr_pdivl_mulr; last exact: lt_0_a. + rewrite [in X in X -> _]ltr_pdivlMr; last exact: lt_0_a. by rewrite mulrC [in X in X -> _]mulrA. rewrite -[X in _ < X](@telescope_prod_int _ 1 i (fun i => a i)) //; last first. by move=> /= k /andP [le1k ltki]; apply/a_neq0/le_trans/le1k. -rewrite (big_cat_int _ _ _ _ (ltW ltiNrho)) /=; last by rewrite ler_addr. +rewrite (big_cat_int _ _ _ _ (ltW ltiNrho)) /=; last by rewrite lerDr. suff hrho_maj : 33%:Q ^ i / 33%:Q ^+ N_rho.+1 < \prod_(Posz N_rho + 1 <= i0 < i :> int) (a (i0 + 1) / a i0). - rewrite /Ka' mulrAC -mulrA ltr_pmul2l; first exact: hrho_maj. + rewrite /Ka' mulrAC -mulrA ltr_pM2l; first exact: hrho_maj. rewrite big_int_cond; apply: prodr_gt0 => j; rewrite andbT => /andP [hj _]. exact/lt_0_rho/le_trans/hj. rewrite -PoszD; case: i lt1i ltiNrho => i //. @@ -384,7 +384,7 @@ Qed. Lemma a_asympt (n : nat) : (N_rho + 1 < n)%N -> 1 / a n < Ka^-1 / 33%:Q ^ n. Proof. -move=> hn; rewrite ltr_pdivr_mulr; last exact: lt_0_a. -rewrite -invfM ltr_pdivl_mull; last exact/mulr_gt0/exprz_gt0/isT/lt_0_Ka. +move=> hn; rewrite ltr_pdivrMr; last exact: lt_0_a. +rewrite -invfM ltr_pdivlMl; last exact/mulr_gt0/exprz_gt0/isT/lt_0_Ka. by rewrite mulr1; apply/a_maj/hn/leq_trans/hn. Qed. diff --git a/theories/bigopz.v b/theories/bigopz.v index 4ce996c..46388ac 100644 --- a/theories/bigopz.v +++ b/theories/bigopz.v @@ -56,7 +56,7 @@ case: m => m; case: n => n; rewrite /index_iotaz => //=. by move=> mn; apply/eqP; rewrite subn_eq0. + by rewrite lez_nat ltnW // subzn ?(ltnW hnm) // absz_nat. - by rewrite size_cat size_rev /index_iota /= !size_map !size_iota addnC subn0. -- rewrite size_map size_rev /index_iota size_iota !NegzE ler_opp2 lez_nat. +- rewrite size_map size_rev /index_iota size_iota !NegzE lerN2 lez_nat. rewrite opprK addrC; case: ifP => hnm; first by rewrite subzn. case: (altP (n =P m)) => [-> | enm]; first by rewrite subnn. apply/eqP; rewrite subn_eq0 ltnNge; move: hnm; rewrite ltnS leq_eqVlt. @@ -76,17 +76,17 @@ case: m => m; case: n => n; rewrite /index_iotaz. - by rewrite in_nil; case: i => xi //; rewrite andbF. - rewrite mem_cat; apply/orP/idP => [[] | ]. + rewrite mem_rev; case/mapP=> xi; rewrite mem_iota add0n; case/andP=> _ hi ->. - by rewrite andbT !NegzE ler_opp2 /= lez_nat. + by rewrite andbT !NegzE lerN2 /= lez_nat. + case/mapP=> xi; rewrite mem_index_iota; case/andP=> _ hi -> /=. by rewrite ltz_nat. case: i => xi. + by rewrite /= => hi; right; apply/mapP; exists xi; rewrite // mem_index_iota. - + rewrite andbT {1}(NegzE xi) (NegzE m) ler_opp2 => hi; left; rewrite mem_rev. + + rewrite andbT {1}(NegzE xi) (NegzE m) lerN2 => hi; left; rewrite mem_rev. rewrite mem_map ?mem_index_iota //; exact: Negz_inj. - apply/idP/idP. case/mapP=> xi; rewrite mem_rev mem_index_iota => hi ->. - by rewrite !NegzE ler_opp2 ltr_opp2 andbC ltz_nat lez_nat. - case: i => // xi; rewrite !NegzE ler_opp2 ltr_opp2 lez_nat ltz_nat andbC => hi. + by rewrite !NegzE lerN2 ltrN2 andbC ltz_nat lez_nat. + case: i => // xi; rewrite !NegzE lerN2 ltrN2 lez_nat ltz_nat andbC => hi. rewrite -NegzE mem_map; last exact: Negz_inj. by rewrite mem_rev mem_index_iota. Qed. @@ -112,12 +112,12 @@ case: m => m; case: n => n // hmn hi; rewrite /index_iotaz /=. by rewrite size_iota -ek leq_subr. - have {}hi : (i - m.+1 < n)%N. move: hi; rewrite NegzE opprK -PoszD ger0_norm //. - by rewrite PoszD -lter_sub_addr subzn ?ltz_nat // ltnNge -ltnS him. + by rewrite PoszD -lterBDr subzn ?ltz_nat // ltnNge -ltnS him. rewrite (nth_map 0%N); last by rewrite /index_iota size_iota subn0. rewrite /index_iota subn0 nth_iota // add0n NegzE addrC subzn //. by rewrite ltnNge -ltnS him. - have {}hmn : (n <= m)%N. - by move: hmn; rewrite !NegzE ler_oppl opprK lez_nat. + by move: hmn; rewrite !NegzE lerNl opprK lez_nat. have hi' : (i < m - n)%N. by move: hi; rewrite !NegzE opprK addrC subzn. have hi'' : (i <= m)%N. @@ -202,7 +202,7 @@ Lemma big_geqz m n (P : pred int) F : Proof. case: m => m; case: n => // n; rewrite /index_iotaz ?big_nil //. by rewrite lez_nat /index_iota; move/eqnP->; rewrite big_nil. -rewrite ![in _ <= _]NegzE ler_opp2 lez_nat /index_iota; move/eqnP->. +rewrite ![in _ <= _]NegzE lerN2 lez_nat /index_iota; move/eqnP->. by rewrite big_nil. Qed. @@ -220,7 +220,7 @@ case: m => m; case: n => n // hmn. by rewrite addNr big_map -NegzE /index_iotaz /= big_cons big_map. rewrite addrC subzSS add0r -!NegzE /index_iotaz -(addn1 m.+1). by rewrite /index_iota subn0 iotaD map_cat rev_cat add0n /= big_cons. -- case: m hmn => [ | m] //; rewrite !NegzE ltr_opp2 ltz_nat => hmn. +- case: m hmn => [ | m] //; rewrite !NegzE ltrN2 ltz_nat => hmn. rewrite addrC subzSS add0r -!NegzE /index_iotaz /index_iota subSn //. by rewrite -[(_ - _).+1]addn1 iotaD rev_cat map_cat subnKC // big_cons. Qed. @@ -240,12 +240,12 @@ Proof. suff -> : index_iotaz (m + a) n = map (fun i => i + a) (index_iotaz m (n - a)). by rewrite big_map. apply: (@eq_from_nth _ 0). - by rewrite size_map !size_index_iotaz ler_sub_addl addrC -addrA opprD. + by rewrite size_map !size_index_iotaz lerBDl addrC -addrA opprD. move=> i; rewrite size_index_iotaz; case: ifP => // hman hi. rewrite nth_index_iotaz // (nth_map 0); last first. - rewrite size_index_iotaz ler_sub_addr hman. + rewrite size_index_iotaz lerBDr hman. by move: hi; rewrite opprD -addrCA addrC. -rewrite nth_index_iotaz 1?addrAC // ?ler_sub_addr //. +rewrite nth_index_iotaz 1?addrAC // ?lerBDr //. by move: hi; rewrite opprD addrA. Qed. @@ -277,7 +277,7 @@ Lemma index_iotaz_add n m p : m <= n -> n <= p -> Proof. move=> hmn hnp. have h : `|n - m| + `|p - n| = `|p - m|%N. - move/leqifP: (leqif_add_distz p n m). + move/leqifP: (leqifD_distz p n m). rewrite hnp hmn orbT addnC; move/eqP; move/(f_equal Posz). by rewrite PoszD; move<-. apply: (@eq_from_nth _ 0); rewrite size_cat !size_index_iotaz hmn hnp. @@ -290,7 +290,7 @@ apply: (@eq_from_nth _ 0); rewrite size_cat !size_index_iotaz hmn hnp. have hmn' : `|n - m | = n - m by apply: ger0_norm; rewrite subr_gte0. rewrite nth_index_iotaz //; last first. rewrite -subzn; last by rewrite leqNgt hi2. - by rewrite lter_sub_addr addrC h ltz_nat. + by rewrite lterBDr addrC h ltz_nat. rewrite nth_index_iotaz //; last exact: le_trans hnp. rewrite -subzn; last by rewrite leqNgt hi2. move: hmn'; rewrite abszE; move->. rewrite addrCA opprB. @@ -310,7 +310,7 @@ Lemma big_int_recr m n F : m <= n -> \big[op/idx]_(m <= i < n + 1 :> int) F i = op (\big[op/idx]_(m <= i < n :> int) F (i)) (F n). Proof. -move=> hmn; rewrite (@big_cat_int n) ?ler_paddr //=. +move=> hmn; rewrite (@big_cat_int n) ?ler_wpDr //=. rewrite big_addz2l (@big_ltz 0 1) // add0r (@big_geqz 1 1) // add0r. by rewrite Monoid.Theory.mulm1. Qed. @@ -339,7 +339,7 @@ rewrite Monoid.Theory.mul1m. rewrite big_ltz_cond // eqxx big_hasC; last first. apply/hasPn => k. rewrite mem_index_iotaz; case/andP=> hkj _. suff : j < k by rewrite lt_def eq_sym; case/andP. - by apply: lt_le_trans hkj; rewrite cpr_add. + by apply: lt_le_trans hkj; rewrite cprD. by rewrite Monoid.Theory.mulm1. Qed. @@ -409,7 +409,7 @@ transitivity (\prod_(0 <= i < bma) (f (Posz (i + 1)%N + a) / f (Posz i + a))). apply: congr_big_nat => // i _ ; by rewrite PoszD addrAC. rewrite (@telescope_prod_nat _ _ _ (fun i => f (Posz i + a))%R) //. - by rewrite add0r -e addrNK. -- move=> k /andP [h0k hbma]; apply: hf; rewrite ler_addr -ltr_subr_addr e. +- move=> k /andP [h0k hbma]; apply: hf; rewrite lerDr -ltrBrDr e. by rewrite lez_nat ltz_nat h0k /=. - have : 0 < b - a by rewrite subr_gt0. by rewrite e ltz_nat. diff --git a/theories/binomialz.v b/theories/binomialz.v index ec7e74d..d797c50 100644 --- a/theories/binomialz.v +++ b/theories/binomialz.v @@ -298,7 +298,7 @@ Proof. elim : m n => [ | m Hm] n. by rewrite ffactn1 ffactn0 mul1r subr0. rewrite ffactnS Hm ffactnS -mulrA; repeat congr (_ * _). -by rewrite -!addrA; congr(_ + _); rewrite -addn1 -oppz_add addrC. +by rewrite -!addrA; congr(_ + _); rewrite -addn1 -oppzD addrC. Qed. (* Do not know yet if signed conditions are better expressed as such or as diff --git a/theories/extra_cauchyreals.v b/theories/extra_cauchyreals.v index 769d4d1..ff43cd2 100644 --- a/theories/extra_cauchyreals.v +++ b/theories/extra_cauchyreals.v @@ -29,7 +29,7 @@ Lemma ltcr_add2r (z x y : creal F) : (x < y)%CR -> (x + z < y + z)%CR. Proof. move=> lt_xy; pose_big_enough i. apply: (@lt_crealP _ (diff lt_xy) i i); rewrite ?diff_gt0 //=. - by rewrite addrAC ler_add2r diffP. + by rewrite addrAC lerD2r diffP. by close. Qed. @@ -37,7 +37,7 @@ Lemma ltcr_add2l (z x y : creal F) : (x < y)%CR -> (z + x < z + y)%CR. Proof. move=> lt_xy; pose_big_enough i. apply: (@lt_crealP _ (diff lt_xy) i i); rewrite ?diff_gt0 //=. - rewrite -addrA ler_add2l diffP //. + rewrite -addrA lerD2l diffP //. by close. Qed. @@ -61,10 +61,10 @@ Proof. move=> ltxy lt0z; pose_big_enough i. apply: (@lt_crealP _ ((diff ltxy) * (diff lt0z)) i i) => //=. - apply: mulr_gt0; exact: diff_gt0. - rewrite -ler_sub_addl -mulrBl; apply: ler_pmul. + rewrite -lerBDl -mulrBl; apply: ler_pM. - by apply: ltW; apply: diff_gt0. - by apply: ltW; apply: diff_gt0. - - by rewrite ler_sub_addl diffP. + - by rewrite lerBDl diffP. - by rewrite -[X in X <= _]add0r -[0]/((0%:CR)%CR i) diffP. by close. Qed. @@ -114,7 +114,7 @@ Lemma mulr_gtcr0 (x y : creal F) : (0 < x -> 0 < y -> 0 < x * y)%CR. move=> lt_0x lt_0y; pose_big_enough i. apply: (@lt_crealP _ ((diff lt_0x) * (diff lt_0y)) i i) => //=. - apply: mulr_gt0; exact: diff_gt0. - rewrite add0r; apply: ler_pmul. + rewrite add0r; apply: ler_pM. - by apply: ltW; apply: diff_gt0. - by apply: ltW; apply: diff_gt0. - by rewrite -[X in X <= _]add0r -[0]/((0%:CR)%CR i) diffP. @@ -143,7 +143,7 @@ Qed. Lemma lt_ubound (x : creal F) : (x < (ubound x + 1)%:CR)%CR. Proof. pose_big_enough i. - apply: (@lt_crealP _ 1 i i) => //=; rewrite ler_add2r. + apply: (@lt_crealP _ 1 i i) => //=; rewrite lerD2r. apply: le_trans (uboundP x i); exact: ler_norm. by close. Qed. @@ -158,7 +158,7 @@ move=> ltxy leyz; pose_big_enough i. apply/eqP; rewrite eq_sym subr_eq -addrA -mulrDr. have <- : 1 = 2%:~R^-1 + 2%:~R^-1 :> F by rewrite [LHS](splitf 2) div1r. by rewrite mulr1. - rewrite ler_subl_addr; apply: le_trans (diffP _ _) _ => //; apply: ltW. + rewrite lerBlDr; apply: le_trans (diffP _ _) _ => //; apply: ltW. by apply: le_modP. by close. Qed. @@ -171,7 +171,7 @@ move=> lexy ltyz; pose_big_enough i. have hpos : 0 < diff ltyz / 2%:~R. apply: divr_gt0; rewrite ?ltr0Sn //; exact: diff_gt0. apply: (@lt_crealP _ ((diff ltyz) / 2%:~R) i i) => //=. - apply: le_trans (@diffP _ _ _ ltyz _ _ _) => //; rewrite -ler_subr_addr. + apply: le_trans (@diffP _ _ _ ltyz _ _ _) => //; rewrite -lerBrDr. suff <- : y i + diff ltyz / 2%:~R = y i + diff ltyz - diff ltyz / 2%:~R. by apply: ltW; apply: le_modP. apply/eqP; rewrite eq_sym subr_eq -addrA -mulrDr. @@ -233,9 +233,9 @@ exists_big_modulus m F. rewrite /d [(_ - _) + _]addrC addrA addrNK opprB addrA [_ - x i]addrC. by rewrite addrA addKr addrC. suff step1 : `|d j + (x i - x j)| + `|d i| < eps. - by apply: le_lt_trans step1; rewrite -[`|d i|]normrN; apply: ler_norm_add. + by apply: le_lt_trans step1; rewrite -[`|d i|]normrN; apply: ler_normD. suff step2 : `|d j| + `|x i - x j| + `|d i| < eps. - by apply: le_lt_trans step2; rewrite ler_add2r; apply: ler_norm_add. + by apply: le_lt_trans step2; rewrite lerD2r; apply: ler_normD. have -> : eps = eps / 3%:~R + eps / 3%:~R + eps / 3%:~R. rewrite /= in eps lt_eps_0 hmi hmj *. rewrite -!mulrDl -[in X in _ = X](mulr1 eps) -!mulrDr -mulrA. @@ -243,8 +243,8 @@ exists_big_modulus m F. rewrite -[X in (X + X + X) / _ = _]/(1%:~R) -!rmorphD /= mulfV //. by rewrite intr_eq0. have heps : 0 < eps / 3%:~R by apply: divr_gt0 => //; rewrite ltr0z. - apply: ltr_add => //; last exact: MP. - apply: ltr_add=> //; first by exact: MP. + apply: ltrD => //; last exact: MP. + apply: ltrD=> //; first by exact: MP. by move=> {MP}; apply: mxP. by close. Qed. diff --git a/theories/extra_mathcomp.v b/theories/extra_mathcomp.v index efa01a0..f6293aa 100644 --- a/theories/extra_mathcomp.v +++ b/theories/extra_mathcomp.v @@ -45,8 +45,8 @@ Lemma ltr_pmul_le_l R (x1 y1 x2 y2 : R) : 0 < x1 -> 0 < x2 -> x1 <= y1 -> x2 < y2 -> x1 * x2 < y1 * y2. Proof. rewrite le_eqVlt => posx1 posx2 /predU1P[<-|lt1] lt2. - by rewrite ltr_pmul2l. -by apply: ltr_pmul=> //; exact: ltW. + by rewrite ltr_pM2l. +by apply: ltr_pM=> //; exact: ltW. Qed. Lemma ltr_pmul_le_r R (x1 y1 x2 y2 : R) : @@ -59,14 +59,14 @@ Lemma exp_incr_expp R (x : R) (H1x : 1 <= x) (m n : nat) : (m <= n)%N -> x ^+ m <= x ^+ n. Proof. move/subnK => <-; rewrite exprD. -exact/ler_pemull/exprn_ege1/H1x/exprn_ge0/le_trans/H1x. +exact/ler_peMl/exprn_ege1/H1x/exprn_ge0/le_trans/H1x. Qed. Lemma exp_incr_expn R (x : R) (H1x : 0 < x < 1) (m n : nat) : (n <= m)%N -> x ^+ m <= x ^+ n. Proof. case/andP: H1x => lt0x ltx1 /subnK <-; rewrite exprD. -exact/ler_pimull/exprn_ile1/ltW/ltx1/ltW/lt0x/exprn_ge0/ltW. +exact/ler_piMl/exprn_ile1/ltW/ltx1/ltW/lt0x/exprn_ge0/ltW. Qed. Lemma ler1q F x: (1 <= ratr x :> F) = (1 <= x). @@ -90,25 +90,25 @@ Implicit Types x y z : algC. Lemma root_le_x (n : nat) x y : (0 < n)%N -> 0 <= x -> 0 <= y -> (n.-root x <= y) = (x <= y ^+ n). Proof. -by move => Hn Hx Hy; rewrite -(ler_pexpn2r Hn) ?rootCK // nnegrE rootC_ge0. +by move => Hn Hx Hy; rewrite -(ler_pXn2r Hn) ?rootCK // nnegrE rootC_ge0. Qed. Lemma root_x_le (n : nat) x y : (0 < n)%N -> 0 <= x -> 0 <= y -> (x <= n.-root y) = (x ^+ n <= y). Proof. -by move => Hn Hx Hy; rewrite -[LHS](ler_pexpn2r Hn) ?rootCK // nnegrE rootC_ge0. +by move => Hn Hx Hy; rewrite -[LHS](ler_pXn2r Hn) ?rootCK // nnegrE rootC_ge0. Qed. Lemma root_lt_x (n : nat) x y : (0 < n)%N -> 0 <= x -> 0 <= y -> (n.-root x < y) = (x < y ^+ n). Proof. -by move=> Hn Hx Hy; rewrite -(ltr_pexpn2r Hn) ?rootCK // nnegrE rootC_ge0. +by move=> Hn Hx Hy; rewrite -(ltr_pXn2r Hn) ?rootCK // nnegrE rootC_ge0. Qed. Lemma root_x_lt (n : nat) x y : (0 < n)%N -> 0 <= x -> 0 <= y -> (x < n.-root y) = (x ^+ n < y). Proof. -by move => Hn Hx Hy; rewrite -[LHS](ltr_pexpn2r Hn) ?rootCK // nnegrE rootC_ge0. +by move => Hn Hx Hy; rewrite -[LHS](ltr_pXn2r Hn) ?rootCK // nnegrE rootC_ge0. Qed. Lemma rootC_leq (m n : nat) x : @@ -123,7 +123,7 @@ Qed. (* Not sure if actually needed in library, but this lemma is helpful to prove one_plus_invx_expx below *) Lemma le_mrootn_n (m n : nat) : m.+1.-root n.+1%:R <= n.+1%:R :> algC. -Proof. by rewrite root_le_x ?ler_eexpr // (ler0n, ler1n). Qed. +Proof. by rewrite root_le_x ?ler_eXnr // (ler0n, ler1n). Qed. Lemma prod_root m n x : (0 < m)%N -> (0 < n)%N -> 0 <= x -> (m * n)%N.-root x = m.-root (n.-root x). @@ -152,13 +152,13 @@ pose_big_enough M. have le1r : 1 <= r by rewrite ltW. have {}lt1r : 0 < r - 1 by rewrite subr_gt0. suff aux (n : nat) : n%:Q * (r - 1) - 1 <= r ^ n. - apply: lt_le_trans (aux k); rewrite -ltr_sub_addr opprK -ltr_pdivr_mulr //. + apply: lt_le_trans (aux k); rewrite -ltrBDr opprK -ltr_pdivrMr //. have: 0 <= (E + 1) / (r - 1) by apply/divr_ge0/ltW/lt1r/addr_ge0. by move/archi_boundP/lt_trans; apply; rewrite ltr_nat. rewrite -pmulrn /exprz; elim: n => [|n ihn]; first by rewrite mul0r. - rewrite mulrSr mulrDl mul1r addrAC -ler_subr_addr; apply: le_trans ihn _. + rewrite mulrSr mulrDl mul1r addrAC -lerBrDr; apply: le_trans ihn _. rewrite exprSr -[r - 1]mul1r -[r in _ * r](subrK 1) mulrDr mulr1 addrAC. - by rewrite -mulrBl ler_addr pmulr_lge0 // subr_ge0 exprn_ege1. + by rewrite -mulrBl lerDr pmulr_lge0 // subr_ge0 exprn_ege1. by close. Qed. @@ -169,7 +169,7 @@ move=> ge0eps /andP [lt0r ltr1]. have hE : 0 <= eps ^-1 by apply/ltW; rewrite invr_gt0. have hr : 1 < r ^-1 by rewrite invf_gt1. have [M hM] := Gseqgt1 hE hr; exists M => n hMn. -rewrite -ltf_pinv //; first by rewrite invr_expz -exprz_inv; exact: hM. +rewrite -ltf_pV2 //; first by rewrite invr_expz -exprz_inv; exact: hM. exact: exprz_gt0. Qed. diff --git a/theories/floor.v b/theories/floor.v index c84bca7..9e6b78a 100644 --- a/theories/floor.v +++ b/theories/floor.v @@ -13,17 +13,17 @@ Definition floorQ (r : rat) := (numq r %/ denq r)%Z. Lemma floorQ_spec (r : rat) : (floorQ r)%:Q <= r < (floorQ r)%:Q + 1. Proof. -rewrite -[r in _ <= r < _]divq_num_den ler_pdivl_mulr ?ltr_pdivr_mulr ?ltr0z //. +rewrite -[r in _ <= r < _]divq_num_den ler_pdivlMr ?ltr_pdivrMr ?ltr0z //. by rewrite -rat1 -intrD -!intrM ler_int ltr_int lez_floor ?ltz_ceil. Qed. Lemma floorQ_epslt1 (r : rat) : 0 <= r - (floorQ r)%:Q < 1. -Proof. by rewrite subr_ge0 ltr_subl_addl floorQ_spec. Qed. +Proof. by rewrite subr_ge0 ltrBlDl floorQ_spec. Qed. Lemma floorQ_grows (r1 r2 : rat) : r1 <= r2 -> floorQ r1 <= floorQ r2. Proof. move => Hr12. -suff: (floorQ r1)%:Q < (floorQ r2 + 1)%:Q by rewrite ltr_int ltz_addr1. +suff: (floorQ r1)%:Q < (floorQ r2 + 1)%:Q by rewrite ltr_int ltzD1. rewrite intrD; case/andP: (floorQ_spec r2) => _; apply: le_lt_trans. by apply: le_trans Hr12; case/andP: (floorQ_spec r1). Qed. @@ -33,12 +33,12 @@ Proof. have /andP[Hfloor1 Hfloor2] := floorQ_spec r. case/andP => Hm1 Hm2. move: (le_lt_trans Hm1 Hfloor2) (le_lt_trans Hfloor1 Hm2). -rewrite -[n in _ + n]rat1 -intrD !ltr_int !ltz_addr1 => ? ?. +rewrite -[n in _ + n]rat1 -intrD !ltr_int !ltzD1 => ? ?. by apply/eqP; rewrite eq_le; apply/andP. Qed. Lemma floorQ_int (m : int) : m = floorQ m%:Q. -Proof. by apply: floorQ_unique; rewrite ltr_int ltz_addr1 !lexx. Qed. +Proof. by apply: floorQ_unique; rewrite ltr_int ltzD1 !lexx. Qed. Lemma floorQ_ge0 (r : rat) : 0 <= r -> 0 <= floorQ r. Proof. by move=> Hrge0; rewrite [0]floorQ_int floorQ_grows. Qed. @@ -50,16 +50,16 @@ Lemma floor_addEpsilon (m : int) (epsilon : rat) : 0 <= epsilon < 1 -> floorQ (m%:Q + epsilon) = m. Proof. move=> /andP[Heps1 Heps2]. -by apply/esym/floorQ_unique; rewrite ler_addl Heps1 intrD ltr_add2l. +by apply/esym/floorQ_unique; rewrite lerDl Heps1 intrD ltrD2l. Qed. Lemma floorQ_div (q : rat) (m : nat) : floorQ (q / m.+1%:Q) = floorQ ((floorQ q)%:Q / m.+1%:Q). Proof. apply/floorQ_unique; move: (floorQ_spec q) (floorQ_spec (q / m.+1%:Q)). -rewrite !ler_pdivl_mulr ?ltr_pdivr_mulr ?ltr0z // intrD -intrM ler_int. +rewrite !ler_pdivlMr ?ltr_pdivrMr ?ltr0z // intrD -intrM ler_int. move=> /andP[_ Hq] /andP[Hdiv /le_lt_trans ->] //. -rewrite -ltz_addr1 -(ltr_int [numDomainType of rat]) intrD. +rewrite -ltzD1 -(ltr_int [numDomainType of rat]) intrD. by rewrite (le_lt_trans Hdiv). Qed. @@ -75,7 +75,7 @@ Lemma floorQ_divn (m : nat) (n : nat) : floorQ (m%:Q / n.+1%:Q) = floorQ (m %/ n.+1)%N%:Q. Proof. apply/esym/floorQ_unique. -rewrite -floorQ_int ler_pdivl_mulr ?ltr_pdivr_mulr ?ltr0z //. +rewrite -floorQ_int ler_pdivlMr ?ltr_pdivrMr ?ltr0z //. rewrite -!natrM ler_nat ltr_nat mulnDl mul1n. by rewrite [m in (_ <= m < _)%N](divn_eq m n.+1) leq_addr ltn_add2l ltn_mod. Qed. diff --git a/theories/hanson.v b/theories/hanson.v index 94596b8..baad385 100644 --- a/theories/hanson.v +++ b/theories/hanson.v @@ -46,7 +46,7 @@ rewrite exp_quo_nat_nat; apply: exp_quo_self_grows => //. - by rewrite divr1. - by rewrite divr_gt0 // ltr0n subn_gt0. - by rewrite ler1n divn_gt0. -by rewrite ler_pdivr_mulr // -natrM ler_nat remark_7_1. +by rewrite ler_pdivrMr // -natrM ler_nat remark_7_1. Qed. Lemma remark_7_3 : @@ -54,10 +54,10 @@ Lemma remark_7_3 : f n%:Q n (a i) / ((n %/ a i) ^ (n %/ a i))%N%:Q%:C <= f n%:Q n (a i) / f (n.+1 - a i)%N%:Q (n.+1 - a i)%N (a i). Proof. -rewrite /= ler_pdivr_mulr; last first. +rewrite /= ler_pdivrMr; last first. by rewrite ltr0q ltr0n expn_gt0 divn_gt0 ?Hain. -rewrite[X in _ <= X]mulrC mulrA ler_pdivl_mulr. -- rewrite mulrC; apply/ler_wpmul2l/remark_7_2. +rewrite[X in _ <= X]mulrC mulrA ler_pdivlMr. +- rewrite mulrC; apply/ler_wpM2l/remark_7_2. by apply: exp_quo_ge0; rewrite // divr_ge0 ?ler0n. - by apply: exp_quo_gt0; rewrite // divr_gt0 // ltr0n ?subn_gt0. Qed. @@ -75,7 +75,7 @@ have {r} ->: 1 + r = n%:Q / (n.+1 - a i)%N%:Q. by rewrite /r -!subzn //; first field; ring_lia. case: (a i) (a_pos i) Hain => // ai' _ Hain'. rewrite subn1 subSS exprMn exprVn ![exp_quo _ _ _ ^+ ai'.+1]exprAC !rootCK //. -rewrite rmorphX !rmorphM !fmorphV !rmorph_int !exprMn !exprVn !exprnP /=. +rewrite rmorphXn !rmorphM !fmorphV !rmorph_int !exprMn !exprVn !exprnP /=. rewrite -subzn ?expfzDr -?invr_expz ?exprz_pintl; [| ring_lia..]. by field; rewrite !intr_eq0 !expf_eq0; lia. Qed. @@ -100,12 +100,12 @@ have -> : n%:Q = num_of_pos posn by []. apply: le_lt_trans (remark_7_3 Hain) _. set lhs := (X in X < _); set rhs := (X in _ < X). suff : lhs ^+ a i < rhs ^+ a i. - rewrite ltr_pexpn2r // nnegrE; last exact: exp_quo_ge0. + rewrite ltr_pXn2r // nnegrE; last exact: exp_quo_ge0. (* roots, hence alg. numbers prevent using posnum based automation *) by rewrite /lhs divr_ge0 // exp_quo_ge0 // divr_ge0 // ler0z. rewrite remark_7_4 // /rhs -mulrA ![_ ^+ _ ^+ a i]exprAC !rootCK //. -rewrite rmorphD rmorphX 15!(rmorph1, rmorph_int, rmorphM, fmorphV) /=. -rewrite [(10%:~R * _) ^+ _]exprMn ltr_pmul2r ?exprn_gt0 ?divr_gt0 ?ltr0n //. +rewrite rmorphD rmorphXn 15!(rmorph1, rmorph_int, rmorphM, fmorphV) /=. +rewrite [(10%:~R * _) ^+ _]exprMn ltr_pM2r ?exprn_gt0 ?divr_gt0 ?ltr0n //. set x := (n.+1 - a i)%N. set y := (a i - 1)%N. rewrite -root_lt_x ?exprn_ge0 ?addr_ge0 ?divr_ge0 ?ler0n ?subn_gt0 //. @@ -127,11 +127,11 @@ Proof. have lt0n : (0 < n)%N by exact: leq_trans (a_pos k) _. have Hinterm : (C n k.+1)%:~R <= ((n ^ n)%N%:~R / (\prod_(i < k.+1) (n %/ a i) ^ (n %/ a i))%N%:~R) :> algC. - rewrite ler_pdivl_mulr. + rewrite ler_pdivlMr. by move: (l8 n k.+1); rewrite big_mkord mulrC -natrM ler_nat. by rewrite ltr0n prodn_gt0 // => i; rewrite expn_gt0; case: (n %/ a i)%N. rewrite !ratr_int -mulrA; apply: le_lt_trans Hinterm _. -rewrite ltr_pmul2l ?ltr0n ?expn_gt0 ?lt0n //= ltr_pdivl_mulr; last first. +rewrite ltr_pM2l ?ltr0n ?expn_gt0 ?lt0n //= ltr_pdivlMr; last first. apply: prodr_gt0 => i _. by rewrite exp_quo_gt0 ?divr_ge0 ?divr_gt0 ?ltr0n ?a_pos. rewrite prodMz /= mulrC -prodf_div. @@ -196,7 +196,7 @@ Proof. exact/ltW/w_seq_gt0. Qed. Lemma w_seq_le_S k : w_seq k <= w_seq k.+1. Proof. rewrite /w_seq big_ord_recr /=. -by rewrite ler_pmulr 1?ltW ?a'_gt1 // prodr_gt0 // => i _. +by rewrite ler_pMr 1?ltW ?a'_gt1 // prodr_gt0 // => i _. Qed. Lemma w_seq_incr k l : (k <= l)%N -> w_seq k <= w_seq l. @@ -216,7 +216,7 @@ rewrite addnS /w_seq big_ord_recr /=. suff -> : exp_quo (a k)%:Q (2 ^ l.+2 - 2) (2 ^ l.+1 * a k) = exp_quo (a k)%:Q (2 ^ l.+1 - 2) (2 ^ l * a k) * (2 ^ l).-root (a' k). rewrite mulrA. - apply: ler_pmul; rewrite ?a'_bound // ?rootC_ge0 ?CratrE ?a_pos ?ler0n //. + apply: ler_pM; rewrite ?a'_bound // ?rootC_ge0 ?CratrE ?a_pos ?ler0n //. by rewrite prodr_ge0 // => i _ ; exact: a'_ge0. rewrite -prod_root ?CratrE ?expn_gt0 ?a_pos ?ler0n //. have -> : (2 ^ l * a k).-root (a k)%:R = exp_quo (a k)%:R 1 (2 ^ l * a k). @@ -234,7 +234,7 @@ Qed. Lemma w_seq_bound_tail k (Hk : (2 <= k)%N) l : w_seq (k + l) <= w_seq k * a' k ^+ 2. Proof. -apply: le_trans (w_seq_bound Hk l) _; rewrite ler_wpmul2l ?w_seq_ge0 //. +apply: le_trans (w_seq_bound Hk l) _; rewrite ler_wpM2l ?w_seq_ge0 //. have -> : a' k ^+ 2 = exp_quo (a k)%:Q 2 (a k). by rewrite /a' /exp_quo -exprM mul1n. rewrite exp_quo_lessn // ?muln_gt0 ?expn_gt0 ?a_pos // ?ler1n ?a_pos //. @@ -284,7 +284,7 @@ Lemma w_ge0 : 0 <= w. Proof. exact/ltW/w_gt0. Qed. Lemma w_lt3 : w < 3%:Q. Proof. -rewrite w_val ltr_pdivr_mulr ?rat_of_Z_Zpos // -subr_gt0. +rewrite w_val ltr_pdivrMr ?rat_of_Z_Zpos // -subr_gt0. have -> : 3%:Q * rat_of_Z (2 * 10 ^ 15) - rat_of_Z 5949909309448377 = rat_of_Z (3 * 2 * 10 ^ 15 - 5949909309448377). ring. @@ -293,7 +293,7 @@ Qed. Lemma w_gt1 : 1 < w. Proof. -rewrite w_val ltr_pdivl_mulr ?rat_of_Z_Zpos // 1?mul1r -subr_gt0. +rewrite w_val ltr_pdivlMr ?rat_of_Z_Zpos // 1?mul1r -subr_gt0. by rewrite -rmorphB rat_of_Z_Zpos. Qed. @@ -317,26 +317,26 @@ have -> : w_seq 4 = a' 0 * a' 1 * a' 2 * a' 3. by rewrite /w_seq !big_ord_recr /= big_ord0 mul1r. have a'0_ubP : a' 0 <= a'0_ub%:C. have ge0a'0 : 0 <= a'0_ub%:C by rewrite ler0q divr_ge0. - rewrite root_le_x // a0 -rmorphX ler_rat exprMn exprVn. - rewrite lter_pdivl_mulr ?exprn_gt0 // -subr_ge0 mulrzl. - by rewrite -!rmorphX -rmorphMz -rmorphB /= rat_of_ZEdef ler0z. + rewrite root_le_x // a0 -rmorphXn ler_rat exprMn exprVn. + rewrite lter_pdivlMr ?exprn_gt0 // -subr_ge0 mulrzl. + by rewrite -!rmorphXn -rmorphMz -rmorphB /= rat_of_ZEdef ler0z. have a'1_ubP : a' 1 <= a'1_ub%:C. have ge0a'1 : 0 <= a'1_ub%:C by rewrite ler0q divr_ge0. - rewrite root_le_x // a1 -rmorphX ler_rat exprMn exprVn. - rewrite lter_pdivl_mulr ?exprn_gt0 // -subr_ge0 mulrzl. - by rewrite -!rmorphX -rmorphMz -rmorphB /= rat_of_ZEdef ler0z. + rewrite root_le_x // a1 -rmorphXn ler_rat exprMn exprVn. + rewrite lter_pdivlMr ?exprn_gt0 // -subr_ge0 mulrzl. + by rewrite -!rmorphXn -rmorphMz -rmorphB /= rat_of_ZEdef ler0z. have a'2_ubP : a' 2 <= a'2_ub%:C. have ge0a'2 : 0 <= a'2_ub%:C by rewrite ler0q divr_ge0. have ge0a2 : 0 <= (a 2)%:Q%:C by rewrite ler0q. - rewrite root_le_x // a2 -rmorphX ler_rat exprMn exprVn. - rewrite lter_pdivl_mulr ?exprn_gt0 // -subr_ge0 mulrzl. - by rewrite -!rmorphX -rmorphMz -rmorphB /= rat_of_ZEdef ler0z. + rewrite root_le_x // a2 -rmorphXn ler_rat exprMn exprVn. + rewrite lter_pdivlMr ?exprn_gt0 // -subr_ge0 mulrzl. + by rewrite -!rmorphXn -rmorphMz -rmorphB /= rat_of_ZEdef ler0z. have a'3_ubP : a' 3 <= a'3_ub%:C. have ge0a'3 : 0 <= a'3_ub%:C by rewrite ler0q divr_ge0. have ge0a3 : 0 <= (a 3)%:Q%:C by rewrite ler0q. - rewrite root_le_x // a3 -rmorphX ler_rat exprMn exprVn. - rewrite lter_pdivl_mulr; last exact: exprn_gt0. - rewrite -subr_ge0 mulrzl -!rmorphX -rmorphMz -rmorphB /=. + rewrite root_le_x // a3 -rmorphXn ler_rat exprMn exprVn. + rewrite lter_pdivlMr; last exact: exprn_gt0. + rewrite -subr_ge0 mulrzl -!rmorphXn -rmorphMz -rmorphB /=. by rewrite rat_of_ZEdef ler0z. have a'4_ubP : a' 4 <= a'4_ub%:C. have ge0a'1 : 0 <= a'4_ub%:C by rewrite ler0q divr_ge0. @@ -344,16 +344,16 @@ have a'4_ubP : a' 4 <= a'4_ub%:C. rewrite root_le_x //. pose t : rat := (rat_of_Z 200)^-1. have -> : a'4_ub = 1 + t by rewrite /a'4_ub /t; field. - rewrite -rmorphX ler_rat a4 exprDn. + rewrite -rmorphXn ler_rat a4 exprDn. have -> : (1808 = 8 + 1800)%N by []. - rewrite big_split_ord /=; apply: ler_paddr. + rewrite big_split_ord /=; apply: ler_wpDr. apply: sumr_ge0 => i. by rewrite expr1n mul1r mulrn_wge0 ?exprn_ge0 ?invr_ge0. rewrite 8!big_ord_recl big_ord0 !expr1n !mul1r /= /bump !add1n. set lhs := (X in _ <= X). suff -> : lhs = rat_of_Z 34077892883014859211 / rat_of_Z 12800000000000000. have ->: 1807%:~R = rat_of_Z 1807 by rewrite rat_of_ZEdef; congr _%:~R. - by rewrite lter_pdivl_mulr // -subr_ge0 -rmorphM -rmorphB rat_of_Z_ZposW. + by rewrite lter_pdivlMr // -subr_ge0 -rmorphM -rmorphB rat_of_Z_ZposW. rewrite {}/lhs bin0 mulr1n bin1 expr0 expr1. have -> : t ^+ 7 *+ 'C(1807, 7) = t ^+ 7 * rat_of_Z 12337390971384003811. rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=. @@ -380,7 +380,7 @@ have a'4_ubP : a' 4 <= a'4_ub%:C. rewrite -!rat_of_Z_of_nat !Nat2Z.inj_mul. by do !(set x := Z.of_nat _; compute in x; rewrite {}/x); field. by rewrite /t; field. -by rewrite 4!rmorphM rmorphX /=; do 4!rewrite ler_pmul ?mulr_ge0 //. +by rewrite 4!rmorphM rmorphXn /=; do 4!rewrite ler_pM ?mulr_ge0 //. Qed. End Computations. @@ -448,7 +448,7 @@ set t10n_to := exp_quo (10 * n)%N%:Q. have wq_ge0 m : 0 <= w%:C ^+ m by rewrite exprn_ge0 // ler0q. suff step1 : cn < t10n_to (2 * k.+1 - 1)%N 2%N * w%:C ^+ n * w_seq k.+1. apply: lt_le_trans step1 _; rewrite -intrM exprSr mulrA. - by apply/ler_wpmul2l/w_upper_bounded/mulr_ge0/wq_ge0/exp_quo_ge0/ler0n. + by apply/ler_wpM2l/w_upper_bounded/mulr_ge0/wq_ge0/exp_quo_ge0/ler0n. rewrite -mulrA; set tw := (X in _ < _ * X). have tw_pos : 0 <= tw by apply: mulr_ge0. have tenn_to_pos : 0 <= ((10 * n)%N%:Q ^+ k)%:C. @@ -457,7 +457,7 @@ suff step2 : cn < ((10 * n)%N%:Q ^+ k)%:C * t10n_to 1%N (a k.+1).-1 * tw. apply: lt_le_trans step2 _; rewrite exp_quo_r_nat. have ->: t10n_to (2 * k.+1 - 1)%N 2%N = t10n_to k 1%N * t10n_to 1%N 2%N. rewrite -exp_quo_plus ?ler0n //; apply: exp_quo_equiv; ring_lia. - apply/ler_wpmul2r/ler_wpmul2l/exp_quo_lessn => //; last by rewrite !mul1n. + apply/ler_wpM2r/ler_wpM2l/exp_quo_lessn => //; last by rewrite !mul1n. by rewrite exp_quo_ge0 // ler0n. have ->: tw = w%:C ^+ n * n%:Q%:C * (w_seq k.+1 / n%:Q%:C). by rewrite mulrACA divff ?lt0r_neq0 // mulr1. @@ -466,7 +466,7 @@ have Helper1 : 0 < \prod_(i < k.+1) a' i by rewrite prodr_gt0. have step3 : w_seq k.+1 / n%:Q%:C >= (\prod_(i < k.+1) exp_quo (a i)%:Q (a i).-1 (a i))^-1. rewrite remark_t2_2 /w_seq invfM // invrK mulrC. - rewrite ler_pdivr_mulr // -mulrA ler_pmulr // mulrC ler_pdivl_mulr // mul1r. + rewrite ler_pdivrMr // -mulrA ler_pMr // mulrC ler_pdivlMr // mul1r. case/andP: Hank => _; rewrite a_rec addn1 ltnS big_mkord => H. by rewrite -prodMz 2!CratrE ler_nat. have ler0_10npow : 0 <= ((10 * n)%N%:Q ^+ k)%:C * t10n_to 1%N (a k.+1).-1. @@ -487,11 +487,11 @@ suff step4 : cn < ((10 * n)%N%:Q ^+ k)%:C * t10n_to 1%N (a k.+1).-1 * ((w_seq k.+1) ^+ n * ((n ^ n)%N%:Q%:C / exp_quo n%:Q (n * (a k.+1).-2)%N ((a k.+1).-1)) / (\prod_(i < k.+1) exp_quo (a i)%:Q (a i).-1 (a i))). - apply: lt_le_trans step4 _; apply/ler_wpmul2l/ler_pmul/step3/ler_pmul => //. + apply: lt_le_trans step4 _; apply/ler_wpM2l/ler_pM/step3/ler_pM => //. - by rewrite invr_ge0. - by rewrite divr_ge0 // ltW. - - by apply/ler_expn2r/w_upper_bounded; rewrite nnegrE // ler0q. - - by rewrite ler_pdivr_mulr //; exact: remark_t2_1. + - by apply/lerXn2r/w_upper_bounded; rewrite nnegrE // ler0q. + - by rewrite ler_pdivrMr //; exact: remark_t2_1. congr (_ < _): (l10 (proj1 (andP Hank))). have -> : forall k1, exp_quo n%:Q (n * (a k1.+1).-2) (a k1.+1).-1 = \prod_(i < k1.+1) exp_quo n%:Q n (a i). @@ -500,7 +500,7 @@ have -> : forall k1, exp_quo n%:Q (n * (a k1.+1).-2) (a k1.+1).-1 - by rewrite muln_gt0 /= muln_gt0; apply/andP. - by rewrite muln_gt0 andbT muln_gt0; apply/andP. lia. -rewrite /w_seq /t10n_to rmorphX -subn1 -prod_is_exp_sum. +rewrite /w_seq /t10n_to rmorphXn -subn1 -prod_is_exp_sum. rewrite -3!mulrA ![_ * (_%:C * _)]mulrCA; congr (_ * _). rewrite -prodrXl -!prodfV -!big_split /=; apply: eq_bigr => i _. rewrite -exprM mul1n [_^-1 / _ in RHS]mulrC [RHS]mulrA [RHS]mulrACA. @@ -513,8 +513,8 @@ Theorem t2_rat n k (Hank : (a k <= n < (a k.+1))%N) : (C n k.+1)%:Q < (10%:Q * n%:Q) ^ k.+1 * (w ^+ n.+1). Proof. suff : (C n k.+1)%:Q%:C < exp_quo (10%:Q * n%:Q) (2 * k.+1) 2 * w%:C ^+ n.+1. - by rewrite /exp_quo exprM sqrtCK -!rmorphX /= -rmorphM /= ltr_rat. -apply: lt_le_trans (t2 Hank) _; apply: ler_wpmul2r. + by rewrite /exp_quo exprM sqrtCK -!rmorphXn /= -rmorphM /= ltr_rat. +apply: lt_le_trans (t2 Hank) _; apply: ler_wpM2r. by rewrite exprn_ge0 ?ler0q. case: n {Hank} => [| n]; first by rewrite mulr0 !exp_quo_0 /= mulnC muln2. by apply: exp_quo_lessn=> //; [ring_lia | lia]. @@ -542,7 +542,7 @@ suff [K [Kpos KP]] : exists K : rat, case=> // k _ /andP [_ leKSn]; exists k.+1; split=> // n m {}/KP KP. suff: (C n m.+1)%:R <= (k%:Q + 1) * 3%:R ^ n. by rewrite -[_ + 1%:R]natrD -[_ ^ n]natrX -natrM ler_nat addn1. - exact/le_trans/ler_wpmul2r/ltW/leKSn/exprz_ge0. + exact/le_trans/ler_wpM2r/ltW/leKSn/exprz_ge0. move mE: 10%:Q => m. have lt0m : 0 < m by rewrite -mE. have le0m : 0 <= m by exact: ltW. @@ -550,14 +550,14 @@ have lt1m : 1 < m by rewrite -mE. have le1m : 1 <= m by exact: ltW. move epsE: (w / 3%:R) => eps. have lt0eps1 : 0 < eps < 1. - by rewrite -epsE ltr_pdivl_mulr // mul0r ltr_pdivr_mulr // mul1r w_lt3 w_gt0. + by rewrite -epsE ltr_pdivlMr // mul0r ltr_pdivrMr // mul1r w_lt3 w_gt0. pose u n k eps : rat := (m * n%:R) ^ k.+1 * eps ^ n.+1. suff hloglog : exists (K : rat), (0 < K) /\ (forall n k, cond n k -> u n k eps < K). have [K [lt0K KP]] := hloglog. exists (K * 3%:Q); split; first exact: mulr_gt0. move=> n k hcond. apply: le_trans (ltW (t2_rat hcond)) _; rewrite -mulrA -exprSz. - rewrite -ler_pdivr_mulr; last exact: exprz_gt0. + rewrite -ler_pdivrMr; last exact: exprz_gt0. by rewrite -mulrA -expr_div_n mE epsE; apply/ltW/KP. have [lt0eps lteps1] := andP lt0eps1. pose loglog n := trunc_log 2 (trunc_log 2 n). @@ -566,7 +566,7 @@ have le0v n : 0 <= v n. by rewrite /v pmulr_lge0 ?exprz_gt0 // exprz_ge0 // mulr_ge0 // ler0n. suff {u} [K [Kpos KP]] : exists K : rat, 0 < K /\ forall n, v n < K. exists K; split => // n k /better_k_bound hkn; apply: le_lt_trans (KP n). - rewrite /u /v ler_pmul2r; last exact: exprz_gt0. + rewrite /u /v ler_pM2r; last exact: exprz_gt0. case: n hkn => [| n] hkn; first by rewrite mulr0 !exp0rz. apply: exp_incr_expp; first by apply: mulr_ege1=> //; rewrite ler1n. by rewrite ltnS -addn2. @@ -585,35 +585,35 @@ pose t n := (m * (y n)%:R) ^ (loglog n).+3 * eps ^ (x n).+1. have le0y n : 0 <= (y n)%:R :> rat by rewrite ler0n. suff {v le0v} [K [Kpos KP]] : exists K : rat, 0 < K /\ forall n, t n < K. pose KK := K + v 0%N + v 1%N. - have ltKKK : K <= KK by rewrite /KK -addrA ler_addl addr_ge0. + have ltKKK : K <= KK by rewrite /KK -addrA lerDl addr_ge0. have ltvKK n : (n <= 1)%N -> v n < KK. rewrite leq_eqVlt ltnS leqn0 /KK => /orP [] /eqP ->. - - by rewrite cpr_add ltr_spaddl. - - by rewrite addrAC cpr_add ltr_spaddl. + - by rewrite cprD ltr_pwDl. + - by rewrite addrAC cprD ltr_pwDl. exists KK; split => [|n]; first exact: lt_le_trans ltKKK. have [le1n | lt1n] := leqP n 1; first exact: ltvKK. apply/lt_le_trans/ltKKK/le_lt_trans/(KP n); rewrite /v /t. (* use case for posreal-style automation... *) - apply/ler_pmul/exp_incr_expn => //. + apply/ler_pM/exp_incr_expn => //. - exact/exprz_ge0/mulr_ge0/ler0n. - exact/exprz_ge0/ltW. - - apply: ler_expn2r; last first. - + by apply: ler_wpmul2l; rewrite // ler_nat ltnW // h1. + - apply: lerXn2r; last first. + + by apply: ler_wpM2l; rewrite // ler_nat ltnW // h1. + by rewrite rpredM // rpred_nat. + by rewrite rpredM // rpred_nat. - by rewrite ltnS h2. pose u n := (m * (x n)%:R) ^+ (2 * (loglog n).+3) * eps ^ x n. suff {t y le0y} [K [Kpos KP]] : exists K : rat, 0 < K /\ forall n, u n < K. exists K; split => // n. apply: le_lt_trans (KP n); rewrite {KP} /u /t. - apply: ler_pmul. + apply: ler_pM. - by apply: exprz_ge0; rewrite pmulr_rge0 // ler0n. - by apply: exprz_ge0; apply: ltW. - - rewrite exprnP PoszM -exprz_exp; apply: ler_expn2r. + - rewrite exprnP PoszM -exprz_exp; apply: lerXn2r. + by apply: rpredM => //; apply: rpred_nat. + by apply: rpredX; apply: rpredM => //; apply: rpred_nat. - - rewrite expfzMl; apply: ler_pmul=> //; first by apply: ler_eexpr. + - rewrite expfzMl; apply: ler_pM=> //; first by apply: ler_eXnr. by rewrite -exprnP -natrX ler_nat /x /y expnS mulnC expnM. - - rewrite -exprnP exprSr; apply: ler_pimulr; last by apply: ltW. + - rewrite -exprnP exprSr; apply: ler_piMr; last by apply: ltW. apply: exprn_ge0; exact: ltW. have {}h2 n : (1 < n)%N -> (x n <= n)%N by apply: h2. pose alpha n := (2 ^ 2 ^ n)%N. @@ -630,16 +630,16 @@ have alphaS n : (alpha n.+1 = alpha n ^ 2)%N. by rewrite /alpha expnS mulnC expnM. have le_0_alpham2 k : 0 <= (alpha k)%:Z - 2%:Z. rewrite /alpha; apply: (@le_trans _ _ ((2 ^ 2 ^ 0)%:Z - 2%:Z)) => //. - by apply: ler_sub=> //; rewrite lez_nat leq_exp2l // leq_exp2l. + by apply: lerB=> //; rewrite lez_nat leq_exp2l // leq_exp2l. have maj_t n : t n.+1 <= t n ^ 2 * l n. rewrite /t 2!expfzMl !exprz_exp expfzMl -2!mulrA -[_ * _ * l n]mulrA. - apply: ler_pmul; first exact: exprz_ge0. (* missing posreal... *) + apply: ler_pM; first exact: exprz_ge0. (* missing posreal... *) - apply: mulr_ge0; apply: exprz_ge0 => //; exact: ltW. - - rewrite ler_weexpn2l //; lia. + - rewrite ler_weXn2l //; lia. rewrite /l mulrCA 2!mulrA -exprzD_nat -mulrA -expfzDr; last exact: lt0r_neq0. - apply: ler_pmul; first exact: exprz_ge0. (* missing posreal... *) + apply: ler_pM; first exact: exprz_ge0. (* missing posreal... *) - apply: exprz_ge0; exact: ltW. - - rewrite alphaS natrX exprnP exprz_exp ler_weexpn2l //; last lia. + - rewrite alphaS natrX exprnP exprz_exp ler_weXn2l //; last lia. by rewrite ler1n expn_gt0. - by rewrite addrCA mulrC addrN addr0 alphaS. have le_0_l n : 0 <= l n. @@ -659,8 +659,8 @@ have lt_l3_1 : l 3%N <= 1. by congr (_ ^ _ * eps ^ _). rewrite expr_le1 //; last exact/mulr_ge0/exprz_ge0/ltW. suff: 2%:R * eps ^ 90 <= 1. - by apply: le_trans; rewrite ler_pmul2l ?ler_piexpz2l. - rewrite epsF expfzMl -expfV mulrA ler_pdivr_mulr; last exact: exprz_gt0. + by apply: le_trans; rewrite ler_pM2l ?ler_piXz2l. + rewrite epsF expfzMl -expfV mulrA ler_pdivrMr; last exact: exprz_gt0. rewrite mul1r -subr_ge0 -!rat_of_Z_pow mulr_natl -rmorphMn -rmorphB. vm_compute; exact: rat_of_Z_ZposW. rewrite [l]lock in lt_l3_1. @@ -673,24 +673,23 @@ have lt_t4_1 : t 4%N < 1. have {hm} : (m * a4%:R) ^14 * eps ^ (M * 14)%N < 1. rewrite PoszM -exprz_exp -expfzMl; apply: exprn_ilt1=> //. rewrite -mulrA pmulr_rge0 // pmulr_rge0 ?ltr0n //; apply: exprz_ge0; exact: ltW. - apply: le_lt_trans. rewrite ler_pmul2l; first by rewrite ler_piexpz2l. + apply: le_lt_trans. rewrite ler_pM2l; first by rewrite ler_piXz2l. by apply: exprz_gt0; rewrite pmulr_rgt0 // ltr0n. pose e := rat_of_Z 992 / rat_of_Z (10 ^ 3). have ltepse : eps < e. - rewrite epsF ltr_pdivr_mulr // /e mulrAC ltr_pdivl_mulr; last exact: rat_of_Z_Zpos. + rewrite epsF ltr_pdivrMr // /e mulrAC ltr_pdivlMr; last exact: rat_of_Z_Zpos. have -> : eps2 = rat_of_Z (6 * 10 ^ 12) * rat_of_Z (10 ^ 3). by rewrite /eps2; ring. - rewrite mulrA ltr_pmul2r ?rat_of_Z_Zpos //. - rewrite -subr_gt0 /eps1 -rmorphM -rmorphB. + rewrite mulrA ltr_pM2r ?rat_of_Z_Zpos // -subr_gt0 /eps1 -rmorphM -rmorphB. exact: rat_of_Z_Zpos. (* long *) suff [M le14M]: exists2 M, (M * 14 <= alpha 4)%N & (m * a4%:R) * (e ^ M) < 1. - move=> hm; exists M => //; apply: le_lt_trans hm. rewrite ler_pmul2l; last first. + move=> hm; exists M => //; apply: le_lt_trans hm. rewrite ler_pM2l; last first. by rewrite pmulr_rgt0 // ltr0n. - by apply: ler_expn2r; apply: ltW; rewrite // divr_gt0 // rat_of_Z_Zpos. + by apply: lerXn2r; apply: ltW; rewrite // divr_gt0 // rat_of_Z_Zpos. suff [M le14M hm]: exists2 M, (M * 14 <= alpha 4)%N & 0 < rat_of_Z (10 ^ 3) ^ M - (m * a4%:R) * rat_of_Z 992 ^ M. exists M => //. - rewrite /e expfzMl -expfV mulrA ltr_pdivr_mulr; last by rewrite exprz_gt0 // rat_of_Z_Zpos. + rewrite /e expfzMl -expfV mulrA ltr_pdivrMr; last by rewrite exprz_gt0 // rat_of_Z_Zpos. by rewrite mul1r -subr_gt0. exists 2000%N; first by rewrite /alpha -subn_eq0. (* FIXME : compute in Z. *) rewrite -mE -!rat_of_Z_pow. @@ -702,11 +701,11 @@ have lt_ln_1 (n : nat) : (3 <= n)%N -> l n <= 1. elim: n => [// | n ihn]. rewrite leq_eqVlt => /predU1P [<- | {}/ihn ihn]; first by rewrite [l]lock. (* unlock does not work... *) suff h : l n.+1 <= (l n) ^ 2 by apply: le_trans h _; apply: mulr_ile1. - rewrite /l expfzMl exprz_exp; apply: ler_pmul. + rewrite /l expfzMl exprz_exp; apply: ler_pM. - exact/exprz_ge0/ler0n. - exact/exprz_ge0/ltW. - by rewrite alphaS natrX exprnP exprz_exp. - rewrite exprz_exp ler_piexpz2l //. + rewrite exprz_exp ler_piXz2l //. - rewrite alphaS -subr_ge0; set a := alpha _; set x := (X in 0 <= X). have {x} -> : x = a%:Z ^+ 2 ^+ 2 - (2%:Z * a%:Z) ^+ 2 + 4%:Z * a%:Z. by rewrite /x; ring. @@ -718,11 +717,11 @@ suff [K [lt0K [N Pn]]] : exists K : rat, 0 < K /\ exists N : nat, (forall n, (N (* a bigenough would be nice here *) pose KK := (K + \sum_(0 <= j < N.+1) t j). have le0sum : 0 <= \sum_(0 <= j < N.+1) t j by apply: sumr_ge0=> n _; exact: ltW. - have lt0KK : 0 < KK by rewrite /KK; apply: ltr_spaddl. - have ltKK : K <= KK by rewrite /KK ler_addl. + have lt0KK : 0 < KK by rewrite /KK; apply: ltr_pwDl. + have ltKK : K <= KK by rewrite /KK lerDl. have KKmaj j : (j <= N)%N -> t j < KK. move=> lej4; rewrite /KK (bigD1_seq j) //=; last by rewrite mem_iota iota_uniq. - - rewrite addrA addrAC cpr_add; apply: ltr_spaddl=> //; apply: sumr_ge0=> n _; exact: ltW. + - rewrite addrA addrAC cprD; apply: ltr_pwDl=> //; apply: sumr_ge0=> n _; exact: ltW. by rewrite mem_index_iota. exists KK; split => //; elim=> [| n ihn]; first exact: KKmaj. case: (ltnP n.+1 N.+1) => [lenN | ltNn]; first exact: KKmaj. @@ -732,7 +731,7 @@ rewrite leq_eqVlt => /predU1P [<- | lt3n]; first by rewrite [t]lock. have {}ihn := ihn lt3n. apply: le_lt_trans (maj_t _) _; apply: (@le_lt_trans _ _ (t n ^ 2)); last first. by apply: mulr_ilt1. -rewrite ger_pmulr; first by apply: lt_ln_1; rewrite ltnS in lt3n; apply: ltn_trans lt3n. +rewrite ger_pMr; first by apply: lt_ln_1; rewrite ltnS in lt3n; apply: ltn_trans lt3n. exact: exprz_gt0. Qed. diff --git a/theories/hanson_elem_analysis.v b/theories/hanson_elem_analysis.v index 7a10733..704b14c 100644 --- a/theories/hanson_elem_analysis.v +++ b/theories/hanson_elem_analysis.v @@ -55,7 +55,7 @@ Lemma exp_quo_less r1 r2 p q : exp_quo r1 p q <= exp_quo r2 p q. Proof. move => Hq H1 H2 Hleq. -by rewrite exp_quo_lessE // ler_expn2r ?ler_rat // nnegrE ler0q. +by rewrite exp_quo_lessE // lerXn2r ?ler_rat // nnegrE ler0q. Qed. Lemma exp_quo_lessn r1 (p1 q1 p2 q2 : nat) : @@ -124,10 +124,10 @@ move => Hq1 Hq2 Hr1 Hr2 Hr1gt0 Hle1r2 Hle12. have Hr1pos : 0 <= r1 by apply: ltW. have Hr2pos : 0 <= r2 by rewrite Hr2 divr_ge0 // ?ler0z. have: r1%:C ^+ (p1 * q2) <= r2%:C ^+ (p1 * q2). - by rewrite ler_expn2r ?ler_rat // nnegrE ler0q. + by rewrite lerXn2r ?ler_rat // nnegrE ler0q. rewrite exp_quo_lessE // => /le_trans -> //; rewrite exp_incr_expp ?ler1q //. -move: Hle12; rewrite Hr1 Hr2 ler_pdivr_mulr ?ltr0n //. -by rewrite mulrAC ler_pdivl_mulr ?ltr0n // -!natrM ler_nat. +move: Hle12; rewrite Hr1 Hr2 ler_pdivrMr ?ltr0n //. +by rewrite mulrAC ler_pdivlMr ?ltr0n // -!natrM ler_nat. Qed. End RationalPower. @@ -141,8 +141,8 @@ Section FourFacts. (* A lemma comparing factorial to a geometric sequence *) Lemma fact_greater_geom i : i.+1`!%:R >= (3%:Q / 2%:Q) ^+ i. Proof. -elim: i => // i IHi; rewrite exprS factS natrM; apply: ler_pmul IHi => //. -by rewrite ler_pdivr_mulr ?ltr0n // mulr_natr -mulrnA ler_nat. +elim: i => // i IHi; rewrite exprS factS natrM; apply: ler_pM IHi => //. +by rewrite ler_pdivrMr ?ltr0n // mulr_natr -mulrnA ler_nat. Qed. (* Formula for a geometric sum in a field *) @@ -161,18 +161,18 @@ Proof. case: n => // n. have step: (1 + n.+1%:Q^-1) ^+ n.+1 <= \sum_(i < n.+2) i`!%:Q^-1. rewrite exprDn; apply: ler_sum => i _; rewrite expr1n mul1r -mulr_natr exprVn. - rewrite ler_pdivr_mull ?ler_pdivl_mulr ?ltr0n ?expn_gt0 ?fact_gt0 //. + rewrite ler_pdivrMl ?ler_pdivlMr ?ltr0n ?expn_gt0 ?fact_gt0 //. by rewrite -natrM bin_ffact -natrX ler_nat ffact_le_expn. have {step}: (1 + n.+1%:Q^-1) ^+ n.+2 <= 2%:Q * \sum_(i < n.+2) i`!%:Q^-1. - rewrite exprS; apply: ler_pmul => //. - by rewrite -[2%:Q]/(1 + 1) ler_add2l invf_le1 // ler1z. -move/le_trans; apply; rewrite -[8%:Q]/(2%:Q * 4%:Q) ler_pmul2l //. + rewrite exprS; apply: ler_pM => //. + by rewrite -[2%:Q]/(1 + 1) lerD2l invf_le1 // ler1z. +move/le_trans; apply; rewrite -[8%:Q]/(2%:Q * 4%:Q) ler_pM2l //. have: 1 + \sum_(i < n.+1) (2%:Q / 3%:Q) ^+ i <= 4%:Q. - rewrite geometric_sum // -[4%:Q]/(1 + 3%:Q) ler_add2l. + rewrite geometric_sum // -[4%:Q]/(1 + 3%:Q) lerD2l. have -> : 1 - 2%:Q / 3%:Q = 3%:Q^-1 by []. - by rewrite invrK ler_pimull // ler_subl_addr ler_addl. -apply: le_trans; rewrite big_ord_recl ler_add2l; apply: ler_sum => i _ /=. -by rewrite -invf_div exprVn lef_pinv ?posrE ?ltr0n ?fact_gt0 ?fact_greater_geom. + by rewrite invrK ler_piMl // lerBlDr lerDl. +apply: le_trans; rewrite big_ord_recl lerD2l; apply: ler_sum => i _ /=. +by rewrite -invf_div exprVn lef_pV2 ?posrE ?ltr0n ?fact_gt0 ?fact_greater_geom. Qed. (* TODO : clean up, use more ^-1 *) @@ -191,11 +191,11 @@ suff: exp_quo (1 + q%:~R / p%:~R) p q <= exp_quo (1 + f%:Q^-1) f.+1 1. by move=> /le_trans -> //; rewrite -exp_quo_r_nat ler_rat one_plus_invn_expn. rewrite exp_quo_lessE ?addr_ge0 ?mulr_ge0 ?invr_ge0 ?ler0n // muln1. have: (1 + f%:~R^-1)%:C ^+ p <= (1 + f%:~R^-1)%:C ^+ (f.+1 * q). - by rewrite exp_incr_expp ?ler1q ?ler_addl ?invr_ge0 ?ler0n 1?ltnW ?ltn_ceil. + by rewrite exp_incr_expp ?ler1q ?lerDl ?invr_ge0 ?ler0n 1?ltnW ?ltn_ceil. apply: le_trans. -rewrite ler_expn2r ?nnegrE ?ler0q ?addr_ge0 ?mulr_ge0 ?invr_ge0 ?ler0n //. -rewrite ler_rat ler_add2l ler_pdivr_mulr ?ltr0n // mulrC. -rewrite ler_pdivl_mulr ?ltr0n ?divn_gt0 //. +rewrite lerXn2r ?nnegrE ?ler0q ?addr_ge0 ?mulr_ge0 ?invr_ge0 ?ler0n //. +rewrite ler_rat lerD2l ler_pdivrMr ?ltr0n // mulrC. +rewrite ler_pdivlMr ?ltr0n ?divn_gt0 //. by rewrite -intrM ler_nat mulnC leq_trunc_div. (* Second part : p < q *) @@ -205,20 +205,20 @@ have Helper0 : (0 < f)%N. have Helper1 : 0 <= 1 + q%:Q / p%:Q. by rewrite addr_ge0 ?divr_ge0 ?ler0n. have Helper2 : 1 + q%:Q / p%:Q <= 1 + (1 + f%:~R). - rewrite ler_add2l -mulrS ler_pdivr_mulr ?ltr0n // -natrM ler_nat. + rewrite lerD2l -mulrS ler_pdivrMr ?ltr0n // -natrM ler_nat. by rewrite ltnW ?ltn_ceil. have Helper3 : (p * f <= q)%N. by rewrite mulnC leq_trunc_div. apply: (@le_trans _ _ (exp_quo (1 + (1 + f%:Q)) p q)). by apply: exp_quo_less; rewrite // !addr_ge0 ?ler0n. apply: (@le_trans _ _ (exp_quo (1 + (1 + f%:Q)) 1 f)). - by apply: exp_quo_lessn; rewrite //= ?ler_addl ?addr_ge0 ?ler0n // mul1n. + by apply: exp_quo_lessn; rewrite //= ?lerDl ?addr_ge0 ?ler0n // mul1n. apply: (@le_trans _ _ (exp_quo ((3 ^ f.+1)%N%:Q) 1 f)). rewrite exp_quo_less // ?addr_ge0 ?ler0n //. by rewrite -rat1 -!natrD ler_nat !add1n replace_exponential. rewrite /exp_quo expr1 !CratrE expnS natrM rootCMr ?ler0n //. have -> : 9%:R = 3%:R * 3%:R :> algC by rewrite -natrM. -by rewrite ler_pmul ?root_le_x ?rootC_ge0 ?ler0n ?natrX // ler_eexpr ?ler1n. +by rewrite ler_pM ?root_le_x ?rootC_ge0 ?ler0n ?natrX // ler_eXnr ?ler1n. Qed. End FourFacts. diff --git a/theories/hanson_elem_arith.v b/theories/hanson_elem_arith.v index e761bb1..97b6fd6 100644 --- a/theories/hanson_elem_arith.v +++ b/theories/hanson_elem_arith.v @@ -207,7 +207,7 @@ Qed. Corollary lt_sum_aV_1 (n : nat) : \sum_(0 <= i < n.+1) (a i)%:Q ^-1 < 1. -Proof. by rewrite sum_aV ltr_pdivr_mulr // mul1r ltr_add2l. Qed. +Proof. by rewrite sum_aV ltr_pdivrMr // mul1r ltrD2l. Qed. (* NOT USED? *) @@ -234,8 +234,8 @@ suff : ((\sum_(0 <= j < i.+1) n.+1 %/ a j)%N%:Q < n.+1%:Q)%R. by rewrite -ltz_nat ltr_int. suff hdiv : (\sum_(0 <= i0 < i.+1) (n.+1%:Q / (a i0)%:Q) < n.+1%:Q)%R. apply: le_lt_trans hdiv; rewrite sumMz; apply: ler_sum => j _. - rewrite ler_pdivl_mulr // -intrM ler_int; exact: leq_trunc_div. -rewrite -mulr_sumr gtr_pmulr; last exact: ltr0z. + rewrite ler_pdivlMr // -intrM ler_int; exact: leq_trunc_div. +rewrite -mulr_sumr gtr_pMr; last exact: ltr0z. exact: lt_sum_aV_1. Qed. diff --git a/theories/harmonic_numbers.v b/theories/harmonic_numbers.v index 1c75101..a0537a9 100644 --- a/theories/harmonic_numbers.v +++ b/theories/harmonic_numbers.v @@ -15,12 +15,11 @@ Lemma ghn_Sn_inhom m n : n >= 0 -> ghn m (int.shift 1 n) = ghn m n + ((n%:Q + 1)^m)^-1. Proof. move=> pn. -rewrite /ghn int.shift2Z big_int_recr /= ?rmorphD //=. -by rewrite -ler_subl_addr. +by rewrite /ghn int.shift2Z big_int_recr /= ?rmorphD //= -lerBlDr. Qed. Lemma ghn_small (m : nat) (n : int) : n <= 0 -> ghn m n = 0. -Proof. by move=> hn; rewrite /ghn big_geqz // ger_addr. Qed. +Proof. by move=> hn; rewrite /ghn big_geqz // gerDr. Qed. Lemma ghn1 (m : nat) : ghn m 1 = 1. Proof. by rewrite /ghn big_int_recr //= big_nil add0r exp1rz. Qed. diff --git a/theories/multinomial.v b/theories/multinomial.v index efe61bf..d8bab11 100644 --- a/theories/multinomial.v +++ b/theories/multinomial.v @@ -226,7 +226,7 @@ Proof. by rewrite tnth_mktuple /aux /= (tnth_nth 0) in_tupleE. suff {P} -> : (('C[l])%:R * p%:R = ('C[tmap_val tl])%:R * monomial [seq i%:R | i <- l] (tmap_val tl) :> int)%R. - rewrite cpr_add; apply: sumr_ge0 => i _; apply: mulr_ge0. + rewrite cprD; apply: sumr_ge0 => i _; apply: mulr_ge0. - by rewrite ler0n. - rewrite /monomial big_seq_cond. apply: prodr_ge0 => j; rewrite andbT => /nth_index hj. diff --git a/theories/ops_for_s.v b/theories/ops_for_s.v index ae59a80..40d1531 100644 --- a/theories/ops_for_s.v +++ b/theories/ops_for_s.v @@ -110,7 +110,7 @@ Theorem recD1 (n k : int) : 0 <= k -> k < n -> P1_horner s n k = 0. Proof. move=> ? ?. rewrite /P1_horner /d.P1_horner. -rewrite (punk.biv_sound_telescoping P1_eq_Delta_Q1); last by rewrite ler_addr. +rewrite (punk.biv_sound_telescoping P1_eq_Delta_Q1); last by rewrite lerDr. set telQ := (X in X + _ + _). set onD := (X in _ + X + _). set remP := (X in _ + _ + X). @@ -152,7 +152,7 @@ Theorem recD2 (n k : int) : 0 < k -> k < n -> P2_horner s n k = 0. Proof. move=> ? ?. rewrite /P2_horner /d.P2_horner. -rewrite (punk.biv_sound_telescoping P2_eq_Delta_Q2); last by rewrite ler_paddr. +rewrite (punk.biv_sound_telescoping P2_eq_Delta_Q2); last by rewrite ler_wpDr. set telQ := (X in X + _ + _). set onD := (X in _ + X + _). set remP := (X in _ + _ + X). @@ -192,8 +192,7 @@ Theorem recD3 (n k : int) : 0 <= k -> k < n -> P3_horner s n k = 0. Proof. move=> ? ?. rewrite /P3_horner /d.P3_horner. -rewrite (punk.biv_sound_telescoping P3_eq_Delta_Q3); - last by rewrite ler_addr. +rewrite (punk.biv_sound_telescoping P3_eq_Delta_Q3); last by rewrite lerDr. set telQ := (X in X + _ + _). set onD := (X in _ + X + _). set remP := (X in _ + _ + X). @@ -235,8 +234,7 @@ Theorem recD4 (n k : int) : 0 <= k -> k + 1 < n -> P4_horner s n k = 0. Proof. move=> ? ?. rewrite /P4_horner /d.P4_horner. -rewrite (punk.biv_sound_telescoping P4_eq_Delta_Q4); - last by rewrite ler_addr. +rewrite (punk.biv_sound_telescoping P4_eq_Delta_Q4); last by rewrite lerDr. set telQ := (X in X + _ + _). set onD := (X in _ + X + _). set remP := (X in _ + _ + X). diff --git a/theories/punk.v b/theories/punk.v index 145ce59..a1080bf 100644 --- a/theories/punk.v +++ b/theories/punk.v @@ -92,8 +92,8 @@ have {}step : P U n = t1 - t2. rewrite [LHS]big_seq_cond [RHS]big_seq_cond; apply: eq_bigr=> i; simpl in i. rewrite andbT mem_index_iota; case/andP=> _ hi. rewrite -big_cat_int //= !int.shift2Z. - - by apply: le_trans range_correct _; rewrite ler_add2r ler_addl. - - by rewrite ler_add2r ler_add2l ltW. + - by apply: le_trans range_correct _; rewrite lerD2r lerDl. + - by rewrite lerD2r lerD2l ltW. have t1_step : t1 = \sum_(a <= k < int.shift r n + b :> int) @@ -131,7 +131,7 @@ have {}t1_step : \sum_(n + b <= k < int.shift r n + b :> int) \sum_(0 <= i < r) cf_P i n * u (int.shift i n) k. - by rewrite t1_step /t11 -big_cat_int // ler_add2r int.shift2Z cpr_add. + by rewrite t1_step /t11 -big_cat_int // lerD2r int.shift2Z cprD. rewrite {}step {}t1_step {}t11_step. rewrite -1![RHS]addrA -3![LHS]addrA; congr (_ + _). rewrite -sumrN [LHS]addrA -big_split /=; congr (_ + _). @@ -141,8 +141,8 @@ rewrite -sumrN [LHS]addrA -big_split /=; congr (_ + _). rewrite exchange_big /= -sumrN -big_split /=. rewrite [LHS]big_seq_cond [RHS]big_seq_cond; apply: eq_bigr=> i /andP []. rewrite mem_index_iota; case/andP=> _ hi _; rewrite !int.shift2Z. -have hl : n + b <= n + i + b by rewrite ler_add2r ler_addl. -have hr : n + i + b <= n + r + b by rewrite ler_add2r ler_add2l ltW. +have hl : n + b <= n + i + b by rewrite lerD2r lerDl. +have hr : n + i + b <= n + r + b by rewrite lerD2r lerD2l ltW. rewrite (big_cat_int _ _ _ hl hr) {hl hr} addrK [n + i + b]addrAC big_addz2l /=. rewrite eq_big_int_nat /=; apply: eq_bigr=> ? _. by rewrite int.shift2Z [n + b + _]addrC. @@ -272,7 +272,7 @@ have PUnk_value : apply: eq_bigr => i. rewrite andbT -/s. move/andP=> [_ i_bound]. apply: eq_bigr => j _. congr (_ * _). - rewrite -big_cat_int ?cpr_add //=. + rewrite -big_cat_int ?cprD //=. by rewrite !int.shift2Z addrAC. have {}PUnk_value : diff --git a/theories/rat_of_Z.v b/theories/rat_of_Z.v index 48b4fb4..1999791 100644 --- a/theories/rat_of_Z.v +++ b/theories/rat_of_Z.v @@ -78,7 +78,7 @@ Proof. by apply/eqP; ring_lia. Qed. Lemma rat_of_Z_pow z n : rat_of_Z (z ^ Z.of_nat n) = rat_of_Z z ^ n. Proof. -rewrite /exprz -rmorphX -Zpower_nat_Z; congr rat_of_Z. +rewrite /exprz -rmorphXn -Zpower_nat_Z; congr rat_of_Z. by elim: n => //= n ->; rewrite exprS. Qed. #[export] Hint Resolve rat_of_Z_ZposW : core. diff --git a/theories/reduce_order.v b/theories/reduce_order.v index ae28776..df25c47 100644 --- a/theories/reduce_order.v +++ b/theories/reduce_order.v @@ -166,7 +166,7 @@ move=> kpos ebk0 ebk1 ebk2 ebk3 /= n. pose p : int := n - k; simpl in p. have -> : n = p + k by rewrite /p addrNK. clearbody p; clear n. -rewrite ler_addr. +rewrite lerDr. suff gen (n : int) : 0 <= n -> n <= p -> b' (n + k) = b (n + k). by move=> p_pos; apply: (gen _ p_pos). move: n. @@ -254,7 +254,7 @@ case: (altP (n =P 1)) => [-> | h1]; first exact: b_Sn2_at_1. pose p : int := n - (2 : int); simpl in p. have hnp : n = p + (2 : int) by rewrite /p addrNK. have {hn h0 h1} le0p : 0 <= p by lia. -have {le0p hnp p} h : (2 : int) <= n by rewrite hnp ler_addr. +have {le0p hnp p} h : (2 : int) <= n by rewrite hnp lerDr. exact: b_Sn2_almost. Qed. diff --git a/theories/s_props.v b/theories/s_props.v index ed5bd75..c2bf165 100644 --- a/theories/s_props.v +++ b/theories/s_props.v @@ -26,19 +26,19 @@ suff philippe (i1 : nat) : (0 < i1)%N -> (i1 <= i)%N -> i%:Q ^+ 2 <= U i1. apply: ler_sum => j; rewrite andbT addn1 ltnS => /andP [h0j hji]. have dpos : 0 < 2%:Q * j%:Q ^+ 3 * (binomialz i j)%:Q * (binomialz (Posz i + j) j)%:Q. - by rewrite !mulr_gt0 ?ltr0z // binz_gt0 ?cpr_add //; exact: leq_trans lei0i. + by rewrite !mulr_gt0 ?ltr0z // binz_gt0 ?cprD //; exact: leq_trans lei0i. rewrite /d normrM normfV normrX expr1n !div1r gtr0_norm //. - rewrite lef_pinv //; last by rewrite posrE mulr_gt0 // mulr_gt0. - by rewrite -2!mulrA ler_pmul2l // mulrA; apply/philippe/leq_trans/lei0i. + rewrite lef_pV2 //; last by rewrite posrE mulr_gt0 // mulr_gt0. + by rewrite -2!mulrA ler_pM2l // mulrA; apply/philippe/leq_trans/lei0i. move=> lt0i1; rewrite {}/U leq_eqVlt => /predU1P[->|hii1]. - rewrite !binz_nat_nat binn mulr1 -!mulrA mulrA ler_pmulr ?mulr_gt0 //. + rewrite !binz_nat_nat binn mulr1 -!mulrA mulrA ler_pMr ?mulr_gt0 //. by move: bigi1; rewrite -rmorphM ler1n muln_gt0 ltr0n bin_gt0 leq_addl andbT. have: i%:Q ^+ 2 <= i1%:Q ^+ 3 * i%:Q ^+ 2. - by rewrite ler_pmull ?exprn_gt0 // exprn_ege1 ?ler1z. -move/le_trans; apply; rewrite -mulrA ler_pmul2l; last first. + by rewrite ler_pMl ?exprn_gt0 // exprn_ege1 ?ler1z. +move/le_trans; apply; rewrite -mulrA ler_pM2l; last first. by rewrite exprn_gt0 ?ltr0n. suff maj : Posz i <= binomialz i i1. - apply: ler_pmul; rewrite ?ler0n ?ler_int //; apply: le_trans maj _. + apply: ler_pM; rewrite ?ler0n ?ler_int //; apply: le_trans maj _. by rewrite !binz_nat_nat lez_nat leq_bin2l ?leq_addr. rewrite binz_nat_nat lez_nat. (* FIXME : n <= 'C(n, m) should be a lemma *) diff --git a/theories/z3irrational.v b/theories/z3irrational.v index 9b96220..9f675ba 100644 --- a/theories/z3irrational.v +++ b/theories/z3irrational.v @@ -40,9 +40,9 @@ pose n_inv_seq (n : nat) := n%:Q^-1. have [/= modulus_n_inv modulus_n_inv_P] : {asympt e : i / n_inv_seq i < e}. exists_big_modulus M rat => /=. move=> eps i lt_eps0 hMi. - rewrite /n_inv_seq -div1r ltr_pdivr_mulr; + rewrite /n_inv_seq -div1r ltr_pdivrMr; last by rewrite ltr0n; raise_big_enough. - rewrite -ltr_pdivr_mull // mulr1. + rewrite -ltr_pdivrMl // mulr1. apply: lt_trans (archi_boundP _) _; first by rewrite ger0E ltW. rewrite ltr_nat; raise_big_enough. by close. @@ -64,10 +64,10 @@ exists_big_modulus m rat. raise_big_enough. apply: le_lt_trans maj _; rewrite telescope_nat //. suff maj : v j < 2%:Q * eps. - rewrite mulNr -mulrN opprB ltr_pdivr_mull // ltr_subl_addr. - apply: lt_trans maj _; rewrite ltr_addl; apply: vpos; exact: ltn_trans ltij. + rewrite mulNr -mulrN opprB ltr_pdivrMl // ltrBlDr. + apply: lt_trans maj _; rewrite ltrDl; apply: vpos; exact: ltn_trans ltij. have maj : v j < j%:Q^-1. - rewrite /v -div1r ltr_pdivr_mulr; last by rewrite exprn_gt0 // ltr0n. + rewrite /v -div1r ltr_pdivrMr; last by rewrite exprn_gt0 // ltr0n. by rewrite mulKf ?ltr1n // lt0r_neq0 // ltr0n. by apply: lt_trans maj _; apply: modulus_n_inv_P; rewrite // pmulr_rgt0. by close. @@ -87,7 +87,7 @@ exists_big_modulus M rat. suff -> : b_over_a_seq i = z3seq i + (\sum_(0 <= k < Posz i + 1 :> int) c i k * s i k) / a i. rewrite opprD addNKr normrN normrM normfV. - rewrite [X in _ / X](gtr0_norm (lt_0_a _)) // ltr_pdivr_mulr ?lt_0_a //. + rewrite [X in _ / X](gtr0_norm (lt_0_a _)) // ltr_pdivrMr ?lt_0_a //. exact: le_lt_trans (ler_norm_sum _ _ _) _. apply: canLR (mulfK _) _; rewrite ?mulrDl ?divfK ?a_neq0 //. rewrite mulr_sumr -big_split /=; apply: eq_bigr => j _. @@ -96,7 +96,7 @@ exists_big_modulus M rat. have step2 (i0 : nat) : (0 <= i0 <= i)%N -> `|c i i0 * s i i0| <= c i i0 * i0%:Q / (2%:Q * i%:Q ^ 2). case/andP=> _ hi0; rewrite normrM [`|c i i0|]gtr0_norm ?lt_0_c //. - rewrite -mulrA ler_pmul2l //; last exact: lt_0_c. + rewrite -mulrA ler_pM2l //; last exact: lt_0_c. apply: s_maj; rewrite // ltr0n; raise_big_enough. apply: (@le_lt_trans _ _ (\sum_(0 <= i0 < i + 1) c i i0 * i0%:Q / (2%:Q * i%:Q ^ 2))). @@ -104,12 +104,12 @@ exists_big_modulus M rat. rewrite addn1 ltnS => hji; exact: step2. apply:(@le_lt_trans _ _ ((\sum_(0 <= i0 < i + 1) c i i0) / (2%:Q * i%:Q))). rewrite mulr_suml; apply: ler_sum_nat => j /andP[h0j]. - rewrite addn1 ltnS => hji; rewrite -mulrA ler_pmul2l ?lt_0_c //. - rewrite mulrA invfM mulrCA ger_pmulr; last by rewrite gtr0E mulr_gt0 ?ltr0n. - by rewrite ler_pdivr_mulr ?ltr0n // mul1r ler_nat. - rewrite mulrC -eq_big_int_nat /= ltr_pmul2r; last first. + rewrite addn1 ltnS => hji; rewrite -mulrA ler_pM2l ?lt_0_c //. + rewrite mulrA invfM mulrCA ger_pMr; last by rewrite gtr0E mulr_gt0 ?ltr0n. + by rewrite ler_pdivrMr ?ltr0n // mul1r ler_nat. + rewrite mulrC -eq_big_int_nat /= ltr_pM2r; last first. rewrite -/(a i); exact: lt_0_a. - rewrite invfM ltr_pdivr_mulr ?ltr0n // mulrC -ltr_pdivr_mulr //. + rewrite invfM ltr_pdivrMr ?ltr0n // mulrC -ltr_pdivrMr //. apply: lt_trans (archi_boundP _) _; last by rewrite ltr_nat; raise_big_enough. by rewrite mulr_ge0 // invr_ge0 ltW. by close. @@ -142,7 +142,7 @@ pose_big_enough m. have aux (i : nat) : 0 < 6%:Q / (i%:Q + 1) ^ 3 / (a (int.shift 1 i) * a i). apply: divr_gt0; first by apply: lt_0_ba_casoratian. apply:mulr_gt0; exact: lt_0_a. - apply: ltr_spaddl => //; apply: sumr_ge0 => i _; exact: ltW. + apply/ltr_pwDl/sumr_ge0 => // i _; exact: ltW. have -> : (z3 - (b_over_a_seq n)%:CR == z3 - (b_over_a_seq m)%:CR + (b_over_a_seq m - b_over_a_seq n)%:CR)%CR. by apply: eq_creal_ext => i /=; ring. @@ -171,18 +171,18 @@ exists large => n hlarge. rewrite cst_crealM. by apply/lecr_mulf2r/divr_ge0/le_0_a; first exact: le_ubound. rewrite {1}z3_eq_b_over_a; apply: (@le_crealP _ n) => i leni /=. - rewrite mul1r ler_subl_addr mulrC -ler_pdivl_mulr ?lt_0_a // mulrDl. - rewrite -[_ / _ / _]mulrA -[_ / _]invfM -expr2 -ler_subl_addr. + rewrite mul1r lerBlDr mulrC -ler_pdivlMr ?lt_0_a // mulrDl. + rewrite -[_ / _ / _]mulrA -[_ / _]invfM -expr2 -lerBlDr. rewrite -/(b_over_a_seq n). have leSnSi : (n.+1 <= i.+1)%N by []. - rewrite z3seqE mulr_sumr (big_cat_nat _ _ _ _ leSnSi) //= mulrDl ler_paddl //. + rewrite z3seqE mulr_sumr (big_cat_nat _ _ _ _ leSnSi) //= mulrDl ler_wpDl //. rewrite divr_ge0 ?exprn_ge0 ?le_0_a ?sumr_ge0 // => k _. by rewrite divr_ge0 ?exprn_ge0 ?ler0n. rewrite big_add1 /= Db_over_a_casoratian; [ | raise_big_enough | exact: leni]. rewrite mulr_suml; apply: ler_sum_nat => j /andP[hnj hji]. - rewrite -mulrSr ler_pmul2l; last by apply/divr_gt0/exprz_gt0; rewrite ltr0n. - rewrite lef_pinv; [| apply: mulr_gt0; exact: lt_0_a..]. - by apply: ler_pmul; rewrite ?le_0_a //; apply: a_incr; lia. + rewrite -mulrSr ler_pM2l; last by apply/divr_gt0/exprz_gt0; rewrite ltr0n. + rewrite lef_pV2; [| apply/mulr_gt0; exact: lt_0_a..]. + by apply: ler_pM; rewrite ?le_0_a //; apply: a_incr; lia. by close. Qed. @@ -252,7 +252,7 @@ have Cpos : 0 < C. by rewrite !(exprz_gt0, mulr_gt0) ?invr_gt0 ?lt_0_Ka ?lt_0_Kdelta. have heps : 0 < eps / C by apply: divr_gt0. have hr : 0 < K2 ^ 3 / 33%:Q < 1. - by rewrite andbC -ltr_pdivl_mulr // invrK mul1r K2_maj divr_gt0 // exprn_gt0. + by rewrite andbC -ltr_pdivlMr // invrK mul1r K2_maj divr_gt0 // exprn_gt0. have [N hN] := Gseqlt1 heps hr. pose_big_enough M. exists M => n hn. @@ -267,10 +267,10 @@ pose_big_enough M. - apply/lt_creal_cst; apply: mulr_gt0; first exact: lt_0_Kdelta. apply: divr_gt0; last by apply: exprn_gt0; rewrite ltr0n. rewrite invr_gt0; exact: lt_0_Ka. - - apply/lt_creal_cst; rewrite ltr_expn2r //; first exact: ltW. + - apply/lt_creal_cst; rewrite ltrXn2r //; first exact: ltW. apply: hanson; raise_big_enough. - apply: lecr_lt_trans (NdeltaP _) _; first by raise_big_enough. - apply/lt_creal_cst; rewrite ltr_pmul2l; last exact: lt_0_Kdelta. + apply/lt_creal_cst; rewrite ltr_pM2l; last exact: lt_0_Kdelta. apply: a_asympt; raise_big_enough. apply: lt_creal_trans aux _; apply/lt_creal_cst; set lhs := (X in (X < _)). have -> : lhs = C * (K2 ^ 3 / 33%:Q) ^ n. @@ -278,7 +278,7 @@ pose_big_enough M. rewrite {}/lhs /C [in RHS]expfzMl exprzAC -[in RHS]expfV. set x := _ ^ n; set y := _ ^ n; field. by rewrite expfz_neq0 ?intr_eq0 // lt0r_neq0 ?lt_0_Ka. - rewrite -ltr_pdivl_mull -[X in _ < X]mulrC; last by rewrite mulrC; exact: Cpos. + rewrite -ltr_pdivlMl -[X in _ < X]mulrC; last by rewrite mulrC; exact: Cpos. apply: hN; raise_big_enough. by close. Qed. diff --git a/theories/z3seq_props.v b/theories/z3seq_props.v index 875b4f5..c4bbfa1 100644 --- a/theories/z3seq_props.v +++ b/theories/z3seq_props.v @@ -30,7 +30,7 @@ Qed. Fact lt_0_Dz3seq (i j : nat) : (j < i)%N -> 0 < z3seq i - z3seq j. Proof. move=> ltji; rewrite Dz3seqE; last exact: ltnW. -rewrite big_nat_recr //=; apply: ltr_paddl; last first. +rewrite big_nat_recr //=; apply: ltr_wpDl; last first. by rewrite invr_gt0 exprn_gt0 // ltr0n; apply: leq_trans ltji. by apply: sumr_ge0 => *; rewrite invr_ge0 exprn_ge0 // ler0n. Qed. @@ -50,16 +50,16 @@ Proof. move=> hr; set r := k.+1%:Q. have hkr : k%:Q = r - 1 by rewrite /r -addn1 PoszD rmorphD addrK. have hrk : r = k%:Q + 1 by rewrite hkr addrK. -have lt1r : 1 < r by rewrite hrk ltr_addr. +have lt1r : 1 < r by rewrite hrk ltrDr. rewrite hkr; set rhs := (X in _ <= X). have {rhs} -> : rhs = 2%:Q^-1 * (2%:Q * r - 1) / (r - 1) ^ 2 * (r ^ 2)^-1. by rewrite /rhs; field; ring_lia. have -> : (r ^ 3)^-1 = r ^-1 * (r ^ 2)^-1 by field; ring_lia. have le0r : 0 <= r by apply: ltW; apply: lt_trans lt1r. -apply: ler_pmul; rewrite ?invr_ge0 ?exprn_ge0 //. -rewrite ler_pdivl_mulr; last first. +apply: ler_pM; rewrite ?invr_ge0 ?exprn_ge0 //. +rewrite ler_pdivlMr; last first. by apply: exprz_gt0; rewrite subr_gt0. -rewrite ler_pdivr_mull; last by apply: lt_trans lt1r. +rewrite ler_pdivrMl; last by apply: lt_trans lt1r. rewrite -subr_ge0; set rhs := (X in _ <= X). have {rhs} -> : rhs = 3%:Q / 2%:Q * r - 1 by rewrite /rhs; field. by rewrite subr_ge0; apply/mulr_ege1/ltW. From 11a05ccd770c0b1728498efc5a58f24a883cff0e Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 12 Oct 2023 16:19:33 +0200 Subject: [PATCH 2/2] Clean up --- theories/binomialz.v | 17 +++++++---------- theories/hanson.v | 19 ++++++++----------- 2 files changed, 15 insertions(+), 21 deletions(-) diff --git a/theories/binomialz.v b/theories/binomialz.v index d797c50..34eee7f 100644 --- a/theories/binomialz.v +++ b/theories/binomialz.v @@ -125,12 +125,10 @@ wlog: m n / n <= 0. case: m => m; last by rewrite !binz_neg // mulr0. rewrite binz_nat_nat -addrA -opprB opprK. case: (ltnP n m) => hnm hwlog. - - rewrite bin_small // subzn // binz_nat_nat bin_small ?mulr0 //. - by rewrite add1n subnSK // leq_subLR leq_addl. - - have {}hnm : (Posz m) - (Posz n.+1) <= 0. - by rewrite subr_le0; apply/leqW/hnm. - rewrite [in RHS]hwlog // opprD opprK addrA subrr add0r addrAC subrr add0r. - by rewrite binz_nat_nat mulrA /exprz /= -exprMn mulrNN mul1r expr1n mul1r. + by rewrite bin_small // subzn // binz_nat_nat bin_small ?mulr0; lia. + have {}hnm : Posz m - Posz n.+1 <= 0 by rewrite subr_le0; apply/leqW/hnm. + rewrite [in RHS]hwlog // subKr addrAC subrr add0r. + by rewrite binz_nat_nat mulrA /exprz /= -exprMn mulrNN mul1r expr1n mul1r. case: m => m; last by rewrite !binz_neg // mulr0. case: n => [n | n _]. case: n => [_ | //]; case:m => [ | m]; first by rewrite !binz0. @@ -139,8 +137,7 @@ rewrite [in RHS]NegzE opprK -addrA subzSS subr0. move: {2}(m + n)%N (leqnn (m + n)) => k; elim: k n m => [n m|k ihk n m hnm]. by rewrite leqn0 addn_eq0; case/andP => /eqP -> /eqP ->; rewrite !binz0. case: m hnm => [ | m] hnm //; case: n hnm => [ | n] hnm. - rewrite bin_1N_posz {}ihk // !addr0 !binz_on_diag /= !mulr1. - by rewrite exprSz mulN1r. + by rewrite bin_1N_posz {}ihk // !addr0 !binz_on_diag /= !mulr1 exprSz mulN1r. rewrite bin_negz_posz ihk; last by move: hnm; rewrite addnS. rewrite ihk; last by move: hnm; rewrite addSn. rewrite exprSzr -!mulrA !mulN1r -mulrBr; congr (_ * _); rewrite -opprD. @@ -156,8 +153,8 @@ Lemma binzSS_weak (F : numFieldType) (n k : int) : 0 <= n -> k + 1 != 0 -> Proof. case: n k => [] // n [k|[|k]] // _ _; last by rewrite !binz_neg // mulr0. rewrite -!PoszD !addn1 !binz_nat_nat mulrAC. -apply: (canRL (mulfK _)); rewrite ?intr_eq0 //. -by rewrite -!rmorphM -!PoszM /= mul_bin_diag mulnC. +apply: canRL (mulfK _) _; rewrite ?intr_eq0 //. +by rewrite -!intrM -!PoszM mul_bin_diag mulnC. Qed. Lemma binzS_weak (F : numFieldType) (n k : int) : n >= 0 -> k + 1 != 0 -> diff --git a/theories/hanson.v b/theories/hanson.v index baad385..af6c441 100644 --- a/theories/hanson.v +++ b/theories/hanson.v @@ -318,26 +318,21 @@ have -> : w_seq 4 = a' 0 * a' 1 * a' 2 * a' 3. have a'0_ubP : a' 0 <= a'0_ub%:C. have ge0a'0 : 0 <= a'0_ub%:C by rewrite ler0q divr_ge0. rewrite root_le_x // a0 -rmorphXn ler_rat exprMn exprVn. - rewrite lter_pdivlMr ?exprn_gt0 // -subr_ge0 mulrzl. - by rewrite -!rmorphXn -rmorphMz -rmorphB /= rat_of_ZEdef ler0z. + by rewrite lter_pdivlMr; ring_lia. have a'1_ubP : a' 1 <= a'1_ub%:C. have ge0a'1 : 0 <= a'1_ub%:C by rewrite ler0q divr_ge0. rewrite root_le_x // a1 -rmorphXn ler_rat exprMn exprVn. - rewrite lter_pdivlMr ?exprn_gt0 // -subr_ge0 mulrzl. - by rewrite -!rmorphXn -rmorphMz -rmorphB /= rat_of_ZEdef ler0z. + by rewrite lter_pdivlMr; ring_lia. have a'2_ubP : a' 2 <= a'2_ub%:C. have ge0a'2 : 0 <= a'2_ub%:C by rewrite ler0q divr_ge0. have ge0a2 : 0 <= (a 2)%:Q%:C by rewrite ler0q. rewrite root_le_x // a2 -rmorphXn ler_rat exprMn exprVn. - rewrite lter_pdivlMr ?exprn_gt0 // -subr_ge0 mulrzl. - by rewrite -!rmorphXn -rmorphMz -rmorphB /= rat_of_ZEdef ler0z. + by rewrite lter_pdivlMr; ring_lia. have a'3_ubP : a' 3 <= a'3_ub%:C. have ge0a'3 : 0 <= a'3_ub%:C by rewrite ler0q divr_ge0. have ge0a3 : 0 <= (a 3)%:Q%:C by rewrite ler0q. rewrite root_le_x // a3 -rmorphXn ler_rat exprMn exprVn. - rewrite lter_pdivlMr; last exact: exprn_gt0. - rewrite -subr_ge0 mulrzl -!rmorphXn -rmorphMz -rmorphB /=. - by rewrite rat_of_ZEdef ler0z. + by rewrite lter_pdivlMr; ring_lia. have a'4_ubP : a' 4 <= a'4_ub%:C. have ge0a'1 : 0 <= a'4_ub%:C by rewrite ler0q divr_ge0. have ge0a4 : 0 <= (a 4)%:Q%:C by rewrite ler0q ler0z. @@ -345,7 +340,9 @@ have a'4_ubP : a' 4 <= a'4_ub%:C. pose t : rat := (rat_of_Z 200)^-1. have -> : a'4_ub = 1 + t by rewrite /a'4_ub /t; field. rewrite -rmorphXn ler_rat a4 exprDn. - have -> : (1808 = 8 + 1800)%N by []. + (* FIXME: *) + (* have -> : (1808 = 8 + 1800)%N by []. *) + change 1808%N with (8 + 1800)%N. rewrite big_split_ord /=; apply: ler_wpDr. apply: sumr_ge0 => i. by rewrite expr1n mul1r mulrn_wge0 ?exprn_ge0 ?invr_ge0. @@ -500,7 +497,7 @@ have -> : forall k1, exp_quo n%:Q (n * (a k1.+1).-2) (a k1.+1).-1 - by rewrite muln_gt0 /= muln_gt0; apply/andP. - by rewrite muln_gt0 andbT muln_gt0; apply/andP. lia. -rewrite /w_seq /t10n_to rmorphXn -subn1 -prod_is_exp_sum. +rewrite /w_seq /t10n_to [in RHS]rmorphXn -subn1 -prod_is_exp_sum. rewrite -3!mulrA ![_ * (_%:C * _)]mulrCA; congr (_ * _). rewrite -prodrXl -!prodfV -!big_split /=; apply: eq_bigr => i _. rewrite -exprM mul1n [_^-1 / _ in RHS]mulrC [RHS]mulrA [RHS]mulrACA.