From 3a16c95f28fe05bcb012baada4469720a3d506e5 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 3 Jun 2020 20:55:17 +0200 Subject: [PATCH] Compat with new maximum in math-comp --- .travis.yml | 4 ++-- config.nix | 2 +- theories/cauchyreals.v | 48 +++++++++++++++++++++--------------------- theories/complex.v | 4 ++-- theories/polyrcf.v | 46 ++++++++++++++++++++-------------------- theories/qe_rcf_th.v | 8 +++---- 6 files changed, 56 insertions(+), 56 deletions(-) diff --git a/.travis.yml b/.travis.yml index 2785dcf..2aac811 100644 --- a/.travis.yml +++ b/.travis.yml @@ -43,7 +43,7 @@ install: | opam repo list opam list sudo chown -R coq:coq /home/coq/${CONTRIB_NAME} - opam pin add -y -n coq-mathcomp-real-closed . + opam pin add -y -n -k path coq-mathcomp-real-closed.dev . opam install -y -vvv --deps-only coq-mathcomp-real-closed " script: @@ -53,7 +53,7 @@ script: export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' set -ex eval \$(opam env) - opam install -y coq-mathcomp-real-closed + opam install -y -vvv coq-mathcomp-real-closed " - docker stop COQ # optional - echo -en 'travis_fold:end:script\\r' diff --git a/config.nix b/config.nix index afc2ea7..79484a6 100644 --- a/config.nix +++ b/config.nix @@ -1,4 +1,4 @@ { coq = "8.10"; - mathcomp = "1.11.0+beta1"; + mathcomp = "mathcomp-1.11.0"; } diff --git a/theories/cauchyreals.v b/theories/cauchyreals.v index 694b4c6..6fd5ad2 100644 --- a/theories/cauchyreals.v +++ b/theories/cauchyreals.v @@ -118,7 +118,7 @@ have [|r_lt0] := lerP 0 r; last first. 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 ?lexU ?mulr_ge0 ?ger0E ?ltW. + by rewrite exprn_ge0 ?le_maxr ?mulr_ge0 ?ger0E ?ltW. rewrite -{1}(addNKr x y) [- _ + _]addrC /= -mulrA. rewrite nderiv_taylor; last exact: mulrC. have [->|p_neq0] := eqVneq p 0. @@ -132,7 +132,7 @@ rewrite exprSr mulrA !normrM mulrC ler_wpmul2l ?normr_ge0 //. suff /ler_wpmul2l /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 // lexU ler01 mulr_ge0 ?ler0n ?ltW. + by rewrite ?exprn_ge0 // le_maxr 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. @@ -150,7 +150,7 @@ Proof. rewrite /poly_accr_bound pmulr_rgt0 //. rewrite ltr_paddr ?ltr01 //. by rewrite sumr_ge0 // => i; rewrite poly_bound_ge0. -by rewrite exprn_gt0 // ltxU ltr01 pmulr_rgt0 ?ltr0n. +by rewrite exprn_gt0 // lt_maxr ltr01 pmulr_rgt0 ?ltr0n. Qed. Lemma poly_accr_bound_ge0 p a r : 0 <= poly_accr_bound p a r. @@ -212,7 +212,7 @@ Proof. rewrite /poly_accr_bound pmulr_rgt0 //. rewrite ltr_paddr ?ltr01 //. by rewrite sumr_ge0 // => i; rewrite poly_bound_ge0. -by rewrite exprn_gt0 // ltxU ltr01 pmulr_rgt0 ?ltr0n. +by rewrite exprn_gt0 // lt_maxr ltr01 pmulr_rgt0 ?ltr0n. Qed. Lemma poly_accr_bound2_ge0 p a r : 0 <= poly_accr_bound2 p a r. @@ -230,7 +230,7 @@ rewrite le0r=> /orP[/eqP->|r_gt0]. 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 ?lexU ?mulr_ge0 ?ger0E ?ltW. + by rewrite exprn_ge0 ?le_maxr ?mulr_ge0 ?ger0E ?ltW. rewrite -{1}(addNKr x y) [- _ + _]addrC /= -mulrA. rewrite nderiv_taylor; last exact: mulrC. have [->|p_neq0] := eqVneq p 0. @@ -250,7 +250,7 @@ rewrite normrM normrX 3!exprSr expr1 !mulrA !ler_wpmul2r ?normr_ge0 //. suff /ler_wpmul2l /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 // lexU ler01 mulr_ge0 ?ler0n ?ltW. + by rewrite ?exprn_ge0 // le_maxr ler01 mulr_ge0 ?ler0n ?ltW. case: (leP _ 1)=> hr. rewrite expr1n exprn_ile1 ?normr_ge0 //. rewrite (le_trans (ler_dist_add a _ _)) // addrC distrC. @@ -358,7 +358,7 @@ rewrite ler_pdivl_mulr ?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 leIx lexU !ler_distl /=. +rewrite le_minl le_maxr !ler_distl /=. set le := <=%R; rewrite {}/le. have [] := lerP=> /= a1N; have [] := lerP=> //= a1P; have [] := lerP=> //= a2P; rewrite ?(andbF, andbT) //; symmetry. @@ -405,7 +405,7 @@ move=> [] accr2_p; last first. by rewrite mulrC ler_wpmul2r // 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 ltxI k1_gt0. +exists (minr k1 k2); first by rewrite lt_minr 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. @@ -416,11 +416,11 @@ move=> {h1} {h2} {sm1}. wlog le_xr1 : a1 a2 r1 r2 k1 k2 r1_gt0 r2_gt0 k1_gt0 k2_gt0 har hk1 hk2 / `|x - a1| <= r1. move=> hwlog h; move: (h)=> /orP [/hwlog|]; first exact. - move=> /(hwlog a2 a1 r2 r1 k2 k1) hwlog' ley; rewrite meetC. + move=> /(hwlog a2 a1 r2 r1 k2 k1) hwlog' ley; rewrite minC. by apply: hwlog'; rewrite 1?orbC // distrC [r2 + _]addrC. move=> _. have [le_yr1|gt_yr1] := (lerP _ r1)=> /= [_|le_yr2]. - by rewrite ltIx hk1. + by rewrite lt_minl hk1. rewrite ltr_pdivl_mulr ?subr_gt0 //. pose z := a1 - r1. have hz1 : `|z - a1| <= r1 by rewrite addrC addKr normrN gtr0_norm. @@ -439,7 +439,7 @@ have hz2 : `|z - a2| <= r2. by rewrite (monoRL (addrK _) (ler_add2r _)) addrC ltW. by move: le_yr2; rewrite ler_norml=> /andP[]. have [<-|neq_zx] := eqVneq z x. - by rewrite -ltr_pdivl_mulr ?subr_gt0 // ltIx hk2 ?orbT // gt_eqF. + by rewrite -ltr_pdivl_mulr ?subr_gt0 // lt_minl hk2 ?orbT // gt_eqF. have lt_zx : z < x. rewrite lt_neqAle neq_zx /=. move: le_xr1; rewrite distrC ler_norml=> /andP[_]. @@ -447,9 +447,9 @@ have lt_zx : z < x. 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 ltIx hk1 ?gt_eqF. + by rewrite lt_minl hk1 ?gt_eqF. rewrite -ltr_pdivl_mulr ?subr_gt0 //. -by rewrite ltIx hk2 ?orbT ?gt_eqF. +by rewrite lt_minl hk2 ?orbT ?gt_eqF. Qed. End monotony. @@ -874,13 +874,13 @@ 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 ?ltxU ?b_gt0. + by elim: iota b => //= a l IHl b b_gt0; rewrite IHl ?lt_maxr ?b_gt0. have [|le_in] := (ltnP n i). elim: i b => [|i IHi] b //. - rewrite ltnS -addn1 iota_add add0n map_cat foldl_cat /= lexU leq_eqVlt. + rewrite ltnS -addn1 iota_add add0n map_cat foldl_cat /= le_maxr 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 ?lexU ?Hxb. + 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 rewrite (le_trans (ler_dist_dist _ _)) ?ltW ?cauchymodP. by close. @@ -1363,7 +1363,7 @@ pose r : F := minr 1 (minr (diff px_gt0 / 4%:R / b1) (diff px_gt0 / 4%:R / b2 / 2%:R)). exists r. - rewrite !ltxI ?ltr01 ?pmulr_rgt0 ?gtr0E ?diff_gt0; + rewrite !lt_minr ?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. @@ -1372,7 +1372,7 @@ pose_big_enough i. 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 ?leIx ?lexx ?uboundP. + + by rewrite ler_add ?le_minl ?lexx ?uboundP. move=> /(_ isT isT). rewrite ler_distl=> /andP[le_py ge_py]. rewrite (lt_le_trans _ le_py) // subr_gt0 -/b1. @@ -1380,7 +1380,7 @@ pose_big_enough i. apply: le_lt_trans (_ : r * b1 < _). by rewrite ler_wpmul2r ?poly_accr_bound_ge0. rewrite -ltr_pdivl_mulr ?poly_accr_bound_gt0 //. - rewrite !ltIx ltr_pmul2r ?invr_gt0 ?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. exists (diff px_gt0 / 4%:R). by rewrite pmulr_rgt0 ?gtr0E ?diff_gt0. @@ -1391,11 +1391,11 @@ pose_big_enough i. 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 ?leIx ?lexx ?uboundP. + + by rewrite ler_add ?le_minl ?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 ?leIx ?lexx ?uboundP. + + by rewrite ler_add ?le_minl ?lexx ?uboundP. rewrite ler_paddl ?uboundP ?ler01 //. move=> /(_ isT isT); rewrite ler_distl=> /andP [haccr _]. move=> /(_ isT isT); rewrite ler_distl=> /andP [hp' _]. @@ -1409,9 +1409,9 @@ pose_big_enough i. rewrite (le_trans (ler_dist_add (x i) _ _)) //. apply: le_trans (_ : r * 2%:R <= _). by rewrite mulrDr mulr1 ler_add // distrC. - by rewrite -ler_pdivl_mulr ?ltr0n // !leIx lexx !orbT. + by rewrite -ler_pdivl_mulr ?ltr0n // !le_minl lexx !orbT. + rewrite -ler_pdivl_mulr ?poly_accr_bound_gt0 //. - by rewrite (le_trans hz) // !leIx lexx !orbT. + by rewrite (le_trans hz) // !le_minl lexx !orbT. by close. Qed. @@ -1518,7 +1518,7 @@ apply: le_trans (_ : u * vi <= _). move=> r2_gt1; rewrite ler_eexpn2l //. rewrite -subn1 leq_subLR add1n (leq_trans _ (leqSpred _)) //. by rewrite max_size_evalC. -rewrite ler_wpmul2l ?exprn_ge0 ?lexU ?ler01 // ler_add //. +rewrite ler_wpmul2l ?exprn_ge0 ?le_maxr ?ler01 // ler_add //. 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 _)) //. diff --git a/theories/complex.v b/theories/complex.v index dfa1a4b..2240a5a 100644 --- a/theories/complex.v +++ b/theories/complex.v @@ -618,10 +618,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) lexU lexx. + by rewrite -(maxrN a) le_maxr 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) lexU lexx orbT. + by rewrite -(maxrN a) le_maxr lexx orbT. congr (_ +i* _); set u := if _ then _ else _. rewrite mulrCA !mulrA. have->: (u * u) = 1. diff --git a/theories/polyrcf.v b/theories/polyrcf.v index c7d8ae6..b9f5fa8 100644 --- a/theories/polyrcf.v +++ b/theories/polyrcf.v @@ -148,7 +148,7 @@ rewrite lead_coefDl ?size_mul ?polyX_eq0 // ?lead_coefMX; last first. 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 leUx => /andP[/Hy Hq Hc]. +rewrite !hornerE le_maxl => /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). @@ -171,7 +171,7 @@ 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 leUx => /andP[/Hy Hq Hc]. +rewrite !hornerE le_maxl => /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). @@ -347,8 +347,8 @@ 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 ltxI dp. -move=> y; rewrite ltxI; case/andP=> hxye hxye'. +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. @@ -1210,9 +1210,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 /= lexU lexx orbT. -* by apply: subitvP hy=> /=; rewrite lexU !lexx. -* by rewrite hc bound_in_itv /= lexU lexx orbT. +* by rewrite bound_in_itv /= le_maxr lexx orbT. +* by apply: subitvP hy=> /=; rewrite le_maxr !lexx. +* by rewrite hc bound_in_itv /= le_maxr lexx orbT. Qed. Lemma next_root_gt p a b : a < b -> p != 0 -> next_root p a b > a. @@ -1220,7 +1220,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 ltxU ab. +* by rewrite lt_maxr ab. Qed. Lemma next_noroot p a b : {in `]a, (next_root p a b)[, noroot p}. @@ -1278,9 +1278,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 /= leIx lexx orbT. -* by apply: subitvP hy=> /=; rewrite leIx !lexx. -* by rewrite hc bound_in_itv /= leIx lexx orbT. +* by rewrite bound_in_itv /= le_minl lexx orbT. +* by apply: subitvP hy=> /=; rewrite le_minl !lexx. +* by rewrite hc bound_in_itv /= le_minl lexx orbT. Qed. Lemma prev_noroot p a b : {in `](prev_root p a b), b[, noroot p}. @@ -1296,7 +1296,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 ltIx ab. +* by rewrite lt_minl ab. Qed. Lemma is_prev_root p a b x : @@ -1457,20 +1457,20 @@ case: leP => //; case: next_rootP=> [|y np0 py0 hy|c np0 ->] hp hpq _. - by rewrite hornerM py0 mul0r. - move=> z hz /=; rewrite rootM negb_or ?hp //. by rewrite (@next_noroot _ a b) //; apply: subitvPr hz. -* case: (altP (q =P 0))=> q0. - move: hpq; rewrite q0 mulr0 root0 next_root0 leUx lexx andbT. - by move/join_r => ->; constructor. +* case: (altP (q =P 0)) => q0. + move: hpq; rewrite q0 mulr0 root0 next_root0 le_maxl lexx andbT. + by move/max_r->; constructor. constructor=> //; first by rewrite mulf_neq0. move=> z hz /=; rewrite rootM negb_or ?hp //. rewrite (@next_noroot _ a b) //; apply: subitvPr hz=> /=. - by move: hpq; rewrite leUx; case/andP. + by move: hpq; rewrite le_maxl; 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 /= !inE /= next_rootM. -by case: (a < x); rewrite // ltxI. +by case: (a < x); rewrite // lt_minr. Qed. Lemma prev_rootM a b (p q : {poly R}) : @@ -1488,19 +1488,19 @@ 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: (altP (q =P 0))=> q0. - move: hpq; rewrite q0 mulr0 root0 prev_root0 lexI lexx andbT. - by move/meet_r => ->; constructor. + move: hpq; rewrite q0 mulr0 root0 prev_root0 le_minr lexx andbT. + by move/min_r->; constructor. constructor=> //; first by rewrite mulf_neq0. move=> z hz /=; rewrite rootM negb_or ?hp //. rewrite (@prev_noroot _ a b) //; apply: subitvPl hz=> /=. - by move: hpq; rewrite lexI; case/andP. + by move: hpq; rewrite le_minr; 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 /= prev_rootM. -by case: (x < b); rewrite // ltUx !(andbT, andbF). +by case: (x < b); rewrite // lt_maxl !(andbT, andbF). Qed. Lemma neighpr_wit p x b : x < b -> p != 0 -> {y | y \in neighpr p x b}. @@ -1809,8 +1809,8 @@ rewrite /sgp_pinfty; wlog lp_gt0 : x p / lead_coef p > 0 => [hwlog|rpx y Hy]. have [z Hz] := poly_pinfty_gt_lc lp_gt0. have {Hz} Hz u : u \in `[z, +oo[ -> Num.sg p.[u] = 1. by rewrite inE andbT => /Hz pu_ge1; rewrite gtr0_sg // (lt_le_trans lp_gt0). -rewrite (@polyrN0_itv _ _ rpx (maxr y z)) ?inE /= ?lexU ?(itvP Hy) //. -by rewrite Hz ?gtr0_sg // inE /= lexU lexx orbT. +rewrite (@polyrN0_itv _ _ rpx (maxr y z)) ?inE /= ?le_maxr ?(itvP Hy) //. +by rewrite Hz ?gtr0_sg // inE /= le_maxr lexx orbT. Qed. Lemma sgp_minftyP x (p : {poly R}) : diff --git a/theories/qe_rcf_th.v b/theories/qe_rcf_th.v index 95e8e70..425beee 100644 --- a/theories/qe_rcf_th.v +++ b/theories/qe_rcf_th.v @@ -793,13 +793,13 @@ rewrite roots_cons; case/and5P => _ xab /eqP hax hx /eqP hs. rewrite !big_cons variation0r add0r (ihs _ _ hs) ?(itvP xab) // => {ihs}. pose y := (head b s); pose ax := midf a x; pose xy := midf x y. rewrite (@sjump_neigh a b _ _ _ ax xy) ?inE ?midf_lte//=; last 2 first. -+ by rewrite /prev_root pq_eq0 hax meet_l ?(itvP xab, midf_lte). ++ by rewrite /prev_root pq_eq0 hax min_l ?(itvP xab, midf_lte). + have hy: y \in `]x, b]. rewrite /y; case: s hs {y xy} => /= [|u s] hu. by rewrite boundr_in_itv /= ?(itvP xab). have /roots_in: u \in roots (p * q) x b by rewrite hu mem_head. by apply: subitvP; rewrite /= !lexx. - by rewrite /next_root pq_eq0 hs join_l ?(itvP hy, midf_lte). + by rewrite /next_root pq_eq0 hs max_l ?(itvP hy, midf_lte). move: @y @xy {hs}; rewrite /cross. by case: s => /= [|y l]; rewrite ?(big_cons, big_nil, variation0r, add0r). Qed. @@ -835,11 +835,11 @@ have pq0 : p * q != 0 by rewrite mulf_neq0. rewrite cindex_seq_mids // sum_varP /cross. apply: congr_variation; apply: (mulrIz (oner_neq0 R)); rewrite -!sgrEz. case hr: roots => [|c s] /=; apply: (@sgr_neighprN _ _ a b) => //; - rewrite /neighpr /next_root ?(negPf pq0) join_l // hr mid_in_itv //=. + rewrite /neighpr /next_root ?(negPf pq0) max_l // hr mid_in_itv //=. by move/eqP: hr; rewrite roots_cons => /and5P [_ /itvP ->]. rewrite -cats1 pairmap_cat /= cats1 map_rcons last_rcons. apply: (@sgr_neighplN _ _ a b) => //. - rewrite /neighpl /prev_root (negPf pq0) meet_l //. + rewrite /neighpl /prev_root (negPf pq0) min_l //. by rewrite mid_in_itv //= last_roots_le. elim: roots {-2 6}a (erefl (roots (p * q) a b)) {hpqa hpqb} hab hlab => {a} [|c s IHs] a Hs hab hlab /=.