diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algC.v | 64 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 141 | ||||
| -rw-r--r-- | mathcomp/field/algnum.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/finfield.v | 12 |
4 files changed, 114 insertions, 106 deletions
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index e1fd4d1..8c1fd96 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -1,9 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice. -From mathcomp Require Import div fintype path bigop finset prime ssralg poly. -From mathcomp Require Import polydiv mxpoly generic_quotient countalg ssrnum. -From mathcomp Require Import closed_field ssrint rat intdiv. +From mathcomp Require Import div fintype path bigop finset prime order ssralg. +From mathcomp Require Import poly polydiv mxpoly generic_quotient countalg. +From mathcomp Require Import ssrnum closed_field ssrint rat intdiv. From mathcomp Require Import algebraics_fundamentals. (******************************************************************************) @@ -53,14 +53,14 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GRing.Theory Num.Theory. +Import Order.Theory GRing.Theory Num.Theory. Local Open Scope ring_scope. (* The Num mixin for an algebraically closed field with an automorphism of *) (* order 2, making it into a field of complex numbers. *) Lemma ComplexNumMixin (L : closedFieldType) (conj : {rmorphism L -> L}) : involutive conj -> ~ conj =1 id -> - {numL | forall x : NumDomainType L numL, `|x| ^+ 2 = x * conj x}. + {numL : numMixin L | forall x : NumDomainType L numL, `|x| ^+ 2 = x * conj x}. Proof. move=> conjK conj_nt. have nz2: 2%:R != 0 :> L. @@ -184,7 +184,7 @@ have normD x y : le (norm (x + y)) (norm x + norm y). apply/posP; exists (i * (x * conj y - y * conj x)); congr (_ * _). rewrite !(rmorphM, rmorphB) iJ !conjK mulNr -mulrN opprB. by rewrite (mulrC x) (mulrC y). -by exists (Num.Mixin normD sposD norm_eq0 pos_linear normM (rrefl _) (rrefl _)). +by exists (NumMixin normD sposD norm_eq0 pos_linear normM (rrefl _) (rrefl _)). Qed. Module Algebraics. @@ -229,8 +229,10 @@ Canonical decFieldType := DecFieldType type decFieldMixin. Axiom closedFieldAxiom : GRing.ClosedField.axiom ringType. Canonical closedFieldType := ClosedFieldType type closedFieldAxiom. -Parameter numMixin : Num.mixin_of ringType. +Parameter numMixin : numMixin idomainType. +Canonical porderType := POrderType ring_display type numMixin. Canonical numDomainType := NumDomainType type numMixin. +Canonical normedDomainType := NormedDomainType type type numMixin. Canonical numFieldType := [numFieldType of type]. Parameter conjMixin : Num.ClosedField.imaginary_mixin_of numDomainType. @@ -422,13 +424,15 @@ have [i i2]: exists i : type, i ^+ 2 = -1. have [i] := @solve_monicpoly _ 2 (nth 0 [:: -1 : type]) isT. by rewrite !big_ord_recl big_ord0 /= mul0r mulr1 !addr0; exists i. move/(_ i)/(congr1 CtoL); rewrite LtoC_K => iL_J. -have/ltr_geF/idP[] := @ltr01 Lnum; rewrite -oppr_ge0 -(rmorphN1 CtoL_rmorphism). -rewrite -i2 rmorphX /= expr2 -{2}iL_J -(svalP LnumMixin). -by rewrite exprn_ge0 ?normr_ge0. +have/lt_geF/idP[] := @ltr01 Lnum; rewrite -oppr_ge0 -(rmorphN1 CtoL_rmorphism). +by rewrite -i2 rmorphX /= expr2 -{2}iL_J -(svalP LnumMixin) exprn_ge0. Qed. -Definition numMixin := sval (ComplexNumMixin conjK conj_nt). +Definition numMixin : numMixin closedFieldType := + sval (ComplexNumMixin conjK conj_nt). +Canonical porderType := POrderType ring_display type numMixin. Canonical numDomainType := NumDomainType type numMixin. +Canonical normedDomainType := NormedDomainType type type numMixin. Canonical numFieldType := [numFieldType of type]. Lemma normK u : `|u| ^+ 2 = u * conj u. @@ -480,18 +484,18 @@ Fact floorC_subproof x : {m | x \is Creal -> ZtoC m <= x < ZtoC (m + 1)}. Proof. have [Rx | _] := boolP (x \is Creal); last by exists 0. without loss x_ge0: x Rx / x >= 0. - have [x_ge0 | /ltrW x_le0] := real_ger0P Rx; first exact. + have [x_ge0 | /ltW x_le0] := real_ge0P Rx; first exact. case/(_ (- x)) => [||m /(_ isT)]; rewrite ?rpredN ?oppr_ge0 //. - rewrite ler_oppr ltr_oppl -!rmorphN opprD /= ltr_neqAle ler_eqVlt. + rewrite ler_oppr ltr_oppl -!rmorphN opprD /= lt_neqAle le_eqVlt. case: eqP => [-> _ | _ /and3P[lt_x_m _ le_m_x]]. - by exists (- m) => _; rewrite lerr rmorphD ltr_addl ltr01. + by exists (- m) => _; rewrite lexx rmorphD ltr_addl ltr01. by exists (- m - 1); rewrite le_m_x subrK. have /ex_minnP[n lt_x_n1 min_n]: exists n, x < n.+1%:R. have [n le_x_n] := rat_algebraic_archimedean algebraic x. - by exists n; rewrite -(ger0_norm x_ge0) (ltr_trans le_x_n) ?ltr_nat. + by exists n; rewrite -(ger0_norm x_ge0) (lt_trans le_x_n) ?ltr_nat. exists n%:Z => _; rewrite addrC -intS lt_x_n1 andbT. case Dn: n => // [n1]; rewrite -Dn. -have [||//|] := @real_lerP _ n%:R x; rewrite ?rpred_nat //. +have [||//|] := @real_leP _ n%:R x; rewrite ?rpred_nat //. by rewrite Dn => /min_n; rewrite Dn ltnn. Qed. @@ -535,7 +539,9 @@ Canonical unitRingType. Canonical comRingType. Canonical comUnitRingType. Canonical idomainType. +Canonical porderType. Canonical numDomainType. +Canonical normedDomainType. Canonical fieldType. Canonical numFieldType. Canonical decFieldType. @@ -663,15 +669,15 @@ Proof. by rewrite /floorC => Rx; case: (floorC_subproof x) => //= m; apply. Qed. Lemma floorC_def x m : m%:~R <= x < (m + 1)%:~R -> floorC x = m. Proof. -case/andP=> lemx ltxm1; apply/eqP; rewrite eqr_le -!ltz_addr1. +case/andP=> lemx ltxm1; apply/eqP; rewrite eq_le -!ltz_addr1. have /floorC_itv/andP[lefx ltxf1]: x \is Creal. by rewrite -[x](subrK m%:~R) rpredD ?realz ?ler_sub_real. -by rewrite -!(ltr_int [numFieldType of algC]) 2?(@ler_lt_trans _ x). +by rewrite -!(ltr_int [numFieldType of algC]) 2?(@le_lt_trans _ _ x). Qed. Lemma intCK : cancel intr floorC. Proof. -by move=> m; apply: floorC_def; rewrite ler_int ltr_int ltz_addr1 lerr. +by move=> m; apply: floorC_def; rewrite ler_int ltr_int ltz_addr1 lexx. Qed. Lemma floorCK : {in Cint, cancel floorC intr}. Proof. by move=> z /eqP. Qed. @@ -757,17 +763,17 @@ Lemma truncC_itv x : 0 <= x -> (truncC x)%:R <= x < (truncC x).+1%:R. Proof. move=> x_ge0; have /andP[lemx ltxm1] := floorC_itv (ger0_real x_ge0). rewrite /truncC x_ge0 -addn1 !pmulrn PoszD gez0_abs ?lemx //. -by rewrite -ltz_addr1 -(ltr_int [numFieldType of algC]) (ler_lt_trans x_ge0). +by rewrite -ltz_addr1 -(ltr_int [numFieldType of algC]) (le_lt_trans x_ge0). Qed. Lemma truncC_def x n : n%:R <= x < n.+1%:R -> truncC x = n. Proof. move=> ivt_n_x; have /andP[lenx _] := ivt_n_x. -by rewrite /truncC (ler_trans (ler0n _ n)) // (@floorC_def _ n) // addrC -intS. +by rewrite /truncC (le_trans (ler0n _ n)) // (@floorC_def _ n) // addrC -intS. Qed. Lemma natCK n : truncC n%:R = n. -Proof. by apply: truncC_def; rewrite lerr ltr_nat /=. Qed. +Proof. by apply: truncC_def; rewrite lexx ltr_nat /=. Qed. Lemma CnatP x : reflect (exists n, x = n%:R) (x \in Cnat). Proof. @@ -782,9 +788,9 @@ Proof. apply/idP/idP=> [m_gt0 | x_ge1]. have /truncC_itv/andP[lemx _]: 0 <= x. by move: m_gt0; rewrite /truncC; case: ifP. - by apply: ler_trans lemx; rewrite ler1n. -have /truncC_itv/andP[_ ltxm1]:= ler_trans ler01 x_ge1. -by rewrite -ltnS -ltC_nat (ler_lt_trans x_ge1). + by apply: le_trans lemx; rewrite ler1n. +have /truncC_itv/andP[_ ltxm1]:= le_trans ler01 x_ge1. +by rewrite -ltnS -ltC_nat (le_lt_trans x_ge1). Qed. Lemma truncC0Pn x : reflect (truncC x = 0%N) (~~ (1 <= x)). @@ -912,14 +918,12 @@ by rewrite pnatr_eq0 ler1n lt0n. Qed. Lemma sqr_Cint_ge1 x : x \in Cint -> x != 0 -> 1 <= x ^+ 2. -Proof. -by move=> Zx nz_x; rewrite -Cint_normK // expr_ge1 ?normr_ge0 ?norm_Cint_ge1. -Qed. +Proof. by move=> Zx nz_x; rewrite -Cint_normK // expr_ge1 ?norm_Cint_ge1. Qed. Lemma Cint_ler_sqr x : x \in Cint -> x <= x ^+ 2. Proof. move=> Zx; have [-> | nz_x] := eqVneq x 0; first by rewrite expr0n. -apply: ler_trans (_ : `|x| <= _); first by rewrite real_ler_norm ?Creal_Cint. +apply: le_trans (_ : `|x| <= _); first by rewrite real_ler_norm ?Creal_Cint. by rewrite -Cint_normK // ler_eexpr // norm_Cint_ge1. Qed. @@ -937,7 +941,7 @@ Lemma dvdCP_nat x y : 0 <= x -> 0 <= y -> (x %| y)%C -> {n | y = n%:R * x}. Proof. move=> x_ge0 y_ge0 x_dv_y; apply: sig_eqW. case/dvdCP: x_dv_y => z Zz -> in y_ge0 *; move: x_ge0 y_ge0 Zz. -rewrite ler_eqVlt => /predU1P[<- | ]; first by exists 22; rewrite !mulr0. +rewrite le_eqVlt => /predU1P[<- | ]; first by exists 22; rewrite !mulr0. by move=> /pmulr_lge0-> /CintEge0-> /CnatP[n ->]; exists n. Qed. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index acafd8f..e8521ec 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -1,11 +1,11 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice. -From mathcomp Require Import div fintype path tuple bigop finset prime ssralg. -From mathcomp Require Import poly polydiv mxpoly countalg closed_field ssrnum. -From mathcomp Require Import ssrint rat intdiv fingroup finalg zmodp cyclic. -From mathcomp Require Import pgroup sylow vector falgebra fieldext separable. -From mathcomp Require Import galois. +From mathcomp Require Import div fintype path tuple bigop finset prime order. +From mathcomp Require Import ssralg poly polydiv mxpoly countalg closed_field. +From mathcomp Require Import ssrnum ssrint rat intdiv fingroup finalg zmodp. +From mathcomp Require Import cyclic pgroup sylow vector falgebra fieldext. +From mathcomp Require Import separable galois. (******************************************************************************) (* The main result in this file is the existence theorem that underpins the *) @@ -112,7 +112,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GroupScope GRing.Theory Num.Theory. +Import Order.Theory Order.Syntax GroupScope GRing.Theory Num.Theory. Local Open Scope ring_scope. Local Notation "p ^ f" := (map_poly f p) : ring_scope. @@ -124,25 +124,25 @@ Lemma rat_algebraic_archimedean (C : numFieldType) (QtoC : Qmorphism C) : integralRange QtoC -> Num.archimedean_axiom C. Proof. move=> algC x. -without loss x_ge0: x / 0 <= x by rewrite -normr_id; apply; apply: normr_ge0. +without loss x_ge0: x / 0 <= x by rewrite -normr_id; apply. have [-> | nz_x] := eqVneq x 0; first by exists 1%N; rewrite normr0. have [p mon_p px0] := algC x; exists (\sum_(j < size p) `|numq p`_j|)%N. -rewrite ger0_norm // real_ltrNge ?rpred_nat ?ger0_real //. -apply: contraL px0 => lb_x; rewrite rootE gtr_eqF // horner_coef size_map_poly. -have x_gt0 k: 0 < x ^+ k by rewrite exprn_gt0 // ltr_def nz_x. +rewrite ger0_norm // real_ltNge ?rpred_nat ?ger0_real //. +apply: contraL px0 => lb_x; rewrite rootE gt_eqF // horner_coef size_map_poly. +have x_gt0 k: 0 < x ^+ k by rewrite exprn_gt0 // lt_def nz_x. move: lb_x; rewrite polySpred ?monic_neq0 // !big_ord_recr coef_map /=. rewrite -lead_coefE (monicP mon_p) natrD rmorph1 mul1r => lb_x. case: _.-1 (lb_x) => [|n]; first by rewrite !big_ord0 !add0r ltr01. rewrite -ltr_subl_addl add0r -(ler_pmul2r (x_gt0 n)) -exprS. -apply: ltr_le_trans; rewrite mulrDl mul1r ltr_spaddr // -sumrN. +apply: lt_le_trans; rewrite mulrDl mul1r ltr_spaddr // -sumrN. rewrite natr_sum mulr_suml ler_sum // => j _. -rewrite coef_map /= fmorph_eq_rat (ler_trans (real_ler_norm _)) //. +rewrite coef_map /= fmorph_eq_rat (le_trans (real_ler_norm _)) //. by rewrite rpredN rpredM ?rpred_rat ?rpredX // ger0_real. -rewrite normrN normrM ler_pmul //=. +rewrite normrN normrM ler_pmul //. rewrite normf_div -!intr_norm -!abszE ler_pimulr ?ler0n //. by rewrite invf_le1 ?ler1n ?ltr0n ?absz_gt0 ?denq_eq0. rewrite normrX ger0_norm ?(ltrW x_gt0) // ler_weexpn2l ?leq_ord //. -by rewrite (ler_trans _ lb_x) // -natrD addn1 ler1n. +by rewrite (le_trans _ lb_x) // -natrD addn1 ler1n. Qed. Definition decidable_embedding sT T (f : sT -> T) := @@ -161,8 +161,8 @@ have [n ub_n]: {n | forall y, root q y -> `|y| < n}. have /monic_Cauchy_bound[n2 ub_n2]: (-1) ^+ d *: (q \Po - 'X) \is monic. rewrite monicE lead_coefZ lead_coef_comp ?size_opp ?size_polyX // -/d. by rewrite lead_coef_opp lead_coefX (monicP mon_q) (mulrC 1) signrMK. - exists (Num.max n1 n2) => y; rewrite ltrNge ler_normr !ler_maxl rootE. - apply: contraL => /orP[]/andP[] => [/ub_n1/gtr_eqF->// | _ /ub_n2/gtr_eqF]. + exists (n1 `|` n2) => y; rewrite ltNge ler_normr !leUx rootE. + apply: contraL => /orP[]/andP[] => [/ub_n1/gt_eqF->// | _ /ub_n2/gt_eqF]. by rewrite hornerZ horner_comp !hornerE opprK mulf_eq0 signr_eq0 => /= ->. have [p [a nz_a Dq]] := rat_poly_scale q; pose N := Num.bound `|n * a%:~R|. pose xa : seq rat := [seq (m%:R - N%:R) / a%:~R | m <- iota 0 N.*2]. @@ -193,13 +193,13 @@ have Dm: m%:R = `|y * a%:~R + N%:R|. by rewrite pmulrn abszE intr_norm Da rmorphD !rmorphM /= numqE mulrAC mulrA. have ltr_Qnat n1 n2 : (n1%:R < n2%:R :> rat = _) := ltr_nat _ n1 n2. have ub_y: `|y * a%:~R| < N%:R. - apply: ler_lt_trans (archi_boundP (normr_ge0 _)); rewrite !normrM. - by rewrite ler_pmul ?normr_ge0 // (ler_trans _ (ler_norm n)) ?ltrW ?ub_n. + apply: le_lt_trans (archi_boundP (normr_ge0 _)); rewrite !normrM. + by rewrite ler_pmul // (le_trans _ (ler_norm n)) ?ltW ?ub_n. apply/mapP; exists m. rewrite mem_iota /= add0n -addnn -ltr_Qnat Dm natrD. - by rewrite (ler_lt_trans (ler_norm_add _ _)) // normr_nat ltr_add2r. + by rewrite (le_lt_trans (ler_norm_add _ _)) // normr_nat ltr_add2r. rewrite Dm ger0_norm ?addrK ?mulfK ?intr_eq0 // -ler_subl_addl sub0r. -by rewrite (ler_trans (ler_norm _)) ?normrN ?ltrW. +by rewrite (le_trans (ler_norm _)) ?normrN ?ltW. Qed. Lemma minPoly_decidable_closure @@ -397,7 +397,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. elim: d => // d IHd in p mon_p s_p p0_le0 *; rewrite ltnS => le_p_d. have /closed_rootP/sig_eqW[y py0]: size (p ^ ofQ x) != 1%N. rewrite size_map_poly size_poly_eq1 eqp_monic ?rpred1 //. - by apply: contraTneq p0_le0 => ->; rewrite rmorph1 hornerC ltr_geF ?ltr01. + by apply: contraTneq p0_le0 => ->; rewrite rmorph1 hornerC lt_geF ?ltr01. have /s_p s_y := py0; have /z_s/sQ_inQ[u Dy] := s_y. have /pQwx[q Dq] := minPolyOver Qx u. have mon_q: q \is monic by have:= monic_minPoly Qx u; rewrite Dq map_monic. @@ -441,10 +441,10 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. case: (find k q _) => c d [[/= qc_le0 qd_ge0 le_cd] [/= le_ac le_db] Dcd]. have [/= le_ce le_ed] := midf_le le_cd; set e := _ / _ in le_ce le_ed. rewrite expnSr natrM invfM mulrA -{}Dcd /narrow /= -[mid _]/e. - have [qe_ge0 // | /ltrW qe_le0] := lerP 0 q.[e]. - do ?split=> //=; [exact: (ler_trans le_ed) | apply: canRL (mulfK nz2) _]. + have [qe_ge0 // | /ltW qe_le0] := lerP 0 q.[e]. + do ?split=> //=; [exact: (le_trans le_ed) | apply: canRL (mulfK nz2) _]. by rewrite mulrBl divfK // mulr_natr opprD addrACA subrr add0r. - do ?split=> //=; [exact: (ler_trans le_ac) | apply: canRL (mulfK nz2) _]. + do ?split=> //=; [exact: (le_trans le_ac) | apply: canRL (mulfK nz2) _]. by rewrite mulrBl divfK // mulr_natr opprD addrACA subrr addr0. have find_root r q ab: xup q ab -> {n | forall x, x \in itv (find n q ab) ->`|(r * q).[x]| < h2}. @@ -457,39 +457,39 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. have{xab} [[]] := findP n _ _ xab; case: (find n q ab) => a1 b1 /=. rewrite -/d => qa1_le0 qb1_ge0 le_ab1 [/= le_aa1 le_b1b] Dab1 le_a1c le_cb1. have /MuP lbMu: c \in itv ab. - by rewrite !inE (ler_trans le_aa1) ?(ler_trans le_cb1). - have Mu_ge0: 0 <= Mu by rewrite (ler_trans _ lbMu) ?normr_ge0. + by rewrite !inE (le_trans le_aa1) ?(le_trans le_cb1). + have Mu_ge0: 0 <= Mu by rewrite (le_trans _ lbMu). have Mdq_ge0: 0 <= Mdq. - by rewrite (ler_trans _ (MdqP 0 _)) ?normr_ge0 ?normr0. + by rewrite (le_trans _ (MdqP 0 _)) ?normr0. suffices lb1 a2 b2 (ab1 := (a1, b1)) (ab2 := (a2, b2)) : xup q ab2 /\ sub_itv ab2 ab1 -> q.[b2] - q.[a2] <= Mdq * wid ab1. - + apply: ler_lt_trans (_ : Mu * Mdq * wid (a1, b1) < h2); last first. + + apply: le_lt_trans (_ : Mu * Mdq * wid (a1, b1) < h2); last first. rewrite {}Dab1 mulrA ltr_pdivr_mulr ?ltr0n ?expn_gt0 //. - rewrite (ltr_le_trans (archi_boundP _)) ?mulr_ge0 ?ltr_nat // -/n. + rewrite (lt_le_trans (archi_boundP _)) ?mulr_ge0 ?ltr_nat // -/n. rewrite ler_pdivl_mull ?ltr0n // -natrM ler_nat. by case: n => // n; rewrite expnS leq_pmul2l // ltn_expl. - rewrite -mulrA hornerM normrM ler_pmul ?normr_ge0 //. - have [/ltrW qc_le0 | qc_ge0] := ltrP q.[c] 0. - by apply: ler_trans (lb1 c b1 _); rewrite ?ler0_norm ?ler_paddl. - by apply: ler_trans (lb1 a1 c _); rewrite ?ger0_norm ?ler_paddr ?oppr_ge0. + rewrite -mulrA hornerM normrM ler_pmul //. + have [/ltW qc_le0 | qc_ge0] := ltrP q.[c] 0. + by apply: le_trans (lb1 c b1 _); rewrite ?ler0_norm ?ler_paddl. + by apply: le_trans (lb1 a1 c _); rewrite ?ger0_norm ?ler_paddr ?oppr_ge0. case{c le_a1c le_cb1 lbMu}=> [[/=qa2_le0 qb2_ge0 le_ab2] [/=le_a12 le_b21]]. pose h := b2 - a2; have h_ge0: 0 <= h by rewrite subr_ge0. have [-> | nz_q] := eqVneq q 0. by rewrite !horner0 subrr mulr_ge0 ?subr_ge0. rewrite -(subrK a2 b2) (addrC h) (nderiv_taylor q (mulrC a2 h)). rewrite (polySpred nz_q) big_ord_recl /= mulr1 nderivn0 addrC addKr. - have [le_aa2 le_b2b] := (ler_trans le_aa1 le_a12, ler_trans le_b21 le_b1b). - have /MqP MqPx1: a2 \in itv ab by rewrite inE le_aa2 (ler_trans le_ab2). - apply: ler_trans (ler_trans (ler_norm _) (ler_norm_sum _ _ _)) _. - apply: ler_trans (_ : `|dq.[h] * h| <= _); last first. + have [le_aa2 le_b2b] := (le_trans le_aa1 le_a12, le_trans le_b21 le_b1b). + have /MqP MqPx1: a2 \in itv ab by rewrite inE le_aa2 (le_trans le_ab2). + apply: le_trans (le_trans (ler_norm _) (ler_norm_sum _ _ _)) _. + apply: le_trans (_ : `|dq.[h] * h| <= _); last first. by rewrite normrM ler_pmul ?normr_ge0 ?MdqP // ?ger0_norm ?ler_sub ?h_ge0. rewrite horner_poly ger0_norm ?mulr_ge0 ?sumr_ge0 // => [|j _]; last first. - by rewrite mulr_ge0 ?exprn_ge0 // (ler_trans _ (MqPx1 _)) ?normr_ge0. + by rewrite mulr_ge0 ?exprn_ge0 // (le_trans _ (MqPx1 _)). rewrite mulr_suml ler_sum // => j _; rewrite normrM -mulrA -exprSr. - by rewrite ler_pmul ?normr_ge0 // normrX ger0_norm. + by rewrite ler_pmul // normrX ger0_norm. have [ab0 xab0]: {ab | xup (p ^ QxR) ab}. have /monic_Cauchy_bound[b pb_gt0]: p ^ QxR \is monic by apply: monic_map. - by exists (0, `|b|); rewrite /xup normr_ge0 p0_le0 ltrW ?pb_gt0 ?ler_norm. + by exists (0, `|b|); rewrite /xup normr_ge0 p0_le0 ltW ?pb_gt0 ?ler_norm. pose ab_ n := find n (p ^ QxR) ab0; pose Iab_ n := itv (ab_ n). pose lim v a := (q_ v ^ QxR).[a]; pose nlim v n := lim v (ab_ n).2. have lim0 a: lim 0 a = 0. @@ -505,57 +505,57 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. have /(find_root r.1)[n ub_rp] := xab0; exists n. have [M Mgt0 ubM]: {M | 0 < M & {in Iab_ n, forall a, `|r.2.[a]| <= M}}. have [M ubM] := poly_itv_bound r.2 (ab_ n).1 (ab_ n).2. - exists (Num.max 1 M) => [|s /ubM vM]; first by rewrite ltr_maxr ltr01. - by rewrite ler_maxr orbC vM. + exists (1 `|` M) => [|s /ubM vM]; first by rewrite ltxU ltr01. + by rewrite lexU orbC vM. exists (h2 / M) => [|a xn_a]; first by rewrite divr_gt0 ?invr_gt0 ?ltr0n. rewrite ltr_pdivr_mulr // -(ltr_add2l h2) -mulr2n -mulr_natl divff //. rewrite -normr1 -(hornerC 1 a) -[1%:P]r_pq_1 hornerD. - rewrite ?(ler_lt_trans (ler_norm_add _ _)) ?ltr_le_add ?ub_rp //. + rewrite ?(le_lt_trans (ler_norm_add _ _)) ?ltr_le_add ?ub_rp //. by rewrite mulrC hornerM normrM ler_wpmul2l ?ubM. have ab_le m n: (m <= n)%N -> (ab_ n).2 \in Iab_ m. move/subnKC=> <-; move: {n}(n - m)%N => n; rewrite /ab_. have /(findP m)[/(findP n)[[_ _]]] := xab0. rewrite /find -iter_add -!/(find _ _) -!/(ab_ _) addnC !inE. - by move: (ab_ _) => /= ab_mn le_ab_mn [/ler_trans->]. + by move: (ab_ _) => /= ab_mn le_ab_mn [/le_trans->]. pose lt v w := 0 < nlim (w - v) (n_ (w - v)). have posN v: lt 0 (- v) = lt v 0 by rewrite /lt subr0 add0r. have posB v w: lt 0 (w - v) = lt v w by rewrite /lt subr0. have posE n v: (n_ v <= n)%N -> lt 0 v = (0 < nlim v n). rewrite /lt subr0 /nlim => /ab_le; set a := _.2; set b := _.2 => Iv_a. - have [-> | /nzP[e e_gt0]] := eqVneq v 0; first by rewrite !lim0 ltrr. + have [-> | /nzP[e e_gt0]] := eqVneq v 0; first by rewrite !lim0 ltxx. move: (n_ v) => m in Iv_a b * => v_gte. without loss lt0v: v v_gte / 0 < lim v b. - move=> IHv; apply/idP/idP => [v_gt0 | /ltrW]; first by rewrite -IHv. - rewrite ltr_def -normr_gt0 ?(ltr_trans _ (v_gte _ _)) ?ab_le //=. - rewrite !lerNgt -!oppr_gt0 -!limN; apply: contra => v_lt0. + move=> IHv; apply/idP/idP => [v_gt0 | /ltW]; first by rewrite -IHv. + rewrite lt_def -normr_gt0 ?(lt_trans _ (v_gte _ _)) ?ab_le //=. + rewrite !leNgt -!oppr_gt0 -!limN; apply: contra => v_lt0. by rewrite -IHv // => c /v_gte; rewrite limN normrN. - rewrite lt0v (ltr_trans e_gt0) ?(ltr_le_trans (v_gte a Iv_a)) //. - rewrite ger0_norm // lerNgt; apply/negP=> /ltrW lev0. + rewrite lt0v (lt_trans e_gt0) ?(lt_le_trans (v_gte a Iv_a)) //. + rewrite ger0_norm // leNgt; apply/negP=> /ltW lev0. have [le_a le_ab] : _ /\ a <= b := andP Iv_a. - have xab: xup (q_ v ^ QxR) (a, b) by move/ltrW in lt0v. + have xab: xup (q_ v ^ QxR) (a, b) by move/ltW in lt0v. have /(find_root (h2 / e)%:P)[n1] := xab; have /(findP n1)[[_ _]] := xab. case: (find _ _ _) => c d /= le_cd [/= le_ac le_db] _ /(_ c)/implyP. - rewrite inE lerr le_cd hornerM hornerC normrM ler_gtF //. - rewrite ger0_norm ?divr_ge0 ?invr_ge0 ?ler0n ?(ltrW e_gt0) // mulrAC. - rewrite ler_pdivl_mulr // ler_wpmul2l ?invr_ge0 ?ler0n // ltrW // v_gte //=. - by rewrite inE -/b (ler_trans le_a) //= (ler_trans le_cd). + rewrite inE lexx le_cd hornerM hornerC normrM le_gtF //. + rewrite ger0_norm ?divr_ge0 ?invr_ge0 ?ler0n ?(ltW e_gt0) // mulrAC. + rewrite ler_pdivl_mulr // ler_wpmul2l ?invr_ge0 ?ler0n // ltW // v_gte //=. + by rewrite inE -/b (le_trans le_a) //= (le_trans le_cd). pose lim_pos m v := exists2 e, e > 0 & forall n, (m <= n)%N -> e < nlim v n. have posP v: reflect (exists m, lim_pos m v) (lt 0 v). apply: (iffP idP) => [v_gt0|[m [e e_gt0 v_gte]]]; last first. - by rewrite (posE _ _ (leq_maxl _ m)) (ltr_trans e_gt0) ?v_gte ?leq_maxr. + by rewrite (posE _ _ (leq_maxl _ m)) (lt_trans e_gt0) ?v_gte ?leq_maxr. have [|e e_gt0 v_gte] := nzP v. - by apply: contraTneq v_gt0 => ->; rewrite /lt subr0 /nlim lim0 ltrr. + by apply: contraTneq v_gt0 => ->; rewrite /lt subr0 /nlim lim0 ltxx. exists (n_ v), e => // n le_vn; rewrite (posE n) // in v_gt0. - by rewrite -(ger0_norm (ltrW v_gt0)) v_gte ?ab_le. + by rewrite -(ger0_norm (ltW v_gt0)) v_gte ?ab_le. have posNneg v: lt 0 v -> ~~ lt v 0. case/posP=> m [d d_gt0 v_gtd]; rewrite -posN. apply: contraL d_gt0 => /posP[n [e e_gt0 nv_gte]]. - rewrite ltr_gtF // (ltr_trans (v_gtd _ (leq_maxl m n))) // -oppr_gt0. - by rewrite /nlim -limN (ltr_trans e_gt0) ?nv_gte ?leq_maxr. + rewrite lt_gtF // (lt_trans (v_gtd _ (leq_maxl m n))) // -oppr_gt0. + by rewrite /nlim -limN (lt_trans e_gt0) ?nv_gte ?leq_maxr. have posVneg v: v != 0 -> lt 0 v || lt v 0. case/nzP=> e e_gt0 v_gte; rewrite -posN; set w := - v. have [m [le_vm le_wm _]] := maxn3 (n_ v) (n_ w) 0%N; rewrite !(posE m) //. - by rewrite /nlim limN -ltr_normr (ltr_trans e_gt0) ?v_gte ?ab_le. + by rewrite /nlim limN -ltr_normr (lt_trans e_gt0) ?v_gte ?ab_le. have posD v w: lt 0 v -> lt 0 w -> lt 0 (v + w). move=> /posP[m [d d_gt0 v_gtd]] /posP[n [e e_gt0 w_gte]]. apply/posP; exists (maxn m n), (d + e) => [|k]; first exact: addr_gt0. @@ -575,20 +575,23 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. rewrite !geq_max => /and3P[/ab_le/ub_rp{ub_rp}ub_rp le_mk le_nk]. rewrite -(ltr_add2r f) -mulr2n -mulr_natr divfK // /nlim /lim Dqvw. rewrite rmorphD hornerD /= -addrA -ltr_subl_addl ler_lt_add //. - by rewrite rmorphM hornerM ler_pmul ?ltrW ?v_gtd ?w_gte. - rewrite -ltr_pdivr_mull ?mulr_gt0 // (ler_lt_trans _ ub_rp) //. + by rewrite rmorphM hornerM ler_pmul ?ltW ?v_gtd ?w_gte. + rewrite -ltr_pdivr_mull ?mulr_gt0 // (le_lt_trans _ ub_rp) //. by rewrite -scalerAl hornerZ -rmorphM mulrN -normrN ler_norm. - pose le v w := (w == v) || lt v w. + pose le v w := (v == w) || lt v w. pose abs v := if le 0 v then v else - v. have absN v: abs (- v) = abs v. - rewrite /abs /le oppr_eq0 opprK posN. + rewrite /abs /le !(eq_sym 0) oppr_eq0 opprK posN. have [-> | /posVneg/orP[v_gt0 | v_lt0]] := altP eqP; first by rewrite oppr0. by rewrite v_gt0 /= -if_neg posNneg. by rewrite v_lt0 /= -if_neg -(opprK v) posN posNneg ?posN. have absE v: le 0 v -> abs v = v by rewrite /abs => ->. - pose QyNum := RealLtMixin posD posM posNneg posB posVneg absN absE (rrefl _). - pose QyNumField := [numFieldType of NumDomainType (Q y) QyNum]. - pose Ry := [realFieldType of RealDomainType _ (RealLeAxiom QyNumField)]. + pose QyNum : realLtMixin (Q y) := + RealLtMixin posD posM posNneg posB posVneg absN absE (rrefl _). + pose QyOrder := + OrderType (LatticeType (POrderType ring_display (Q y) QyNum) QyNum) QyNum. + pose QyNumField := [numFieldType of NumDomainType QyOrder QyNum]. + pose Ry := [realFieldType of [realDomainType of QyNumField]]. have archiRy := @rat_algebraic_archimedean Ry _ alg_integral. by exists (ArchiFieldType Ry archiRy); apply: [rmorphism of idfun]. have some_realC: realC. @@ -626,7 +629,7 @@ have sCle m n: (m <= n)%N -> {subset sQ (z_ m) <= sQ (z_ n)}. have R'i n: i \notin sQ (x_ n). rewrite /x_; case: (xR n) => x [Rn QxR] /=. apply: contraL (@ltr01 Rn) => /sQ_inQ[v Di]. - suffices /eqP <-: - QxR v ^+ 2 == 1 by rewrite oppr_gt0 -lerNgt sqr_ge0. + suffices /eqP <-: - QxR v ^+ 2 == 1 by rewrite oppr_gt0 -leNgt sqr_ge0. rewrite -rmorphX -rmorphN fmorph_eq1 -(fmorph_eq1 (ofQ x)) rmorphN eqr_oppLR. by rewrite rmorphX Di Di2. have szX2_1: size ('X^2 + 1) = 3. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index c191a0e..be7dd6c 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -358,7 +358,8 @@ pose Saut (mu : subAut) : {rmorphism Sdom mu -> Sdom mu} := (projT2 mu).2. have SinjZ Qr (QrC : numF_inj Qr) a x: QrC (a *: x) = QtoC a * QrC x. rewrite mulrAC; apply: canRL (mulfK _) _. by rewrite intr_eq0 denq_neq0. - by rewrite mulrzr mulrzl -!rmorphMz scalerMzl -scaler_int -mulrzr -numqE. + by rewrite mulrzr mulrzl -!rmorphMz scalerMzl -[x *~ _]scaler_int -mulrzr + -numqE. have Sinj_poly Qr (QrC : numF_inj Qr) p: map_poly QrC (map_poly (in_alg Qr) p) = pQtoC p. - rewrite -map_poly_comp; apply: eq_map_poly => a. diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index 19871cb..efe5cea 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -568,7 +568,7 @@ End FinFieldExists. Section FinDomain. -Import ssrnum ssrint algC cyclotomic Num.Theory. +Import order ssrnum ssrint algC cyclotomic Order.Theory Num.Theory. Local Infix "%|" := dvdn. (* Hide polynomial divisibility. *) Variable R : finUnitRingType. @@ -625,18 +625,18 @@ without loss n_gt1: / (1 < n)%N by rewrite ltnNge; apply: wlog_neg. have [q_gt0 n_gt0] := (ltnW q_gt1, ltnW n_gt1). have [z z_prim] := C_prim_root_exists n_gt0. have zn1: z ^+ n = 1 by apply: prim_expr_order. -have /eqP-n1z: `|z| == 1. - by rewrite -(pexpr_eq1 n_gt0) ?normr_ge0 // -normrX zn1 normr1. -suffices /eqP/normC_sub_eq[t n1t [Dq Dz]]: `|q%:R - z| == `|q%:R| - `|z|. +have /eqP-n1z: `|z| == 1 by rewrite -(pexpr_eq1 n_gt0) // -normrX zn1 normr1. +suffices /eqP/normC_sub_eq[t n1t [Dq Dz]]: + `|q%:R - z : algC| == `|q%:R : algC| - `|z|. suffices z1: z == 1 by rewrite leq_eqVlt -dvdn1 (prim_order_dvd z_prim) z1. by rewrite Dz n1z mul1r -(eqr_pmuln2r q_gt0) Dq normr_nat mulr_natl. pose aq d : algC := (cyclotomic (z ^+ (n %/ d)) d).[q%:R]. suffices: `|aq n| <= (q - 1)%:R. - rewrite eqr_le ler_sub_dist andbT n1z normr_nat natrB //; apply: ler_trans. + rewrite eq_le ler_sub_dist andbT n1z normr_nat natrB //; apply: le_trans. rewrite {}/aq horner_prod divnn n_gt0 expr1 normr_prod. rewrite (bigD1 (Ordinal n_gt1)) ?coprime1n //= !hornerE ler_pemulr //. elim/big_ind: _ => // [|d _]; first exact: mulr_ege1. - rewrite !hornerE; apply: ler_trans (ler_sub_dist _ _). + rewrite !hornerE; apply: le_trans (ler_sub_dist _ _). by rewrite normr_nat normrX n1z expr1n ler_subr_addl (leC_nat 2). have Zaq d: d %| n -> aq d \in Cint. move/(dvdn_prim_root z_prim)=> zd_prim. |