From 317267c618ecff861ec6539a2d6063cef298d720 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Fri, 22 Nov 2019 10:02:04 +0100 Subject: New generalised induction idiom (#434) Replaced the legacy generalised induction idiom with a more robust one that does not rely on the `{-2}` numerical occurrence selector, using either new helper lemmas `ubnP` and `ltnSE` or a specific `nat` induction principle `ltn_ind`. Added (non-strict in)equality induction helper lemmas Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression along with some (in)equality, in preparation for some generalised induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed `ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember that the inductive value remains below the initial one. Used the change log to give notice to users to update the generalised induction idioms in their proofs to one of the new forms before Mathcomp 1.11.--- mathcomp/field/algebraics_fundamentals.v | 2 +- mathcomp/field/algnum.v | 2 +- mathcomp/field/closed_field.v | 9 +++++---- mathcomp/field/cyclotomic.v | 12 +++++------- mathcomp/field/fieldext.v | 4 ++-- mathcomp/field/galois.v | 13 +++++++------ mathcomp/field/separable.v | 18 ++++++++++-------- 7 files changed, 31 insertions(+), 29 deletions(-) (limited to 'mathcomp/field') diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 2d576c4..18fa55a 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -648,7 +648,7 @@ have /all_sig[n_ FTA] z: {n | z \in sQ (z_ n)}. have [p]: exists p, [&& p \is monic, root p z & p \is a polyOver (sQ (z_ n))]. have [p mon_p pz0] := algC z; exists (p ^ QtoC). by rewrite map_monic mon_p pz0 -(pQof (z_ n)); apply/polyOver_poly. - elim: {p}_.+1 {-2}p n (ltnSn (size p)) => // d IHd p n lepd pz0. + have [d lepd] := ubnP (size p); elim: d => // d IHd in p n lepd * => pz0. have [t [t_C t_z gal_t]]: exists t, [/\ z_ n \in sQ t, z \in sQ t & is_Gal t]. have [y /and3P[y_C y_z _]] := PET [:: z_ n; z]. by have [t /(sQtrans y)t_y] := galQ y; exists t; rewrite !t_y. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index f494a09..c191a0e 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -439,7 +439,7 @@ have nu_inj n y: nu (Sinj (ext n) y) = Sinj (ext n) (Saut (ext n) y). rewrite /nu; case: (mem_ext _ _ _); move: _.+1 => n1 y1 Dy /=. without loss /subnK Dn1: n n1 y y1 Dy / (n <= n1)%N. by move=> IH; case/orP: (leq_total n n1) => /IH => [/(_ y) | /(_ y1)]->. - elim: {n}(_ - n)%N {-1}n => [|k IHk] n in Dn1 y Dy *. + move: (n1 - n)%N => k in Dn1; elim: k => [|k IHk] in n Dn1 y Dy *. by move: y1 Dy; rewrite -Dn1 => y1 /fmorph_inj ->. rewrite addSnnS in Dn1; move/IHk: Dn1 => /=. case: (unpickle _) => [z|] /=; last exact. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index b55a48e..a6f7514 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -878,10 +878,11 @@ have Kclosed: GRing.ClosedField.axiom Kfield. apply/eqP; rewrite EtoKeq0 (eq_map_poly (toEleS _ _ _ _)) map_poly_comp Dpj. rewrite -rootE -[pj]minXpE ?ext1root // -Dpj size_map_poly. by rewrite size_addl ?size_polyXn ltnS ?size_opp ?size_poly. - rewrite {w}/pj; elim: {-9}j lemj => // k IHk lemSk. - move: lemSk (lemSk); rewrite {1}leq_eqVlt ltnS => /predU1P[<- | lemk] lemSk. - rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)) map_poly_id //= /incEp. - by rewrite codeK eqxx pickleK. + rewrite {w}/pj; set j0 := (j in tagged (E_ _) j). + elim: {+}j lemj => // k IHk lemSk; rewrite {}/j0 in IHk *. + have:= lemSk; rewrite leq_eqVlt ltnS => /predU1P[Dm | lemk]. + rewrite -{}Dm in lemSk *; rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)). + by rewrite map_poly_id //= /incEp codeK eqxx pickleK. rewrite (eq_map_poly (toEleS _ _ _ _)) map_poly_comp {}IHk //= /incEp codeK. by rewrite -if_neg neq_ltn lemk. suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}. diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index dcb4a5b..d80a909 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -149,7 +149,7 @@ Qed. Lemma Cintr_Cyclotomic n z : n.-primitive_root z -> pZtoC 'Phi_n = cyclotomic z n. Proof. -elim: {n}_.+1 {-2}n z (ltnSn n) => // m IHm n z0 le_mn prim_z0. +elim/ltn_ind: n z => n IHn z0 prim_z0. rewrite /'Phi_n; case: (C_prim_root_exists _) => z /=. have n_gt0 := prim_order_gt0 prim_z0; rewrite prednK // => prim_z. have [uDn _ inDn] := divisors_correct n_gt0. @@ -159,8 +159,7 @@ have defXn1: cyclotomic z n * pZtoC q = 'X^n - 1. rewrite (prod_cyclotomic prim_z) (big_rem n) ?inDn //=. rewrite divnn n_gt0 rmorph_prod /=; congr (_ * _). apply: eq_big_seq => d; rewrite mem_rem_uniq ?inE //= inDn => /andP[n'd ddvn]. - rewrite -IHm ?dvdn_prim_root // -ltnS (leq_ltn_trans _ le_mn) //. - by rewrite ltn_neqAle n'd dvdn_leq. + by rewrite -IHn ?dvdn_prim_root // ltn_neqAle n'd dvdn_leq. have mapXn1 (R1 R2 : ringType) (f : {rmorphism R1 -> R2}): map_poly f ('X^n - 1) = 'X^n - 1. - by rewrite rmorphB /= rmorph1 map_polyXn. @@ -263,8 +262,7 @@ have co_fg (R : idomainType): n%:R != 0 :> R -> @coprimep R (intrp f) (intrp g). suffices fzk0: root (pZtoC f) zk. have [] // := negP (coprimep_root (co_fg _ _) fzk0). by rewrite pnatr_eq0 -lt0n. -move: gzk0 cokn; rewrite {zk}Dzk; elim: {k}_.+1 {-2}k (ltnSn k) => // m IHm k. -rewrite ltnS => lekm gzk0 cokn. +move: gzk0 cokn; rewrite {zk}Dzk; elim/ltn_ind: k => k IHk gzk0 cokn. have [|k_gt1] := leqP k 1; last have [p p_pr /dvdnP[k1 Dk]] := pdivP k_gt1. rewrite -[leq k 1](mem_iota 0 2) !inE => /pred2P[k0 | ->]; last first. by rewrite -Df dv_pf. @@ -287,8 +285,8 @@ suffices: coprimep (pZtoC f) (pZtoC (g \Po 'X^p)). rewrite -exprM -Dk [_ == 0]gzk0 implybF => /negP[]. have: root pz (z ^+ k1). by rewrite root_cyclotomic // prim_root_exp_coprime. - rewrite -Dpz -Dfg rmorphM rootM => /orP[] //= /IHm-> //. - rewrite (leq_trans _ lekm) // -[k1]muln1 Dk ltn_pmul2l ?prime_gt1 //. + rewrite -Dpz -Dfg rmorphM rootM => /orP[] //= /IHk-> //. + rewrite -[k1]muln1 Dk ltn_pmul2l ?prime_gt1 //. by have:= ltnW k_gt1; rewrite Dk muln_gt0 => /andP[]. suffices: coprimep f (g \Po 'X^p). case/Bezout_coprimepP=> [[u v]]; rewrite -size_poly_eq1. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 64239f3..86d3d39 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -555,8 +555,8 @@ Qed. Lemma Fadjoin_sum_direct : directv sumKx. Proof. -rewrite directvE /=; case Dn: {-2}n (leqnn n) => // [m] {Dn}. -elim: m => [|m IHm] ltm1n; rewrite ?big_ord1 // !(big_ord_recr m.+1) /=. +rewrite directvE /=; case: (ubnPgeq n) (isT : n > 0) => -[//|m] ltmn _. +elim: m ltmn => [|m IHm] ltm1n; rewrite ?big_ord1 // !(big_ord_recr m.+1) /=. do [move/(_ (ltnW ltm1n))/eqP; set S := (\sum_i _)%VS] in IHm *. rewrite -IHm dimv_add_leqif; apply/subvP=> z; rewrite memv_cap => /andP[Sz]. case/memv_cosetP=> y Ky Dz; rewrite memv0 Dz mulf_eq0 expf_eq0 /=. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 7937a24..4aaef57 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -561,7 +561,7 @@ have [[p F0p splitLp] [autL DautL]] := (splittingFieldP, enum_AEnd). suffices{K} autL_px q: q != 0 -> q %| q1 -> size q > 1 -> has (fx_root q) autL. set q := minPoly K x; have: q \is monic := monic_minPoly K x. have: q %| q1 by rewrite minPolyS // sub1v. - elim: {q}_.+1 {-2}q (ltnSn (size q)) => // d IHd q leqd q_dv_q1 mon_q. + have [d] := ubnP (size q); elim: d q => // d IHd q leqd q_dv_q1 mon_q. have nz_q: q != 0 := monic_neq0 mon_q. have [|q_gt1|q_1] := ltngtP (size q) 1; last first; last by rewrite polySpred. by exists nil; rewrite big_nil -eqp_monic ?monic1 // -size_poly_eq1 q_1. @@ -571,7 +571,7 @@ suffices{K} autL_px q: q != 0 -> q %| q1 -> size q > 1 -> has (fx_root q) autL. have q2_dv_q1: q2 %| q1 by rewrite (dvdp_trans _ q_dv_q1) // Dq dvdp_mulr. rewrite Dq; have [r /eqP->] := IHd q2 leqd q2_dv_q1 mon_q2. by exists (f x :: r); rewrite big_cons mulrC. -elim: {q}_.+1 {-2}q (ltnSn (size q)) => // d IHd q leqd nz_q q_dv_q1 q_gt1. +have [d] := ubnP (size q); elim: d q => // d IHd q leqd nz_q q_dv_q1 q_gt1. without loss{d leqd IHd nz_q q_gt1} irr_q: q q_dv_q1 / irreducible_poly q. move=> IHq; apply: wlog_neg => not_autLx_q; apply: IHq => //. split=> // q2 q2_neq1 q2_dv_q; rewrite -dvdp_size_eqp // eqn_leq dvdp_leq //=. @@ -645,9 +645,10 @@ have [f homLf fxz]: exists2 f : 'End(Lz), kHom 1 imL f & f (inLz x) = z. pose f1 := (inLz^-1 \o f \o inLz)%VF; have /kHomP[fM fFid] := homLf. have Df1 u: inLz (f1 u) = f (inLz u). rewrite !comp_lfunE limg_lfunVK //= -[limg _]/(asval imL). - have [r def_pz defLz] := splitLpz. - have []: all (mem r) r /\ inLz u \in imL by split; first apply/allP. - rewrite -{1}defLz; elim/last_ind: {-1}r {u}(inLz u) => [|r1 y IHr1] u. + have [r def_pz defLz] := splitLpz; set r1 := r. + have: inLz u \in <<1 & r1>>%VS by rewrite defLz. + have: all (mem r) r1 by apply/allP. + elim/last_ind: r1 {u}(inLz u) => [|r1 y IHr1] u. by rewrite Fadjoin_nil => _ Fu; rewrite fFid // (subvP (sub1v _)). rewrite all_rcons adjoin_rcons => /andP[rr1 ry] /Fadjoin_polyP[pu r1pu ->]. rewrite (kHom_horner homLf) -defLz; last exact: seqv_sub_adjoin; last first. @@ -1353,7 +1354,7 @@ Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of E -> L) x : P x -> c_ x != 0 -> exists2 a, a \in E & \sum_(y | P y) c_ y * y a != 0. Proof. -elim: {P}_.+1 c_ x {-2}P (ltnSn #|P|) => // n IHn c_ x P lePn Px nz_cx. +have [n] := ubnP #|P|; elim: n c_ x P => // n IHn c_ x P lePn Px nz_cx. rewrite ltnS (cardD1x Px) in lePn; move/IHn: lePn => {n IHn}/=IH_P. have [/eqfun_inP c_Px'_0 | ] := boolP [forall (y | P y && (y != x)), c_ y == 0]. exists 1; rewrite ?mem1v // (bigD1 x Px) /= rmorph1 mulr1. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index a482632..bc2eecb 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -482,9 +482,9 @@ Lemma extendDerivation_horner p : extendDerivation K p.[x] = (map_poly D p).[x] + p^`().[x] * Dx K. Proof. move=> Kp sepKx; have:= separable_root_der; rewrite {}sepKx /= => nz_pKx'x. -rewrite {-1}(divp_eq p (minPoly K x)) lfunE /= Fadjoin_poly_mod // raddfD /=. -rewrite {1}(Derivation_mul_poly derD) ?divp_polyOver ?minPolyOver //. -rewrite derivD derivM !{1}hornerD !{1}hornerM minPolyxx !{1}mulr0 !{1}add0r. +rewrite [in RHS](divp_eq p (minPoly K x)) lfunE /= Fadjoin_poly_mod ?raddfD //=. +rewrite (Derivation_mul_poly derD) ?divp_polyOver ?minPolyOver //. +rewrite derivM !{1}hornerD !{1}hornerM minPolyxx !{1}mulr0 !{1}add0r. rewrite mulrDl addrA [_ + (_ * _ * _)]addrC {2}/Dx -mulrA -/Dx. by rewrite [_ / _]mulrC (mulVKf nz_pKx'x) mulrN addKr. Qed. @@ -528,12 +528,14 @@ have DK_0: (K <= lker D)%VS. apply/subvP=> v Kv; rewrite memv_ker lfunE /= Fadjoin_polyC //. by rewrite derivC horner0. have Dder: Derivation <> D. - apply/allP=> u /vbasis_mem Kx_u; apply/allP=> v /vbasis_mem Kx_v. - rewrite !lfunE /= -{-2}(Fadjoin_poly_eq Kx_u) -{-3}(Fadjoin_poly_eq Kx_v). + apply/allP=> u /vbasis_mem Kx_u; apply/allP=> v /vbasis_mem Kx_v; apply/eqP. + rewrite !lfunE /=; set Px := Fadjoin_poly K x. + set Px_u := Px u; rewrite -(Fadjoin_poly_eq Kx_u) -/Px -/Px_u. + set Px_v := Px v; rewrite -(Fadjoin_poly_eq Kx_v) -/Px -/Px_v. rewrite -!hornerM -hornerD -derivM. - rewrite Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver //. - rewrite {2}(divp_eq (_ * _) (minPoly K x)) derivD derivM pKx'_0 mulr0 addr0. - by rewrite hornerD hornerM minPolyxx mulr0 add0r. + rewrite /Px Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver //. + rewrite [in RHS](divp_eq (Px_u * Px_v) (minPoly K x)) derivD derivM. + by rewrite pKx'_0 mulr0 addr0 hornerD hornerM minPolyxx mulr0 add0r. have{Dder DK_0}: x \in lker D by apply: subvP Kx_x; apply: derKx_0. apply: contraLR => K'x; rewrite memv_ker lfunE /= Fadjoin_polyX //. by rewrite derivX hornerC oner_eq0. -- cgit v1.2.3