From 3d59e27836b665d63240af898fa8086cb29a9cd5 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 3 Dec 2020 20:00:21 +0100 Subject: [PATCH 1/2] update scripts to mathcomp 1.11 + fix namespace --- _CoqProject | 8 +++++++ meta.yml | 2 +- theories/cauchyreals.v | 16 ++++++------- theories/complex.v | 8 ++++--- theories/ordered_qelim.v | 49 ++++++++++++++++++++-------------------- theories/polyorder.v | 2 +- theories/polyrcf.v | 30 ++++++++++++------------ theories/qe_rcf.v | 14 +++++------- theories/qe_rcf_th.v | 6 ++--- theories/realalg.v | 15 ++++++------ 10 files changed, 79 insertions(+), 71 deletions(-) diff --git a/_CoqProject b/_CoqProject index bceb192..c44e700 100644 --- a/_CoqProject +++ b/_CoqProject @@ -10,3 +10,11 @@ theories/realalg.v theories/mxtens.v -R theories mathcomp.real_closed +-arg -w -arg -projection-no-head-constant +-arg -w -arg -redundant-canonical-projection +-arg -w -arg -notation-overridden +-arg -w -arg +duplicate-clear +-arg -w -arg +non-primitive-record +-arg -w -arg +undeclared-scope +-arg -w -arg -ambiguous-paths +-arg -w -arg -uniform-inheritance diff --git a/meta.yml b/meta.yml index c0da14b..7190728 100644 --- a/meta.yml +++ b/meta.yml @@ -80,7 +80,7 @@ dependencies: description: |- [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough) -namespace: mathcomp +namespace: mathcomp.real_closed keywords: - name: real closed field diff --git a/theories/cauchyreals.v b/theories/cauchyreals.v index 6fd5ad2..e76b4f0 100644 --- a/theories/cauchyreals.v +++ b/theories/cauchyreals.v @@ -21,6 +21,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope creal_scope. Delimit Scope creal_scope with CR. Section poly_extra. @@ -43,7 +44,7 @@ Lemma size_nderivn (R : realDomainType) (p : {poly R}) n : size p^`N(n) = (size p - n)%N. Proof. rewrite -size_derivn nderivn_def -mulr_natl. -by rewrite -polyC1 -!polyC_muln size_Cmul // pnatr_eq0 -lt0n fact_gt0. +by rewrite -polyC1 -!polyCMn size_Cmul // pnatr_eq0 -lt0n fact_gt0. Qed. End poly_extra. @@ -531,7 +532,7 @@ Lemma splitf (n : nat) (e : F) : e = iterop n +%R (e / n%:R) e. Proof. case: n=> // n; set e' := (e / _). have -> : e = e' * n.+1%:R by rewrite mulfVK ?pnatr_eq0. -move: e'=> {e} e; rewrite iteropS. +move: e'=> {}e; rewrite iteropS. by elim: n=> /= [|n <-]; rewrite !mulr_natr ?mulr1n. Qed. @@ -694,7 +695,7 @@ Proof. apply: eq_crealP; exists (fun _ => 0%N). by move=> e i e_gt0 _; rewrite subrr normr0. Qed. -Hint Resolve eq_creal_refl. +Hint Resolve eq_creal_refl : core. Lemma neq_creal_sym x y : x != y -> y != x. Proof. @@ -802,7 +803,7 @@ Qed. Lemma le_creal_refl (x : creal) : (x <= x)%CR. Proof. by apply: (@le_crealP 0%N). Qed. -Hint Resolve le_creal_refl. +Hint Resolve le_creal_refl : core. Lemma lt_neq_creal (x y : creal) : (x < y)%CR -> x != y. Proof. @@ -1300,7 +1301,7 @@ have cop_q'_d': coprimep p' q'. by rewrite (dvdp_trans (dvdp_gcdr _ _)) ?dvdp_gdco. suff : (p' * q').[x] * (d ^+ (size p + size q)).[x] == 0. case/poly_mul_creal_eq0_coprime. - + by rewrite coprimep_expr // coprimep_mull ?coprimep_gdco. + + by rewrite coprimep_expr // coprimepMl ?coprimep_gdco. + move=> p'q'x_eq0. have : p'.[x] * q'.[x] == 0 by rewrite -horner_crealM. case/poly_mul_creal_eq0_coprime=> // /dvdp_creal_eq0 hp'q'. @@ -1493,7 +1494,7 @@ rewrite ger0_norm; last first. 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 normrX; case: (val l)=> // {l} l. +rewrite normrX; case: (val l)=> // {}l. by rewrite ler_pexpn2r -?topredE //= ?uboundP ?ltW ?ubound_gt0. Qed. @@ -1670,8 +1671,7 @@ Notation "x ^+ n" := (exp_creal x n) : creal_scope. Notation "`| x |" := (norm_creal x) : creal_scope. -Hint Resolve eq_creal_refl. -Hint Resolve le_creal_refl. +Hint Resolve eq_creal_refl le_creal_refl : core. Notation lbound_of p := (@lboundP _ _ _ p _ _ _). Notation lbound0_of p := (@lbound0P _ _ p _ _ _). diff --git a/theories/complex.v b/theories/complex.v index 2240a5a..58bdd5a 100644 --- a/theories/complex.v +++ b/theories/complex.v @@ -7,6 +7,7 @@ From mathcomp Require Import bigop order ssralg ssrint div ssrnum rat poly closed_field. From mathcomp Require Import polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg. +From mathcomp Require Import mxpoly. (**********************************************************************) (* This files defines the extension R[i] of a real field R, *) @@ -37,6 +38,7 @@ Local Notation sqrtr := Num.sqrt. Record complex (R : Type) : Type := Complex { Re : R; Im : R }. +Declare Scope complex_scope. Delimit Scope complex_scope with C. Local Open Scope complex_scope. @@ -797,7 +799,7 @@ rewrite !xpair_eqE /= [_ == i']eq_sym [_ == j']eq_sym (negPf neq'_ij) /=. set z := (_ && _); suff /negPf -> : ~~ z by rewrite subrr mulr0. by apply: contraL lt_j'i' => /andP [/eqP <- /eqP <-]; rewrite ltnNge ltnW. Qed. -Hint Resolve skew_direct_sum. +Hint Resolve skew_direct_sum : core. Lemma rank_skew : \rank skew = (n * n.-1)./2. Proof. @@ -1054,7 +1056,7 @@ pose L2fun : 'M[R]_n -> _ := \+ ((mulmx (u^T) \o trmx) \+ (mulmx (v^T)))). pose L2 := lin_mx [linear of L2fun]. have [] := @Lemma4 _ _ 1%:M _ [::L1; L2] (erefl _). -+ by move: HrV; rewrite mxrank1 !dvdn2 ?negbK odd_mul andbb. ++ by move: HrV; rewrite mxrank1 !dvdn2 ?negbK oddM andbb. + by move=> ? _ /=; rewrite submx1. + suff {f fE}: L1 *m L2 = L2 *m L1. move: L1 L2 => L1 L2 commL1L2 La Lb. @@ -1131,7 +1133,7 @@ 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. have n_odd : odd n by rewrite dvdn2 /= ?negbK in dvd2n *. - have {2}<- : odd (n.+1 * n) = 0%N :> nat by rewrite odd_mul /= andNb. + have {2}<- : odd (n.+1 * n) = 0%N :> nat by rewrite oddM /= andNb. by rewrite odd_double_half Gauss_dvdl // coprime_pexpl // coprime2n. + move=> L; rewrite 2!in_cons in_nil orbF => /orP [] /eqP ->; apply/rV_subP => v /submxP [s -> {v}]; rewrite mulmxA; apply/skewP; diff --git a/theories/ordered_qelim.v b/theories/ordered_qelim.v index ad22a36..bbc9259 100644 --- a/theories/ordered_qelim.v +++ b/theories/ordered_qelim.v @@ -79,7 +79,7 @@ Canonical term_eqType (T : eqType) := Arguments term_eqP T {x y}. Prenex Implicits term_eq. - +Declare Scope oterm_scope. Bind Scope oterm_scope with term. Bind Scope oterm_scope with formula. Delimit Scope oterm_scope with oT. @@ -169,6 +169,7 @@ Definition le_of_oclause (R : Type) (x : oclause R) := End OrderedClause. +Declare Scope oclause_scope. Delimit Scope oclause_scope with OCLAUSE. Open Scope oclause_scope. @@ -364,60 +365,60 @@ split=> t1. - rewrite /eq0_rform; move: (ub_var t1) => m. set tr := _ m. suffices: all (@rterm R) (tr.1 :: tr.2)%PAIR. - case: tr => {t1} t1 r /= /andP[t1_r]. + case: tr => {}t1 r /= /andP[t1_r]. by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr. have: all (@rterm R) [::] by []. rewrite {}/tr; elim: t1 [::] => //=. + move=> t1 IHt1 t2 IHt2 r. - move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r]. - move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r]. + move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. + move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. + by move=> t1 IHt1 r /IHt1; case: to_rterm. + by move=> t1 IHt1 n r /IHt1; case: to_rterm. + move=> t1 IHt1 t2 IHt2 r. - move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r]. - move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r]. + move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. + move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. + move=> t1 IHt1 r. - by move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /=; rewrite all_rcons. + by move/IHt1; case: to_rterm => {r IHt1}t1 r /=; rewrite all_rcons. + by move=> t1 IHt1 n r /IHt1; case: to_rterm. - rewrite /lt0_rform; move: (ub_var t1) => m; set tr := _ m. suffices: all (@rterm R) (tr.1 :: tr.2)%PAIR. - case: tr => {t1} t1 r /= /andP[t1_r]. + case: tr => {}t1 r /= /andP[t1_r]. by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr. have: all (@rterm R) [::] by []. rewrite {}/tr; elim: t1 [::] => //=. + move=> t1 IHt1 t2 IHt2 r. - move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r]. - move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r]. + move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. + move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. + by move=> t1 IHt1 r /IHt1; case: to_rterm. + by move=> t1 IHt1 n r /IHt1; case: to_rterm. + move=> t1 IHt1 t2 IHt2 r. - move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r]. - move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r]. + move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. + move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. + move=> t1 IHt1 r. - by move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /=; rewrite all_rcons. + by move/IHt1; case: to_rterm => {r IHt1}t1 r /=; rewrite all_rcons. + by move=> t1 IHt1 n r /IHt1; case: to_rterm. - rewrite /leq0_rform; move: (ub_var t1) => m; set tr := _ m. suffices: all (@rterm R) (tr.1 :: tr.2)%PAIR. - case: tr => {t1} t1 r /= /andP[t1_r]. + case: tr => {}t1 r /= /andP[t1_r]. by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr. have: all (@rterm R) [::] by []. rewrite {}/tr; elim: t1 [::] => //=. + move=> t1 IHt1 t2 IHt2 r. - move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r]. - move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r]. + move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. + move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. + by move=> t1 IHt1 r /IHt1; case: to_rterm. + by move=> t1 IHt1 n r /IHt1; case: to_rterm. + move=> t1 IHt1 t2 IHt2 r. - move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r]. - move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r]. + move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. + move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. + move=> t1 IHt1 r. - by move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /=; rewrite all_rcons. + by move/IHt1; case: to_rterm => {r IHt1}t1 r /=; rewrite all_rcons. + by move=> t1 IHt1 n r /IHt1; case: to_rterm. Qed. @@ -546,8 +547,8 @@ elim: t r0 m => /=; try do [ first by [rewrite takel_cat // -htake1 size_take geq_minr]; rewrite -(rsub_acc r1 r3 t1') {hub1'}// -{htake1}htake2 {r3}cat_take_drop; by elim: r2 m => //= u r2 IHr2 m; rewrite IHr2 -| do [ move=> t1 IHt1 r m; do 2!move/IHt1=> {IHt1}IHt1 - | move=> t1 IHt1 n r m; do 2!move/IHt1=> {IHt1}IHt1]; +| do [ move=> t1 IHt1 r m; do 2!move/IHt1=> {}IHt1 + | move=> t1 IHt1 n r m; do 2!move/IHt1=> {}IHt1]; case: to_rterm IHt1 => t1' r1 [-> -> hsub1 <-]; split=> {hsub1}//; by elim: r1 m => //= u r1 IHr1 m; rewrite IHr1]. move=> t1 IH r m letm /IH {IH} /(_ letm) {letm}. @@ -715,7 +716,7 @@ have and_ok bcs1 bcs2: ok bcs1 -> ok bcs2 -> ok (and_odnf bcs1 bcs2). case/and3P=> ok11 ok12 ok1 ok2; rewrite cat_ok ?{}IH1 {bcs1 ok1}//. elim: bcs2 ok2 => //= cl2 bcs2 IH2 /andP[ok2 /IH2->]. by rewrite /dnf_rterm /= !all_cat andbT ok11; case/and3P: ok12=> -> -> ->. -elim: f b => //=; try by [move=> _ ? ? [] | move=> ? ? ? ? [] /= /andP[]; auto]. +elim: f b => //=; do ?by [move=> ? ? ? [] | move=> ? ? ? ? [] /= /andP[]; auto]. - by do 2!case. - by rewrite /dnf_rterm => ? ? [] /= ->. - by rewrite /dnf_rterm => ? ? [] /=; rewrite andbC !andbT. @@ -1034,7 +1035,7 @@ rewrite /oclause_to_w /= !all_map. apply/allP => [] [oc_eq oc_neq oc_le oc_lt] hoc; rewrite /dnf_rterm /= andbT. rewrite -all_cat; apply/allP=> u hu; move/terms_of_neq_leq_elim: hoc => /=. move/(_ u); rewrite !mem_cat. -have {hu} hu : [|| u \in oc_eq, u \in oc_neq, u \in oc_le | u \in oc_lt]. +have {}hu : [|| u \in oc_eq, u \in oc_neq, u \in oc_le | u \in oc_lt]. by move: hu; rewrite mem_cat; case/orP=> ->; rewrite ?orbT. move/(_ hu); case/orP; last first. move: rneq. @@ -1083,7 +1084,7 @@ have -> : move: (dnf_rterm_subproof hdnf). rewrite /oclause_to_w; elim: (oclause_neq_leq_elim bc) => /= [|a l ih]. by split=> //; case. -case/andP=> h1 h2; have {ih h2} ih := (ih h2); split. +case/andP=> h1 h2; have {h2} ih := (ih h2); split. - case/orP. move/(valid_QE_wproj i e h1)=> /= [x /=] [] // [] h2 [] _ [] h3 _; exists x. by left. diff --git a/theories/polyorder.v b/theories/polyorder.v index 4a96dcc..4134fc0 100644 --- a/theories/polyorder.v +++ b/theories/polyorder.v @@ -164,7 +164,7 @@ Qed. Lemma mu_opp p x : \mu_x (-p) = \mu_x p. Proof. -rewrite -mulN1r -polyC1 -polyC_opp mul_polyC mu_mulC //. +rewrite -mulN1r -polyC1 -polyCN mul_polyC mu_mulC //. by rewrite -oppr0 (inj_eq (inv_inj (@opprK _))) oner_eq0. Qed. diff --git a/theories/polyrcf.v b/theories/polyrcf.v index a6611c0..688a408 100644 --- a/theories/polyrcf.v +++ b/theories/polyrcf.v @@ -115,7 +115,7 @@ Section SgpInfty. Lemma sgp_pinfty_sym p : sgp_pinfty (p \Po -'X) = sgp_minfty p. Proof. rewrite /sgp_pinfty /sgp_minfty lead_coef_comp ?size_opp ?size_polyX //. -by rewrite lead_coef_opp lead_coefX mulrC. +by rewrite lead_coefN lead_coefX mulrC. Qed. Lemma poly_pinfty_gt_lc p : @@ -197,22 +197,22 @@ Proof. move=> p_neq0 x; rewrite in_itv /=; apply/contra_leN. by case/rootP/(cauchy_boundP p_neq0)/ltr_normlP; rewrite ltr_oppl. Qed. -Hint Resolve le_cauchy_bound. +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. Qed. -Hint Resolve ge_cauchy_bound. +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. -Hint Resolve cauchy_bound_gt0. +Hint Resolve cauchy_bound_gt0 : core. Lemma cauchy_bound_ge0 p : cauchy_bound p >= 0. Proof. by rewrite ltW. Qed. -Hint Resolve cauchy_bound_ge0. +Hint Resolve cauchy_bound_ge0 : core. End CauchyBound. @@ -843,7 +843,7 @@ case: eqVneq => [->|p0]; first by exists [::]; constructor. case: (boolP (p^`() == 0)) => [|p'0]. rewrite -derivn1 -derivn_poly0 => /size1_polyC pC; exists [::]. by constructor=> // x; rewrite pC rootC -polyC_eq0 -pC (negPf p0) andbF. -have {ihn} /ihn /(_ a b) [sp'] : (size p^`() <= n)%N. +have {}/ihn /(_ a b) [sp'] : (size p^`() <= n)%N. rewrite -ltnS; apply: leq_trans sp; rewrite size_deriv prednK // lt0n. by rewrite size_poly_eq0 p0. elim: sp' a => [|r1 sp' hsp'] a hp'. @@ -896,18 +896,18 @@ Proof. by case: rootsP=> //=; rewrite eqxx. Qed. Lemma roots_on_roots : forall p a b, p != 0 -> roots_on p `]a, b[ (roots p a b). Proof. by move=> a b p; case: rootsP. Qed. -Hint Resolve roots_on_roots. +Hint Resolve roots_on_roots : core. Lemma sorted_roots a b p : sorted <%R (roots p a b). Proof. by case: rootsP. Qed. -Hint Resolve sorted_roots. +Hint Resolve sorted_roots : core. Lemma path_roots p a b : path <%R a (roots p a b). Proof. case: rootsP=> //= p0 hp sp; rewrite path_min_sorted //. by apply/allP=> y; rewrite -hp; case/andP => /itvP ->. Qed. -Hint Resolve path_roots. +Hint Resolve path_roots : core. Lemma root_is_roots (p : {poly R}) (a b : R) : p != 0 -> forall x, x \in `]a, b[ -> root p x = (x \in roots p a b). @@ -1264,7 +1264,7 @@ have [->|p0] := eqVneq p 0; first by rewrite roots0. by apply: (@sorted_uniq _ <%R); [apply: lt_trans | apply: ltxx|]. Qed. -Hint Resolve uniq_roots. +Hint Resolve uniq_roots : core. Lemma in_roots p (a b x : R) : (x \in roots p a b) = [&& root p x, x \in `]a, b[ & p != 0]. @@ -1421,7 +1421,7 @@ 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} p. +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. @@ -1461,7 +1461,7 @@ 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} p. +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. @@ -1663,7 +1663,7 @@ Lemma rootsRP p a b : Proof. move=> rpa rpb. have [->|p_neq0] := eqVneq p 0; first by rewrite rootsR0 roots0. -apply: (eq_sorted_irr lt_trans); rewrite ?sorted_roots // => x. +apply: (irr_sorted_eq lt_trans); rewrite ?sorted_roots // => x. rewrite -roots_on_rootsR -?roots_on_roots //=. case: (boolP (root _ _)); rewrite ?(andbT, andbF) //. apply: contraLR; rewrite in_itv negb_and -!leNgt. @@ -1677,10 +1677,10 @@ Proof. rewrite /sgp_pinfty; wlog lp_gt0 : x p / lead_coef p > 0 => [hwlog|rpx y Hy]. have [|/(hwlog x p) //|/eqP] := ltrgtP (lead_coef p) 0; last first. by rewrite lead_coef_eq0 => /eqP -> ? ? ?; rewrite lead_coef0 horner0. - rewrite -[p]opprK lead_coef_opp oppr_cp0 => /(hwlog x _) Hp HNp y Hy. + rewrite -[p]opprK lead_coefN oppr_cp0 => /(hwlog x _) Hp HNp y Hy. by rewrite hornerN !sgrN Hp => // z /HNp; rewrite rootN. have [z Hz] := poly_pinfty_gt_lc lp_gt0. -have {Hz} Hz u : u \in `[z, +oo[ -> Num.sg p.[u] = 1. +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) //. diff --git a/theories/qe_rcf.v b/theories/qe_rcf.v index 0138efa..deca5d2 100644 --- a/theories/qe_rcf.v +++ b/theories/qe_rcf.v @@ -100,6 +100,7 @@ Definition to_rterm := fix loop (t : GRing.term R) : term := End QF. +Declare Scope qf_scope. Bind Scope qf_scope with term. Bind Scope qf_scope with formula. Delimit Scope qf_scope with qfT. @@ -581,14 +582,14 @@ Lemma eval_NatMulPoly p n e : eval_poly e (n +** p)%qfT = (eval_poly e p) *+ n. Proof. elim: p; rewrite //= ?mul0rn // => c p ->. -rewrite mulrnDl mulr_natl polyC_muln; congr (_+_). +rewrite mulrnDl mulr_natl polyCMn; congr (_+_). by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC. Qed. Lemma eval_OppPoly p e : eval_poly e (-- p)%qfT = - eval_poly e p. Proof. elim: p; rewrite //= ?oppr0 // => t ts ->. -by rewrite !mulNr !opprD polyC_opp mul1r. +by rewrite !mulNr !opprD polyCN mul1r. Qed. Lemma eval_Horner e p x : eval e (Horner p x) = (eval_poly e p).[eval e x]. @@ -804,12 +805,9 @@ Qed. Lemma eval_PolyComb e sq sc : eval_poly e (PolyComb sq sc) = poly_comb (map (eval_poly e) sq) sc. Proof. -rewrite /PolyComb /poly_comb size_map. -rewrite -BigOp.bigopE -val_enum_ord -filter_index_enum !big_map. -apply: (big_ind2 (fun u v => eval_poly e u = v)). -+ by rewrite /= mul0r add0r. -+ by move=> x x' y y'; rewrite eval_MulPoly=> -> ->. -by move=> i _; rewrite eval_ExpPoly /= (nth_map [::]). +rewrite /PolyComb /poly_comb size_map -BigOp.bigopE -val_enum_ord/= big_map. +rewrite (@big_morph _ _ _ 1%R *%R _ _ (eval_MulPoly _))/= ?mul0r ?add0r//. +by rewrite big_enum; under eq_bigr do rewrite eval_ExpPoly/= -(nth_map _ 0)//. Qed. Definition pcq (sq : seq {poly F}) i := diff --git a/theories/qe_rcf_th.v b/theories/qe_rcf_th.v index 5445612..16a3691 100644 --- a/theories/qe_rcf_th.v +++ b/theories/qe_rcf_th.v @@ -969,7 +969,7 @@ Qed. Lemma changes_mods_cindex p q : changes_mods p q = cindexR q p. Proof. -elim: mods {-2}p {-2}q (erefl (mods p q)) => [|r s IHs] {p q} p q hrpq. +elim: mods {-2}p {-2}q (erefl (mods p q)) => [|r s IHs] {}p {}q hrpq. move/eqP: hrpq; rewrite mods_eq0 => /eqP ->. by rewrite changes_mods0p cindexRpC. rewrite changes_mods_rec cindexR_rec IHs //. @@ -1025,7 +1025,7 @@ Lemma changes_itv_mods_cindex a b : a < b -> forall p q, changes_itv_mods a b p q = cindex a b q p. Proof. move=> hab p q. -elim: mods {-2}p {-2}q (erefl (mods p q)) => [|r s IHs] {p q} p q hrpq. +elim: mods {-2}p {-2}q (erefl (mods p q)) => [|r s IHs] {}p {}q hrpq. move/eqP: hrpq; rewrite mods_eq0 => /eqP ->. by rewrite changes_itv_mods0p cindexpC. have p_neq0 : p != 0 by rewrite -(mods_eq0 p q) hrpq. @@ -1279,7 +1279,7 @@ have [|bq_neq0] := boolP (bounding_poly sq == 0). apply/andP; split; apply/hasP; by exists 0; rewrite //= ?lead_coef0 ?mulr0 ltxx. move=> /size_prod_eq1 Hsq. - have {Hsq} Hsq q : q \in sq -> q = (lead_coef q)%:P. + have {}Hsq q : q \in sq -> q = (lead_coef q)%:P. by move=> /Hsq sq1; rewrite [q]size1_polyC ?sq1 // lead_coefC. apply: (@equivP (\big[andb/true]_(q <- sq) (0 < lead_coef q))); last first. split; [move=> sq0; exists 0; move: sq0|move=> [x]]; diff --git a/theories/realalg.v b/theories/realalg.v index d65d095..1037b80 100644 --- a/theories/realalg.v +++ b/theories/realalg.v @@ -73,14 +73,14 @@ Record algcreal := AlgCReal { Lemma monic_annul_creal x : annul_creal x \is monic. Proof. by case: x. Qed. -Hint Resolve monic_annul_creal. +Hint Resolve monic_annul_creal : core. Lemma annul_creal_eq0 x : (annul_creal x == 0) = false. Proof. by rewrite (negPf (monic_neq0 _)). Qed. Lemma root_annul_creal x : ((annul_creal x).[x] == 0)%CR. Proof. by case: x. Qed. -Hint Resolve root_annul_creal. +Hint Resolve root_annul_creal : core. Definition cst_algcreal (x : F) := AlgCReal (monicXsubC _) (@root_cst_creal _ x). @@ -137,8 +137,7 @@ Lemma div_annihilant_algcreal_neq0 (x y : algcreal) : div_annihilant (annul_creal x) (annul_creal y) != 0. Proof. by move=> ?; rewrite div_annihilant_neq0 ?monic_neq0. Qed. -Hint Resolve eq_creal_refl. -Hint Resolve le_creal_refl. +Hint Resolve eq_creal_refl le_creal_refl : core. Lemma simplify_algcreal (x : algcreal) (x_neq0 : (x != 0)%CR) : {y | ((annul_creal y).[0] != 0) & ((y != 0)%CR * (x == y)%CR)%type}. @@ -345,7 +344,7 @@ Record algdom := AlgDom { Lemma radius_alg_ge0 x : 0 <= radius_alg x. Proof. by case: x. Qed. Lemma monic_annul_algdom x : annul_algdom x \is monic. Proof. by case: x. Qed. -Hint Resolve monic_annul_algdom. +Hint Resolve monic_annul_algdom : core. Lemma annul_algdom_eq0 x : (annul_algdom x == 0) = false. Proof. by rewrite (negPf (monic_neq0 _)). Qed. @@ -1498,15 +1497,15 @@ Local Notation "p ^ f" := (map_poly f p) : ring_scope. Lemma root_annul_realalg (x : R) : root ((annul_realalg x) ^ realalg_of _) x. Proof. exact: RealAlg.root_annul_alg. Qed. -Hint Resolve root_annul_realalg. +Hint Resolve root_annul_realalg : core. Lemma monic_annul_realalg (x : R) : annul_realalg x \is monic. Proof. exact: RealAlg.monic_annul_alg. Qed. -Hint Resolve monic_annul_realalg. +Hint Resolve monic_annul_realalg : core. Lemma annul_realalg_neq0 (x : R) : annul_realalg x != 0%R. Proof. exact: RealAlg.annul_alg_neq0. Qed. -Hint Resolve annul_realalg_neq0. +Hint Resolve annul_realalg_neq0 : core. Lemma realalg_algebraic : integralRange (realalg_of F). Proof. by move=> x; exists (annul_realalg x). Qed. From 4adc1e54cffd7fad254b30fd168c5b791a191b91 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 3 Dec 2020 21:22:13 +0100 Subject: [PATCH 2/2] Update theories/cauchyreals.v --- theories/cauchyreals.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/cauchyreals.v b/theories/cauchyreals.v index e76b4f0..037c64a 100644 --- a/theories/cauchyreals.v +++ b/theories/cauchyreals.v @@ -1671,7 +1671,7 @@ Notation "x ^+ n" := (exp_creal x n) : creal_scope. Notation "`| x |" := (norm_creal x) : creal_scope. -Hint Resolve eq_creal_refl le_creal_refl : core. +#[global] Hint Resolve eq_creal_refl le_creal_refl : core. Notation lbound_of p := (@lboundP _ _ _ p _ _ _). Notation lbound0_of p := (@lbound0P _ _ p _ _ _).