From 4c189fa4eb8804d10e4ddcc8d6f9d2c67a6fc05a Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 24 Mar 2024 15:22:56 +0100 Subject: [PATCH 1/2] Simplifications, phase 1 --- .nix/config.nix | 2 +- .nix/coq-nix-toolbox.nix | 2 +- theories/polyrcf.v | 751 ++++++++++++++++++++++----------------- theories/qe_rcf_th.v | 39 +- 4 files changed, 442 insertions(+), 352 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 5e41710..e107c2a 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -31,7 +31,7 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "8.16"; + default-bundle = "8.19"; ## write one `bundles.name` attribute set per ## alternative configuration diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index fd19200..0664b1a 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"1cad18e8537b4f6d6ad97d6eb57fa61e3dbcad59" +"abb4982c7d47a00005ede4bae2e2c47d895a41dc" diff --git a/theories/polyrcf.v b/theories/polyrcf.v index e99007e..60a9a24 100644 --- a/theories/polyrcf.v +++ b/theories/polyrcf.v @@ -1,12 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. -From mathcomp -Require Import bigop order ssralg poly polydiv ssrnum zmodp. -From mathcomp -Require Import polyorder path interval ssrint. +From mathcomp Require Import all_ssreflect all_algebra. +Require Import polyorder. (****************************************************************************) (* This files contains basic (and unformatted) theory for polynomials *) @@ -35,7 +30,7 @@ Require Import polyorder path interval ssrint. (****************************************************************************) -Import Order.TTheory GRing.Theory Num.Theory Num.Def Pdiv.Idomain. +Import Order.Theory GRing.Theory Num.Theory Pdiv.Idomain. Set Implicit Arguments. Unset Strict Implicit. @@ -46,6 +41,9 @@ Local Open Scope ring_scope. Local Notation noroot p := (forall x, ~~ root p x). Local Notation mid x y := ((x + y) / 2%:R). +Local Notation maxr := Num.max. +Local Notation minr := Num.min. +Local Notation sgr := Num.sg. Section more. Section SeqR. @@ -96,9 +94,9 @@ Section PolyNumDomain. Variable R : numDomainType. Implicit Types (p q : {poly R}). -Definition sgp_pinfty (p : {poly R}) := sgr (lead_coef p). +Definition sgp_pinfty (p : {poly R}) := Num.sg (lead_coef p). Definition sgp_minfty (p : {poly R}) := - sgr ((-1) ^+ (size p).-1 * (lead_coef p)). + Num.sg ((-1) ^+ (size p).-1 * (lead_coef p)). End PolyNumDomain. @@ -173,24 +171,34 @@ Lemma cauchy_boundP (p : {poly R}) x : p != 0 -> p.[x] = 0 -> `| x | < cauchy_bound p. Proof. move=> np0 rpx; rewrite ltr_spaddl ?ltr01 //. -case e: (size p) => [|n]; first by move: np0; rewrite -size_poly_eq0 e eqxx. -have lcp : `|lead_coef p| > 0 by move: np0; rewrite -lead_coef_eq0 -normr_gt0. -case: (lerP `|x| 1) => cx1. - rewrite (le_trans cx1) // ler_pdivl_mull // mulr1. - by rewrite big_ord_recr /= /lead_coef e ler_addr sumr_ge0. -have xp : 0 < `|x| by rewrite (lt_trans _ cx1) ?ltr01. -rewrite ler_pdivl_mull // /lead_coef e /= big_ord_recr /= ler_paddr //. -case es: n e => [|m] e. - by move: rpx np0; rewrite (@size1_polyC _ p) ?e // hornerC => -> /eqP. -have/ler_pmul2r <-: 0 < `|x| ^+ m by rewrite exprn_gt0. -rewrite -mulrA -exprS -(normrX m.+1) -normrM -es big_distrl /=. -apply: le_trans (_ : \sum_(i < n) `|p`_i * x ^+ i| <= _). - move/eqP: rpx; rewrite horner_coef e -es big_ord_recr /= addrC addr_eq0. - by move/eqP ->; rewrite normrN ler_norm_sum. -rewrite es; apply: ler_sum => i _. -by rewrite normrM normrX ler_pmul ?exprn_ge0 // ler_eexpn2l // leq_ord. -(* this could be improved a little bit with int exponents *) -Qed. +have sp_gt0 : (size p > 0)%N by rewrite size_poly_gt0. +have lcn0 : `|lead_coef p| != 0 by rewrite normr_eq0 lead_coef_eq0. +have lcp : `|lead_coef p| > 0 by rewrite lt_def lcn0 /=. +have [x_le1|x_gt1] := lerP `|x| 1. + rewrite (le_trans x_le1) // ler_pdivl_mull // mulr1. + by rewrite polySpred// big_ord_recr/= ler_addr sumr_ge0. +have x_gt0 : `|x| > 0 by rewrite (lt_trans ltr01). +have [sp_le1|sp_gt1] := leqP (size p) 1. + by move: rpx np0; rewrite [p]size1_polyC// hornerC polyC_eq0 => /eqP->. +rewrite ler_pdivl_mull//. +pose n := (size p).-1; have n_gt0 : (n > 0)%N by rewrite /n -subn1 subn_gt0. +have : `|p`_n| * `|x| ^+ n <= \sum_(i < n) `|p`_i * x ^+ i|. + rewrite (le_trans _ (ler_norm_sum _ _ _))//. + have := rpx; rewrite horner_coef polySpred// !big_ord_recr/=. + by move=> /(canRL (@addrK _ _))->; rewrite sub0r normrN normrM normrX. +rewrite -[n in _ ^+ n]prednK// exprS mulrA. +rewrite -[X in _ X -> _]ler_pdivl_mulr ?exprn_gt0// => /le_trans->//. +rewrite polySpred// big_ord_recr/= ler_paddr// mulr_suml ler_sum => //i _. +rewrite normrM normrX ler_pdivr_mulr ?exprn_gt0// ler_pmul ?exprn_ge0//. +by rewrite ler_weexpn2l// 1?ltW// -ltnS prednK//. +Qed. + +Lemma root_in_cauchy_bound (p : {poly R}) : p != 0 -> + {subset root p <= `](- cauchy_bound p), (cauchy_bound p)[ }. +Proof. by move=> p_neq0 x /eqP /(cauchy_boundP p_neq0); rewrite ltr_norml. Qed. + +Definition root_cauchy_boundP (p : {poly R}) pN0 x (rpx : root p x) := + itvP (root_in_cauchy_bound pN0 rpx). Lemma le_cauchy_bound p : p != 0 -> {in `]-oo, (- cauchy_bound p)], noroot p}. Proof. @@ -214,9 +222,18 @@ Lemma cauchy_bound_ge0 p : cauchy_bound p >= 0. Proof. by rewrite ltW. Qed. Hint Resolve cauchy_bound_ge0 : core. +Lemma cauchy_bound_neq0 p : cauchy_bound p != 0. Proof. by rewrite gt_eqF. Qed. +Hint Resolve cauchy_bound_neq0 : core. + End CauchyBound. End PolyRealField. +#[export] +Hint Resolve le_cauchy_bound ge_cauchy_bound : core. +#[export] +Hint Resolve cauchy_bound_gt0 cauchy_bound_ge0 : core. +#[export] +Hint Resolve cauchy_bound_neq0 : core. (************************************************************) (* Definitions and properties for polynomials in a rcfType. *) @@ -234,134 +251,157 @@ Implicit Types p q r : {poly R}. (* we restate poly_ivt in a nicer way. Perhaps the def of PolyRCF should *) (* be moved in this file, juste above this section *) -Lemma poly_ivt (p : {poly R}) (a b : R) : - a <= b -> 0 \in `[p.[a], p.[b]] -> { x : R | x \in `[a, b] & root p x }. -Proof. by move=> leab root_p_ab; apply/sig2W/poly_ivt. Qed. - -Lemma polyrN0_itv (i : interval R) (p : {poly R}) : - {in i, noroot p} -> - forall y x : R, y \in i -> x \in i -> sgr p.[x] = sgr p.[y]. -Proof. -move=> hi y x hy hx; wlog xy: x y hx hy / x <= y. - by move=> hwlog; case: (leP x y) => [|/ltW] /hwlog ->. -have hxyi: (`[x, y] <= i)%O. - by case: i hx hy {hi} => [bl br] /andP [hx _] /andP []; rewrite /<=%O /= hx. -move: (hi _ hx) (hi _ hy); rewrite /root; do 2 case: sgrP => //. - move=> /ltW py0 /ltW p0x; case: (@poly_ivt (- p) x y) => //. - by rewrite !hornerN -oppr_itvcc oppr0 in_itv /= py0. - by move=> z hz; rewrite rootN (negPf (hi z _)) //; apply: (le_trans hz). -move=> /ltW p0y /ltW px0; case: (@poly_ivt p x y); rewrite ?in_itv /= ?px0 //=. -by move=> z hz; rewrite (negPf (hi z _)) //; apply: (le_trans hz). -Qed. - -Lemma poly_div_factor (a : R) (P : {poly R} -> Prop) : - (forall k, P k%:P) -> - (forall p n k, p.[a] != 0 -> P p -> P (p * ('X - a%:P)^+(n.+1) + k%:P)%R) - -> forall p, P p. -Proof. -move=> Pk Pq p. -move: {-2}p (leqnn (size p)); elim: (size p)=> {p} [|n ihn] p spn. - by move: spn; rewrite leqn0 size_poly_eq0 -polyC0; move/eqP->; exact: Pk. -case: (leqP (size p) 1)=> sp1; first by rewrite [p]size1_polyC ?sp1//. -rewrite (Pdiv.IdomainMonic.divp_eq (monicXsubC a) p). -rewrite [_ %% _]size1_polyC; last first. - by rewrite -ltnS (@leq_trans (size ('X - a%:P))) // - ?ltn_modp ?polyXsubC_eq0 ?size_XsubC. -have [n' [q hqa hp]] := multiplicity_XsubC (p %/ ('X - a%:P)) a. -rewrite divpN0 ?size_XsubC ?polyXsubC_eq0 ?sp1 //= in hqa. -rewrite hp -mulrA -exprSr; apply: Pq=> //; apply: ihn. -rewrite (@leq_trans (size (q * ('X - a%:P) ^+ n'))) //. - rewrite size_mul ?expf_eq0 ?polyXsubC_eq0 ?andbF //; last first. - by apply: contraNneq hqa => ->; rewrite root0. - by rewrite size_exp_XsubC addnS leq_addr. -by rewrite -hp size_divp ?polyXsubC_eq0 ?size_XsubC // leq_subLR. +Definition poly_ivtW := poly_ivt. + +Lemma poly_ivt p a b : a <= b -> p.[a] * p.[b] <= 0 -> + {x | x \in `[a, b] & root p x}. +Proof. +move=> le_ab sgp; apply/sig2W; have []//= := @poly_ivt _ (p.[b] *: p) a b. + by rewrite !hornerZ sqr_ge0 mulrC sgp. +move=> x axb; have [|?] := boolP (root p b); last by rewrite rootZ //; exists x. +by move=> rpb; exists b; rewrite // in_itv/= lexx andbT. +Qed. + +Lemma poly_ivtoo p a b : a <= b -> p.[a] * p.[b] < 0 -> + {x | x \in `]a, b[ & root p x}. +Proof. +move=> le_ab; rewrite lt_neqAle mulf_eq0 negb_or -andbA => /and3P[pa0 pb0]. +move=> /(poly_ivt le_ab) [c cab rpc]. +exists c => //; rewrite in_itv; apply/andP => /=. +by split; rewrite lt_neqAle (itvP cab) andbT; [move: pa0|move: pb0]; + apply: contraNneq; [move->|move<-]. +Qed. + +Definition has_ivt_root p a b := + if (a <= b) && (p.[a] * p.[b] <= 0) =P true isn't ReflectT pp then None + else Some (projT1 (poly_ivt (proj1 (andP pp)) (proj2 (andP pp)))). +Notation ivt_root p a b := (odflt 0 (has_ivt_root p a b)). + +CoInductive has_itv_root_spec p a b : bool -> option R -> Type := +| HasItvRoot x of (p.[a] * p.[b] <= 0) & x \in `[a, b] & root p x : + has_itv_root_spec p a b true (Some x) +| NoItvRoot of (p.[a] * p.[b] > 0) : has_itv_root_spec p a b false None. + +Lemma has_itv_rootP p a b : a <= b -> + has_itv_root_spec p a b (p.[a] * p.[b] <= 0) (has_ivt_root p a b). +Proof. +move=> le_ab; rewrite /has_ivt_root; case: eqP => /= [pp|/negP]. + move: {-}(pp) => /andP[_ pab]; rewrite {1}pab; constructor => //; + by case: poly_ivt. +by rewrite le_ab /= -ltNge => pab; rewrite lt_geF //; constructor. +Qed. + +Lemma some_ivt_root p a b x : has_ivt_root p a b = Some x -> root p x. +Proof. +by rewrite /has_ivt_root; case: eqP => //= pp; case: poly_ivt => //= ??? [<-]. +Qed. + +Lemma has_ivt_rootE p a b : + has_ivt_root p a b = (a <= b) && (p.[a] * p.[b] <= 0) :> bool. +Proof. by rewrite /has_ivt_root; case: eqP => //= /negP/negPf->. Qed. + +Lemma ivt_root_in p a b : a <= b -> p.[a] * p.[b] <= 0 -> + ivt_root p a b \in `[a, b]. +Proof. by move=> ab; case: has_itv_rootP. Qed. + +Lemma ivt_rootP p a b : a <= b -> p.[a] * p.[b] <= 0 -> + root p (ivt_root p a b). +Proof. by move=> leab; case: has_itv_rootP. Qed. + +Lemma sub_cc_itv a b (i : interval R) : + (a \in i) -> (b \in i) -> (`[a, b] <= i)%O. +Proof. +case: i => [c d]; rewrite !inE/= !/(_ <= Interval _ _)%O/=. +by move=> /andP[-> _] /andP[_ ->]. +Qed. + +Lemma sub_oo_itv a b (i : interval R) : + (a \in i) -> (b \in i) -> (`]a, b[ <= i)%O. +Proof. +case: i => [c d]; rewrite !inE/= !/(_ <= Interval _ _)%O/=. +move=> /andP[ca _] /andP[_ bd]. +by rewrite (le_trans ca) ?bnd_simp// (le_trans _ bd) ?bnd_simp. +Qed. + +Lemma polyrN0_itv (i : interval R) (p : {poly R}) : {in i, noroot p} -> + {in i & , forall y x : R, sgr p.[x] = sgr p.[y]}. +Proof. +move=> hi y x hy hx; wlog xy: x y hx hy / x <= y => [hwlog|]. + by case/orP: (le_total x y)=> xy; [|symmetry]; apply: hwlog. +have hxyi: {subset `[x, y] <= i} by apply/subitvP; rewrite sub_cc_itv. +have [r _ rin|] := @has_itv_rootP p x y xy. + by rewrite (negPf (hi _ _)) // hxyi. +rewrite -sgr_cp0 sgrM eq_sym; do 2!case: sgzP => //; +by rewrite ?(mul0r, mulr0, mul1r, mulr1, oner_eq0) // => _ _ /eqP. Qed. Lemma nth_root x n : x > 0 -> { y | y > 0 & y ^+ (n.+1) = x }. Proof. -move=> l0x. -case: (ltrgtP x 1)=> hx; last by exists 1; rewrite ?hx ?lter01// expr1n. - case: (@poly_ivt ('X ^+ n.+1 - x%:P) 0 1); first by rewrite ler01. - rewrite in_itv /= ?(hornerE, horner_exp) expr0n expr1n. - by rewrite sub0r oppr_le0 subr_ge0 !ltW. - move=> y hy; rewrite rootE ?(hornerE, horner_exp) subr_eq0. - move/eqP=> hyx; exists y; rewrite //= lt0r (itvP hy) andbT. - by apply: contra_eq_neq hyx => ->; rewrite expr0n /=; case: sgrP l0x. -case: (@poly_ivt ('X ^+ n.+1 - x%:P) 0 x); first by rewrite ltW. - rewrite in_itv /= ?(hornerE, horner_exp) expr0n sub0r oppr_le0 subr_ge0. - by rewrite ler_eexpr // ltW. -move=> y hy; rewrite rootE ?(hornerE, horner_exp) subr_eq0. -move/eqP=> hyx; exists y; rewrite //= lt0r (itvP hy) andbT. -by apply: contra_eq_neq hyx => ->; rewrite expr0n /=; case: sgrP l0x. -Qed. - -Lemma poly_cont x p e : - e > 0 -> exists2 d, d > 0 & forall y, `|y - x| < d -> `|p.[y] - p.[x]| < e. -Proof. -elim/(@poly_div_factor x): p e => [|p n k pxn0 Pp] e ep. - by exists 1; rewrite ?ltr01// => y hy; rewrite !hornerC subrr normr0. -case: (Pp (`|p.[x]|/2%:R)). - by rewrite pmulr_lgt0 ?invr_gte0//= ?ltr0Sn// normrE. -move=> d' d'p He'. -case: (@nth_root (e / ((3%:R / 2%:R) * `|p.[x]|)) n). - by rewrite ltr_pdivl_mulr ?mul0r ?pmulr_rgt0 ?invr_gt0 ?normrE ?ltr0Sn. -move=> d dp rootd. -exists (minr d d'); first by rewrite lt_minr dp. -move=> y; rewrite lt_minr; case/andP=> hxye hxye'. -rewrite !(hornerE, horner_exp) subrr expr0n mulr0n mulr0 add0r addrK normrM. -apply: le_lt_trans (_ : `|p.[y]| * d ^+ n.+1 < _). - by rewrite ler_wpmul2l ?normrE // normrX ler_expn2r -?topredE /= ?normrE 1?ltW. -rewrite rootd mulrCA gtr_pmulr //. -rewrite ltr_pdivr_mulr ?mul1r ?pmulr_rgt0 ?invr_gt0 ?ltr0Sn ?normrE //. -rewrite mulrDl mulrDl divff; last by rewrite -mulr2n pnatr_eq0. -rewrite !mul1r mulrC -ltr_subl_addr. -by rewrite (le_lt_trans _ (He' y _)) // ler_sub_dist. +move=> x_gt0; apply/sig2_eqW; pose p := ('X ^+ n.+1 - x%:P). +have xS_ge1: x + 1 >= 1 by rewrite ler_paddl // ltW. +have xS_ge0: x + 1 > 0 by rewrite (lt_le_trans (@ltr01 _)). +have [//||y /andP[y_ge0 _]] := @poly_ivtW _ p 0 (x + 1); first exact: ltW. + rewrite !(hornerE, horner_exp) expr0n /= sub0r oppr_le0 (ltW x_gt0) /=. + by rewrite subr_ge0 (le_trans _ (ler_eexpr _ _)) // ler_paddr ?ler01. +rewrite /root !(hornerE, horner_exp) subr_eq0 => /eqP x_eq; exists y => //. +rewrite lt_neqAle y_ge0 andbT; apply: contra_eqN x_eq => /eqP<-. +by rewrite eq_sym expr0n gt_eqF. +Qed. + +(* REMOVE or DISPLACE *) +Lemma poly_div_factor (a : R) (P : {poly R} -> Prop) : (forall k, P k%:P) -> + (forall p n k, ~~ root p a -> P p -> P (p * ('X - a%:P) ^+ n.+1 + k%:P)%R) -> + forall p, P p. +Proof. +move=> Pk Pq p; elim: size {-2}p (leqnn (size p)) => {p} [p|n ihn p size_p]. + by rewrite size_poly_leq0 => /eqP->; apply: Pk. +have [/size1_polyC->//|p_gt1] := leqP (size p) 1. +have p_neq0 : p != 0 by rewrite -size_poly_eq0 -lt0n ltnW. +rewrite (Pdiv.IdomainMonic.divp_eq (monicXsubC a) p). +have [n' [q /implyP rqa pmod_eq]] := multiplicity_XsubC (p %/ ('X - a%:P)) a. +have Xsuba_neq0 : 'X - a%:P != 0 by rewrite -size_poly_eq0 size_XsubC. +have /size1_polyC-> : (size (p %% ('X - a%:P))%R <= 1)%N. + by rewrite -ltnS (leq_trans (ltn_modpN0 _ _))// ?size_XsubC. +rewrite pmod_eq -mulrA -exprSr; apply: Pq; last apply: ihn. + by rewrite rqa// divpN0// ?size_XsubC. +have [->//|q_neq0] := eqVneq q 0; first by rewrite size_poly0. +rewrite (@leq_trans (size (q * ('X - a%:P) ^ n')))//. + rewrite size_Mmonic// ?monic_exp ?monicXsubC//. + by rewrite size_exp_XsubC addnS/= leq_addr. +rewrite -pmod_eq -ltnS (leq_trans _ size_p)// ltn_divpl//. +by rewrite size_Mmonic// ?monicXsubC// ?size_XsubC ?addn2. Qed. Lemma poly_ltsp_roots p (rs : seq R) : (size rs >= size p)%N -> uniq rs -> all (root p) rs -> p = 0. Proof. -move=> hrs urs rrs; apply: contraTeq hrs => np0. +move=> hrs urs rrs; apply/eqP; apply: contraLR hrs=> np0. by rewrite -ltnNge; apply: max_poly_roots. Qed. -Lemma ivt_sign (p : {poly R}) (a b : R) : - a <= b -> sgr p.[a] * sgr p.[b] = -1 -> { x : R | x \in `]a, b[ & root p x}. +Theorem poly_rolle a b p : + a < b -> p.[a] = p.[b] -> {c | c \in `]a, b[ & p^`().[c] = 0}. Proof. -move=> hab /eqP; rewrite mulrC mulr_sg_eqN1=> /andP [spb0 /eqP spb]. -case: (@poly_ivt (sgr p.[b] *: p) a b) => //. - by rewrite in_itv /= !hornerZ {1}spb mulNr -!normrEsg oppr_cp0 !normrE. -move=> c hc; rewrite rootZ ?sgr_eq0 // => rpc; exists c=> //. -(* need for a lemma reditvP *) -rewrite !in_itv /= !lt_neqAle andbACA [(_ <= _) && _]hc andbT eq_sym -negb_or. -apply: contraL rpc => /orP [] /eqP ->; rewrite /root ?(negPf spb0) //. -by rewrite -sgr_cp0 -[sgr _]opprK -spb eqr_oppLR oppr0 sgr_cp0. -Qed. - -Let rolle_weak a b p : - a < b -> p.[a] = 0 -> p.[b] = 0 -> +gen have rolle_weak : a b p / a < b -> p.[a] = 0 -> p.[b] = 0 -> {c | (c \in `]a, b[) & (p^`().[c] == 0) || (p.[c] == 0)}. -Proof. -move=> lab pa0 pb0; apply/sig2W. -have [->|p0] := eqVneq p 0. - by exists (mid a b); rewrite ?mid_in_itv // derivC horner0 eqxx. -have [n [p' p'a0 hp]] := multiplicity_XsubC p a; rewrite p0 /= in p'a0. -case: n hp pa0 p0 pb0 p'a0=> [ | n -> _ p0 pb0 p'a0]. - by rewrite {1}expr0 mulr1 rootE=> -> /eqP ->. -have [m [q qb0 hp']] := multiplicity_XsubC p' b. -rewrite (contraNneq _ p'a0) /= in qb0 => [|->]; last exact: root0. -case: m hp' pb0 p0 p'a0 qb0=> [|m]. - rewrite {1}expr0 mulr1=> -> /eqP. - rewrite !(hornerE, horner_exp, mulf_eq0). - by rewrite !expf_eq0 !subr_eq0 !(gt_eqF lab) !andbF !orbF !rootE=> ->. -move=> -> _ p0 p'a0 qb0; case: (sgrP (q.[a] * q.[b])); first 2 last. -- move=> sqasb; case: (@ivt_sign q a b)=> //; first exact: ltW. - by apply/eqP; rewrite -sgrM sgr_cp0. - move=> c lacb rqc; exists c=> //. - by rewrite !hornerM (eqP rqc) !mul0r eqxx orbT. -- move/eqP; rewrite mulf_eq0 (rootPf qb0) orbF; move/eqP=> qa0. - by move: p'a0; rewrite ?rootM rootE qa0 eqxx. -- move=> hspq; rewrite !derivCE /= !mul1r mulrDl !pmulrn. + move=> lab pa0 pb0; have ltab := ltW lab; apply/sig2W. + have [->|p_neq0] := eqVneq p 0. + by exists (mid a b); rewrite ?mid_in_itv// derivC horner0 eqxx. + have [n [p' p'a0 hp]] := multiplicity_XsubC p a; rewrite p_neq0 /= in p'a0. + case: n hp pa0 p_neq0 pb0 p'a0 => [ | n -> _ p0 pb0 p'a0]. + by rewrite {1}expr0 mulr1 rootE=> ->; move/eqP->. + have [m [q qb0 hp']] := multiplicity_XsubC p' b. + rewrite (contraNneq _ p'a0) /= in qb0 => [|->]; last exact: root0. + case: m hp' pb0 p0 p'a0 qb0=> [|m]. + rewrite {1}expr0 mulr1=> ->; move/eqP. + rewrite !(hornerE, horner_exp, mulf_eq0). + by rewrite !expf_eq0 !subr_eq0 !(gt_eqF lab) !andbF !orbF !rootE=> ->. + move=> -> _ p0 p'a0 qb0; case: (sgrP (q.[a] * q.[b])); first 2 last. + - move=> /poly_ivtoo [] // c lacb rqc; exists c=> //. + by rewrite !hornerM (eqP rqc) !mul0r eqxx orbT. + - move/eqP; rewrite mulf_eq0 (rootPf qb0) orbF; move/eqP=> qa0. + by move: p'a0; rewrite ?rootM rootE qa0 eqxx. + move=> hspq; rewrite !derivCE /= !mul1r mulrDl !pmulrn. set xan := (('X - a%:P) ^+ n); set xbm := (('X - b%:P) ^+ m). have ->: ('X - a%:P) ^+ n.+1 = ('X - a%:P) * xan by rewrite exprS. have ->: ('X - b%:P) ^+ m.+1 = ('X - b%:P) * xbm by rewrite exprS. @@ -370,79 +410,105 @@ move=> -> _ p0 p'a0 qb0; case: (sgrP (q.[a] * q.[b])); first 2 last. = (y * z * x) * (xbm * xan). by move=> x y z; rewrite mulrCA !mulrA [_ * y]mulrC mulrA. rewrite !fac -!mulrDl; set r := _ + _ + _. - case: (@ivt_sign (sgr q.[b] *: r) a b); first exact: ltW. - rewrite !hornerZ !sgr_smul mulrACA -expr2 sqr_sg (rootPf qb0) mul1r. + case: (@poly_ivtoo (sgr q.[b] *: r) a b) => // [|c lecb]. + rewrite !hornerZ mulrACA -expr2 sqr_sg (rootPf qb0) mul1r. rewrite !(subrr, mul0r, mulr0, addr0, add0r, hornerC, hornerXsubC, - hornerD, hornerN, hornerM, hornerMn). - rewrite [_ * _%:R]mulrC -!mulrA !pmulrn !mulrzl !sgrMz -sgrM. - rewrite mulrAC mulrA -mulrA sgrM -opprB mulNr sgrN sgrM. - by rewrite !gtr0_sg ?subr_gt0 ?mulr1 // mulrC. -move=> c lacb; rewrite rootE hornerZ mulf_eq0. -rewrite sgr_cp0 (rootPf qb0) orFb=> rc0. -by exists c=> //; rewrite !hornerM !mulf_eq0 rc0. -Qed. - -Theorem rolle a b p : - a < b -> p.[a] = p.[b] -> {c | c \in `]a, b[ & p^`().[c] = 0}. -Proof. -move=> lab pab. -wlog pb0 : p pab / p.[b] = 0. - case/(_ (p - p.[b]%:P)); rewrite ?hornerE ?pab ?subrr //. - by move=> c acb; rewrite derivE derivC subr0 => hc; exists c. + hornerD, hornerN, hornerM, hornerMn) [_ * _%:R]mulrC. + rewrite mulrACA pmulr_llt0 // mulrACA pmulr_rlt0 ?mulr_gt0 ?ltr0n //. + by rewrite -opprB mulNr oppr_lt0 mulr_gt0 ?subr_gt0. + rewrite rootE hornerZ mulf_eq0 sgr_cp0 (rootPf qb0) orFb => rc0. + by exists c => //; rewrite !hornerM !mulf_eq0 rc0. +move=> lab pab; wlog pb0 : p pab / p.[b] = 0 => [hwlog|]. + case: (hwlog (p - p.[b]%:P)); rewrite ?hornerE ?pab ?subrr //. + by move=> c acb; rewrite derivE derivC subr0=> hc; exists c. move: pab; rewrite pb0=> pa0. -have: forall rs : seq R, {subset rs <= `]a, b[} -> - (size p <= size rs)%N -> uniq rs -> all (root p) rs -> p = 0. +have: (forall rs : seq R, {subset rs <= `]a, b[} -> + (size p <= size rs)%N -> uniq rs -> all (root p) rs -> p = 0). by move=> rs hrs; apply: poly_ltsp_roots. elim: (size p) a b lab pa0 pb0=> [|n ihn] a b lab pa0 pb0 max_roots. rewrite (@max_roots [::]) //=. by exists (mid a b); rewrite ?mid_in_itv // derivE horner0. case: (@rolle_weak a b p); rewrite // ?pa0 ?pb0 //=. -move=> c hc; case: eqVneq => p'c0 pc0; first by exists c. +move=> c hc; case: (altP (_ =P 0))=> //= p'c0 pc0; first by exists c. suff: { d : R | d \in `]a, c[ & (p^`()).[d] = 0 }. case=> [d hd] p'd0; exists d=> //. - by apply: subitvPr hd; rewrite /<=%O /= (itvP hc). -apply: ihn => //; [by rewrite (itvP hc) | exact/eqP |]. + by apply: subitvPr hd; rewrite bnd_simp (itvP hc). + apply: ihn => //; [by rewrite (itvP hc)|exact/eqP|]. move=> rs hrs srs urs rrs; apply: (max_roots (c :: rs))=> //=; last exact/andP. - move=> x; rewrite in_cons; case/predU1P=> [-> //|hx]. - by apply: subitvPr (hrs _ _); rewrite /<=%O //= (itvP hc). -by rewrite urs andbT; apply/negP; move/hrs; rewrite bound_in_itv. + move=> x; rewrite in_cons; case/predU1P=> hx; first by rewrite hx. + have: x \in `]a, c[ by apply: hrs. + by apply: subitvPr; rewrite bnd_simp (itvP hc). +by rewrite urs andbT; apply/negP => /hrs; rewrite bound_in_itv. Qed. -Theorem mvt a b p : - a < b -> {c | c \in `]a, b[ & p.[b] - p.[a] = p^`().[c] * (b - a)}. +Theorem poly_mvt a b p : a < b -> + {c | c \in `]a, b[ & p.[b] - p.[a] = p^`().[c] * (b - a)}. Proof. -move=> lab. pose q := (p.[b] - p.[a])%:P * ('X - a%:P) - (b - a)%:P * (p - p.[a]%:P). -case: (@rolle a b q) => // [|c lacb q'x0]. - by rewrite !hornerE !subrr !mulr0 mulrC !subrr. -exists c=> //; move/eqP: q'x0; rewrite !derivE !(mul0r,add0r,subr0,mulr1). -by rewrite !hornerE mulrC subr_eq0; move/eqP. +move=> lt_ab; have [//||c le_acb q'x0] := @poly_rolle a b q. + by rewrite /q !hornerE !(subrr,mulr0) mulrC subrr. +exists c=> //; move: q'x0; rewrite /q !derivE !(mul0r,add0r,subr0,mulr1). +by move/eqP; rewrite !hornerE mulrC subr_eq0; move/eqP. Qed. -Lemma ler_hornerW a b p : {in `]a, b[, forall x, p^`().[x] >= 0} -> +Lemma poly_lipshitz p a b : + { k | k >= 1 & {in `[a, b] &, forall x y, `|p.[y] - p.[x]| <= k * `|y - x| }}. +Proof. +have [ub p_le] := @poly_itv_bound _ p^`() a b; exists (1 + `|ub|). + by rewrite lerDl. +move=> x y xi yi; wlog lt_xy : x y xi yi / x < y => [hw|]. + set d := `|y - _|; have [/hw->//|xy|xy//] := ltrgtP x y; last first. + by rewrite /d xy !subrr normr0 mulr0. + by rewrite /d (distrC y) (distrC p.[y]) hw. +have [c ci ->] := poly_mvt p lt_xy; rewrite normrM ler_pM2r ?p_le //; last first. + by rewrite ?normr_gt0 ?subr_eq0 gt_eqF. +rewrite ler_wpDl // (le_trans _ (ler_norm _)) // p_le //. +by have: c \in `[a, b] by apply: subitvP ci; rewrite sub_oo_itv. +Qed. + +Lemma poly_cont x p e : e > 0 -> + exists2 d, d > 0 & forall y, `|y - x| < d -> `|p.[y] - p.[x]| < e. +Proof. +move=> e_gt0; have [k k_ge1 kP] := poly_lipshitz p (x - e) (x + e). +have k_gt0 : k > 0 by rewrite (lt_le_trans ltr01). +exists (e / k) => [|y]; first by rewrite mulr_gt0 ?invr_gt0. +have [y_small|y_big] := lerP `|y - x| e. + rewrite ltr_pdivl_mulr // mulrC; apply/le_lt_trans/kP => //; + by rewrite -![_ \in _]ler_distl ?subrr ?normr0 // ?ltW. +by move=> /(lt_trans y_big); rewrite ltr_pmulr // invf_gt1 // le_gtF. +Qed. + +Lemma ler_hornerW a b p : (forall x, x \in `]a, b[ -> p^`().[x] >= 0) -> {in `[a, b] &, {homo horner p : x y / x <= y}}. Proof. -move=> der_nneg x y axb ayb; rewrite le_eqVlt => /predU1P[->//|ltxy]. -have [c xcy /(canRL (@subrK _ _))->]:= mvt p ltxy. +move=> der_nneg x y axb ayb; rewrite le_eqVlt => /orP[/eqP->//|ltxy]. +have [c xcy /(canRL (@subrK _ _))->]:= poly_mvt p ltxy. rewrite ler_addr mulr_ge0 ?subr_ge0 ?(ltW ltxy) ?der_nneg //. -by apply: subitvP xcy; rewrite /<=%O /= /<=%O /= (itvP axb) (itvP ayb). +by apply: subitvP xcy; rewrite /(_ <= _)%O/= !bnd_simp ?(itvP axb) ?(itvP ayb). Qed. End Prelim. +Lemma le_itv (a a' b b' : itv_bound R) : + (Interval a b <= Interval a' b')%O = (a' <= a)%O && (b <= b')%O. +Proof. by []. Qed. + Section MonotonictyAndRoots. Section DerPos. -Variables (p : {poly R}) (a b : R). +Variable (p : {poly R}). -Hypothesis der_pos : {in `]a, b[, forall x, p^`().[x] > 0}. +Variables (a b : R). + +Hypothesis der_gt0 : forall x, x \in `]a, b[ -> (p^`()).[x] > 0. Lemma ltr_hornerW : {in `[a, b] &, {homo horner p : x y / x < y}}. Proof. -move=> x y axb ayb ltxy; have [c xcy /(canRL (@subrK _ _))->]:= mvt p ltxy. -rewrite ltr_addr mulr_gt0 ?subr_gt0 ?der_pos //. -by apply: subitvP xcy; rewrite /<=%O /= /<=%O /= (itvP axb) (itvP ayb). +move=> x y axb ayb ltxy; have [c xcy /(canRL (@subrK _ _))->]:= poly_mvt p ltxy. +rewrite ltr_addr mulr_gt0 ?subr_gt0 ?der_gt0 //. +apply: subitvP xcy; rewrite le_itv !bnd_simp. +by rewrite /= (itvP axb) (itvP ayb). Qed. Lemma ler_horner : {in `[a, b] &, {mono horner p : x y / x <= y}}. @@ -451,16 +517,17 @@ Proof. exact/le_mono_in/ltr_hornerW. Qed. Lemma ltr_horner : {in `[a, b] &, {mono horner p : x y / x < y}}. Proof. exact/leW_mono_in/ler_horner. Qed. +Lemma derp_inj : {in `[a, b] &, injective (horner p)}. +Proof. exact/inc_inj_in/ler_horner. Qed. + Lemma derpr x : x \in `]a, b] -> p.[x] > p.[a]. Proof. -move=> axb; rewrite ltr_horner ?(itvP axb) //. -by apply: subitvPl axb; rewrite bound_lexx. +by move=> axb; rewrite ltr_horner ?(itvP axb) // subset_itv_oc_cc. Qed. Lemma derpl x : x \in `[a, b[ -> p.[x] < p.[b]. Proof. -move=> axb; rewrite ltr_horner ?(itvP axb) //. -by apply: subitvPr axb; rewrite bound_lexx. +by move=> axb; rewrite ltr_horner ?(itvP axb) // subset_itv_co_cc. Qed. Lemma derprW x : x \in `[a, b] -> p.[x] >= p.[a]. @@ -468,76 +535,149 @@ Proof. by move=> axb; rewrite ler_horner ?(itvP axb). Qed. Lemma derplW x : x \in `[a, b] -> p.[x] <= p.[b]. Proof. by move=> axb; rewrite ler_horner ?(itvP axb). Qed. - End DerPos. Section NoRoot_sg. -Variables (p : {poly R}) (a b c : R). +Variable (p : {poly R}). +Variables (a b c : R). + +Hypothesis lt_ab : a < b. Hypothesis derp_neq0 : {in `]a, b[, noroot p^`()}. -Hypothesis acb : c \in `]a, b[. +Let mid_in : mid a b \in `]a, b[. Proof. exact: mid_in_itv. Qed. +Hint Resolve mid_in : core. + +Local Notation s := (p^`().[mid a b] < 0). +Local Notation sp' := ((- 1) ^+ s). +Let q := (sp' *: p). + +Lemma sgr_sign : sgr ((-1) ^+ s) = (-1) ^+ s :> R. +Proof. by case: s; rewrite ?(sgr1, sgrN1). Qed. + +Fact signpE : p = (sp' *: q). +Proof. by rewrite scalerA [_ ^+ _ * _]sqrr_sign scale1r. Qed. + +Fact sgp x : sgr p.[x] = sp' * sgr q.[x]. +Proof. by rewrite {1}signpE hornerZ sgrM sgr_sign. Qed. + +Fact derq_gt0 x : x \in `]a, b[ -> (q^`()).[x] > 0. +Proof. +move=> hx; rewrite derivZ hornerZ -sgr_cp0 neqr0_sign ?(derp_neq0 _) //. +rewrite sgrM sgr_id mulr_sg_eq1 ?derp_neq0 //=. +by apply/eqP; apply: (@polyrN0_itv `]a, b[). +Qed. +Hint Resolve derq_gt0 : core. + +Lemma lgtr_horner : {in `[a, b] &, forall x y, + p.[x] < p.[y] = (sp' * x < sp' * y)}. +Proof. +move=> x y axb ayb; rewrite /= [in LHS]signpE ![(_ *: q).[_]]hornerZ. +by case: s; rewrite ?mul1r ?mulN1r ?ltr_opp2 (ltr_horner derq_gt0). +Qed. -Local Notation sp'c := (sgr p^`().[c]). -Local Notation q := (sp'c *: p). +Lemma lger_horner : {in `[a, b] &, forall x y, + p.[x] <= p.[y] = (sp' * x <= sp' * y)}. +Proof. +move=> x y axb ayb; rewrite /= [in LHS]signpE ![(_ *: q).[_]]hornerZ. +by case: s; rewrite ?mul1r ?mulN1r ?ler_opp2 (ler_horner derq_gt0). +Qed. -Fact derq_pos x : x \in `]a, b[ -> (q^`()).[x] > 0. +Lemma horner_inj : {in `[a, b] &, injective (horner p)}. Proof. -move=> hx; rewrite derivZ hornerZ -sgr_cp0 sgr_smul mulr_sg_eq1 derp_neq0 //. -exact/eqP/(@polyrN0_itv `]a, b[). +move=> x y xab yab; rewrite signpE ![(_ *: q).[_]]hornerE. +by move=> /mulfI /(derp_inj derq_gt0)-> //; rewrite signr_eq0. Qed. -Definition derq0r := derpr derq_pos. -Definition derq0l := derpl derq_pos. -Definition derqpr := derprW derq_pos. -Definition derqnl := derplW derq_pos. -Fact sgp x : sgr p.[x] = sp'c * sgr q.[x]. -Proof. by rewrite hornerZ sgr_smul mulrA -expr2 sqr_sg derp_neq0 ?mul1r. Qed. +Lemma uniq_root : {in `[a, b] &, forall x y, root p x -> root p y -> x = y}. +Proof. by move=> x y ?? /eqP? /eqP rpy; apply: horner_inj; rewrite //rpy. Qed. + +Lemma sgrB (x y : R) : sgr (x - y) = (- 1) ^+ (x < y)%R *+ (x != y). +Proof. +case: ltrgtP => //= [xy|xy|->]; last by rewrite subrr sgr0. + by rewrite ltr0_sg ?subr_lt0. +by rewrite gtr0_sg ?subr_gt0. +Qed. -Fact hsgp x : 0 < q.[x] -> sgr p.[x] = sp'c. -Proof. by rewrite -sgr_cp0 sgp => /eqP->; rewrite mulr1. Qed. +Lemma root_sgp : {in `[a, b] &, forall x y, root p x -> + sgr p.[y] = (- 1) ^+ s * sgr (y - x)}. +Proof. +move=> x y xab yab rpx; rewrite {1}signpE hornerZ sgrM sgr_sign; congr (_ * _). +have rqx : root q x by rewrite /root hornerZ mulf_eq0 [p.[_] == _]rpx orbT. +rewrite sgrB; have [xy|xy|<-]/= := ltrgtP x y; last first. +- by rewrite hornerZ sgrM (eqP rpx) sgr0 mulr0. +- by apply/eqP; rewrite sgr_cp0 -(eqP rqx) (ltr_horner derq_gt0). +- by apply/eqP; rewrite sgr_cp0 -(eqP rqx) (ltr_horner derq_gt0). +Qed. -Fact hsgpN x : q.[x] < 0 -> sgr p.[x] = - sp'c. -Proof. by rewrite -sgr_cp0 sgp => /eqP->; rewrite mulrN1. Qed. -Lemma ders0r : p.[a] = 0 -> {in `]a, b], forall x, sgr p.[x] = sp'c}. +Lemma root_has_ivt r : r \in `[a, b] -> root p r -> + {in `[a, r] & `[r, b], forall x y, p.[x] * p.[y] <= 0}. Proof. -move=> pa0 x hx; rewrite hsgp // (le_lt_trans _ (derq0r _)) //. -by rewrite hornerZ pa0 mulr0. +move=> rab rpr x y xar yrb; rewrite -sgr_le0 sgrM. +have xab : x \in `[a, b] + by apply: subitvP xar; rewrite /= le_itv !bnd_simp ?(itvP rab). +have yab : y \in `[a, b] + by apply: subitvP yrb; rewrite /= le_itv !bnd_simp ?(itvP rab). +rewrite ?(root_sgp _ _ rpr)// mulrACA [_ ^+ _ * _]sqrr_sign mul1r -sgrM sgr_le0. +by rewrite mulr_le0_ge0 ?subr_ge0 ?subr_le0 ?(itvP xar) ?(itvP yrb). Qed. -Lemma derspr : sgr p.[a] = sp'c -> {in `[a, b], forall x, sgr p.[x] = sp'c}. +Lemma noroot_noivt : {in `[a, b], forall r, ~~ root p r} -> + {in `[a, b] &, forall x y, p.[x] * p.[y] > 0}. Proof. -move=> spa x hx; rewrite hsgp // (lt_le_trans _ (derqpr _)) //. -by rewrite -sgr_cp0 hornerZ sgr_smul spa -expr2 sqr_sg derp_neq0. +move=> rpr x y xar yrb; wlog lt_xy : x y xar yrb / x <= y => [hw|]. + by have /orP[/hw->//|/hw] := le_total x y; rewrite mulrC; apply. +rewrite ltNge; case: has_itv_rootP => // r _ r_in. +rewrite (negPf (rpr _ _)) //; apply: subitvP r_in; +by rewrite le_itv !bnd_simp /= ?(itvP xar) ?(itvP yrb). Qed. -Lemma ders0l : p.[b] = 0 -> {in `[a, b[, forall x, sgr p.[x] = -sp'c}. +Fact gtr0_sgp x : 0 < q.[x] -> sgr p.[x] = sp'. +Proof. by move=> qx_gt0; rewrite sgp gtr0_sg ?mulr1. Qed. + +Fact ltr0_sgpN x : q.[x] < 0 -> sgr p.[x] = - sp'. +Proof. by move=> qx_gt0; rewrite sgp ltr0_sg ?mulrN1. Qed. + +Lemma root_dersr : p.[a] = 0 -> {in `]a, b], forall x, sgr p.[x] = sp'}. Proof. -move=> pb0 x hx; rewrite hsgpN // (lt_le_trans (derq0l _)) //. -by rewrite hornerZ pb0 mulr0. +move=> pa0 x xab; have qa0 : q.[a] = 0 by rewrite hornerE pa0 mulr0. +by rewrite gtr0_sgp// -qa0 (derpr derq_gt0). Qed. -Lemma derspl : sgr p.[b] = -sp'c -> {in `[a, b], forall x, sgr p.[x] = -sp'c}. +Lemma derspr : sgr p.[a] = sp' -> {in `[a, b], forall x, sgr p.[x] = sp'}. Proof. -move=> spb x hx; rewrite hsgpN // (le_lt_trans (derqnl _)) //. -by rewrite -sgr_cp0 hornerZ sgr_smul spb mulrN -expr2 sqr_sg derp_neq0. +move=> pa_sp' x xab; rewrite gtr0_sgp// (lt_le_trans _ (derprW derq_gt0 _))//. +by rewrite hornerE -sgr_cp0 sgrM sgr_sign pa_sp' [_ * _]sqrr_sign. +Qed. + +Lemma root_dersl : p.[b] = 0 -> {in `[a, b[, forall x, sgr p.[x] = - sp'}. +Proof. +move=> pb0 x xab; have qb0 : q.[b] = 0 by rewrite hornerE pb0 mulr0. +by rewrite ltr0_sgpN// -qb0 (derpl derq_gt0). +Qed. + +Lemma derspl : sgr p.[b] = - sp' -> forall x, x \in `[a, b] -> sgr p.[x] = - sp'. +Proof. +move=> pbNsp' x xab; rewrite ltr0_sgpN// (le_lt_trans (derplW derq_gt0 _))//. +by rewrite hornerE -sgr_cp0 sgrM sgr_sign pbNsp' mulrN [_ * _]sqrr_sign. Qed. End NoRoot_sg. Section DerNeg. -Variables (p : {poly R}) (a b : R). +Variable (p : {poly R}). -Hypothesis der_neg : {in `]a, b[, forall x, (p^`()).[x] < 0}. +Variables (a b : R). -Let dern_pos x : x \in `]a, b[ -> ((- p)^`()).[x] > 0. +Hypothesis der_neg : forall x, x \in `]a, b[ -> (p^`()).[x] < 0. +Let dern_gt0 x : x \in `]a, b[ -> ((- p)^`()).[x] > 0. Proof. by move=> axb; rewrite derivN hornerN oppr_gt0 der_neg. Qed. Lemma gtr_hornerW : {in `[a, b] &, {homo horner p : x y /~ x < y}}. Proof. -by move=> x y axb ayb yx; rewrite -ltr_opp2 -!hornerN (ltr_hornerW dern_pos). +by move=> x y axb ayb yx; rewrite -ltr_opp2 -!hornerN (ltr_hornerW dern_gt0). Qed. Lemma ger_horner : {in `[a, b] &, {mono horner p : x y /~ x <= y}}. @@ -548,14 +688,12 @@ Proof. exact/leW_nmono_in/ger_horner. Qed. Lemma dernr x : x \in `]a, b] -> p.[x] < p.[a]. Proof. -move=> axb; rewrite gtr_horner ?(itvP axb) //. -by apply: subitvPl axb; rewrite bound_lexx. +by move=> axb; rewrite gtr_horner ?(itvP axb) //; apply: subset_itv_oc_cc. Qed. Lemma dernl x : x \in `[a, b[ -> p.[x] > p.[b]. Proof. -move=> axb; rewrite gtr_horner ?(itvP axb) //. -by apply: subitvPr axb; rewrite bound_lexx. +by move=> axb; rewrite gtr_horner ?(itvP axb) //; apply: subset_itv_co_cc. Qed. Lemma dernrW x : x \in `[a, b] -> p.[x] <= p.[a]. @@ -566,23 +704,22 @@ Proof. by move=> axb; rewrite ger_horner ?(itvP axb). Qed. End DerNeg. + Variable (p : {poly R}) (a b : R). Section der_root. Hypothesis der_pos : forall x, x \in `]a, b[ -> (p^`()).[x] > 0. -Lemma derp_root : a <= b -> 0 \in `]p.[a], p.[b][ -> +Lemma derp_root : a <= b -> p.[a] * p.[b] < 0 -> { r : R | [/\ forall x, x \in `[a, r[ -> p.[x] < 0, p.[r] = 0, r \in `]a, b[ & forall x, x \in `]r, b] -> p.[x] > 0] }. Proof. -move=> leab hpab. -have /eqP hs : sgr p.[a] * sgr p.[b] == -1. - by rewrite -sgrM sgr_cp0 pmulr_llt0 ?(itvP hpab). -case: (ivt_sign leab hs) => r arb pr0; exists r; split => //; last 2 first. +move=> leab hpab; have [r arb pr0] := poly_ivtoo leab hpab. +exists r; split => //; last 2 first. - by move/eqP: pr0. - move=> x rxb; have hd : forall t, t \in `]r, b[ -> 0 < (p^`()).[t]. by move=> t ht; rewrite der_pos // ?(subitvPl _ ht) /<=%O //= ?(itvP arb). @@ -594,32 +731,6 @@ Qed. End der_root. -(* Section der_root_sg. *) - -(* Hypothesis der_pos : forall x, x \in `]a, b[ -> (p^`()).[x] != 0. *) - -(* Lemma derp_root : a <= b -> sgr p.[a] != sgr p.[b] -> *) -(* { r : R | *) -(* [/\ forall x, x \in `[a, r[ -> p.[x] < 0, *) -(* p.[r] = 0, *) -(* r \in `]a, b[ & *) -(* forall x, x \in `]r, b] -> p.[x] > 0] }. *) -(* Proof. *) -(* move=> leab hpab. *) -(* have hs : sgr p.[a] * sgr p.[b] == -1. *) -(* by rewrite -sgrM sgr_cp0 mulr_lt0_gt0 ?(itvP hpab). *) -(* case: (ivt_sign ivt leab hs) => r arb pr0; exists r; split => //; last 2 first. *) -(* - by move/eqP: pr0. *) -(* - move=> x rxb; have hd : forall t, t \in `]r, b[ -> 0 < (p^`()).[t]. *) -(* by move=> t ht; rewrite der_pos // ?(subitvPl _ ht) //= ?(itvP arb). *) -(* by rewrite (derpr hd) ?(eqP pr0). *) -(* - move=> x rxb; have hd : forall t, t \in `]a, r[ -> 0 < (p^`()).[t]. *) -(* by move=> t ht; rewrite der_pos // ?(subitvPr _ ht) //= ?(itvP arb). *) -(* by rewrite (derpl hd) ?(eqP pr0). *) -(* Qed. *) - -(* End der_root. *) - End MonotonictyAndRoots. Section RootsOn. @@ -785,7 +896,8 @@ case: (lerP 0 p.[a]) => ha. case: (lerP p.[b] 0) => hb. left => x; case: (boolP (x \in _)) => //= axb; rewrite rootE lt_eqF //. by rewrite (lt_le_trans (derpl hp'pos _)) // (subitvPl _ axb) /<=%O /=. -case: (derp_root hp'pos (ltW leab) _) => [|r [h1 h2 h3] h4]; first exact/andP. +case: (derp_root hp'pos (ltW leab) _) => [|r [h1 h2 h3] h4]; + first by rewrite pmulr_llt0. right; exists r => x; rewrite in_cons in_nil (itv_splitUeq h3). have [->|exr] := eqVneq; rewrite ?orbT ?orbF /=; first by apply/eqP. case: rootP => px0; rewrite (andbT, andbF) //; apply/negP; case/orP=> hx. @@ -1422,39 +1534,42 @@ Proof. by rewrite /sgp_right size_poly0. Qed. Lemma sgr_neighpr b p x : {in neighpr p x b, forall y, (sgr p.[y] = sgp_right p x)}. Proof. -elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {}p. - rewrite leqn0 size_poly_eq0 /neighpr; move/eqP=> -> /= y. - by rewrite next_root0 itv_xx. -rewrite leq_eqVlt ltnS; case/predU1P => [sp|]; last exact: ihn. -rewrite /sgp_right sp /=; case px0: root=> /=; last first. - move=> y; rewrite /neighpr => hy /=. - apply/esym/(@polyrN0_itv `[x, y]) => [z||]; - do ?by rewrite bound_in_itv /<=%O /= (itvP hy). - rewrite (@itv_splitU _ _ (BRight x)) ?bound_lexx /<=%O /= ?(itvP hy) //. - rewrite itv_xx; case/predU1P=> hz; first by rewrite hz px0. +have [n] := ubnP (size p); elim: n => // -[_|n ihn] in p *; rewrite ltnS. + by move=> /size_poly_leq0P-> y; rewrite /neighpr next_root0 itv_xx. +rewrite leq_eqVlt ltnS; case/orP; last exact: ihn. +move/eqP=> sp; rewrite /sgp_right sp /=. +have pN0 : p != 0 by apply: contra_eq_neq sp => ->; rewrite size_poly0. +case px0: root=> /=; last first. + move=> y; rewrite /neighpr => hy /=; symmetry. + apply: (@polyrN0_itv `[x, y]); do ?by rewrite bound_in_itv ?bnd_simp /= (itvP hy). + move=> z; rewrite (@itv_splitU _ _ (BRight x)) + ?bound_in_itv /= ?bnd_simp ?(itvP hy) //. + rewrite itv_xx /=; case/predU1P=> hz; first by rewrite hz px0. rewrite (@next_noroot p x b) //. - by apply: subitvPr hz; rewrite /<=%O /= (itvP hy). + by apply: subitvPr hz=> /=; rewrite !bnd_simp (itvP hy). have <-: size p^`() = n by rewrite size_deriv sp. -rewrite -/(sgp_right p^`() x) /neighpr => y hy /=. -case: (@neighpr_wit (p * p^`()) x b)=> [||m]. -* case: next_rootP hy => [|? ? ? /itvP -> //|c p0 -> _]. - by rewrite itv_xx. - by case: leP; rewrite ?itv_xx. +rewrite -/(sgp_right p^`() x). +move=> y; rewrite /neighpr=> hy /=. +case: (@neighpr_wit (p * p^`()) x b)=> [||m hm]. +* case: next_rootP hy; first by rewrite itv_xx. + by move=> ? ? ?; move/itvP->. + by move=> c p0 -> _; case: lerP => _; rewrite ?itv_xx //; move/itvP->. * rewrite mulf_neq0 //. - by apply: contra_eq_neq sp => ->; rewrite size_poly0. - (* Todo : a lemma for this *) - apply: contra_eq_neq (size_deriv p) => ->; rewrite sp /=. + move: (size_deriv p); rewrite sp /=; move/eqP; apply: contraTneq=> ->. rewrite size_poly0; apply: contraTneq px0=> hn; rewrite -hn in sp. - by case/eqP/size_poly1P: sp => c nc0 ->; rewrite rootC. -* rewrite neighpr_mul; case/andP=> /= hmp hmp'. + by move/eqP: sp; case/size_poly1P=> c nc0 ->; rewrite rootC. +* move: hm; rewrite neighpr_mul /neighpr inE /=; case/andP=> hmp hmp'. + have lt_xm : x < m by rewrite (itvP hmp). rewrite (polyrN0_itv _ hmp) //; last exact: next_noroot. - rewrite (@ders0r p x m (mid x m)) ?(eqP px0) ?mid_in_itv ?bound_in_itv //; - rewrite /<=%O /= ?(itvP hmp) //; last first. + have midxmxb : mid x m \in neighpr p^`() x b. + rewrite (subitvP _ (@mid_in_itv _ false true _ _ _)) //=. + by rewrite ?lerr le_itv !bnd_simp (itvP hmp'). + rewrite (@root_dersr p x m) ?(eqP px0) ?mid_in_itv ?bound_in_itv //; + rewrite ?bnd_simp /= ?(itvP hmp) //; last first. move=> u hu /=; rewrite (@next_noroot _ x b) //. - by apply: subitvPr hu; rewrite /<=%O /= (itvP hmp'). - rewrite ihn ?size_deriv ?sp /neighpr //. - by rewrite (subitvP _ (@mid_in_itv _ false false _ _ _)); - rewrite /<=%O /= /<=%O //= ?lexx (itvP hmp'). + by apply: subitvPr hu; rewrite /= ?bnd_simp (itvP hmp'). + rewrite neqr0_sign// ?(@next_noroot _ x b)//. + by rewrite ihn ?size_deriv ?sp /neighpr. Qed. Lemma sgr_neighpl a p x : @@ -1462,44 +1577,45 @@ Lemma sgr_neighpl a p x : (sgr p.[y] = (-1) ^+ (odd (\mu_x p)) * sgp_right p x) }. Proof. -elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {}p. - rewrite leqn0 size_poly_eq0 /neighpl; move/eqP=> -> /= y. - by rewrite prev_root0 itv_xx. -rewrite leq_eqVlt ltnS; case/predU1P => [sp y|]; last exact: ihn. -rewrite /sgp_right sp /=; case px0: root=> /=; last first. - rewrite /neighpl => hy /=; symmetry. +have [n] := ubnP (size p); elim: n => // -[_|n ihn] in p *; rewrite ltnS. + by move=> /size_poly_leq0P-> y; rewrite /neighpl prev_root0 itv_xx. +rewrite leq_eqVlt ltnS; case/orP; last exact: ihn. +move/eqP=> sp; rewrite /sgp_right sp /=. +have pN0 : p != 0 by apply: contra_eq_neq sp => ->; rewrite size_poly0. +case px0: root=> /=; last first. + move=> y; rewrite /neighpl => hy /=; symmetry. move: (negbT px0); rewrite -mu_gt0; last first. - by apply: contraFneq px0 => ->; rewrite rootC. - rewrite -leqNgt leqn0; move/eqP ->; rewrite /= expr0 mul1r. - apply/esym/(@polyrN0_itv `[y, x]) => [z||]; - do ?by rewrite bound_in_itv /<=%O /= (itvP hy). - rewrite (@itv_splitU _ _ (BLeft x)) ?bound_lexx /<=%O /= ?(itvP hy) //. - rewrite itv_xx /= orbC; case/predU1P=> [->|hz]; first by rewrite px0. + by apply: contraFN px0; move/eqP->; rewrite rootC. + rewrite -leqNgt leqn0; move/eqP=> -> /=; rewrite expr0 mul1r. + symmetry; apply: (@polyrN0_itv `[y, x]); + do ?by rewrite bound_in_itv ?bnd_simp /= (itvP hy). + move=> z; rewrite (@itv_splitU _ _ (BLeft x)) ?bound_in_itv ?bnd_simp /= ?(itvP hy) //. + rewrite itv_xx /= orbC; case/predU1P=> hz; first by rewrite hz px0. rewrite (@prev_noroot p a x) //. - by apply: subitvPl hz; rewrite /<=%O /= (itvP hy). + by apply: subitvPl hz=> /=; rewrite bnd_simp (itvP hy). have <-: size p^`() = n by rewrite size_deriv sp. -rewrite -/(sgp_right p^`() x) /neighpl=> hy /=. -case: (@neighpl_wit (p * p^`()) a x)=> [||m]. +rewrite -/(sgp_right p^`() x). +move=> y; rewrite /neighpl=> hy /=. +case: (@neighpl_wit (p * p^`()) a x)=> [||m hm]. * case: prev_rootP hy; first by rewrite itv_xx. - by move=> ? ? ? /itvP ->. - by move=> c p0 -> _; case: ltP; rewrite ?itv_xx. + by move=> ? ? ?; move/itvP->. + by move=> c p0 -> _; case: lerP => _; rewrite ?itv_xx //; move/itvP->. * rewrite mulf_neq0 //. - by apply: contra_eq_neq sp => ->; rewrite size_poly0. - (* Todo : a lemma for this *) - apply: contra_eq_neq (size_deriv p) => ->; rewrite sp /=. + move: (size_deriv p); rewrite sp /=; move/eqP; apply: contraTneq=> ->. rewrite size_poly0; apply: contraTneq px0=> hn; rewrite -hn in sp. - by case/eqP/size_poly1P: sp => c nc0 ->; rewrite rootC. -* rewrite neighpl_mul; case/andP=> /= hmp hmp'. + by move/eqP: sp; case/size_poly1P=> c nc0 ->; rewrite rootC. +* move: hm; rewrite neighpl_mul /neighpl inE /=; case/andP=> hmp hmp'. + have lt_xm : m < x by rewrite (itvP hmp). + have midxmxb : mid m x \in neighpl p^`() a x. + rewrite (subitvP _ (@mid_in_itv _ false true _ _ _)) //= + ?le_itv ?bnd_simp (itvP hmp')//. rewrite (polyrN0_itv _ hmp) //; last exact: prev_noroot. - rewrite (@ders0l p m x (mid m x)) ?(eqP px0) ?mid_in_itv ?bound_in_itv; - rewrite /<=%O //= ?(itvP hmp) //; last first. + rewrite (@root_dersl p m x) ?(eqP px0) ?mid_in_itv ?bound_in_itv //; + rewrite /= ?bnd_simp ?(itvP hmp) //; last first. move=> u hu /=; rewrite (@prev_noroot _ a x) //. - by apply: subitvPl hu; rewrite /<=%O /= (itvP hmp'). - rewrite ihn ?size_deriv ?sp /neighpl //; last first. - by rewrite (subitvP _ (@mid_in_itv _ true true _ _ _)); - rewrite /<=%O /= /<=%O //= ?lexx (itvP hmp'). - rewrite mu_deriv // oddB ?mu_gt0 //=; last by rewrite -size_poly_eq0 sp. - by rewrite signr_addb /= mulrN1 mulNr opprK. + by apply: subitvPl hu; rewrite /= ?bnd_simp (itvP hmp'). + rewrite neqr0_sign ?(@prev_noroot _ a x)// ihn// ?size_deriv ?sp//. + by rewrite mu_deriv// oddB ?mu_gt0//= signr_addb mulrN1 mulNr opprK. Qed. Lemma sgp_right_deriv (p : {poly R}) x : @@ -1704,8 +1820,9 @@ Proof. move=> size_p_even. have [->|p_neq0] := eqVneq p 0; first by exists 0; rewrite root0. pose b := cauchy_bound p. -have [] := @ivt_sign p (-b) b; last by move=> x _; exists x. +have [] := @poly_ivtoo p (-b) b; last by move=> x _; exists x. by rewrite ge0_cp // ?cauchy_bound_ge0. +rewrite -sgr_cp0 sgrM. rewrite (sgp_minftyP (le_cauchy_bound p_neq0)) ?bound_in_itv //. rewrite (sgp_pinftyP (ge_cauchy_bound p_neq0)) ?bound_in_itv //. move: size_p_even; rewrite polySpred //= negbK /sgp_minfty -signr_odd => ->. @@ -1713,4 +1830,4 @@ by rewrite expr1 mulN1r sgrN mulNr -expr2 sqr_sg lead_coef_eq0 p_neq0. Qed. End PolyRCFPdiv. -End PolyRCF. +End PolyRCF. \ No newline at end of file diff --git a/theories/qe_rcf_th.v b/theories/qe_rcf_th.v index f51e648..37c54b5 100644 --- a/theories/qe_rcf_th.v +++ b/theories/qe_rcf_th.v @@ -1,12 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq choice path fintype. -From mathcomp -Require Import div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint. -From mathcomp -Require Import polyorder polyrcf interval matrix mxtens. +From mathcomp Require Import all_ssreflect all_algebra. +Require Import polyorder polyrcf mxtens. Set Implicit Arguments. Unset Strict Implicit. @@ -22,24 +17,6 @@ Section extra. Variable R : rcfType. Implicit Types (p q : {poly R}). - -(* Proof. *) -(* move=> sq; rewrite comp_polyE; case hp: (size p) => [|n]. *) -(* move/eqP: hp; rewrite size_poly_eq0 => /eqP ->. *) -(* by rewrite !big_ord0 mulr1 lead_coef0. *) -(* rewrite big_ord_recr /= addrC lead_coefDl. *) -(* by rewrite lead_coefZ lead_coef_exp // !lead_coefE hp. *) -(* rewrite (leq_ltn_trans (size_sum _ _ _)) // size_scale; last first. *) -(* rewrite -[n]/(n.+1.-1) -hp -lead_coefE ?lead_coef_eq0 //. *) -(* by rewrite -size_poly_eq0 hp. *) -(* rewrite polySpred ?ltnS ?expf_eq0; last first. *) -(* by rewrite andbC -size_poly_eq0 gtn_eqF // ltnW. *) -(* apply/bigmax_leqP => i _; rewrite size_exp. *) -(* have [->|/size_scale->] := eqVneq p`_i 0; first by rewrite scale0r size_poly0. *) -(* by rewrite (leq_trans (size_exp_leq _ _)) // ltn_mul2l -subn1 subn_gt0 sq /=. *) -(* Qed. *) - - Lemma mul2n n : (2 * n = n + n)%N. Proof. by rewrite mulSn mul1n. Qed. Lemma mul3n n : (3 * n = n + (n + n))%N. Proof. by rewrite !mulSn addn0. Qed. Lemma exp3n n : (3 ^ n)%N = (3 ^ n).-1.+1. @@ -148,9 +125,6 @@ rewrite leq_min mu_opp mu_mul ?mulf_neq0 ?qpq0 ?q0 // leq_addl. by rewrite mu_mulC // lcn_neq0. Qed. -(* Lemma sgp_right0 : forall (x : R), sgp_right 0 x = 0. *) -(* Proof. by move=> x; rewrite /sgp_right size_poly0. Qed. *) - End extra. Section ctmat. @@ -240,7 +214,7 @@ Notation midf a b := ((a + b) / 2%:~R). Local Notation sgp_is q s := (fun x => (sgr q.[x] == s)). Definition constraints (z : seq R) (sq : seq {poly R}) (sigma : seq int) := - (\sum_(x <- z) \prod_(i < size sq) (sgz (sq`_i).[x] == sigma`_i))%N. + (\sum_(x <- z) \prod_(i < size sq) (sgz (sq`_i).[x] == (sigma`_i)%R))%N. Definition taq (z : seq R) (q : {poly R}) : int := \sum_(x <- z) (sgz q.[x]). @@ -753,8 +727,7 @@ Lemma noroot_cross p a b : a <= b -> Proof. move=> le_ab noroot_ab; rewrite /cross /variation. have [] := ltrP; last by rewrite mulr0. -rewrite mulr1 -sgr_cp0 sgrM => /eqP. -by move=> /(ivt_sign le_ab) [x /noroot_ab /negPf->]. +by move=> /(poly_ivtoo le_ab) [x /noroot_ab /negPf->]. Qed. Lemma cross_pmul p q a b : q.[a] > 0 -> q.[b] > 0 -> @@ -1005,7 +978,7 @@ Qed. Lemma changes_itv_mods_rec a b : a < b -> forall p q, ~~ root (p * q) a -> ~~ root (p * q) b -> - changes_itv_mods a b p q = cross (p * q) a b + changes_itv_mods a b p q = cross (p * q) a b + changes_itv_mods a b q (next_mod p q). Proof. move=> lt_ab p q rpqa rpqb. @@ -1205,7 +1178,7 @@ move=> y2 _ rqy2 hy2xb hy2 q_neq0. have lty12 : y2 < y1. by apply: lt_trans (_ : x < _); rewrite 1?(itvP hy1xb) 1?(itvP hy2xb). have : q.[y2] = q.[y1] by rewrite rqy1 rqy2. -case/(rolle lty12) => z hz rz; constructor 3; exists z. +case/(poly_rolle lty12) => z hz rz; constructor 3; exists z. rewrite rz eqxx /= big_all; apply/allP => r r_sq. have xy : x \in `]y2, y1[ by rewrite in_itv /= 1?(itvP hy1xb) 1?(itvP hy2xb). rewrite -sgr_cp0 (@polyrN0_itv _ `]y2, y1[ _ _ x) ?sgr_cp0 ?hsq // => t. From 1ff4586cfeabc66dc16cc76397d6094f30205334 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 26 Mar 2024 10:10:35 +0100 Subject: [PATCH 2/2] mathcomp 2.1.0 and 2.2.0 renamings and Coq compat --- .github/workflows/docker-action.yml | 5 - .github/workflows/nix-action-8.16.yml | 461 -------------------------- .nix/config.nix | 7 - README.md | 4 +- _CoqProject | 1 + coq-mathcomp-real-closed.opam | 4 +- meta.yml | 18 +- theories/cauchyreals.v | 360 ++++++++++---------- theories/complex.v | 66 ++-- theories/polyrcf.v | 108 +++--- theories/qe_rcf_th.v | 2 +- theories/realalg.v | 223 +++++-------- 12 files changed, 366 insertions(+), 893 deletions(-) delete mode 100644 .github/workflows/nix-action-8.16.yml diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 110e731..9837315 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,13 +17,8 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.0.0-coq-8.16' - - 'mathcomp/mathcomp:2.0.0-coq-8.17' - - 'mathcomp/mathcomp:2.0.0-coq-8.18' - - 'mathcomp/mathcomp:2.1.0-coq-8.16' - 'mathcomp/mathcomp:2.1.0-coq-8.17' - 'mathcomp/mathcomp:2.1.0-coq-8.18' - - 'mathcomp/mathcomp:2.2.0-coq-8.16' - 'mathcomp/mathcomp:2.2.0-coq-8.17' - 'mathcomp/mathcomp:2.2.0-coq-8.18' - 'mathcomp/mathcomp:2.2.0-coq-8.19' diff --git a/.github/workflows/nix-action-8.16.yml b/.github/workflows/nix-action-8.16.yml deleted file mode 100644 index 88da2db..0000000 --- a/.github/workflows/nix-action-8.16.yml +++ /dev/null @@ -1,461 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.16\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "coq" - mathcomp: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.16\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp" - mathcomp-algebra-tactics: - needs: - - coq - - mathcomp-zify - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-algebra-tactics - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.16\" --argstr job \"mathcomp-algebra-tactics\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "coq-elpi" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-zify' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-zify" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-algebra-tactics" - mathcomp-bigenough: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-bigenough - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.16\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-bigenough" - mathcomp-finmap: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-finmap - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.16\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ - \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-finmap" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-real-closed - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.16\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-real-closed" - mathcomp-zify: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-zify - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.16\" --argstr job \"mathcomp-zify\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-zify" -name: Nix CI for bundle 8.16 -'on': - pull_request: - paths: - - .github/workflows/nix-action-8.16.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-8.16.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.nix/config.nix b/.nix/config.nix index e107c2a..51173d4 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -47,13 +47,6 @@ mathcomp-zify.override.version = "master"; multinomials.override.version = "master"; }; in { - "8.16".coqPackages = common-bundles // { - coq.override.version = "8.16"; - mathcomp.override.version = "2.0.0"; - multinomials.job = false; # broken with dune on 8.16 in nixpkgs - coqeal.job = false; - mathcomp-apery.job = false; - }; "8.17".coqPackages = common-bundles // { coq.override.version = "8.17"; mathcomp.override.version = "2.1.0"; diff --git a/README.md b/README.md index f68793c..a68c7e2 100644 --- a/README.md +++ b/README.md @@ -24,9 +24,9 @@ order theory of real closed field, through quantifier elimination. - Cyril Cohen (initial) - Assia Mahboubi (initial) - License: [CeCILL-B](CECILL-B) -- Compatible Coq versions: Coq 8.16 or later +- Compatible Coq versions: Coq 8.17 or later - Additional dependencies: - - [MathComp ssreflect 2.0 or later](https://math-comp.github.io) + - [MathComp ssreflect 2.1 or later](https://math-comp.github.io) - [MathComp algebra](https://math-comp.github.io) - [MathComp field](https://math-comp.github.io) - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough) diff --git a/_CoqProject b/_CoqProject index c44e700..151b11e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -18,3 +18,4 @@ theories/mxtens.v -arg -w -arg +undeclared-scope -arg -w -arg -ambiguous-paths -arg -w -arg -uniform-inheritance +-arg -w -arg -deprecated-since-8.19 diff --git a/coq-mathcomp-real-closed.opam b/coq-mathcomp-real-closed.opam index 22341c7..545b3a3 100644 --- a/coq-mathcomp-real-closed.opam +++ b/coq-mathcomp-real-closed.opam @@ -21,8 +21,8 @@ order theory of real closed field, through quantifier elimination.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {>= "8.16"} - "coq-mathcomp-ssreflect" {>= "2.0"} + "coq" {>= "8.17"} + "coq-mathcomp-ssreflect" {>= "2.1"} "coq-mathcomp-algebra" "coq-mathcomp-field" "coq-mathcomp-bigenough" {>= "1.0.0"} diff --git a/meta.yml b/meta.yml index 55ee65f..be363f4 100644 --- a/meta.yml +++ b/meta.yml @@ -39,24 +39,14 @@ license: file: CECILL-B supported_coq_versions: - text: Coq 8.16 or later - opam: '{>= "8.16"}' + text: Coq 8.17 or later + opam: '{>= "8.17"}' tested_coq_opam_versions: -- version: '2.0.0-coq-8.16' - repo: 'mathcomp/mathcomp' -- version: '2.0.0-coq-8.17' - repo: 'mathcomp/mathcomp' -- version: '2.0.0-coq-8.18' - repo: 'mathcomp/mathcomp' -- version: '2.1.0-coq-8.16' - repo: 'mathcomp/mathcomp' - version: '2.1.0-coq-8.17' repo: 'mathcomp/mathcomp' - version: '2.1.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '2.2.0-coq-8.16' - repo: 'mathcomp/mathcomp' - version: '2.2.0-coq-8.17' repo: 'mathcomp/mathcomp' - version: '2.2.0-coq-8.18' @@ -77,9 +67,9 @@ tested_coq_opam_versions: dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{>= "2.0"}' + version: '{>= "2.1"}' description: |- - [MathComp ssreflect 2.0 or later](https://math-comp.github.io) + [MathComp ssreflect 2.1 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra description: |- diff --git a/theories/cauchyreals.v b/theories/cauchyreals.v index 8fcda25..8be0693 100644 --- a/theories/cauchyreals.v +++ b/theories/cauchyreals.v @@ -73,7 +73,7 @@ Proof. have [r_ge0|r_lt0] := lerP 0 r; last first. by move=> hr; have := le_lt_trans hr r_lt0; rewrite normr_lt0. rewrite ler_distl=> /andP[lx ux]. -rewrite ler_paddl //. +rewrite ler_wpDl //. elim/poly_ind: p=> [|p c ihp]. by rewrite horner0 normr0 size_poly0 big_ord0. rewrite hornerMXaddC size_MXaddC. @@ -81,25 +81,25 @@ have [->|p_neq0 /=] := altP eqP. rewrite horner0 !mul0r !add0r size_poly0. have [->|c_neq0] /= := altP eqP; first by rewrite normr0 big_ord0. rewrite big_ord_recl big_ord0 addr0 coefC /=. - by rewrite ler_pmulr ?normr_gt0 // ler_addl ler_maxr !normr_ge0. + by rewrite ler_pMr ?normr_gt0 // lerDl ler_maxr !normr_ge0. rewrite big_ord_recl coefD coefMX coefC eqxx add0r. -rewrite (le_trans (ler_norm_add _ _)) // addrC ler_add //. +rewrite (le_trans (ler_normD _ _)) // addrC lerD //. by rewrite expr0 mulr1. rewrite normrM. -move: ihp=> /(ler_wpmul2r (normr_ge0 x)) /le_trans-> //. +move: ihp=> /(ler_wpM2r (normr_ge0 x)) /le_trans-> //. rewrite mulr_suml ler_sum // => i _. rewrite coefD coefC coefMX /= addr0 exprSr mulrA. -rewrite ler_wpmul2l //. +rewrite ler_wpM2l //. by rewrite ?mulr_ge0 ?exprn_ge0 ?ler_maxr ?addr_ge0 ?normr_ge0 // ltrW. rewrite (ger0_norm r_ge0) ler_norml opprD. -rewrite (le_trans _ lx) ?(le_trans ux) // ler_add2r. +rewrite (le_trans _ lx) ?(le_trans ux) // lerD2r. by rewrite ler_normr lexx. -by rewrite ler_oppl ler_normr lexx orbT. +by rewrite lerNl ler_normr lexx orbT. Qed. Lemma poly_bound_gt0 p a r : 0 < poly_bound p a r. Proof. -rewrite ltr_paddr // sumr_ge0 // => i _. +rewrite ltr_wpDr // sumr_ge0 // => i _. by rewrite mulr_ge0 ?exprn_ge0 ?addr_ge0 ?ler_maxr ?normr_ge0 // ltrW. Qed. @@ -118,8 +118,8 @@ have [|r_lt0] := lerP 0 r; last first. by move=> hr; have := le_lt_trans hr r_lt0; rewrite normr_lt0. rewrite le0r=> /orP[/eqP->|r_gt0 hx hy]. by rewrite !normr_le0 !subr_eq0=> /eqP-> /eqP->; rewrite !subrr normr0 mul0r. -rewrite mulrA mulrDr mulr1 ler_paddl ?mulr_ge0 ?normr_ge0 //=. - by rewrite exprn_ge0 ?le_maxr ?mulr_ge0 ?ger0E ?ltW. +rewrite mulrA mulrDr mulr1 ler_wpDl ?mulr_ge0 ?normr_ge0 //=. + by rewrite exprn_ge0 ?le_max ?mulr_ge0 ?ger0E ?ltW. rewrite -{1}(addNKr x y) [- _ + _]addrC /= -mulrA. rewrite nderiv_taylor; last exact: mulrC. have [->|p_neq0] := eqVneq p 0. @@ -129,29 +129,29 @@ rewrite -[size _]prednK ?lt0n ?size_poly_eq0 //. rewrite big_ord_recl expr0 mulr1 nderivn0 addrC addKr !mulr_sumr. have := le_trans (ler_norm_sum _ _ _); apply. rewrite ler_sum // => i _. -rewrite exprSr mulrA !normrM mulrC ler_wpmul2l ?normr_ge0 //. -suff /ler_wpmul2l /le_trans : +rewrite exprSr mulrA !normrM mulrC ler_wpM2l ?normr_ge0 //. +suff /ler_wpM2l /le_trans : `|(y - x) ^+ i| <= maxr 1 (2%:R * r) ^+ (size p).-1. - apply; rewrite ?normr_ge0 // mulrC ler_wpmul2l ?poly_boundP //. - by rewrite ?exprn_ge0 // le_maxr ler01 mulr_ge0 ?ler0n ?ltW. + apply; rewrite ?normr_ge0 // mulrC ler_wpM2l ?poly_boundP //. + by rewrite ?exprn_ge0 // le_max ler01 mulr_ge0 ?ler0n ?ltW. case: (leP _ 1)=> hr. rewrite expr1n normrX exprn_ile1 ?normr_ge0 //. - rewrite (le_trans (ler_dist_add a _ _)) // addrC distrC. - by rewrite (le_trans _ hr) // mulrDl ler_add ?mul1r. + rewrite (le_trans (ler_distD a _ _)) // addrC distrC. + by rewrite (le_trans _ hr) // mulrDl lerD ?mul1r. apply: le_trans (_ : (2%:R * r) ^+ i <= _). - rewrite normrX ler_expn2r -?topredE /= ?normr_ge0 ?mulr_ge0 ?ler0n //. + rewrite normrX lerXn2r -?topredE /= ?normr_ge0 ?mulr_ge0 ?ler0n //. by rewrite ltW. - rewrite (le_trans (ler_dist_add a _ _)) // addrC distrC. - by rewrite mulrDl ler_add ?mul1r. -by rewrite ler_eexpn2l // ltnW. + rewrite (le_trans (ler_distD a _ _)) // addrC distrC. + by rewrite mulrDl lerD ?mul1r. +by rewrite ler_eXn2l // ltnW. Qed. Lemma poly_accr_bound_gt0 p a r : 0 < poly_accr_bound p a r. Proof. rewrite /poly_accr_bound pmulr_rgt0 //. - rewrite ltr_paddr ?ltr01 //. + rewrite ltr_wpDr ?ltr01 //. by rewrite sumr_ge0 // => i; rewrite poly_bound_ge0. -by rewrite exprn_gt0 // lt_maxr ltr01 pmulr_rgt0 ?ltr0n. +by rewrite exprn_gt0 // lt_max ltr01 pmulr_rgt0 ?ltr0n. Qed. Lemma poly_accr_bound_ge0 p a r : 0 <= poly_accr_bound p a r. @@ -211,9 +211,9 @@ Definition poly_accr_bound2 (p : {poly F}) (a r : F) : F Lemma poly_accr_bound2_gt0 p a r : 0 < poly_accr_bound2 p a r. Proof. rewrite /poly_accr_bound pmulr_rgt0 //. - rewrite ltr_paddr ?ltr01 //. + rewrite ltr_wpDr ?ltr01 //. by rewrite sumr_ge0 // => i; rewrite poly_bound_ge0. -by rewrite exprn_gt0 // lt_maxr ltr01 pmulr_rgt0 ?ltr0n. +by rewrite exprn_gt0 // lt_max ltr01 pmulr_rgt0 ?ltr0n. Qed. Lemma poly_accr_bound2_ge0 p a r : 0 <= poly_accr_bound2 p a r. @@ -230,8 +230,8 @@ rewrite le0r=> /orP[/eqP->|r_gt0]. rewrite !normr_le0 !subr_eq0. by move=> nxy /eqP xa /eqP xb; rewrite xa xb eqxx in nxy. move=> neq_xy hx hy. -rewrite mulrA mulrDr mulr1 ler_paddl ?mulr_ge0 ?normr_ge0 //=. - by rewrite exprn_ge0 ?le_maxr ?mulr_ge0 ?ger0E ?ltW. +rewrite mulrA mulrDr mulr1 ler_wpDl ?mulr_ge0 ?normr_ge0 //=. + by rewrite exprn_ge0 ?le_max ?mulr_ge0 ?ger0E ?ltW. rewrite -{1}(addNKr x y) [- _ + _]addrC /= -mulrA. rewrite nderiv_taylor; last exact: mulrC. have [->|p_neq0] := eqVneq p 0. @@ -243,25 +243,25 @@ have [->|p'_neq0] := eqVneq p^`() 0. rewrite -[size _]prednK ?lt0n ?size_poly_eq0 // big_ord_recl expr1. rewrite addrAC subrr add0r mulrDl mulfK; last by rewrite subr_eq0 eq_sym. rewrite nderivn1 addrAC subrr add0r mulr_sumr normrM normfV. -rewrite ler_pdivr_mulr ?normr_gt0; last by rewrite subr_eq0 eq_sym. +rewrite ler_pdivrMr ?normr_gt0; last by rewrite subr_eq0 eq_sym. rewrite mulrAC -expr2 mulrC mulr_suml. have := le_trans (ler_norm_sum _ _ _); apply. rewrite ler_sum // => i _ /=; rewrite /bump /= !add1n. -rewrite normrM normrX 3!exprSr expr1 !mulrA !ler_wpmul2r ?normr_ge0 //. -suff /ler_wpmul2l /le_trans : +rewrite normrM normrX 3!exprSr expr1 !mulrA !ler_wpM2r ?normr_ge0 //. +suff /ler_wpM2l /le_trans : `|(y - x)| ^+ i <= maxr 1 (2%:R * r) ^+ (size p^`()).-1. - apply; rewrite ?normr_ge0 // mulrC ler_wpmul2l ?poly_boundP //. - by rewrite ?exprn_ge0 // le_maxr ler01 mulr_ge0 ?ler0n ?ltW. + apply; rewrite ?normr_ge0 // mulrC ler_wpM2l ?poly_boundP //. + by rewrite ?exprn_ge0 // le_max ler01 mulr_ge0 ?ler0n ?ltW. case: (leP _ 1)=> hr. rewrite expr1n exprn_ile1 ?normr_ge0 //. - rewrite (le_trans (ler_dist_add a _ _)) // addrC distrC. - by rewrite (le_trans _ hr) // mulrDl ler_add ?mul1r. + rewrite (le_trans (ler_distD a _ _)) // addrC distrC. + by rewrite (le_trans _ hr) // mulrDl lerD ?mul1r. apply: le_trans (_ : (2%:R * r) ^+ i <= _). - rewrite ler_expn2r -?topredE /= ?normr_ge0 ?mulr_ge0 ?ler0n //. + rewrite lerXn2r -?topredE /= ?normr_ge0 ?mulr_ge0 ?ler0n //. by rewrite ltW. - rewrite (le_trans (ler_dist_add a _ _)) // addrC distrC. - by rewrite mulrDl ler_add ?mul1r. -by rewrite ler_eexpn2l // ltnW. + rewrite (le_trans (ler_distD a _ _)) // addrC distrC. + by rewrite mulrDl lerD ?mul1r. +by rewrite ler_eXn2l // ltnW. Qed. End polyorder_field_extra. @@ -314,7 +314,7 @@ Lemma accr_negN p a r : accr_pos p a r -> accr_neg (- p) a r. Proof. case=> [[k k_gt0 hk] h]. split; [ exists k=> // x y nxy hx hy; - by rewrite !hornerN -opprD mulNr ltr_opp2; apply: hk + by rewrite !hornerN -opprD mulNr ltrN2; apply: hk | by move=> x hx; rewrite derivN hornerN oppr_lt0; apply: h ]. Qed. @@ -322,7 +322,7 @@ Lemma accr_posN p a r : accr_neg p a r -> accr_pos (- p) a r. Proof. case=> [[k k_gt0 hk] h]. split; [ exists k=> // x y nxy hx hy; - by rewrite !hornerN -opprD mulNr ltr_oppr; apply: hk + by rewrite !hornerN -opprD mulNr ltrNr; apply: hk | by move=> x hx; rewrite derivN hornerN oppr_gt0; apply: h ]. Qed. @@ -335,8 +335,8 @@ Lemma strong_mono_bound p a r : strong_mono p a r Proof. case=> [] [[k k_gt0 hk] _]; exists k^-1; rewrite ?invr_gt0=> // x y hx hy; have [->|neq_xy] := eqVneq x y; do ?[by rewrite !subrr normr0 mulr0]; -move: (hk _ _ neq_xy hx hy); rewrite 1?ltr_oppr ler_pdivl_mull //; -rewrite -ler_pdivl_mulr ?normr_gt0 ?subr_eq0 // => /ltW /le_trans-> //; +move: (hk _ _ neq_xy hx hy); rewrite 1?ltrNr ler_pdivlMl //; +rewrite -ler_pdivlMr ?normr_gt0 ?subr_eq0 // => /ltW /le_trans-> //; by rewrite -normfV -normrM ler_normr lexx ?orbT. Qed. @@ -355,21 +355,21 @@ Proof. move=> r1_gt0 r2_gt0 le_ar. rewrite /merge_intervals /=. set l : F := minr _ _; set u : F := maxr _ _. -rewrite ler_pdivl_mulr ?gtr0E // -{2}[2%:R]ger0_norm ?ger0E //. +rewrite ler_pdivlMr ?gtr0E // -{2}[2%:R]ger0_norm ?ger0E //. rewrite -normrM mulrBl mulfVK ?pnatr_eq0 // ler_distl. rewrite opprB addrCA addrK (addrC (l + u)) addrA addrNK. -rewrite -!mulr2n !mulr_natr !ler_muln2r !orFb. -rewrite le_minl le_maxr !ler_distl /=. +rewrite -!mulr2n !mulr_natr !lerMn2r !orFb. +rewrite ge_min le_max !ler_distl /=. set le := <=%R; rewrite {}/le. have [] := lerP=> /= a1N; have [] := lerP=> //= a1P; have [] := lerP=> //= a2P; rewrite ?(andbF, andbT) //; symmetry. rewrite ltW // (le_lt_trans _ a1P) //. - rewrite (monoLR (addrK _) (ler_add2r _)) -addrA. - rewrite (monoRL (addNKr _) (ler_add2l _)) addrC. + rewrite (monoLR (addrK _) (lerD2r _)) -addrA. + rewrite (monoRL (addNKr _) (lerD2l _)) addrC. by rewrite (le_trans _ le_ar) // ler_normr opprB lexx orbT. rewrite ltW // (lt_le_trans a1N) //. -rewrite (monoLR (addrK _) (ler_add2r _)) -addrA. -rewrite (monoRL (addNKr _) (ler_add2l _)) addrC ?[r2 + _]addrC. +rewrite (monoLR (addrK _) (lerD2r _)) -addrA. +rewrite (monoRL (addNKr _) (lerD2l _)) addrC ?[r2 + _]addrC. by rewrite (le_trans _ le_ar) // ler_normr lexx. Qed. @@ -392,21 +392,21 @@ move=> [] accr2_p; last first. suff: 0 < 0 :> F by rewrite ltxx. have r_gt0 : 0 < r1 + r2 by rewrite ?addr_gt0. apply: (lt_trans (pm_gt0 _) (pm_lt0 _)). - rewrite -(@ler_pmul2l _ (r1 + r2)) //. + rewrite -(@ler_pM2l _ (r1 + r2)) //. rewrite -{1}[r1 + r2]ger0_norm ?(ltW r_gt0) //. rewrite -normrM mulrBr /m mulrC mulrVK ?unitfE ?gt_eqF //. rewrite mulrDl opprD addrA addrC addrA addKr. rewrite distrC -mulrBr normrM ger0_norm ?(ltW r1_gt0) //. - by rewrite mulrC ler_wpmul2r // ltW. - rewrite -(@ler_pmul2l _ (r1 + r2)) //. + by rewrite mulrC ler_wpM2r // ltW. + rewrite -(@ler_pM2l _ (r1 + r2)) //. rewrite -{1}[r1 + r2]ger0_norm ?(ltW r_gt0) //. rewrite -normrM mulrBr /m mulrC mulrVK ?unitfE ?gt_eqF //. rewrite mulrDl opprD addrA addrK. rewrite -mulrBr normrM ger0_norm ?(ltW r2_gt0) //. - by rewrite mulrC ler_wpmul2r // ltW. + by rewrite mulrC ler_wpM2r // ltW. case: accr2_p=> [[k2 k2_gt0 hk2]] h2. left; split; last by move=> x; rewrite split_interval // => /orP [/h1|/h2]. -exists (minr k1 k2); first by rewrite lt_minr k1_gt0. +exists (minr k1 k2); first by rewrite lt_min k1_gt0. move=> x y neq_xy; rewrite !split_interval //. wlog lt_xy: x y neq_xy / y < x. move=> hwlog; have [] := ltrP y x; first exact: hwlog. @@ -421,36 +421,36 @@ wlog le_xr1 : a1 a2 r1 r2 k1 k2 by apply: hwlog'; rewrite 1?orbC // distrC [r2 + _]addrC. move=> _. have [le_yr1|gt_yr1] := (lerP _ r1)=> /= [_|le_yr2]. - by rewrite lt_minl hk1. -rewrite ltr_pdivl_mulr ?subr_gt0 //. + by rewrite gt_min hk1. +rewrite ltr_pdivlMr ?subr_gt0 //. pose z := a1 - r1. have hz1 : `|z - a1| <= r1 by rewrite addrC addKr normrN gtr0_norm. have gt_yr1' : y + r1 < a1. rewrite addrC; move: gt_yr1. - rewrite (monoLR (addrNK _) (ltr_add2r _)). + rewrite (monoLR (addrNK _) (ltrD2r _)). rewrite /z ltr_normr opprB=> /orP[|-> //]. - rewrite (monoRL (addrK a1) (ltr_add2r _))=> /lt_trans /(_ lt_xy). + rewrite (monoRL (addrK a1) (ltrD2r _))=> /lt_trans /(_ lt_xy). by rewrite ltNge addrC; move: le_xr1; rewrite ler_distl=> /andP [_ ->]. -have lt_yz : y < z by rewrite (monoRL (addrK _) (ltr_add2r _)). +have lt_yz : y < z by rewrite (monoRL (addrK _) (ltrD2r _)). have hz2 : `|z - a2| <= r2. move: (har); rewrite ler_norml=> /andP [la ua]. rewrite addrAC ler_distl ua andbT. rewrite -[a1](addrNK y) -[_ - _ + _ - _]addrA. - rewrite ler_add //. - by rewrite (monoRL (addrK _) (ler_add2r _)) addrC ltW. + rewrite lerD //. + by rewrite (monoRL (addrK _) (lerD2r _)) addrC ltW. by move: le_yr2; rewrite ler_norml=> /andP[]. have [<-|neq_zx] := eqVneq z x. - by rewrite -ltr_pdivl_mulr ?subr_gt0 // lt_minl hk2 ?orbT // gt_eqF. + by rewrite -ltr_pdivlMr ?subr_gt0 // gt_min hk2 ?orbT // gt_eqF. have lt_zx : z < x. rewrite lt_neqAle neq_zx /=. move: le_xr1; rewrite distrC ler_norml=> /andP[_]. - by rewrite !(monoLR (addrK _) (ler_add2r _)) addrC. + by rewrite !(monoLR (addrK _) (lerD2r _)) addrC. rewrite -{1}[x](addrNK z) -{1}[p.[x]](addrNK p.[z]). -rewrite !addrA -![_ - _ + _ - _]addrA mulrDr ltr_add //. - rewrite -ltr_pdivl_mulr ?subr_gt0 //. - by rewrite lt_minl hk1 ?gt_eqF. -rewrite -ltr_pdivl_mulr ?subr_gt0 //. -by rewrite lt_minl hk2 ?orbT ?gt_eqF. +rewrite !addrA -![_ - _ + _ - _]addrA mulrDr ltrD //. + rewrite -ltr_pdivlMr ?subr_gt0 //. + by rewrite gt_min hk1 ?gt_eqF. +rewrite -ltr_pdivlMr ?subr_gt0 //. +by rewrite gt_min hk2 ?orbT ?gt_eqF. Qed. End monotony. @@ -487,7 +487,7 @@ Variable F : realFieldType. (* {asympt e : i / P e i} -> {asympt e : i / P (e * k) i}. *) (* Proof. *) (* case=> m hm; exists (fun e => m (e * k))=> e i he hi. *) -(* by apply: hm=> //; rewrite -ltr_pdivr_mulr // mul0r. *) +(* by apply: hm=> //; rewrite -ltr_pdivrMr // mul0r. *) (* Qed. *) (* Lemma asympt_mulRL (k : F) (hk : 0 < k) (P : F -> nat -> Prop) : *) @@ -495,7 +495,7 @@ Variable F : realFieldType. (* Proof. *) (* case=> m hm; exists (fun e => m (e / k))=> e i he hi. *) (* rewrite -[e](@mulfVK _ k) ?gtr_eqF //. *) -(* by apply: hm=> //; rewrite -ltr_pdivr_mulr ?invr_gt0 // mul0r. *) +(* by apply: hm=> //; rewrite -ltr_pdivrMr ?invr_gt0 // mul0r. *) (* Qed. *) Lemma asymptP (P1 : F -> nat -> Prop) (P2 : F -> nat -> Prop) : @@ -509,7 +509,7 @@ Qed. (* {asympt e : i j / P e i j} -> {asympt e : i j / P (e * k) i j}. *) (* Proof. *) (* case=> m hm; exists (fun e => m (e * k))=> e i j he hi hj. *) -(* by apply: hm=> //; rewrite -ltr_pdivr_mulr // mul0r. *) +(* by apply: hm=> //; rewrite -ltr_pdivrMr // mul0r. *) (* Qed. *) (* Lemma asympt2_mulRL (k : F) (hk : 0 < k) (P : F -> nat -> nat -> Prop) : *) @@ -517,7 +517,7 @@ Qed. (* Proof. *) (* case=> m hm; exists (fun e => m (e / k))=> e i j he hi hj. *) (* rewrite -[e](@mulfVK _ k) ?gtr_eqF //. *) -(* by apply: hm=> //; rewrite -ltr_pdivr_mulr ?invr_gt0 // mul0r. *) +(* by apply: hm=> //; rewrite -ltr_pdivrMr ?invr_gt0 // mul0r. *) (* Qed. *) (* Lemma asympt2P (P1 : F -> nat -> nat -> Prop) (P2 : F -> nat -> nat -> Prop) : *) @@ -537,23 +537,23 @@ by elim: n=> /= [|n <-]; rewrite !mulr_natr ?mulr1n. Qed. Lemma splitD (x y e : F) : x < e / 2%:R -> y < e / 2%:R -> x + y < e. -Proof. by move=> hx hy; rewrite [e](splitf 2) ltr_add. Qed. +Proof. by move=> hx hy; rewrite [e](splitf 2) ltrD. Qed. Lemma divrn_gt0 (e : F) (n : nat) : 0 < e -> (0 < n)%N -> 0 < e / n%:R. Proof. by move=> e_gt0 n_gt0; rewrite pmulr_rgt0 ?gtr0E. Qed. Lemma split_norm_add (x y e : F) : `|x| < e / 2%:R -> `|y| < e / 2%:R -> `|x + y| < e. -Proof. by move=> hx hy; rewrite (le_lt_trans (ler_norm_add _ _)) // splitD. Qed. +Proof. by move=> hx hy; rewrite (le_lt_trans (ler_normD _ _)) // splitD. Qed. Lemma split_norm_sub (x y e : F) : `|x| < e / 2%:R -> `|y| < e / 2%:R -> `|x - y| < e. -Proof. by move=> hx hy; rewrite (le_lt_trans (ler_norm_sub _ _)) // splitD. Qed. +Proof. by move=> hx hy; rewrite (le_lt_trans (ler_normB _ _)) // splitD. Qed. Lemma split_dist_add (z x y e : F) : `|x - z| < e / 2%:R -> `|z - y| < e / 2%:R -> `|x - y| < e. Proof. -by move=> *; rewrite (le_lt_trans (ler_dist_add z _ _)) ?splitD // 1?distrC. +by move=> *; rewrite (le_lt_trans (ler_distD z _ _)) ?splitD // 1?distrC. Qed. Definition creal_axiom (x : nat -> F) := {asympt e : i j / `|x i - x j| < e}. @@ -585,8 +585,8 @@ Lemma ltr_distl_creal (e : F) (i : nat) (x : creal) (j : nat) (a b : F) : `| x i - a | <= b - e -> `| x j - a | < b. Proof. move=> e_gt0 hi hj hb. -rewrite (le_lt_trans (ler_dist_add (x i) _ _)) ?ltr_le_add //. -by rewrite -[b](addrNK e) addrC ler_lt_add ?cauchymodP. +rewrite (le_lt_trans (ler_distD (x i) _ _)) ?ltr_leD //. +by rewrite -[b](addrNK e) addrC ler_ltD ?cauchymodP. Qed. Lemma ltr_distr_creal (e : F) (i : nat) (x : creal) (j : nat) (a b : F) : @@ -741,7 +741,7 @@ Lemma ltr_creal (e : F) (i : nat) (x : creal) (j : nat) (a : F) : Proof. move=> e_gt0 hi hj ha; have := cauchymodP e_gt0 hj hi. rewrite ltr_distl=> /andP[_ /lt_le_trans-> //]. -by rewrite -(ler_add2r (- e)) addrK. +by rewrite -(lerD2r (- e)) addrK. Qed. Lemma gtr_creal (e : F) (i : nat) (x : creal) (j : nat) (a : F) : @@ -750,7 +750,7 @@ Lemma gtr_creal (e : F) (i : nat) (x : creal) (j : nat) (a : F) : Proof. move=> e_gt0 hi hj ha; have := cauchymodP e_gt0 hj hi. rewrite ltr_distl=> /andP[/(le_lt_trans _)-> //]. -by rewrite -(ler_add2r e) addrNK. +by rewrite -(lerD2r e) addrNK. Qed. Definition diff (x y : creal) (lt_xy : (x < y)%CR) : F := projT1 (sigW lt_xy). @@ -766,7 +766,7 @@ Lemma diffP (x y : creal) (lt_xy : (x < y)%CR) i : Proof. rewrite /diff; case: (sigW _)=> /= e /andP[e_gt0 he] hi hj. rewrite ltW // (@gtr_creal e (cauchymod y e)) // (le_trans _ he) //. -rewrite !mulrDr mulr1 !addrA !ler_add2r ltW //. +rewrite !mulrDr mulr1 !addrA !lerD2r ltW //. by rewrite (@ltr_creal e (cauchymod x e)) // addrK. Qed. @@ -785,9 +785,9 @@ Lemma lt_crealP e i j (e_gt0 : 0 < e) (x y : creal) : Proof. move=> hi hj he; exists (e / 5%:R); rewrite pmulr_rgt0 ?gtr0E //=. rewrite ltW // (@gtr_creal (e / 5%:R) j) ?pmulr_rgt0 ?gtr0E //. -rewrite (le_trans _ he) // -addrA (monoLR (addrNK _) (ler_add2r _)). +rewrite (le_trans _ he) // -addrA (monoLR (addrNK _) (lerD2r _)). rewrite ltW // (@ltr_creal (e / 5%:R) i) ?pmulr_rgt0 ?gtr0E //. -rewrite -!addrA ler_addl !addrA -mulrA -{1}[e]mulr1 -!(mulrBr, mulrDr). +rewrite -!addrA lerDl !addrA -mulrA -{1}[e]mulr1 -!(mulrBr, mulrDr). rewrite pmulr_rge0 // {1}[1](splitf 5) /= !mul1r !mulrDr mulr1. by rewrite !opprD !addrA !addrK addrN. Qed. @@ -797,7 +797,7 @@ Lemma le_crealP i (x y : creal) : Proof. move=> hi lt_yx; pose_big_enough j. have := hi j; big_enough => /(_ isT); apply/negP; rewrite -ltNge. - by rewrite (lt_le_trans _ (diff_of lt_yx)) ?ltr_spaddr ?diff_gt0. + by rewrite (lt_le_trans _ (diff_of lt_yx)) ?ltr_pwDr ?diff_gt0. by close. Qed. @@ -817,7 +817,7 @@ Lemma creal_lt_always (x y : creal) i (lt_xy : (x < y)%CR) : (cauchymod x (diff lt_xy) <= i)%N -> (cauchymod y (diff lt_xy) <= i)%N -> x i < y i. Proof. -by move=> hx hy; rewrite (lt_le_trans _ (diff_of lt_xy)) ?ltr_addl ?diff_gt0. +by move=> hx hy; rewrite (lt_le_trans _ (diff_of lt_xy)) ?ltrDl ?diff_gt0. Qed. Definition creal_gt0_always := @creal_lt_always 0. @@ -848,7 +848,7 @@ Qed. Lemma ge0_modP (x : creal) (x_ge0 : (0 <= x)%CR) eps i : 0 < eps -> (le_mod x_ge0 eps <= i)%N -> - eps < x i. Proof. -by move=> eps_gt0 hi; rewrite -(ltr_add2r eps) addNr -[0]/(0%CR i) le_modP. +by move=> eps_gt0 hi; rewrite -(ltrD2r eps) addNr -[0]/(0%CR i) le_modP. Qed. Lemma opp_crealP (x : creal) : creal_axiom (fun i => - x i). @@ -874,15 +874,15 @@ Lemma ubound_subproof (x : creal) : {b : F | b > 0 & forall i, `|x i| <= b}. Proof. pose_big_enough i; first set b := 1 + `|x i|. exists (foldl maxr b [seq `|x n| | n <- iota 0 i]) => [|n]. - have : 0 < b by rewrite ltr_spaddl. - by elim: iota b => //= a l IHl b b_gt0; rewrite IHl ?lt_maxr ?b_gt0. + have : 0 < b by rewrite ltr_pwDl. + by elim: iota b => //= a l IHl b b_gt0; rewrite IHl ?lt_max ?b_gt0. have [|le_in] := (ltnP n i). elim: i b => [|i IHi] b //. - rewrite ltnS -addn1 iotaD add0n map_cat foldl_cat /= le_maxr leq_eqVlt. + rewrite ltnS -addn1 iotaD add0n map_cat foldl_cat /= le_max leq_eqVlt. by case/orP=> [/eqP->|/IHi->] //; rewrite lexx orbT. set xn := `|x n|; suff : xn <= b. - by elim: iota xn b => //= a l IHl xn b Hxb; rewrite IHl ?le_maxr ?Hxb. - rewrite -ler_subl_addr (le_trans (ler_norm _)) //. + by elim: iota xn b => //= a l IHl xn b Hxb; rewrite IHl ?le_max ?Hxb. + rewrite -lerBlDr (le_trans (ler_norm _)) //. by rewrite (le_trans (ler_dist_dist _ _)) ?ltW ?cauchymodP. by close. Qed. @@ -904,11 +904,11 @@ exists_big_modulus m F. move=> e i j e_gt0 hi hj. rewrite -[_ * _]subr0 -(subrr (x j * y i)) opprD opprK addrA. rewrite -mulrBl -addrA -mulrBr split_norm_add // !normrM. - have /ler_wpmul2l /le_lt_trans-> // := uboundP y i. - rewrite -ltr_pdivl_mulr ?ubound_gt0 ?cauchymodP //. + have /ler_wpM2l /le_lt_trans-> // := uboundP y i. + rewrite -ltr_pdivlMr ?ubound_gt0 ?cauchymodP //. by rewrite !pmulr_rgt0 ?invr_gt0 ?ubound_gt0 ?ltr0n. - rewrite mulrC; have /ler_wpmul2l /le_lt_trans-> // := uboundP x j. - rewrite -ltr_pdivl_mulr ?ubound_gt0 ?cauchymodP //. + rewrite mulrC; have /ler_wpM2l /le_lt_trans-> // := uboundP x j. + rewrite -ltr_pdivlMr ?ubound_gt0 ?cauchymodP //. by rewrite !pmulr_rgt0 ?gtr0E ?ubound_gt0. by close. Qed. @@ -924,15 +924,15 @@ exists_big_modulus m F. move=> e i j e_gt0 hi hj. have /andP[xi_neq0 xj_neq0] : (x i != 0) && (x j != 0). by rewrite -!normr_gt0 !(lt_le_trans _ (lbound0_of x_neq0)) ?lbound_gt0. - rewrite -(@ltr_pmul2r _ `|x i * x j|); last by rewrite normr_gt0 mulf_neq0. + rewrite -(@ltr_pM2r _ `|x i * x j|); last by rewrite normr_gt0 mulf_neq0. rewrite -normrM !mulrBl mulrA mulVf // mulrCA mulVf // mul1r mulr1. apply: lt_le_trans (_ : e * d ^+ 2 <= _). by apply: cauchymodP; rewrite // !pmulr_rgt0 ?lbound_gt0. - rewrite ler_wpmul2l ?(ltW e_gt0) // normrM. + rewrite ler_wpM2l ?(ltW e_gt0) // normrM. have /(_ j) hx /= := lbound0_of x_neq0. - have -> // := (le_trans (ler_wpmul2l _ (hx _ _))). + have -> // := (le_trans (ler_wpM2l _ (hx _ _))). by rewrite ltW // lbound_gt0. - by rewrite ler_wpmul2r ?normr_ge0 // lbound0P. + by rewrite ler_wpM2r ?normr_ge0 // lbound0P. by close. Qed. Definition inv_creal (x : creal) (x_neq0 : x != 0) := CReal (inv_crealP x_neq0). @@ -953,7 +953,7 @@ Proof. exists_big_modulus m F=> [e i j e_gt0 hi hj|]. rewrite (le_lt_trans (@poly_accr_bound1P _ p (x (cauchymod x 1)) 1 _ _ _ _)); do ?[by rewrite ?e_gt0 | by rewrite ltW // cauchymodP]. - rewrite -ltr_pdivl_mulr ?poly_accr_bound_gt0 ?cauchymodP //. + rewrite -ltr_pdivlMr ?poly_accr_bound_gt0 ?cauchymodP //. by rewrite pmulr_rgt0 ?invr_gt0 ?poly_accr_bound_gt0. by close. Qed. @@ -967,12 +967,12 @@ pose d := lbound neq_px_py. pose_big_enough i. pose k := 2%:R + poly_accr_bound p (y i) d. have /andP[d_gt0 k_gt0] : (0 < d) && (0 < k). - rewrite ?(ltr_spaddl, poly_accr_bound_ge0); + rewrite ?(ltr_pwDl, poly_accr_bound_ge0); by rewrite ?ltr0n ?ltW ?ltr01 ?lbound_gt0. pose_big_enough j. apply: (@neq_crealP (d / k) j j) => //. by rewrite ?(pmulr_lgt0, invr_gt0, ltr0n). - rewrite ler_pdivr_mulr //. + rewrite ler_pdivrMr //. have /(_ j) // := (lbound_of neq_px_py). big_enough=> /(_ isT isT). apply: contraLR; rewrite -!ltNge=> hxy. @@ -980,10 +980,10 @@ pose_big_enough i. + by rewrite ltW // cauchymodP. + rewrite ltW // (@split_dist_add (y j)) //; last first. by rewrite cauchymodP ?divrn_gt0. - rewrite ltr_pdivl_mulr ?ltr0n // (le_lt_trans _ hxy) //. - by rewrite ler_wpmul2l ?normr_ge0 // ler_paddr // poly_accr_bound_ge0. - rewrite (le_lt_trans _ hxy) // ler_wpmul2l ?normr_ge0 //. - by rewrite ler_paddl // ?ler0n. + rewrite ltr_pdivlMr ?ltr0n // (le_lt_trans _ hxy) //. + by rewrite ler_wpM2l ?normr_ge0 // ler_wpDr // poly_accr_bound_ge0. + rewrite (le_lt_trans _ hxy) // ler_wpM2l ?normr_ge0 //. + by rewrite ler_wpDl // ?ler0n. by close. by close. Qed. @@ -1027,11 +1027,11 @@ move=> x y eq_xy z t eq_zt; apply: eq_crealP. exists_big_modulus m F. move=> e i e_gt0 hi. rewrite (@split_dist_add (y i * z i)) // -(mulrBl, mulrBr) normrM. - have /ler_wpmul2l /le_lt_trans-> // := uboundP z i. - rewrite -ltr_pdivl_mulr ?ubound_gt0 ?eq_modP //. + have /ler_wpM2l /le_lt_trans-> // := uboundP z i. + rewrite -ltr_pdivlMr ?ubound_gt0 ?eq_modP //. by rewrite !pmulr_rgt0 ?invr_gt0 ?ubound_gt0 ?ltr0n. - rewrite mulrC; have /ler_wpmul2l /le_lt_trans-> // := uboundP y i. - rewrite -ltr_pdivl_mulr ?ubound_gt0 ?eq_modP //. + rewrite mulrC; have /ler_wpM2l /le_lt_trans-> // := uboundP y i. + rewrite -ltr_pdivlMr ?ubound_gt0 ?eq_modP //. by rewrite !pmulr_rgt0 ?invr_gt0 ?ubound_gt0 ?ltr0n. by close. Qed. @@ -1042,13 +1042,13 @@ Lemma eq_creal_inv (x y : creal) (x_neq0 : x != 0) (y_neq0 : y != 0) : Proof. move=> eq_xy; apply: eq_crealP; exists_big_modulus m F. move=> e i e_gt0 hi /=. - rewrite -(@ltr_pmul2r _ (lbound x_neq0 * lbound y_neq0)); + rewrite -(@ltr_pM2r _ (lbound x_neq0 * lbound y_neq0)); do ?by rewrite ?pmulr_rgt0 ?lbound_gt0. apply: le_lt_trans (_ : `|(x i)^-1 - (y i)^-1| * (`|x i| * `|y i|) < _). - rewrite ler_wpmul2l ?normr_ge0 //. + rewrite ler_wpM2l ?normr_ge0 //. apply: le_trans (_ : `|x i| * lbound y_neq0 <= _). - by rewrite ler_wpmul2r ?lbound_ge0 ?lbound0P. - by rewrite ler_wpmul2l ?normr_ge0 ?lbound0P. + by rewrite ler_wpM2r ?lbound_ge0 ?lbound0P. + by rewrite ler_wpM2l ?normr_ge0 ?lbound0P. rewrite -!normrM mulrBl mulKf ?creal_neq0_always //. rewrite mulrCA mulVf ?mulr1 ?creal_neq0_always //. by rewrite distrC eq_modP ?pmulr_rgt0 ?lbound_gt0. @@ -1074,14 +1074,14 @@ have le_zt : (z <= t)%CR by apply: eq_le_creal. have le_xy : (y <= x)%CR by apply: eq_le_creal; apply: eq_creal_sym. pose_big_enough i. apply: (@lt_crealP e' i i)=> //. - rewrite ltW // -(ltr_add2r e'). + rewrite ltW // -(ltrD2r e'). rewrite (le_lt_trans _ (@le_modP _ _ le_zt _ _ _ _)) //. - rewrite -addrA (monoLR (@addrNK _ _) (@ler_add2r _ _)) ltW //. + rewrite -addrA (monoLR (@addrNK _ _) (@lerD2r _ _)) ltW //. rewrite (lt_le_trans (@le_modP _ _ le_xy e' _ _ _)) //. - rewrite -(monoLR (@addrNK _ _) (@ler_add2r _ _)) ltW //. + rewrite -(monoLR (@addrNK _ _) (@lerD2r _ _)) ltW //. rewrite (lt_le_trans _ (diff_of lxz)) //. - rewrite -addrA ler_lt_add // /e' -!mulrDr gtr_pmulr ?diff_gt0 //. - by rewrite [X in _ < X](splitf 4) /= mul1r !ltr_addr ?gtr0E. + rewrite -addrA ler_ltD // /e' -!mulrDr gtr_pMr ?diff_gt0 //. + by rewrite [X in _ < X](splitf 4) /= mul1r !ltrDr ?gtr0E. by close. Qed. Global Existing Instance lt_creal_morph_Proper. @@ -1106,10 +1106,10 @@ Proof. move=> neq_xy; pose_big_enough i. have := (@lboundP _ _ neq_xy i); big_enough => /(_ isT isT). have [le_xy|/ltW le_yx'] := lerP (x i) (y i). - rewrite -(ler_add2r (x i)) ?addrNK addrC. + rewrite -(lerD2r (x i)) ?addrNK addrC. move=> /lt_crealP; rewrite ?lbound_gt0; big_enough. by do 3!move/(_ isT); left. - rewrite -(ler_add2r (y i)) ?addrNK addrC. + rewrite -(lerD2r (y i)) ?addrNK addrC. move=> /lt_crealP; rewrite ?lbound_gt0; big_enough. by do 3!move/(_ isT); right. by close. @@ -1119,7 +1119,7 @@ Lemma lt_creal_neq (x y : creal) : (x < y -> x != y)%CR. Proof. move=> lxy; pose_big_enough i. apply: (@neq_crealP (diff lxy) i i); rewrite ?diff_gt0 //. - rewrite distrC ler_normr (monoRL (addrK _) (ler_add2r _)) addrC. + rewrite distrC ler_normr (monoRL (addrK _) (lerD2r _)) addrC. by rewrite (diff_of lxy). by close. Qed. @@ -1133,7 +1133,7 @@ move=> lt_xy lt_yz; pose_big_enough i. apply: (@lt_crealP (diff lt_xy + diff lt_yz) i i) => //. by rewrite addr_gt0 ?diff_gt0. rewrite (le_trans _ (diff_of lt_yz)) //. - by rewrite addrA ler_add2r (diff_of lt_xy). + by rewrite addrA lerD2r (diff_of lt_xy). by close. Qed. @@ -1220,8 +1220,8 @@ have d_gt0 : 0 < d by rewrite pmulr_rgt0 lbound_gt0. pose_big_enough i. apply: (@neq_crealP d i i)=> //; rewrite subr0 normrM. apply: le_trans (_ : `|x i| * lbound y_neq0 <= _). - by rewrite ler_wpmul2r ?lbound_ge0 // lbound0P. - by rewrite ler_wpmul2l ?normr_ge0 // lbound0P. + by rewrite ler_wpM2r ?lbound_ge0 // lbound0P. + by rewrite ler_wpM2l ?normr_ge0 // lbound0P. by close. Qed. @@ -1230,9 +1230,9 @@ Proof. move=> xy_neq0; pose_big_enough i. apply: (@neq_crealP ((ubound x)^-1 * lbound xy_neq0) i i) => //. by rewrite pmulr_rgt0 ?invr_gt0 ?lbound_gt0 ?ubound_gt0. - rewrite subr0 ler_pdivr_mull ?ubound_gt0 //. + rewrite subr0 ler_pdivrMl ?ubound_gt0 //. have /(_ i)-> // := (le_trans (lbound0_of xy_neq0)). - by rewrite normrM ler_wpmul2r ?normr_ge0 ?uboundP. + by rewrite normrM ler_wpM2r ?normr_ge0 ?uboundP. by close. Qed. @@ -1249,9 +1249,9 @@ move=> /Bezout_eq1_coprimepP /sig_eqW [[u v] /= hpq]; pose_big_enough i. move=> px0; apply: pqx0; apply: mul_creal_neq0=> //. apply: (@mul_neq0_creal v.[x]). apply: (@neq_crealP 2%:R^-1 i i); rewrite ?gtr0E //. - rewrite /= subr0 -hornerM -(ler_add2l `|upxi|). - rewrite (le_trans _ (ler_norm_add _ _)) // hpqi normr1. - rewrite (monoLR (addrNK _) (ler_add2r _)). + rewrite /= subr0 -hornerM -(lerD2l `|upxi|). + rewrite (le_trans _ (ler_normD _ _)) // hpqi normr1. + rewrite (monoLR (addrNK _) (lerD2r _)). by rewrite {1}[1](splitf 2) /= mul1r addrK. move=> qx0; apply: pqx0; apply: mul_creal_neq0=> //. apply: (@mul_neq0_creal u.[x]). @@ -1270,7 +1270,7 @@ Lemma root_poly_expn_creal p k x : (0 < k)%N Proof. move=> k_gt0 pkx_eq0; apply: eq_crealP; exists_big_modulus m F. move=> e i e_gt0 hi; rewrite /= subr0. - rewrite -(@ltr_pexpn2r _ k) -?topredE /= ?normr_ge0 ?ltW //. + rewrite -(@ltr_pXn2r _ k) -?topredE /= ?normr_ge0 ?ltW //. by rewrite -normrX -horner_exp (@eq0_modP _ pkx_eq0) ?exprn_gt0 //. by close. Qed. @@ -1327,11 +1327,11 @@ pose_big_enough i. set upxi := (u * _).[_] => hpqi. apply: (@neq_crealP ((ubound v.[x])%CR^-1 / 2%:R) i i) => //. by rewrite pmulr_rgt0 ?gtr0E // ubound_gt0. - rewrite /= subr0 ler_pdivr_mull ?ubound_gt0 //. + rewrite /= subr0 ler_pdivrMl ?ubound_gt0 //. apply: le_trans (_ : `|(v * q).[x i]| <= _); last first. - by rewrite hornerM normrM ler_wpmul2r ?normr_ge0 ?(uboundP v.[x]). - rewrite -(ler_add2l `|upxi|) (le_trans _ (ler_norm_add _ _)) // hpqi normr1. - rewrite (monoLR (addrNK _) (ler_add2r _)). + by rewrite hornerM normrM ler_wpM2r ?normr_ge0 ?(uboundP v.[x]). + rewrite -(lerD2l `|upxi|) (le_trans _ (ler_normD _ _)) // hpqi normr1. + rewrite (monoLR (addrNK _) (lerD2r _)). rewrite {1}[1](splitf 2) /= mul1r addrK ltW // /upxi hornerM. by rewrite (@eq0_modP _ upx_eq0) ?gtr0E. by close. @@ -1364,25 +1364,25 @@ pose r : F := minr 1 (minr (diff px_gt0 / 4%:R / b1) (diff px_gt0 / 4%:R / b2 / 2%:R)). exists r. - rewrite !lt_minr ?ltr01 ?pmulr_rgt0 ?gtr0E ?diff_gt0; + rewrite !lt_min ?ltr01 ?pmulr_rgt0 ?gtr0E ?diff_gt0; by rewrite ?poly_accr_bound2_gt0 ?poly_accr_bound_gt0. pose_big_enough i. exists i => //; left; split; last first. move=> y hy; have := (@poly_accr_bound1P _ p^`() 0 (1 + ubound x) (x i) y). - rewrite ?subr0 ler_paddl ?ler01 ?uboundP //. + rewrite ?subr0 ler_wpDl ?ler01 ?uboundP //. rewrite (le_trans (_ : _ <= r + `|x i|)) ?subr0; last 2 first. - + rewrite (monoRL (addrNK _) (ler_add2r _)). - by rewrite (le_trans (ler_sub_dist _ _)). - + by rewrite ler_add ?le_minl ?lexx ?uboundP. + + rewrite (monoRL (addrNK _) (lerD2r _)). + by rewrite (le_trans (lerB_dist _ _)). + + by rewrite lerD ?ge_min ?lexx ?uboundP. move=> /(_ isT isT). rewrite ler_distl=> /andP[le_py ge_py]. rewrite (lt_le_trans _ le_py) // subr_gt0 -/b1. rewrite (lt_le_trans _ (diff0_of px_gt0)) //. apply: le_lt_trans (_ : r * b1 < _). - by rewrite ler_wpmul2r ?poly_accr_bound_ge0. - rewrite -ltr_pdivl_mulr ?poly_accr_bound_gt0 //. - rewrite !lt_minl ltr_pmul2r ?invr_gt0 ?poly_accr_bound_gt0 //. - by rewrite gtr_pmulr ?diff_gt0 // invf_lt1 ?gtr0E ?ltr1n ?orbT. + by rewrite ler_wpM2r ?poly_accr_bound_ge0. + rewrite -ltr_pdivlMr ?poly_accr_bound_gt0 //. + rewrite !gt_min ltr_pM2r ?invr_gt0 ?poly_accr_bound_gt0 //. + by rewrite gtr_pMr ?diff_gt0 // invf_lt1 ?gtr0E ?ltr1n ?orbT. exists (diff px_gt0 / 4%:R). by rewrite pmulr_rgt0 ?gtr0E ?diff_gt0. move=> y z neq_yz hy hz. @@ -1390,29 +1390,29 @@ pose_big_enough i. have := @poly_accr_bound2P _ p 0 (1 + ubound x) z y; rewrite eq_sym !subr0. rewrite neq_yz ?ler01 ?ubound_ge0=> // /(_ isT). rewrite (le_trans (_ : _ <= r + `|x i|)); last 2 first. - + rewrite (monoRL (addrNK _) (ler_add2r _)). - by rewrite (le_trans (ler_sub_dist _ _)). - + by rewrite ler_add ?le_minl ?lexx ?uboundP. + + rewrite (monoRL (addrNK _) (lerD2r _)). + by rewrite (le_trans (lerB_dist _ _)). + + by rewrite lerD ?ge_min ?lexx ?uboundP. rewrite (le_trans (_ : _ <= r + `|x i|)); last 2 first. - + rewrite (monoRL (addrNK _) (ler_add2r _)). - by rewrite (le_trans (ler_sub_dist _ _)). - + by rewrite ler_add ?le_minl ?lexx ?uboundP. - rewrite ler_paddl ?uboundP ?ler01 //. + + rewrite (monoRL (addrNK _) (lerD2r _)). + by rewrite (le_trans (lerB_dist _ _)). + + by rewrite lerD ?ge_min ?lexx ?uboundP. + rewrite ler_wpDl ?uboundP ?ler01 //. move=> /(_ isT isT); rewrite ler_distl=> /andP [haccr _]. move=> /(_ isT isT); rewrite ler_distl=> /andP [hp' _]. - rewrite (lt_le_trans _ haccr) // (monoRL (addrK _) (ltr_add2r _)). - rewrite (lt_le_trans _ hp') // (monoRL (addrK _) (ltr_add2r _)). + rewrite (lt_le_trans _ haccr) // (monoRL (addrK _) (ltrD2r _)). + rewrite (lt_le_trans _ hp') // (monoRL (addrK _) (ltrD2r _)). rewrite (lt_le_trans _ (diff0_of px_gt0)) //. - rewrite {2}[diff _](splitf 4) /= -!addrA ltr_add2l ltr_spaddl //. + rewrite {2}[diff _](splitf 4) /= -!addrA ltrD2l ltr_pwDl //. by rewrite pmulr_rgt0 ?gtr0E ?diff_gt0. - rewrite -/b1 -/b2 ler_add //. - + rewrite -ler_pdivl_mulr ?poly_accr_bound2_gt0 //. - rewrite (le_trans (ler_dist_add (x i) _ _)) //. + rewrite -/b1 -/b2 lerD //. + + rewrite -ler_pdivlMr ?poly_accr_bound2_gt0 //. + rewrite (le_trans (ler_distD (x i) _ _)) //. apply: le_trans (_ : r * 2%:R <= _). - by rewrite mulrDr mulr1 ler_add // distrC. - by rewrite -ler_pdivl_mulr ?ltr0n // !le_minl lexx !orbT. - + rewrite -ler_pdivl_mulr ?poly_accr_bound_gt0 //. - by rewrite (le_trans hz) // !le_minl lexx !orbT. + by rewrite mulrDr mulr1 lerD // distrC. + by rewrite -ler_pdivlMr ?ltr0n // !ge_min lexx !orbT. + + rewrite -ler_pdivlMr ?poly_accr_bound_gt0 //. + by rewrite (le_trans hz) // !ge_min lexx !orbT. by close. Qed. @@ -1474,13 +1474,13 @@ Lemma bound_poly_boundP (z : creal) i (q : {poly {poly F}}) (a r : F) j : Proof. rewrite /poly_bound. pose f (q : {poly F}) (k : nat) := `|q^`N(j.+1)`_k| * (`|a| + `|r|) ^+ k. -rewrite ler_add //=. +rewrite lerD //=. rewrite (big_ord_widen (sizeY q) (f q.[(z i)%:P])); last first. rewrite size_nderivn leq_subLR (leq_trans (max_size_evalC _ _)) //. by rewrite leq_addl. rewrite big_mkcond /= ler_sum // /f => k _. case: ifP=> _; last by rewrite mulr_ge0 ?exprn_ge0 ?addr_ge0 ?normr_ge0. -rewrite ler_wpmul2r ?exprn_ge0 ?addr_ge0 ?normr_ge0 //. +rewrite ler_wpM2r ?exprn_ge0 ?addr_ge0 ?normr_ge0 //. rewrite !horner_coef. rewrite !(@big_morph _ _ (fun p => p^`N(j.+1)) 0 +%R); do ?[by rewrite raddf0|by move=> x y /=; rewrite raddfD]. @@ -1492,10 +1492,10 @@ rewrite ger0_norm; last first. rewrite -polyC_exp coefMC coef_norm_poly2 mulr_ge0 ?normr_ge0 //. by rewrite exprn_ge0 ?ltW ?ubound_gt0. rewrite size_norm_poly2 ler_sum //= => l _. -rewrite !{1}coef_nderivn normrMn ler_pmuln2r ?bin_gt0 ?leq_addr //. -rewrite -!polyC_exp !coefMC coef_norm_poly2 normrM ler_wpmul2l ?normr_ge0 //. +rewrite !{1}coef_nderivn normrMn ler_pMn2r ?bin_gt0 ?leq_addr //. +rewrite -!polyC_exp !coefMC coef_norm_poly2 normrM ler_wpM2l ?normr_ge0 //. rewrite normrX; case: (val l)=> // {}l. -by rewrite ler_pexpn2r -?topredE //= ?uboundP ?ltW ?ubound_gt0. +by rewrite ler_pXn2r -?topredE //= ?uboundP ?ltW ?ubound_gt0. Qed. Lemma bound_poly_bound_ge0 z q a r i : 0 <= bound_poly_bound z q a r i. @@ -1513,13 +1513,13 @@ Proof. rewrite /poly_accr_bound /bound_poly_accr_bound /=. set ui := _ ^+ _; set u := _ ^+ _; set vi := 1 + _. apply: le_trans (_ : u * vi <= _). - rewrite ler_wpmul2r //. + rewrite ler_wpM2r //. by rewrite addr_ge0 ?ler01 // sumr_ge0 //= => j _; rewrite poly_bound_ge0. rewrite /ui /u; case: (ltP 1%R); last by rewrite !expr1n. - move=> r2_gt1; rewrite ler_eexpn2l //. + move=> r2_gt1; rewrite ler_eXn2l //. rewrite -subn1 leq_subLR add1n (leq_trans _ (leqSpred _)) //. by rewrite max_size_evalC. -rewrite ler_wpmul2l ?exprn_ge0 ?le_maxr ?ler01 // ler_add //. +rewrite ler_wpM2l ?exprn_ge0 ?le_max ?ler01 // lerD //. pose f j := poly_bound q.[(z i)%:P]^`N(j.+1) a r. rewrite (big_ord_widen (sizeY q).-1 f); last first. rewrite -subn1 leq_subLR add1n (leq_trans _ (leqSpred _)) //. @@ -1545,16 +1545,16 @@ exists_big_modulus m F. do ?by rewrite ?subr0 ?uboundP. apply: le_lt_trans (_ : `|y i - y j| * bound_poly_accr_bound x p 0 (ubound y) < _). - by rewrite ler_wpmul2l ?normr_ge0 // bound_poly_accr_boundP. - rewrite -ltr_pdivl_mulr ?bound_poly_accr_bound_gt0 //. + by rewrite ler_wpM2l ?normr_ge0 // bound_poly_accr_boundP. + rewrite -ltr_pdivlMr ?bound_poly_accr_bound_gt0 //. by rewrite cauchymodP // !pmulr_rgt0 ?gtr0E ?bound_poly_accr_bound_gt0. rewrite -[p]swapXYK ![(swapXY (swapXY _)).[_, _]]horner2_swapXY. rewrite (le_lt_trans (@poly_accr_bound1P _ _ 0 (ubound x) _ _ _ _)) //; do ?by rewrite ?subr0 ?uboundP. apply: le_lt_trans (_ : `|x i - x j| * bound_poly_accr_bound y (swapXY p) 0 (ubound x) < _). - by rewrite ler_wpmul2l ?normr_ge0 // bound_poly_accr_boundP. - rewrite -ltr_pdivl_mulr ?bound_poly_accr_bound_gt0 //. + by rewrite ler_wpM2l ?normr_ge0 // bound_poly_accr_boundP. + rewrite -ltr_pdivlMr ?bound_poly_accr_bound_gt0 //. by rewrite cauchymodP // !pmulr_rgt0 ?gtr0E ?bound_poly_accr_bound_gt0. by close. Qed. @@ -1580,12 +1580,12 @@ apply: eq_crealP; exists_big_modulus m F. move=> e i e_gt0 hi /=; rewrite subr0. rewrite (hpq (y i)) addrCA subrr addr0 split_norm_add // normrM. apply: le_lt_trans (_ : (ubound u.[y, x - y]) * `|p.[x i]| < _). - by rewrite ler_wpmul2r ?normr_ge0 // (uboundP u.[y, x - y] i). - rewrite -ltr_pdivl_mull ?ubound_gt0 //. + by rewrite ler_wpM2r ?normr_ge0 // (uboundP u.[y, x - y] i). + rewrite -ltr_pdivlMl ?ubound_gt0 //. by rewrite (@eq0_modP _ px_eq0) // !pmulr_rgt0 ?gtr0E ?ubound_gt0. apply: le_lt_trans (_ : (ubound v.[y, x - y]) * `|q.[y i]| < _). - by rewrite ler_wpmul2r ?normr_ge0 // (uboundP v.[y, x - y] i). - rewrite -ltr_pdivl_mull ?ubound_gt0 //. + by rewrite ler_wpM2r ?normr_ge0 // (uboundP v.[y, x - y] i). + rewrite -ltr_pdivlMl ?ubound_gt0 //. by rewrite (@eq0_modP _ qy_eq0) // !pmulr_rgt0 ?gtr0E ?ubound_gt0. by close. Qed. @@ -1604,12 +1604,12 @@ apply: eq_crealP; exists_big_modulus m F. by rewrite -normr_gt0 (lt_le_trans _ (lbound0_of y_neq0)) ?lbound_gt0. rewrite split_norm_add // normrM. apply: le_lt_trans (_ : (ubound u.[y, x / y_neq0]) * `|p.[x i]| < _). - by rewrite ler_wpmul2r ?normr_ge0 // (uboundP u.[y, x / y_neq0] i). - rewrite -ltr_pdivl_mull ?ubound_gt0 //. + by rewrite ler_wpM2r ?normr_ge0 // (uboundP u.[y, x / y_neq0] i). + rewrite -ltr_pdivlMl ?ubound_gt0 //. by rewrite (@eq0_modP _ px_eq0) // !pmulr_rgt0 ?gtr0E ?ubound_gt0. apply: le_lt_trans (_ : (ubound v.[y, x / y_neq0]) * `|q.[y i]| < _). - by rewrite ler_wpmul2r ?normr_ge0 // (uboundP v.[y, x / y_neq0] i). - rewrite -ltr_pdivl_mull ?ubound_gt0 //. + by rewrite ler_wpM2r ?normr_ge0 // (uboundP v.[y, x / y_neq0] i). + rewrite -ltr_pdivlMl ?ubound_gt0 //. by rewrite (@eq0_modP _ qy_eq0) // !pmulr_rgt0 ?gtr0E ?ubound_gt0. by close. Qed. diff --git a/theories/complex.v b/theories/complex.v index 837b34c..7823df5 100644 --- a/theories/complex.v +++ b/theories/complex.v @@ -23,7 +23,7 @@ Import Order.TTheory GRing.Theory Num.Theory. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Obligation Tactic := idtac. +#[local] Obligation Tactic := idtac. Local Open Scope ring_scope. @@ -210,13 +210,11 @@ Proof. by move=> a b /=; simpc; rewrite subrr. Qed. Lemma real_complex_is_multiplicative : multiplicative (real_complex R). Proof. by split=> // a b /=; simpc; rewrite !mulr0 !mul0r addr0 subr0. Qed. -HB.instance Definition _ := - GRing.isAdditive.Build R [zmodType of R[i]] (real_complex R) - real_complex_is_additive. +HB.instance Definition _ := GRing.isAdditive.Build R R[i] + (real_complex R) real_complex_is_additive. -HB.instance Definition _ := - GRing.isMultiplicative.Build R [ringType of R[i]] (real_complex R) - real_complex_is_multiplicative. +HB.instance Definition _ := GRing.isMultiplicative.Build R R[i] + (real_complex R) real_complex_is_multiplicative. End ComplexField_realFieldType. @@ -335,10 +333,10 @@ Qed. Lemma lec_normD x y : lec (normC (x + y)) (normC x + normC y). Proof. move: x y => [a b] [c d] /=; simpc; rewrite addr0 eqxx /=. -rewrite -(@ler_pexpn2r _ 2) -?topredE /= ?(ler_paddr, sqrtr_ge0) //. +rewrite -(@ler_pXn2r _ 2) -?topredE /= ?(ler_wpDr, sqrtr_ge0) //. rewrite [X in _ <= X] sqrrD ?sqr_sqrtr; - do ?by rewrite ?(ler_paddr, sqrtr_ge0, sqr_ge0, mulr_ge0) //. -rewrite -addrA addrCA (monoRL (addrNK _) (ler_add2r _)) !sqrrD. + do ?by rewrite ?(ler_wpDr, sqrtr_ge0, sqr_ge0, mulr_ge0) //. +rewrite -addrA addrCA (monoRL (addrNK _) (lerD2r _)) !sqrrD. set u := _ *+ 2; set v := _ *+ 2. rewrite [a ^+ _ + _ + _]addrAC [b ^+ _ + _ + _]addrAC -addrA. rewrite [u + _] addrC [X in _ - X]addrAC [b ^+ _ + _]addrC. @@ -346,12 +344,12 @@ rewrite [u]lock [v]lock !addrA; set x := (a ^+ 2 + _ + _ + _). rewrite -addrA addrC addKr -!lock addrC. have [huv|] := ger0P (u + v); last first. by move=> /ltW /le_trans -> //; rewrite pmulrn_lge0 // mulr_ge0 ?sqrtr_ge0. -rewrite -(@ler_pexpn2r _ 2) -?topredE //=; last first. +rewrite -(@ler_pXn2r _ 2) -?topredE //=; last first. by rewrite ?(pmulrn_lge0, mulr_ge0, sqrtr_ge0) //. -rewrite -mulr_natl !exprMn !sqr_sqrtr ?(ler_paddr, sqr_ge0) //. -rewrite -mulrnDl -mulr_natl !exprMn ler_pmul2l ?exprn_gt0 ?ltr0n //. -rewrite sqrrD mulrDl !mulrDr -!exprMn addrAC -!addrA ler_add2l !addrA. -rewrite [_ + (b * d) ^+ 2]addrC -addrA ler_add2l. +rewrite -mulr_natl !exprMn !sqr_sqrtr ?(ler_wpDr, sqr_ge0) //. +rewrite -mulrnDl -mulr_natl !exprMn ler_pM2l ?exprn_gt0 ?ltr0n //. +rewrite sqrrD mulrDl !mulrDr -!exprMn addrAC -!addrA lerD2l !addrA. +rewrite [_ + (b * d) ^+ 2]addrC -addrA lerD2l. have: 0 <= (a * d - b * c) ^+ 2 by rewrite sqr_ge0. by rewrite sqrrB addrAC subr_ge0 [_ * c]mulrC mulrACA [d * _]mulrC. Qed. @@ -429,12 +427,10 @@ Proof. by move=> [a b] [c d] /=; simpc; rewrite [d - _]addrC. Qed. Lemma conjc_is_multiplicative : multiplicative (@conjc R). Proof. by split=> [[a b] [c d]|] /=; simpc. Qed. -HB.instance Definition _ := - GRing.isAdditive.Build [zmodType of R[i]] [zmodType of R[i]] conjc +HB.instance Definition _ := GRing.isAdditive.Build R[i] R[i] conjc conjc_is_additive. -HB.instance Definition _ := - GRing.isMultiplicative.Build [ringType of R[i]] [ringType of R[i]] conjc +HB.instance Definition _ := GRing.isMultiplicative.Build R[i] R[i] conjc conjc_is_multiplicative. Lemma conjcK : involutive (@conjc R). @@ -507,7 +503,7 @@ Lemma normc_def (z : R[i]) : `|z| = (sqrtr ((Re z)^+2 + (Im z)^+2))%:C. Proof. by case: z. Qed. Lemma add_Re2_Im2 (z : R[i]) : ((Re z)^+2 + (Im z)^+2)%:C = `|z|^+2. -Proof. by rewrite normc_def -rmorphX sqr_sqrtr ?addr_ge0 ?sqr_ge0. Qed. +Proof. by rewrite normc_def -rmorphXn sqr_sqrtr ?addr_ge0 ?sqr_ge0. Qed. Lemma addcJ (z : R[i]) : z + z^*%C = 2%:R * (Re z)%:C. Proof. by rewrite ReJ_add mulrC mulfVK ?pnatr_eq0. Qed. @@ -554,9 +550,7 @@ Implicit Types (k : R) (x y z : Rcomplex R). Lemma conjc_is_scalable : scalable (conjc : Rcomplex R -> Rcomplex R). Proof. by move=> a [b c]; simpc. Qed. HB.instance Definition _ := - GRing.isScalable.Build R - [the lmodType R of R[i]] [the zmodType of R[i]] *:%R conjc - conjc_is_scalable. + GRing.isScalable.Build R R[i] R[i] *:%R conjc conjc_is_scalable. End RComplexLMod. @@ -581,11 +575,11 @@ End RComplexLMod. (* case: (boolP (0 <= x)) (@ivt ('X^2 - x%:P) 0 (1 + x))=> px; last first. *) (* by move=> _; exists 0; rewrite lerr eqxx. *) (* case. *) -(* * by rewrite ler_paddr ?ler01. *) +(* * by rewrite ler_wpDr ?ler01. *) (* * rewrite !horner_lin oppr_le0 px /=. *) (* rewrite subr_ge0 (@ler_trans _ (1 + x)) //. *) -(* by rewrite ler_paddl ?ler01 ?lerr. *) -(* by rewrite ler_pemulr // addrC -subr_ge0 ?addrK // subr0 ler_paddl ?ler01. *) +(* by rewrite ler_wpDl ?ler01 ?lerr. *) +(* by rewrite ler_peMr // addrC -subr_ge0 ?addrK // subr0 ler_wpDl ?ler01. *) (* * move=> y hy; rewrite /root !horner_lin; move/eqP. *) (* move/(canRL (@addrNK _ _)); rewrite add0r=> <-. *) (* by exists y; case/andP: hy=> -> _; rewrite eqxx. *) @@ -632,10 +626,10 @@ have F2: `|a| <= sqrtr (a^+2 + b^+2). by rewrite addrC -subr_ge0 addrK exprn_even_ge0. have F3: 0 <= (sqrtr (a ^+ 2 + b ^+ 2) - a) / 2%:R. rewrite mulr_ge0 // subr_ge0 (le_trans _ F2) //. - by rewrite -(maxrN a) le_maxr lexx. + by rewrite -(maxrN a) le_max lexx. have F4: 0 <= (sqrtr (a ^+ 2 + b ^+ 2) + a) / 2%:R. rewrite mulr_ge0 // -{2}[a]opprK subr_ge0 (le_trans _ F2) //. - by rewrite -(maxrN a) le_maxr lexx orbT. + by rewrite -(maxrN a) le_max lexx orbT. congr (_ +i* _); set u := if _ then _ else _. rewrite mulrCA !mulrA. have->: (u * u) = 1. @@ -647,7 +641,7 @@ congr (_ +i* _); set u := if _ then _ else _. rewrite mulrCA -mulrA -mulrDr [sqrtr _ * _]mulrC. rewrite -mulr2n -sqrtrM // mulrAC !mulrA ?[_ * (_ - _)]mulrC -subr_sqr. rewrite sqr_sqrtr; last first. - by rewrite ler_paddr // exprn_even_ge0. + by rewrite ler_wpDr // exprn_even_ge0. rewrite [_^+2 + _]addrC addrK -mulrA -expr2 sqrtrM ?exprn_even_ge0 //. rewrite !sqrtr_sqr -(mulr_natr (_ * _)). rewrite [`|_^-1|]ger0_norm // -mulrA [_ * _%:R]mulrC divff //. @@ -702,7 +696,7 @@ Proof. by rewrite normcE sqr_sqrtc. Qed. Lemma normc_ge_Re (x : R[i]) : `|Re x|%:C <= `|x|. Proof. -by case: x => a b; simpc; rewrite -sqrtr_sqr ler_wsqrtr // ler_addl sqr_ge0. +by case: x => a b; simpc; rewrite -sqrtr_sqr ler_wsqrtr // lerDl sqr_ge0. Qed. Lemma normcJ (x : R[i]) : `|x^*%C| = `|x|. @@ -1063,11 +1057,11 @@ move: u v => u v in fE *. pose L1fun : 'M[R]_n -> _ := 2%:R^-1 \*: (mulmxr u \+ (mulmxr v \o trmx) \+ ((mulmx (u^T)) \- (mulmx (v^T) \o trmx))). -pose L1 := lin_mx [linear of L1fun]. +pose L1 := lin_mx L1fun. pose L2fun : 'M[R]_n -> _ := 2%:R^-1 \*: (((@GRing.opp _) \o (mulmxr u \o trmx) \+ mulmxr v) \+ ((mulmx (u^T) \o trmx) \+ (mulmx (v^T)))). -pose L2 := lin_mx [linear of L2fun]. +pose L2 := lin_mx L2fun. have [] := @Lemma4 _ _ 1%:M _ [::L1; L2] (erefl _). + by move: HrV; rewrite mxrank1 !dvdn2 ?negbK oddM andbb. + by move=> ? _ /=; rewrite submx1. @@ -1141,8 +1135,8 @@ suff: exists a, eigenvalue (restrict V f) a. by move=> [a /eigenvalue_restrict Hf]; exists a; apply: Hf. case: (\rank V) (restrict V f) => {f f_stabV V m} [|n] f in Hn dvd2n *. by rewrite dvdn0 in Hn. -pose L1 := lin_mx [linear of mulmxr f \+ (mulmx f^T)]. -pose L2 := lin_mx [linear of mulmxr f \o mulmx f^T]. +pose L1 := lin_mx (mulmxr f \+ mulmx f^T). +pose L2 := lin_mx (mulmxr f \o mulmx f^T). have [] /= := IHk _ (leqnn _) _ _ (skew R[i] n.+1) _ [::L1; L2] (erefl _). + rewrite rank_skew; apply: contra Hn. rewrite -(@dvdn_pmul2r 2) //= -expnSr muln2 -[_.*2]add0n. @@ -1197,7 +1191,7 @@ move=> /(_ m.+1 1 _ f) []; last by move=> a; exists a. + by rewrite submx1. Qed. -Lemma complex_acf_axiom : GRing.closed_field_axiom [ringType of R[i]]. +Lemma complex_acf_axiom : GRing.closed_field_axiom R[i]. Proof. move=> n c n_gt0; pose p := 'X^n - \poly_(i < n) c i. suff [x rpx] : exists x, root p x. @@ -1247,7 +1241,7 @@ Definition complexalg := realalg[i]. HB.instance Definition _ := Num.ClosedField.on complexalg. -Lemma complexalg_algebraic : integralRange (@ratr [unitRingType of complexalg]). +Lemma complexalg_algebraic : integralRange (@ratr complexalg). Proof. move=> x; suff [p p_monic] : integralOver (real_complex _ \o realalg_of _) x. by rewrite (eq_map_poly (fmorph_eq_rat _)); exists p. diff --git a/theories/polyrcf.v b/theories/polyrcf.v index 60a9a24..53ea5b4 100644 --- a/theories/polyrcf.v +++ b/theories/polyrcf.v @@ -127,12 +127,12 @@ rewrite lead_coefDl ?size_mulX ?size_polyC // ?lead_coefMX; last first. by apply: (leq_trans (leq_b1 _)); rewrite size_poly_gt0. move=> lq_gt0; have [y Hy] := IHq lq_gt0. pose z := (1 + (lead_coef q) ^-1 * `|c|); exists (maxr y z) => x. -have z_gt0: 0 < z by rewrite ltr_spaddl ?ltr01 ?mulr_ge0 ?invr_ge0 // ltW. -rewrite !hornerE le_maxl => /andP[/Hy Hq Hc]. +have z_gt0: 0 < z by rewrite ltr_pwDl ?ltr01 ?mulr_ge0 ?invr_ge0 // ltW. +rewrite !hornerE ge_max => /andP[/Hy Hq Hc]. apply: le_trans (_ : lead_coef q * z + c <= _); last first. - rewrite ler_add2r (le_trans (_ : _ <= q.[x] * z)) // ?ler_pmul2r //. - by rewrite ler_pmul2l // (lt_le_trans _ Hq). -rewrite mulrDr mulr1 -addrA ler_addl mulVKf ?gt_eqF //. + rewrite lerD2r (le_trans (_ : _ <= q.[x] * z)) // ?ler_pM2r //. + by rewrite ler_pM2l // (lt_le_trans _ Hq). +rewrite mulrDr mulr1 -addrA lerDl mulVKf ?gt_eqF //. by rewrite -[c]opprK subr_ge0 normrN ler_norm. Qed. @@ -149,14 +149,14 @@ rewrite lead_coefDl ?size_mulX ?size_polyC // ?lead_coefMX; last first. move=> lq_gt0; have [y Hy _] := poly_pinfty_gt_lc lq_gt0. pose z := (1 + (lead_coef q) ^-1 * (`|m| + `|c|)); exists (maxr y z) => x. have z_gt0 : 0 < z. - by rewrite ltr_spaddl ?ltr01 ?mulr_ge0 ?invr_ge0 ?addr_ge0 // ?ltW. -rewrite !hornerE le_maxl => /andP[/Hy Hq Hc]. + by rewrite ltr_pwDl ?ltr01 ?mulr_ge0 ?invr_ge0 ?addr_ge0 // ?ltW. +rewrite !hornerE ge_max => /andP[/Hy Hq Hc]. apply: le_trans (_ : lead_coef q * z + c <= _); last first. - rewrite ler_add2r (le_trans (_ : _ <= q.[x] * z)) // ?ler_pmul2r //. - by rewrite ler_pmul2l // (lt_le_trans _ Hq). -rewrite mulrDr mulr1 mulVKf ?gt_eqF // addrA -(addrA _ _ c) ler_paddr //. + rewrite lerD2r (le_trans (_ : _ <= q.[x] * z)) // ?ler_pM2r //. + by rewrite ler_pM2l // (lt_le_trans _ Hq). +rewrite mulrDr mulr1 mulVKf ?gt_eqF // addrA -(addrA _ _ c) ler_wpDr //. by rewrite -[c]opprK subr_ge0 normrN ler_norm. -by rewrite ler_paddl ?ler_norm // ?ltW. +by rewrite ler_wpDl ?ler_norm // ?ltW. Qed. End SgpInfty. @@ -170,27 +170,27 @@ Definition cauchy_bound (p : {poly R}) := Lemma cauchy_boundP (p : {poly R}) x : p != 0 -> p.[x] = 0 -> `| x | < cauchy_bound p. Proof. -move=> np0 rpx; rewrite ltr_spaddl ?ltr01 //. +move=> np0 rpx; rewrite ltr_pwDl ?ltr01 //. have sp_gt0 : (size p > 0)%N by rewrite size_poly_gt0. have lcn0 : `|lead_coef p| != 0 by rewrite normr_eq0 lead_coef_eq0. have lcp : `|lead_coef p| > 0 by rewrite lt_def lcn0 /=. have [x_le1|x_gt1] := lerP `|x| 1. - rewrite (le_trans x_le1) // ler_pdivl_mull // mulr1. - by rewrite polySpred// big_ord_recr/= ler_addr sumr_ge0. + rewrite (le_trans x_le1) // ler_pdivlMl // mulr1. + by rewrite polySpred// big_ord_recr/= lerDr sumr_ge0. have x_gt0 : `|x| > 0 by rewrite (lt_trans ltr01). have [sp_le1|sp_gt1] := leqP (size p) 1. by move: rpx np0; rewrite [p]size1_polyC// hornerC polyC_eq0 => /eqP->. -rewrite ler_pdivl_mull//. +rewrite ler_pdivlMl//. pose n := (size p).-1; have n_gt0 : (n > 0)%N by rewrite /n -subn1 subn_gt0. have : `|p`_n| * `|x| ^+ n <= \sum_(i < n) `|p`_i * x ^+ i|. rewrite (le_trans _ (ler_norm_sum _ _ _))//. have := rpx; rewrite horner_coef polySpred// !big_ord_recr/=. by move=> /(canRL (@addrK _ _))->; rewrite sub0r normrN normrM normrX. rewrite -[n in _ ^+ n]prednK// exprS mulrA. -rewrite -[X in _ X -> _]ler_pdivl_mulr ?exprn_gt0// => /le_trans->//. -rewrite polySpred// big_ord_recr/= ler_paddr// mulr_suml ler_sum => //i _. -rewrite normrM normrX ler_pdivr_mulr ?exprn_gt0// ler_pmul ?exprn_ge0//. -by rewrite ler_weexpn2l// 1?ltW// -ltnS prednK//. +rewrite -[X in _ X -> _]ler_pdivlMr ?exprn_gt0// => /le_trans->//. +rewrite polySpred// big_ord_recr/= ler_wpDr// mulr_suml ler_sum => //i _. +rewrite normrM normrX ler_pdivrMr ?exprn_gt0// ler_pM ?exprn_ge0//. +by rewrite ler_weXn2l// 1?ltW// -ltnS prednK//. Qed. Lemma root_in_cauchy_bound (p : {poly R}) : p != 0 -> @@ -203,19 +203,19 @@ Definition root_cauchy_boundP (p : {poly R}) pN0 x (rpx : root p x) := Lemma le_cauchy_bound p : p != 0 -> {in `]-oo, (- cauchy_bound p)], noroot p}. Proof. move=> p_neq0 x; rewrite in_itv /=; apply/contra_leN. -by case/rootP/(cauchy_boundP p_neq0)/ltr_normlP; rewrite ltr_oppl. +by case/rootP/(cauchy_boundP p_neq0)/ltr_normlP; rewrite ltrNl. Qed. Hint Resolve le_cauchy_bound : core. Lemma ge_cauchy_bound p : p != 0 -> {in `[cauchy_bound p, +oo[, noroot p}. Proof. move=> p_neq0 x; rewrite in_itv andbT /=; apply/contra_leN. -by case/rootP/(cauchy_boundP p_neq0)/ltr_normlP; rewrite ltr_oppl. +by case/rootP/(cauchy_boundP p_neq0)/ltr_normlP; rewrite ltrNl. Qed. Hint Resolve ge_cauchy_bound : core. Lemma cauchy_bound_gt0 p : cauchy_bound p > 0. -Proof. by rewrite ltr_spaddl ?ltr01 // mulrC divr_ge0 ?normr_ge0 ?sumr_ge0. Qed. +Proof. by rewrite ltr_pwDl ?ltr01 // mulrC divr_ge0 ?normr_ge0 ?sumr_ge0. Qed. Hint Resolve cauchy_bound_gt0 : core. Lemma cauchy_bound_ge0 p : cauchy_bound p >= 0. @@ -338,11 +338,11 @@ Qed. Lemma nth_root x n : x > 0 -> { y | y > 0 & y ^+ (n.+1) = x }. Proof. move=> x_gt0; apply/sig2_eqW; pose p := ('X ^+ n.+1 - x%:P). -have xS_ge1: x + 1 >= 1 by rewrite ler_paddl // ltW. +have xS_ge1: x + 1 >= 1 by rewrite ler_wpDl // ltW. have xS_ge0: x + 1 > 0 by rewrite (lt_le_trans (@ltr01 _)). have [//||y /andP[y_ge0 _]] := @poly_ivtW _ p 0 (x + 1); first exact: ltW. rewrite !(hornerE, horner_exp) expr0n /= sub0r oppr_le0 (ltW x_gt0) /=. - by rewrite subr_ge0 (le_trans _ (ler_eexpr _ _)) // ler_paddr ?ler01. + by rewrite subr_ge0 (le_trans _ (ler_eXnr _ _)) // ler_wpDr ?ler01. rewrite /root !(hornerE, horner_exp) subr_eq0 => /eqP x_eq; exists y => //. rewrite lt_neqAle y_ge0 andbT; apply: contra_eqN x_eq => /eqP<-. by rewrite eq_sym expr0n gt_eqF. @@ -473,9 +473,9 @@ move=> e_gt0; have [k k_ge1 kP] := poly_lipshitz p (x - e) (x + e). have k_gt0 : k > 0 by rewrite (lt_le_trans ltr01). exists (e / k) => [|y]; first by rewrite mulr_gt0 ?invr_gt0. have [y_small|y_big] := lerP `|y - x| e. - rewrite ltr_pdivl_mulr // mulrC; apply/le_lt_trans/kP => //; + rewrite ltr_pdivlMr // mulrC; apply/le_lt_trans/kP => //; by rewrite -![_ \in _]ler_distl ?subrr ?normr0 // ?ltW. -by move=> /(lt_trans y_big); rewrite ltr_pmulr // invf_gt1 // le_gtF. +by move=> /(lt_trans y_big); rewrite ltr_pMr // invf_gt1 // le_gtF. Qed. Lemma ler_hornerW a b p : (forall x, x \in `]a, b[ -> p^`().[x] >= 0) -> @@ -483,7 +483,7 @@ Lemma ler_hornerW a b p : (forall x, x \in `]a, b[ -> p^`().[x] >= 0) -> Proof. move=> der_nneg x y axb ayb; rewrite le_eqVlt => /orP[/eqP->//|ltxy]. have [c xcy /(canRL (@subrK _ _))->]:= poly_mvt p ltxy. -rewrite ler_addr mulr_ge0 ?subr_ge0 ?(ltW ltxy) ?der_nneg //. +rewrite lerDr mulr_ge0 ?subr_ge0 ?(ltW ltxy) ?der_nneg //. by apply: subitvP xcy; rewrite /(_ <= _)%O/= !bnd_simp ?(itvP axb) ?(itvP ayb). Qed. @@ -506,7 +506,7 @@ Hypothesis der_gt0 : forall x, x \in `]a, b[ -> (p^`()).[x] > 0. Lemma ltr_hornerW : {in `[a, b] &, {homo horner p : x y / x < y}}. Proof. move=> x y axb ayb ltxy; have [c xcy /(canRL (@subrK _ _))->]:= poly_mvt p ltxy. -rewrite ltr_addr mulr_gt0 ?subr_gt0 ?der_gt0 //. +rewrite ltrDr mulr_gt0 ?subr_gt0 ?der_gt0 //. apply: subitvP xcy; rewrite le_itv !bnd_simp. by rewrite /= (itvP axb) (itvP ayb). Qed. @@ -573,14 +573,14 @@ Lemma lgtr_horner : {in `[a, b] &, forall x y, p.[x] < p.[y] = (sp' * x < sp' * y)}. Proof. move=> x y axb ayb; rewrite /= [in LHS]signpE ![(_ *: q).[_]]hornerZ. -by case: s; rewrite ?mul1r ?mulN1r ?ltr_opp2 (ltr_horner derq_gt0). +by case: s; rewrite ?mul1r ?mulN1r ?ltrN2 (ltr_horner derq_gt0). Qed. Lemma lger_horner : {in `[a, b] &, forall x y, p.[x] <= p.[y] = (sp' * x <= sp' * y)}. Proof. move=> x y axb ayb; rewrite /= [in LHS]signpE ![(_ *: q).[_]]hornerZ. -by case: s; rewrite ?mul1r ?mulN1r ?ler_opp2 (ler_horner derq_gt0). +by case: s; rewrite ?mul1r ?mulN1r ?lerN2 (ler_horner derq_gt0). Qed. Lemma horner_inj : {in `[a, b] &, injective (horner p)}. @@ -677,7 +677,7 @@ Proof. by move=> axb; rewrite derivN hornerN oppr_gt0 der_neg. Qed. Lemma gtr_hornerW : {in `[a, b] &, {homo horner p : x y /~ x < y}}. Proof. -by move=> x y axb ayb yx; rewrite -ltr_opp2 -!hornerN (ltr_hornerW dern_gt0). +by move=> x y axb ayb yx; rewrite -ltrN2 -!hornerN (ltr_hornerW dern_gt0). Qed. Lemma ger_horner : {in `[a, b] &, {mono horner p : x y /~ x <= y}}. @@ -777,13 +777,13 @@ End RootsOn. (* Proof. by move=> a; apply: inv_inj; apply: symr_inv. Qed. *) (* Lemma ltr_sym : forall a x y, (symr a x < symr a y) = (y < x). *) -(* Proof. by move=> a x y; rewrite lter_add2r lter_oppr opprK. Qed. *) +(* Proof. by move=> a x y; rewrite lterD2rr lterNr opprK. Qed. *) (* Lemma symr_add_itv : forall a b x, *) (* (a < symr (a + b) x < b) = (a < x < b). *) (* Proof. *) (* move=> a b x; rewrite andbC. *) -(* by rewrite lter_subrA lter_add2r -lter_addlA lter_add2l. *) +(* by rewrite lter_subrA lterD2rr -lter_addlA lterD2rl. *) (* Qed. *) Lemma roots_on_comp p a b s : @@ -819,7 +819,7 @@ Lemma max_roots_on p a b x s : Proof. move/allP=> lsx /roots_on_comp/=/min_roots_on[]. apply/allP=> y; rewrite -[y]opprK (mem_map oppr_inj). - by move/lsx; rewrite ltr_opp2. + by move/lsx; rewrite ltrN2. rewrite oppr_itv root_comp !hornerE !opprK=> -> rxb -> rax. by split=> //; apply/roots_on_comp. Qed. @@ -1217,9 +1217,9 @@ Qed. Lemma next_root_in p a b : next_root p a b \in `[a, maxr b a]. Proof. case: next_rootP => [p0|y np0 py0 hy _|c np0 hc _]. -* by rewrite bound_in_itv /<=%O /= le_maxr lexx orbT. -* by apply: subitvP hy; rewrite /<=%O /= /<=%O /= le_maxr !lexx. -* by rewrite hc bound_in_itv /<=%O /= le_maxr lexx orbT. +* by rewrite bound_in_itv /<=%O /= le_max lexx orbT. +* by apply: subitvP hy; rewrite /<=%O /= /<=%O /= le_max !lexx. +* by rewrite hc bound_in_itv /<=%O /= le_max lexx orbT. Qed. Lemma next_root_gt p a b : a < b -> p != 0 -> next_root p a b > a. @@ -1227,7 +1227,7 @@ Proof. move=> ab np0; case: next_rootP=> [p0|y _ py0 hy _|c _ -> _]. * by rewrite p0 eqxx in np0. * by rewrite (itvP hy). -* by rewrite lt_maxr ab. +* by rewrite lt_max ab. Qed. Lemma next_noroot p a b : {in `]a, (next_root p a b)[, noroot p}. @@ -1285,9 +1285,9 @@ Qed. Lemma prev_root_in p a b : prev_root p a b \in `[minr a b, b]. Proof. case: prev_rootP => [p0|y np0 py0 hy _|c np0 hc _]. -* by rewrite bound_in_itv /<=%O /= le_minl lexx orbT. -* by apply: subitvP hy; rewrite /<=%O /= /<=%O /= le_minl !lexx. -* by rewrite hc bound_in_itv /<=%O /= le_minl lexx orbT. +* by rewrite bound_in_itv /<=%O /= ge_min lexx orbT. +* by apply: subitvP hy; rewrite /<=%O /= /<=%O /= ge_min !lexx. +* by rewrite hc bound_in_itv /<=%O /= ge_min lexx orbT. Qed. Lemma prev_noroot p a b : {in `](prev_root p a b), b[, noroot p}. @@ -1303,7 +1303,7 @@ Proof. move=> ab np0; case: prev_rootP=> [p0|y _ py0 hy _|c _ -> _]. * by rewrite p0 eqxx in np0. * by rewrite (itvP hy). -* by rewrite lt_minl ab. +* by rewrite gt_min ab. Qed. Lemma is_prev_root p a b x : @@ -1460,18 +1460,18 @@ case: leP => //; case: next_rootP=> [|y np0 py0 hy|c np0 ->] hp hpq _. - move=> z hz /=; rewrite rootM negb_or ?hp //. by rewrite (@next_noroot _ a b) //; apply: subitvPr hz. * case: (eqVneq q 0) hpq => [->|q0 hpq]. - rewrite mulr0 root0 next_root0 le_maxl lexx andbT. + rewrite mulr0 root0 next_root0 ge_max lexx andbT. by move/max_r->; constructor. constructor=> //; first by rewrite mulf_neq0. move=> z hz /=; rewrite rootM negb_or ?hp // (@next_noroot _ a b) //. - by apply: subitvPr hz=> /=; move: hpq; rewrite le_maxl; case/andP. + by apply: subitvPr hz=> /=; move: hpq; rewrite ge_max; case/andP. Qed. Lemma neighpr_mul a b p q : (neighpr (p * q) a b) =i [predI (neighpr p a b) & (neighpr q a b)]. Proof. move=> x; rewrite !inE /<=%O /= /<=%O /= next_rootM. -by case: (a < x); rewrite // lt_minr. +by case: (a < x); rewrite // lt_min. Qed. Lemma prev_rootM a b (p q : {poly R}) : @@ -1489,18 +1489,18 @@ case: ltP => //; case: (@prev_rootP p)=> [|y np0 py0 hy|c np0 ->] hp hpq _. - move=> z hz /=; rewrite rootM negb_or ?hp //. by rewrite (@prev_noroot _ a b) //; apply: subitvPl hz. * case: (eqVneq q 0) hpq => [->|q0 hpq]. - rewrite mulr0 root0 prev_root0 le_minr lexx andbT. + rewrite mulr0 root0 prev_root0 le_min lexx andbT. by move/min_r->; constructor. constructor=> //; first by rewrite mulf_neq0. move=> z hz /=; rewrite rootM negb_or ?hp // (@prev_noroot _ a b) //. - by apply: subitvPl hz=> /=; move: hpq; rewrite le_minr; case/andP. + by apply: subitvPl hz=> /=; move: hpq; rewrite le_min; case/andP. Qed. Lemma neighpl_mul a b p q : (neighpl (p * q) a b) =i [predI (neighpl p a b) & (neighpl q a b)]. Proof. move=> x; rewrite !inE /<=%O /= /<=%O /= prev_rootM. -by case: (x < b); rewrite // lt_maxl !(andbT, andbF). +by case: (x < b); rewrite // gt_max !(andbT, andbF). Qed. Lemma neighpr_wit p x b : x < b -> p != 0 -> {y | y \in neighpr p x b}. @@ -1639,7 +1639,7 @@ Proof. have [->|q0] := eqVneq q 0; first by rewrite /sgp_right !(size_poly0,mulr0). have [->|p0] := eqVneq p 0; first by rewrite /sgp_right !(size_poly0,mul0r). case: (@neighpr_wit (p * q) x (1 + x))=> [||m hpq]; do ?by rewrite mulf_neq0. - by rewrite ltr_spaddl ?ltr01. + by rewrite ltr_pwDl ?ltr01. rewrite -(@sgr_neighpr (1 + x) _ _ m) //; move: hpq; rewrite neighpr_mul. by case/andP=> /= hp hq; rewrite hornerM sgrM !(@sgr_neighpr (1 + x) _ x). Qed. @@ -1653,7 +1653,7 @@ Qed. Lemma sgp_right_square p x : p != 0 -> sgp_right p x * sgp_right p x = 1. Proof. move=> np0; case: (@neighpr_wit p x (1 + x))=> [||m hpq] //. - by rewrite ltr_spaddl ?ltr01. + by rewrite ltr_pwDl ?ltr01. rewrite -(@sgr_neighpr (1 + x) _ _ m) //. by rewrite -expr2 sqr_sg (@next_noroot _ x (1 + x)). Qed. @@ -1800,8 +1800,8 @@ have [z Hz] := poly_pinfty_gt_lc lp_gt0. have {}Hz u : u \in `[z, +oo[ -> Num.sg p.[u] = 1. rewrite in_itv andbT => /Hz pu_ge1. by rewrite gtr0_sg // (lt_le_trans lp_gt0). -rewrite (@polyrN0_itv _ _ rpx (maxr y z)) ?in_itv /= ?le_maxr ?(itvP Hy) //. -by rewrite Hz ?gtr0_sg // in_itv /= le_maxr lexx orbT. +rewrite (@polyrN0_itv _ _ rpx (maxr y z)) ?in_itv /= ?le_max ?(itvP Hy) //. +by rewrite Hz ?gtr0_sg // in_itv /= le_max lexx orbT. Qed. Lemma sgp_minftyP x (p : {poly R}) : @@ -1811,8 +1811,8 @@ Proof. move=> rpx y Hy; rewrite -sgp_pinfty_sym. have ->: p.[y] = (p \Po -'X).[-y] by rewrite horner_comp !hornerE opprK. apply: (@sgp_pinftyP (- x)) => /= [z Hz|]. - by rewrite root_comp !hornerE rpx // in_itv /= ler_oppl (itvP Hz). -by rewrite in_itv /= ler_opp2 (itvP Hy). + by rewrite root_comp !hornerE rpx // in_itv /= lerNl (itvP Hz). +by rewrite in_itv /= lerN2 (itvP Hy). Qed. Lemma odd_poly_root (p : {poly R}) : ~~ odd (size p) -> {x | root p x}. diff --git a/theories/qe_rcf_th.v b/theories/qe_rcf_th.v index 37c54b5..760ea34 100644 --- a/theories/qe_rcf_th.v +++ b/theories/qe_rcf_th.v @@ -1071,7 +1071,7 @@ Lemma ccount_weakP p sq : p != 0 -> (ccount_weak p sq > 0). Proof. move=> p_neq0; rewrite -constraints1P /constraints ltr0n lt0n. -rewrite -(@pnatr_eq0 [numDomainType of int]) natr_sum psumr_eq0 //. +rewrite -(@pnatr_eq0 int) natr_sum psumr_eq0 //. rewrite -has_predC /=. apply: (iffP hasP) => [[x rpx /= prod_neq0]|[x /andP[rpx]]]. exists x; rewrite -rootE [root _ _]roots_on_rootsR // rpx /=. diff --git a/theories/realalg.v b/theories/realalg.v index 765719f..31bd220 100644 --- a/theories/realalg.v +++ b/theories/realalg.v @@ -1,15 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From HB Require Import structures. -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. -From mathcomp -Require Import bigop order ssralg ssrnum ssrint rat poly polydiv polyorder. -From mathcomp -Require Import perm matrix mxpoly polyXY binomial generic_quotient. -From mathcomp -Require Import cauchyreals separable zmodp bigenough. +From mathcomp Require Import all_ssreflect all_algebra all_field. +From mathcomp Require Import archimedean bigenough. +Require Import polyorder cauchyreals. (*************************************************************************) (* This files constructs the real closure of an archimedian field in the *) @@ -46,7 +40,7 @@ rewrite !comp_polyE size_map_poly; apply: (big_ind2 (fun x y => x ^ f = y)). + by rewrite rmorph0. + by move=> u u' v v' /=; rewrite rmorphD /= => -> ->. move=> /= i _; rewrite -mul_polyC rmorphM /= map_polyC mul_polyC. -by rewrite coef_map rmorphX. +by rewrite coef_map rmorphXn. Qed. End extras. @@ -401,15 +395,15 @@ Lemma to_algcreal_ofP p c r i j : 0 <= r -> (i <= j)%N -> Proof. move=> r_ge0 leij; pose r' := r * 2%:R ^- j * (2%:R ^+ (j - i) - 1). apply: le_trans (_ : r' <= _); last first. - rewrite /r' -mulrA ler_wpmul2l // ler_pdivr_mull ?exprn_gt0 ?ltr0n //. + rewrite /r' -mulrA ler_wpM2l // ler_pdivrMl ?exprn_gt0 ?ltr0n //. rewrite -{2}(subnK leij) exprD mulfK ?gt_eqF ?exprn_gt0 ?ltr0n //. - by rewrite ger_addl lerN10. + by rewrite gerDl lerN10. rewrite /r' subrX1 addrK mul1r -{1 2}(subnK leij); set f := _ c r. elim: (_ - _)%N=> [|k ihk]; first by rewrite subrr normr0 big_ord0 mulr0 lexx. rewrite addSn big_ord_recl /= mulrDr. -rewrite (le_trans (ler_dist_add (f (k + i)%N) _ _)) //. -rewrite ler_add ?expr0 ?mulr1 ?to_algcreal_of_recP // (le_trans ihk) //. -rewrite exprSr invfM -!mulrA !ler_wpmul2l ?invr_ge0 ?exprn_ge0 ?ler0n //. +rewrite (le_trans (ler_distD (f (k + i)%N) _ _)) //. +rewrite lerD ?expr0 ?mulr1 ?to_algcreal_of_recP // (le_trans ihk) //. +rewrite exprSr invfM -!mulrA !ler_wpM2l ?invr_ge0 ?exprn_ge0 ?ler0n //. by rewrite mulr_sumr ler_sum // => l _ /=; rewrite exprS mulKf ?pnatr_eq0. Qed. @@ -422,7 +416,7 @@ pose_big_modulus m F. move=> hwlog; case/orP: (leq_total i j)=> /hwlog; last exact. by rewrite distrC; apply. rewrite (le_lt_trans (to_algcreal_ofP _ _ _ _)) ?radius_alg_ge0 //. - rewrite ltr_pdivr_mulr ?gtr0E // -ltr_pdivr_mull //. + rewrite ltr_pdivrMr ?gtr0E // -ltr_pdivrMl //. by rewrite upper_nthrootP. by close. Qed. @@ -437,11 +431,11 @@ pose_big_modulus m F. move=> hwlog; case/orP: (leq_total i j)=> /hwlog; first exact. by rewrite distrC; apply. rewrite ger0_norm ?subr_ge0; last first. - by rewrite ?lef_pinv -?topredE /= ?gtr0E // ler_eexpn2l ?ltr1n. - rewrite -(@ltr_pmul2l _ (2%:R ^+ i )) ?gtr0E //. + by rewrite ?lef_pV2 -?topredE /= ?gtr0E // ler_eXn2l ?ltr1n. + rewrite -(@ltr_pM2l _ (2%:R ^+ i )) ?gtr0E //. rewrite mulrBr mulfV ?gt_eqF ?gtr0E //. - rewrite (le_lt_trans (_ : _ <= 1)) // ?ger_addl ?oppr_le0 ?mulr_ge0 ?ger0E //. - by rewrite -ltr_pdivr_mulr // mul1r upper_nthrootP. + rewrite (le_lt_trans (_ : _ <= 1)) // ?gerDl ?oppr_le0 ?mulr_ge0 ?ger0E //. + by rewrite -ltr_pdivrMr // mul1r upper_nthrootP. by close. Qed. Definition exp2k_creal := CReal exp2k_crealP. @@ -450,7 +444,7 @@ Lemma exp2k_creal_eq0 : (exp2k_creal == 0)%CR. Proof. apply: eq_crealP; exists_big_modulus m F. move=> e i e_gt0 hi /=. - rewrite subr0 gtr0_norm ?gtr0E // -ltf_pinv -?topredE /= ?gtr0E //. + rewrite subr0 gtr0_norm ?gtr0E // -ltf_pV2 -?topredE /= ?gtr0E //. by rewrite invrK upper_nthrootP. by close. Qed. @@ -471,7 +465,7 @@ have: ((p).[u - cr * exp2k_creal] * (p).[u + cr * exp2k_creal] <= 0)%CR. rewrite addrNK -addrA -opprD -mulr2n -[_ / _ *+ _]mulr_natr. by rewrite -mulrA exprSr invfM mulfVK ?pnatr_eq0. rewrite addrK -addrA -mulr2n -[_ / _ *+ _]mulr_natr. - rewrite -mulrA exprSr invfM mulfVK ?pnatr_eq0 // => /ler_pmul2l<-. + rewrite -mulrA exprSr invfM mulfVK ?pnatr_eq0 // => /ler_pM2l<-. rewrite mulr0 mulrCA !mulrA [X in X * _]mulrAC -mulrA. by rewrite mulr_ge0_le0 // -expr2 exprn_even_ge0. rewrite exp2k_creal_eq0 mul_creal0 opp_creal0 add_creal0. @@ -481,7 +475,7 @@ pose_big_enough i. by rewrite !pmulr_rgt0 ?invr_gt0 ?ltr0n ?lbound_gt0. rewrite add0r [u]lock /= -!expr2. rewrite -[_.[_] ^+ _]ger0_norm ?exprn_even_ge0 // normrX. - rewrite ler_pexpn2r -?topredE /= ?lbound_ge0 ?normr_ge0 //. + rewrite ler_pXn2r -?topredE /= ?lbound_ge0 ?normr_ge0 //. by rewrite -lock (le_trans _ (lbound0_of pu0)). by close. Qed. @@ -540,7 +534,7 @@ have [|ncop] := boolP (coprimep p p^`()). rewrite (le_trans (to_algcreal_ofP _ _ _ (leq0n _))) ?(ltW r_gt0) //. by rewrite expr0 divr1. + by rewrite ltW // cauchymodP. - rewrite -ltr_pdivl_mull //. + rewrite -ltr_pdivlMl //. by rewrite (@eq_modP _ _ _ eq_py_px) // ?pmulr_rgt0 ?invr_gt0. by close. case: (@smaller_factor _ p p^`() x); rewrite ?monic_annul_creal //. @@ -564,29 +558,18 @@ Proof. by apply/eq_algcrealP; apply: to_algdomK. Qed. Canonical eq_algcreal_encModRel := EncModRel eq_algcreal eq_algcreal_to_algdom. Local Open Scope quotient_scope. +Local Notation "\pi ( x )" := (\pi x) : quotient_scope. (***************************************************************************) (* Algebraic numbers are the quotient of algcreal by their setoid equality *) (***************************************************************************) Definition alg := {eq_quot eq_algcreal}. -Definition alg_of of (phant F) := alg. -Identity Coercion type_alg_of : alg_of >-> alg. +HB.instance Definition _ := Choice.on alg. +HB.instance Definition _ := EqQuotient.on alg. -Notation "{ 'alg' F }" := (alg_of (Phant F)). - -(* A lot of structure is inherited *) -Canonical alg_eqType := [eqType of alg]. -Canonical alg_choiceType := [choiceType of alg]. -Canonical alg_quotType := [quotType of alg]. -Canonical alg_eqQuotType := [eqQuotType eq_algcreal of alg]. -Canonical alg_of_eqType := [eqType of {alg F}]. -Canonical alg_of_choiceType := [choiceType of {alg F}]. -Canonical alg_of_quotType := [quotType of {alg F}]. -Canonical alg_of_eqQuotType := [eqQuotType eq_algcreal of {alg F}]. - -Definition to_alg_def (phF : phant F) : F -> {alg F} := - lift_embed {alg F} cst_algcreal. +Definition to_alg_def (phF : phant F) : F -> alg := + lift_embed alg cst_algcreal. Notation to_alg := (@to_alg_def (Phant F)). Notation "x %:RA" := (to_alg x) (at level 2, left associativity, format "x %:RA"). @@ -597,44 +580,44 @@ Canonical to_alg_pi_morph := PiEmbed to_alg. Local Notation zero_alg := 0%:RA. Local Notation one_alg := 1%:RA. -Lemma equiv_alg (x y : algcreal) : (x == y)%CR <-> (x = y %[mod {alg F}]). +Lemma equiv_alg (x y : algcreal) : (x == y)%CR <-> (x = y %[mod alg]). Proof. split; first by move=> /eq_algcrealP /eqquotP ->. by move=> /eqquotP /eq_algcrealP. Qed. -Lemma nequiv_alg (x y : algcreal) : reflect (x != y)%CR (x != y %[mod {alg F}]). +Lemma nequiv_alg (x y : algcreal) : reflect (x != y)%CR (x != y %[mod alg]). Proof. by rewrite eqquotE; apply: neq_algcrealP. Qed. Arguments nequiv_alg {x y}. Prenex Implicits nequiv_alg. -Lemma pi_algK (x : algcreal) : (repr (\pi_{alg F} x) == x)%CR. +Lemma pi_algK (x : algcreal) : (repr (\pi_alg x) == x)%CR. Proof. by apply/equiv_alg; rewrite reprK. Qed. -Definition add_alg := lift_op2 {alg F} add_algcreal. +Definition add_alg := lift_op2 alg add_algcreal. -Lemma pi_add : {morph \pi_{alg F} : x y / add_algcreal x y >-> add_alg x y}. +Lemma pi_add : {morph \pi_alg : x y / add_algcreal x y >-> add_alg x y}. Proof. by unlock add_alg=> x y; rewrite -equiv_alg /= !pi_algK. Qed. Canonical add_pi_morph := PiMorph2 pi_add. -Definition opp_alg := lift_op1 {alg F} opp_algcreal. +Definition opp_alg := lift_op1 alg opp_algcreal. -Lemma pi_opp : {morph \pi_{alg F} : x / opp_algcreal x >-> opp_alg x}. +Lemma pi_opp : {morph \pi_alg : x / opp_algcreal x >-> opp_alg x}. Proof. by unlock opp_alg=> x; rewrite -equiv_alg /= !pi_algK. Qed. Canonical opp_pi_morph := PiMorph1 pi_opp. -Definition mul_alg := lift_op2 {alg F} mul_algcreal. +Definition mul_alg := lift_op2 alg mul_algcreal. -Lemma pi_mul : {morph \pi_{alg F} : x y / mul_algcreal x y >-> mul_alg x y}. +Lemma pi_mul : {morph \pi_alg : x y / mul_algcreal x y >-> mul_alg x y}. Proof. by unlock mul_alg=> x y; rewrite -equiv_alg /= !pi_algK. Qed. Canonical mul_pi_morph := PiMorph2 pi_mul. -Definition inv_alg := lift_op1 {alg F} inv_algcreal. +Definition inv_alg := lift_op1 alg inv_algcreal. -Lemma pi_inv : {morph \pi_{alg F} : x / inv_algcreal x >-> inv_alg x}. +Lemma pi_inv : {morph \pi_alg : x / inv_algcreal x >-> inv_alg x}. Proof. unlock inv_alg=> x; symmetry; rewrite -equiv_alg /= /inv_algcreal. case: eq_algcreal_dec=> /= [|x'_neq0]. @@ -669,20 +652,19 @@ Qed. HB.instance Definition _ := GRing.isZmodule.Build alg add_algA add_algC add_0alg add_Nalg. -HB.instance Definition _ := GRing.Zmodule.on {alg F}. -Lemma add_pi x y : \pi_{alg F} x + \pi_{alg F} y - = \pi_{alg F} (add_algcreal x y). +Lemma add_pi x y : \pi_alg x + \pi_alg y + = \pi_alg (add_algcreal x y). Proof. by rewrite [_ + _]piE. Qed. -Lemma opp_pi x : - \pi_{alg F} x = \pi_{alg F} (opp_algcreal x). +Lemma opp_pi x : - \pi_alg x = \pi_alg (opp_algcreal x). Proof. by rewrite [- _]piE. Qed. -Lemma zeroE : 0 = \pi_{alg F} zero_algcreal. +Lemma zeroE : 0 = \pi_alg zero_algcreal. Proof. by rewrite [0]piE. Qed. -Lemma sub_pi x y : \pi_{alg F} x - \pi_{alg F} y - = \pi_{alg F} (add_algcreal x (opp_algcreal y)). +Lemma sub_pi x y : \pi_alg x - \pi_alg y + = \pi_alg (add_algcreal x (opp_algcreal y)). Proof. by rewrite [_ - _]piE. Qed. Lemma mul_algC : commutative mul_alg. @@ -714,13 +696,13 @@ Proof. by rewrite piE -(rwP neq_algcrealP) (rwP neq_creal_cst) oner_eq0. Qed. HB.instance Definition _ := GRing.Zmodule_isComRing.Build alg mul_algA mul_algC mul_1alg mul_alg_addl nonzero1_alg. -HB.instance Definition _ := GRing.ComRing.on {alg F}. +HB.instance Definition _ := GRing.ComRing.on alg. -Lemma mul_pi x y : \pi_{alg F} x * \pi_{alg F} y - = \pi_{alg F} (mul_algcreal x y). +Lemma mul_pi x y : \pi_alg x * \pi_alg y + = \pi_alg (mul_algcreal x y). Proof. by rewrite [_ * _]piE. Qed. -Lemma oneE : 1 = \pi_{alg F} one_algcreal. +Lemma oneE : 1 = \pi_alg one_algcreal. Proof. by rewrite [1]piE. Qed. Lemma mul_Valg (x : alg) : x != zero_alg -> mul_alg (inv_alg x) x = one_alg. @@ -741,25 +723,24 @@ Qed. Lemma to_alg_additive : additive to_alg. Proof. -move=> x y /=; rewrite !piE sub_pi -equiv_alg /=. +move=> x y /=; rewrite !piE/= -equiv_alg /=. by apply: eq_crealP; exists m0=> * /=; rewrite subrr normr0. Qed. HB.instance Definition _ := - GRing.isAdditive.Build F [zmodType of {alg F}] to_alg to_alg_additive. + GRing.isAdditive.Build F alg to_alg to_alg_additive. Lemma to_alg_multiplicative : multiplicative to_alg. Proof. -split=> [x y |] //; rewrite !piE mul_pi -equiv_alg. +split=> [x y |] //; rewrite !piE -equiv_alg. by apply: eq_crealP; exists m0=> * /=; rewrite subrr normr0. Qed. HB.instance Definition _ := - GRing.isMultiplicative.Build F [ringType of {alg F}] to_alg - to_alg_multiplicative. + GRing.isMultiplicative.Build F alg to_alg to_alg_multiplicative. Lemma expn_pi (x : algcreal) (n : nat) : - (\pi_{alg F} x) ^+ n = \pi (exp_algcreal x n). + (\pi_alg x) ^+ n = \pi_alg (exp_algcreal x n). Proof. rewrite /exp_algcreal; case: n=> [|n]; first by rewrite expr0 oneE. rewrite exprS iteropS; elim: n=> /= [|n ihn]; rewrite ?expr0 ?mulr1 //. @@ -767,7 +748,7 @@ by rewrite exprS ihn mul_pi. Qed. Lemma horner_pi (p : {poly F}) (x : algcreal) : - (p ^ to_alg).[\pi_alg x] = \pi (horner_algcreal p x). + (p ^ to_alg).[\pi_alg x] = \pi_alg (horner_algcreal p x). Proof. rewrite horner_coef /horner_algcreal size_map_poly. apply: (big_ind2 (fun x y => x = \pi_alg y)). @@ -777,37 +758,36 @@ by move=> i /= _; rewrite expn_pi coef_map /= [_ * _]piE. Qed. (* Defining annihilating polynomials for algebraics *) -Definition annul_alg : {alg F} -> {poly F} := locked (annul_creal \o repr). +Definition annul_alg : alg -> {poly F} := locked (annul_creal \o repr). Lemma root_annul_algcreal (x : algcreal) : ((annul_alg (\pi x)).[x] == 0)%CR. Proof. by unlock annul_alg; rewrite /= -pi_algK root_annul_creal. Qed. -Lemma root_annul_alg (x : {alg F}) : root ((annul_alg x) ^ to_alg) x. +Lemma root_annul_alg (x : alg) : root ((annul_alg x) ^ to_alg) x. Proof. apply/rootP; rewrite -[x]reprK horner_pi /= zeroE -equiv_alg. by rewrite horner_algcrealE root_annul_algcreal. Qed. -Lemma monic_annul_alg (x : {alg F}) : annul_alg x \is monic. +Lemma monic_annul_alg (x : alg) : annul_alg x \is monic. Proof. by unlock annul_alg; rewrite monic_annul_creal. Qed. -Lemma annul_alg_neq0 (x : {alg F}) : annul_alg x != 0. +Lemma annul_alg_neq0 (x : alg) : annul_alg x != 0. Proof. by rewrite monic_neq0 ?monic_annul_alg. Qed. HB.instance Definition _ := GRing.ComRing_isField.Build alg mul_Valg inv_alg0. -HB.instance Definition _ := GRing.Field.on {alg F}. -Lemma inv_pi x : (\pi_{alg F} x)^-1 = \pi_{alg F} (inv_algcreal x). +Lemma inv_pi x : (\pi_alg x)^-1 = \pi_alg (inv_algcreal x). Proof. by rewrite [_^-1]piE. Qed. -Lemma div_pi x y : \pi_{alg F} x / \pi_{alg F} y - = \pi_{alg F} (mul_algcreal x (inv_algcreal y)). +Lemma div_pi x y : \pi_alg x / \pi_alg y + = \pi_alg (mul_algcreal x (inv_algcreal y)). Proof. by rewrite [_ / _]piE. Qed. -Definition lt_alg := lift_fun2 {alg F} lt_algcreal. -Definition le_alg := lift_fun2 {alg F} le_algcreal. +Definition lt_alg := lift_fun2 alg lt_algcreal. +Definition le_alg := lift_fun2 alg le_algcreal. -Lemma lt_alg_pi : {mono \pi_{alg F} : x y / lt_algcreal x y >-> lt_alg x y}. +Lemma lt_alg_pi : {mono \pi_alg : x y / lt_algcreal x y >-> lt_alg x y}. Proof. move=> x y; unlock lt_alg; rewrite /lt_algcreal. by do 2!case: ltVge_algcreal_dec=> //=; rewrite !pi_algK. @@ -815,7 +795,7 @@ Qed. Canonical lt_alg_pi_mono := PiMono2 lt_alg_pi. -Lemma le_alg_pi : {mono \pi_{alg F} : x y / le_algcreal x y >-> le_alg x y}. +Lemma le_alg_pi : {mono \pi_alg : x y / le_algcreal x y >-> le_alg x y}. Proof. move=> x y; unlock le_alg; rewrite /le_algcreal. by do 2!case: ltVge_algcreal_dec=> //=; rewrite !pi_algK. @@ -823,9 +803,9 @@ Qed. Canonical le_alg_pi_mono := PiMono2 le_alg_pi. -Definition norm_alg := lift_op1 {alg F} norm_algcreal. +Definition norm_alg := lift_op1 alg norm_algcreal. -Lemma norm_alg_pi : {morph \pi_{alg F} : x / norm_algcreal x >-> norm_alg x}. +Lemma norm_alg_pi : {morph \pi_alg : x / norm_algcreal x >-> norm_alg x}. Proof. move=> x; unlock norm_alg; rewrite /norm_algcreal /le_algcreal. by do 2!case: ltVge_algcreal_dec=> //=; rewrite !(pi_opp, pi_algK, reprK). @@ -833,11 +813,6 @@ Qed. Canonical norm_alg_pi_morph := PiMorph1 norm_alg_pi. -(* begin hide *) -(* Lemma norm_pi (x : algcreal) : `|\pi_{alg F} x| = \pi (norm_algcreal x). *) -(* Proof. by rewrite /norm_algcreal -lt_pi -zeroE -lerNgt fun_if -opp_pi. Qed. *) -(* end hide *) - Lemma add_alg_gt0 x y : lt_alg zero_alg x -> lt_alg zero_alg y -> lt_alg zero_alg (x + y). Proof. @@ -845,7 +820,7 @@ rewrite -[x]reprK -[y]reprK !piE -!(rwP lt_algcrealP). move=> x_gt0 y_gt0; pose_big_enough i. apply: (@lt_crealP _ (diff x_gt0 + diff y_gt0) i i) => //. by rewrite addr_gt0 ?diff_gt0. - by rewrite /= add0r ler_add // ?diff0P. + by rewrite /= add0r lerD // ?diff0P. by close. Qed. @@ -857,8 +832,8 @@ move=> x_gt0 y_gt0; pose_big_enough i. apply: (@lt_crealP _ (diff x_gt0 * diff y_gt0) i i) => //. by rewrite pmulr_rgt0 ?diff_gt0. rewrite /= add0r (le_trans (_ : _ <= diff x_gt0 * (repr y) i)) //. - by rewrite ler_wpmul2l ?(ltW (diff_gt0 _)) // diff0P. - by rewrite ler_wpmul2r ?diff0P ?ltW ?creal_gt0_always. + by rewrite ler_wpM2l ?(ltW (diff_gt0 _)) // diff0P. + by rewrite ler_wpM2r ?diff0P ?ltW ?creal_gt0_always. by close. Qed. @@ -876,11 +851,11 @@ Proof. rewrite -[x]reprK -[y]reprK !piE; apply/lt_algcrealP/lt_algcrealP=> /= hxy. pose_big_enough i. apply: (@lt_crealP _ (diff hxy) i i); rewrite ?diff_gt0 //. - by rewrite (monoLR (addNKr _) (ler_add2l _)) addrC diff0P. + by rewrite (monoLR (addNKr _) (lerD2l _)) addrC diff0P. by close. pose_big_enough i. apply: (@lt_crealP _ (diff hxy) i i); rewrite ?diff_gt0 //. - by rewrite (monoRL (addrK _) (ler_add2r _)) add0r addrC diffP. + by rewrite (monoRL (addrK _) (lerD2r _)) add0r addrC diffP. by close. Qed. @@ -923,22 +898,21 @@ Qed. HB.instance Definition _ := Num.IntegralDomain_isLtReal.Build alg add_alg_gt0 mul_alg_gt0 gt0_alg_nlt0 sub_alg_gt0 lt0_alg_total norm_algN ge0_norm_alg le_alg_def. -HB.instance Definition _ := Num.RealDomain.on {alg F}. -Lemma lt_pi x y : \pi_{alg F} x < \pi y = lt_algcreal x y. +Lemma lt_pi x y : \pi_alg x < \pi y = lt_algcreal x y. Proof. by rewrite [_ < _]lt_alg_pi. Qed. -Lemma le_pi x y : \pi_{alg F} x <= \pi y = le_algcreal x y. +Lemma le_pi x y : \pi_alg x <= \pi y = le_algcreal x y. Proof. by rewrite [_ <= _]le_alg_pi. Qed. -Lemma norm_pi (x : algcreal) : `|\pi_{alg F} x| = \pi (norm_algcreal x). +Lemma norm_pi (x : algcreal) : `|\pi_alg x| = \pi (norm_algcreal x). Proof. by rewrite [`|_|]piE. Qed. -Lemma lt_algP (x y : algcreal) : reflect (x < y)%CR (\pi_{alg F} x < \pi y). +Lemma lt_algP (x y : algcreal) : reflect (x < y)%CR (\pi_alg x < \pi y). Proof. by rewrite lt_pi; apply: lt_algcrealP. Qed. Arguments lt_algP {x y}. -Lemma le_algP (x y : algcreal) : reflect (x <= y)%CR (\pi_{alg F} x <= \pi y). +Lemma le_algP (x y : algcreal) : reflect (x <= y)%CR (\pi_alg x <= \pi y). Proof. by rewrite le_pi; apply: le_algcrealP. Qed. Arguments le_algP {x y}. Prenex Implicits lt_algP le_algP. @@ -972,7 +946,7 @@ rewrite piE -(rwP lt_algP) /= => _; pose_big_enough i. by close. Qed. -Definition inf_alg (x : {alg F}) : F := +Definition inf_alg (x : alg) : F := let: exist2 d _ _ := inf_alg_proof x in d. Lemma inf_alg_gt0 x : 0 < inf_alg x. @@ -985,11 +959,11 @@ Lemma approx_proof x e : {y | 0 < e -> `|x - y%:RA| < e}. Proof. elim/quotW:x => x; pose_big_enough i. exists (x i)=> e_gt0; rewrite (lt_trans _ (inf_lt_alg _)) //. - rewrite !piE sub_pi norm_pi -(rwP lt_algP) /= norm_algcrealE /=. + rewrite !piE norm_pi -(rwP lt_algP) /= norm_algcrealE /=. pose_big_enough j. apply: (@lt_crealP _ (inf_alg e / 2%:R) j j) => //. by rewrite pmulr_rgt0 ?gtr0E ?inf_alg_gt0. - rewrite /= {2}[inf_alg e](splitf 2) /= ler_add2r. + rewrite /= {2}[inf_alg e](splitf 2) /= lerD2r. by rewrite ltW // cauchymodP ?pmulr_rgt0 ?gtr0E ?inf_alg_gt0. by close. by close. @@ -1003,7 +977,7 @@ Proof. by unlock approx; case: approx_proof=> /= y hy /hy /lt_le_trans hy' /hy'. Qed. -Lemma alg_archi : Num.archimedean_axiom [numDomainType of {alg F}]. +Lemma alg_archi : Num.archimedean_axiom alg. Proof. move=> x; move: {x}`|x| (normr_ge0 x) => x x_ge0. pose a := approx x 1%:RA; exists (Num.bound (a + 1)). @@ -1013,8 +987,7 @@ rewrite -ler_to_alg rmorphD /= (le_trans _ (ltW hxa)) //. by move=> /(_ isT) /(lt_trans _)->. Qed. -HB.instance Definition _ := Num.RealField_isArchimedean.Build alg alg_archi. -HB.instance Definition _ := Num.ArchimedeanField.on {alg F}. +HB.instance Definition _ := Num.NumDomain_bounded_isArchimedean.Build alg alg_archi. (**************************************************************************) (* At this stage, algebraics form an archimedian field. We now build the *) @@ -1060,7 +1033,7 @@ Qed. (* any sequence of algebraic can be expressed as a sequence of polynomials in a unique algebraic *) Lemma pet_alg_proof (s : seq alg) : - { ap : {alg F} * seq {poly F} | + { ap : alg * seq {poly F} | [forall i : 'I_(size s), (ap.2`_i ^ to_alg).[ap.1] == s`_i] & size ap.2 = size s }. Proof. @@ -1088,7 +1061,7 @@ Qed. (* the polynomial p. *) (****************************************************************************) -Definition pet_alg s : {alg F} := +Definition pet_alg s : alg := let: exist2 (a, _) _ _ := pet_alg_proof s in a. Definition pet_alg_poly s : seq {poly F}:= let: exist2 (_, sp) _ _ := pet_alg_proof s in sp. @@ -1105,7 +1078,7 @@ move=> [a sp] /= /forallP hs hsize; have [lt_is|le_si] := ltnP i (size s). by rewrite !nth_default ?hsize // rmorph0 horner0. Qed. -Definition poly_ground := locked (fun (p : {poly {alg F}}) => +Definition poly_ground := locked (fun (p : {poly alg}) => swapXY (Poly (pet_alg_poly p)) : {poly {poly F}}). Lemma sizeY_poly_ground p : sizeY (poly_ground p) = size p. @@ -1170,7 +1143,7 @@ move: u'a_eq0=> /ihn [] //; first by rewrite -ltnS (leq_trans size_u'). by move=> r; exists r. Qed. -Definition annul_pet_alg (p : {poly {alg F}}) : {poly F} := +Definition annul_pet_alg (p : {poly alg}) : {poly F} := if (p != 0) =P true is ReflectT p_neq0 then let: exist2 r _ _ := annul_from_alg_proof p_neq0 (annul_alg_neq0 _) (root_annul_alg _) in r @@ -1209,11 +1182,11 @@ Notation "x %:RA" := (to_alg _ x) Lemma upper_nthrootVP (F : archiFieldType) (x : F) (i : nat) : 0 < x -> (Num.bound (x ^-1) <= i)%N -> 2%:R ^- i < x. Proof. -move=> x_gt0 hx; rewrite -ltf_pinv -?topredE //= ?gtr0E //. +move=> x_gt0 hx; rewrite -ltf_pV2 -?topredE //= ?gtr0E //. by rewrite invrK upper_nthrootP. Qed. -Notation "{ 'alg' F }" := (alg_of (Phant F)). +Notation "{ 'alg' F }" := (alg F). Section AlgAlg. @@ -1303,7 +1276,7 @@ Lemma to_alg_creal_repr (x : {alg F}) : (to_alg_creal (repr x) == x%:CR)%CR. Proof. apply: eq_crealP; exists_big_modulus m {alg F}. move=> e i e_gt0 hi /=; rewrite (le_lt_trans _ (inf_lt_alg _)) //. - rewrite -{2}[x]reprK !piE sub_pi norm_pi. + rewrite -{2}[x]reprK !piE norm_pi. rewrite -(rwP (le_algP _ _)) norm_algcrealE /=; pose_big_enough j. apply: (@le_crealP _ j)=> k hk /=. by rewrite ltW // cauchymodP ?inf_alg_gt0. @@ -1317,11 +1290,11 @@ Lemma cst_pi (x : algcreal F) : ((\pi_{alg F} x)%:CR == to_alg_creal x)%CR. Proof. apply: eq_crealP; exists_big_modulus m {alg F}. move=> e i e_gt0 hi /=; rewrite (lt_trans _ (inf_lt_alg _)) //. - rewrite !piE sub_pi norm_pi /= -(rwP (lt_algP _ _)) norm_algcrealE /=. + rewrite !piE norm_pi /= -(rwP (lt_algP _ _)) norm_algcrealE /=. pose_big_enough j. apply: (@lt_crealP _ (inf_alg e / 2%:R) j j) => //. by rewrite ?divrn_gt0 ?inf_alg_gt0. - rewrite /= {2}[inf_alg _](splitf 2) ler_add2r ltW // distrC. + rewrite /= {2}[inf_alg _](splitf 2) lerD2r ltW // distrC. by rewrite cauchymodP ?divrn_gt0 ?inf_alg_gt0. by close. by close. @@ -1361,7 +1334,7 @@ have [||[u v] /= [hu hv] hpq] := @resultant_in_ideal _ (poly_ground (annul_alg x)) (annul_pet_alg (annul_alg x) ^ polyC). + rewrite ltn_neqAle eq_sym sp_neq1 //= lt0n size_poly_eq0. by rewrite poly_ground_eq0 annul_alg_neq0. -+ rewrite size_map_polyC -(size_map_poly [rmorphism of to_alg _]) /=. ++ rewrite size_map_polyC -(size_map_poly (to_alg _)) /=. rewrite (root_size_gt1 _ (root_annul_pet_alg _)) //. by rewrite map_poly_eq0 annul_pet_alg_neq0 ?annul_alg_neq0. move: hpq=> /(f_equal (map_poly (map_poly (to_alg _)))). @@ -1399,13 +1372,12 @@ by rewrite -ler_to_alg from_algK hax -ler_to_alg from_algK. Qed. HB.instance Definition _ := Num.RealField_isClosed.Build (alg F) ivt. -HB.instance Definition _ := Num.RealClosedField.on {alg F}. End AlgAlgAlg. End RealAlg. HB.export RealAlg. -Notation "{ 'realclosure' F }" := (RealAlg.alg_of (Phant F)). +Notation "{ 'realclosure' F }" := (RealAlg.alg F). Notation annul_realalg := RealAlg.annul_alg. Notation realalg_of F := (@RealAlg.to_alg_def _ (Phant F)). @@ -1442,19 +1414,8 @@ Definition realalg := {realclosure rat}. HB.instance Definition _ := Num.RealClosedField.on realalg. Module RatRealAlg. -HB.instance Definition _ := Countable.copy - (RealAlg.algdom [archiFieldType of rat]) - (pcan_type (@RealAlg.encode_algdomK [archiFieldType of rat])). -HB.instance Definition _ := Countable.on realalg. +HB.instance Definition _ := Countable.copy (RealAlg.algdom rat) + (pcan_type (@RealAlg.encode_algdomK rat)). +#[export] HB.instance Definition _ := Countable.on realalg. End RatRealAlg. HB.export RatRealAlg. - -(* From mathcomp -Require Import countalg. *) -(* Canonical realalg_countZmodType := [countZmodType of realalg]. *) -(* Canonical realalg_countRingType := [countRingType of realalg]. *) -(* Canonical realalg_countComRingType := [countComRingType of realalg]. *) -(* Canonical realalg_countUnitRingType := [countUnitRingType of realalg]. *) -(* Canonical realalg_countComUnitRingType := [countComUnitRingType of realalg]. *) -(* Canonical realalg_countIdomainType := [countIdomainType of realalg]. *) -(* Canonical realalg_countFieldTypeType := [countFieldType of realalg]. *)