From 9ac7ae1cb26335a1db29f7ec8a1697f3075abf46 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 26 Mar 2024 10:10:35 +0100 Subject: [PATCH] mathcomp 2.1.0 and 2.2.0 renamings and Coq compat --- theories/cauchyreals.v | 360 +++++++++++++++++++-------------------- theories/complex.v | 66 ++++--- theories/ordered_qelim.v | 30 ++-- theories/polyrcf.v | 108 ++++++------ theories/qe_rcf.v | 22 +-- theories/qe_rcf_th.v | 2 +- theories/realalg.v | 223 ++++++++++-------------- 7 files changed, 383 insertions(+), 428 deletions(-) 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/ordered_qelim.v b/theories/ordered_qelim.v index a2c776f..69502a6 100644 --- a/theories/ordered_qelim.v +++ b/theories/ordered_qelim.v @@ -82,21 +82,21 @@ Declare Scope oterm_scope. Bind Scope oterm_scope with term. Bind Scope oterm_scope with formula. Delimit Scope oterm_scope with oT. -Arguments Add _ _%oT _%oT. -Arguments Opp _ _%oT. -Arguments NatMul _ _%oT _%N. -Arguments Mul _ _%oT _%oT. -Arguments Mul _ _%oT _%oT. -Arguments Inv _ _%oT. -Arguments Exp _ _%oT _%N. -Arguments Equal _ _%oT _%oT. -Arguments Unit _ _%oT. -Arguments And _ _%oT _%oT. -Arguments Or _ _%oT _%oT. -Arguments Implies _ _%oT _%oT. -Arguments Not _ _%oT. -Arguments Exists _ _%N _%oT. -Arguments Forall _ _%N _%oT. +Arguments Add _ _%_oT _%_oT. +Arguments Opp _ _%_oT. +Arguments NatMul _ _%_oT _%_N. +Arguments Mul _ _%_oT _%_oT. +Arguments Mul _ _%_oT _%_oT. +Arguments Inv _ _%_oT. +Arguments Exp _ _%_oT _%_N. +Arguments Equal _ _%_oT _%_oT. +Arguments Unit _ _%_oT. +Arguments And _ _%_oT _%_oT. +Arguments Or _ _%_oT _%_oT. +Arguments Implies _ _%_oT _%_oT. +Arguments Not _ _%_oT. +Arguments Exists _ _%_N _%_oT. +Arguments Forall _ _%_N _%_oT. Arguments Bool [T]. Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not. 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.v b/theories/qe_rcf.v index 4d9201f..0c54c55 100644 --- a/theories/qe_rcf.v +++ b/theories/qe_rcf.v @@ -104,17 +104,17 @@ Declare Scope qf_scope. Bind Scope qf_scope with term. Bind Scope qf_scope with formula. Delimit Scope qf_scope with qfT. -Arguments Add _ _%qfT _%qfT. -Arguments Opp _ _%qfT. -Arguments NatMul _ _%qfT _%N. -Arguments Mul _ _%qfT _%qfT. -Arguments Mul _ _%qfT _%qfT. -Arguments Exp _ _%qfT _%N. -Arguments Equal _ _%qfT _%qfT. -Arguments And _ _%qfT _%qfT. -Arguments Or _ _%qfT _%qfT. -Arguments Implies _ _%qfT _%qfT. -Arguments Not _ _%qfT. +Arguments Add _ _%_qfT _%_qfT. +Arguments Opp _ _%_qfT. +Arguments NatMul _ _%_qfT _%_N. +Arguments Mul _ _%_qfT _%_qfT. +Arguments Mul _ _%_qfT _%_qfT. +Arguments Exp _ _%_qfT _%_N. +Arguments Equal _ _%_qfT _%_qfT. +Arguments And _ _%_qfT _%_qfT. +Arguments Or _ _%_qfT _%_qfT. +Arguments Implies _ _%_qfT _%_qfT. +Arguments Not _ _%_qfT. Arguments Bool [R]. Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not Lt. 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]. *)