Skip to content

Commit

Permalink
Compat with new maximum in math-comp
Browse files Browse the repository at this point in the history
  • Loading branch information
@CohenCyril
CohenCyril committed Jun 10, 2020
1 parent 06eedf3 commit 3a16c95
Show file tree
Hide file tree
Showing 6 changed files with 56 additions and 56 deletions.
4 changes: 2 additions & 2 deletions .travis.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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'
2 changes: 1 addition & 1 deletion config.nix
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
{
coq = "8.10";
mathcomp = "1.11.0+beta1";
mathcomp = "mathcomp-1.11.0";
}
48 changes: 24 additions & 24 deletions theories/cauchyreals.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -439,17 +439,17 @@ 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[_].
by rewrite !(monoLR (addrK _) (ler_add2r _)) 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 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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -1372,15 +1372,15 @@ 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.
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 !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.
Expand All @@ -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' _].
Expand All @@ -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.

Expand Down Expand Up @@ -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 _)) //.
Expand Down
4 changes: 2 additions & 2 deletions theories/complex.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
46 changes: 23 additions & 23 deletions theories/polyrcf.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand All @@ -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).
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -1210,17 +1210,17 @@ 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.
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}.
Expand Down Expand Up @@ -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}.
Expand All @@ -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 :
Expand Down Expand Up @@ -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}) :
Expand All @@ -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}.
Expand Down Expand Up @@ -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}) :
Expand Down
8 changes: 4 additions & 4 deletions theories/qe_rcf_th.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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 /=.
Expand Down

0 comments on commit 3a16c95

Please sign in to comment.