From 0b1ea03dafcf36880657ba910eec28ab78ccd018 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Thu, 13 Dec 2018 12:55:43 +0100 Subject: Adjust implicits of cancellation lemmas Like injectivity lemmas, instances of cancellation lemmas (whose conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or `ocancel`) are passed to generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should not have trailing on-demand implicits _just before_ the `cancel` conclusion, as these would be inconvenient to insert (requiring essentially an explicit eta-expansion). We therefore use `Arguments` or `Prenex Implicits` directives to make all such arguments maximally inserted implicits. We don’t, however make other arguments implicit, so as not to spoil direct instantiation of the lemmas (in, e.g., `rewrite -[y](invmK injf)`). We have also tried to do this with lemmas whose statement matches a `cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern unification will pick up `f = fun x => E[x]`). We also adjusted implicits of a few stray injectivity lemmas, and defined constants. We provide a shorthand for reindexing a bigop with a permutation. Finally we used the new implicit signatures to simplify proofs that use injectivity or cancellation lemmas. --- mathcomp/field/algC.v | 7 ++++--- mathcomp/field/algnum.v | 4 ++-- mathcomp/field/closed_field.v | 4 ++-- mathcomp/field/fieldext.v | 19 +++++++++---------- mathcomp/field/galois.v | 3 +++ 5 files changed, 20 insertions(+), 17 deletions(-) (limited to 'mathcomp/field') diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index fc01763..ae60027 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -279,7 +279,7 @@ Canonical eqType := EqType type eqMixin. Definition choiceMixin : Choice.mixin_of type := EquivQuot.choiceMixin _. Canonical choiceType := ChoiceType type choiceMixin. -Definition countMixin : Countable.mixin_of type := CanCountMixin (@reprK _ _). +Definition countMixin : Countable.mixin_of type := CanCountMixin reprK. Canonical countType := CountType type countMixin. Definition CtoL (u : type) := rootQtoL (repr u). @@ -607,7 +607,8 @@ Local Notation intrp := (map_poly intr). Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj _ : injective ZtoC) : core. + +Local Hint Resolve (intr_inj : injective ZtoC) : core. (* Specialization of a few basic ssrnum order lemmas. *) @@ -882,7 +883,7 @@ Lemma CintE x : (x \in Cint) = (x \in Cnat) || (- x \in Cnat). Proof. apply/idP/idP=> [/CintP[[n | n] ->] | ]; first by rewrite Cnat_nat. by rewrite NegzE opprK Cnat_nat orbT. -by case/pred2P=> [<- | /(canLR (@opprK _)) <-]; rewrite ?rpredN rpred_nat. +by case/pred2P=> [<- | /(canLR opprK) <-]; rewrite ?rpredN rpred_nat. Qed. Lemma Cnat_norm_Cint x : x \in Cint -> `|x| \in Cnat. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 1db4aa4..3053eb9 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -56,7 +56,7 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj _ : injective ZtoC) : core. +Local Hint Resolve (intr_inj : injective ZtoC) : core. Local Notation QtoCm := [rmorphism of QtoC]. (* Number fields and rational spans. *) @@ -417,7 +417,7 @@ have ext1 mu0 x: {mu1 | exists y, x = Sinj mu1 y by apply/polyOverP=> i; rewrite coef_map memvZ ?memv_line. have splitQr: splittingFieldFor K pr fullv. apply: splittingFieldForS (sub1v (Sub K algK)) (subvf _) _; exists rr => //. - congr (_ %= _): (eqpxx pr); apply: (@map_poly_inj _ _ QrC). + congr (_ %= _): (eqpxx pr); apply/(map_poly_inj QrC). rewrite Sinj_poly Dr -Drr big_map rmorph_prod; apply: eq_bigr => zz _. by rewrite rmorphB /= map_polyX map_polyC. have [f1 aut_f1 Df1]:= kHom_extends (sub1v (ASpace algK)) hom_f Qpr splitQr. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 76039d1..c338002 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -714,7 +714,7 @@ have EmulV: GRing.Field.axiom Einv. rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE. by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; apply: dvdp_mull. pose Efield := FieldType _ (FieldMixin EmulV Einv0). -pose Ecount := CountType Efield (CanCountMixin (@reprK _ _)). +pose Ecount := CountType Efield (CanCountMixin reprK). pose FtoE := [rmorphism of PtoE \o polyC]; pose w : E := PtoE 'X. have defPtoE q: (map_poly FtoE q).[w] = PtoE q. by rewrite map_poly_comp horner_map [_.['X]]comp_polyXr. @@ -783,7 +783,7 @@ have eqKtrans : transitive eqKrep. do [rewrite -toEtrans ?le_max // -maxnA => lez2m] in lez3m *. by rewrite (toEtrans (maxn (tag z2) (tag z3))) // eq_z23 -toEtrans. pose K := {eq_quot (EquivRel _ eqKrefl eqKsym eqKtrans)}%qT. -have cntK : Countable.mixin_of K := CanCountMixin (@reprK _ _). +have cntK : Countable.mixin_of K := CanCountMixin reprK. pose EtoKrep i (x : E i) : K := \pi%qT (Tagged E x). have [EtoK piEtoK]: {EtoK | forall i, EtoKrep i =1 EtoK i} by exists EtoKrep. pose FtoK := EtoK 0%N; rewrite {}/EtoKrep in piEtoK. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 99db561..7c89607 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -1468,7 +1468,7 @@ Proof. move/subfx_irreducibleP: irr_p => /=/(_ nz_p) min_p; set d := (size p).-1. have Dd: d.+1 = size p by rewrite polySpred. pose Fz2v x : 'rV_d := poly_rV (sval (sig_eqW (subfxE x)) %% p). -pose vFz : 'rV_d -> subFExtend := subfx_eval \o @rVpoly F d. +pose vFz : 'rV_d -> subFExtend := subfx_eval \o rVpoly. have FLinj: injective subfx_inj by apply: fmorph_inj. have Fz2vK: cancel Fz2v vFz. move=> x; rewrite /vFz /Fz2v; case: (sig_eqW _) => /= q ->. @@ -1479,7 +1479,7 @@ suffices vFzK: cancel vFz Fz2v. apply: inj_can_sym Fz2vK _ => v1 v2 /(congr1 subfx_inj)/eqP. rewrite -subr_eq0 -!raddfB /= subfx_inj_eval // => /min_p/implyP. rewrite leqNgt implybNN -Dd ltnS size_poly linearB subr_eq0 /=. -by move/eqP/(can_inj (@rVpolyK _ _)). +by move/eqP/(can_inj rVpolyK). Qed. Definition SubfxVectMixin := VectMixin min_subfx_vectAxiom. @@ -1559,7 +1559,7 @@ pose ucrL := [comUnitRingType of ComRingType urL mulC]. have mul0 := GRing.Field.IdomainMixin unitE. pose fL := FieldType (IdomainType ucrL mul0) unitE. exists [fieldExtType F of faL for fL]; first by rewrite dimvf; apply: mul1n. -exists [linear of toPF as @rVpoly _ _]. +exists [linear of toPF as rVpoly]. suffices toLM: lrmorphism (toL : {poly F} -> aL) by exists (LRMorphism toLM). have toLlin: linear toL. by move=> a q1 q2; rewrite -linearP -modp_scalel -modp_add. @@ -1592,13 +1592,13 @@ have mul1: left_id L1 mul. move=> x; rewrite /mul L1K mul1r /toL modp_small ?rVpolyK // -Dn ltnS. by rewrite size_poly. have mulD: left_distributive mul +%R. - move=> x y z; apply: canLR (@rVpolyK _ _) _. + move=> x y z; apply: canLR rVpolyK _. by rewrite !raddfD mulrDl /= !toL_K /toL modp_add. -have nzL1: L1 != 0 by rewrite -(can_eq (@rVpolyK _ _)) L1K raddf0 oner_eq0. +have nzL1: L1 != 0 by rewrite -(can_eq rVpolyK) L1K raddf0 oner_eq0. pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1. pose rL := ComRingType (RingType vL mulM) mulC. have mulZl: GRing.Lalgebra.axiom mul. - move=> a x y; apply: canRL (@rVpolyK _ _) _; rewrite !linearZ /= toL_K. + move=> a x y; apply: canRL rVpolyK _; rewrite !linearZ /= toL_K. by rewrite -scalerAl modp_scalel. have mulZr: @GRing.Algebra.axiom _ (LalgType F rL mulZl). by move=> a x y; rewrite !(mulrC x) scalerAl. @@ -1607,7 +1607,7 @@ pose uaL := [unitAlgType F of AlgType F urL mulZr]. pose faL := [FalgType F of uaL]. have unitE: GRing.Field.mixin_of urL. move=> x nz_x; apply/unitrP; set q := rVpoly x. - have nz_q: q != 0 by rewrite -(can_eq (@rVpolyK _ _)) raddf0 in nz_x. + have nz_q: q != 0 by rewrite -(can_eq rVpolyK) raddf0 in nz_x. have /Bezout_eq1_coprimepP[u upq1]: coprimep p q. have /contraR := irr_p _ _ (dvdp_gcdl p q); apply. have: size (gcdp p q) <= size q by apply: leq_gcdpr. @@ -1627,11 +1627,10 @@ have q_z q: rVpoly (map_poly iota q).[z] = q %% p. rewrite linearZ /= L1K alg_polyC modp_add; congr (_ + _); last first. by rewrite modp_small // size_polyC; case: (~~ _) => //; apply: ltnW. by rewrite !toL_K IHq mulrC modp_mul mulrC modp_mul. -exists z; first by rewrite /root -(can_eq (@rVpolyK _ _)) q_z modpp linear0. +exists z; first by rewrite /root -(can_eq rVpolyK) q_z modpp linear0. apply/vspaceP=> x; rewrite memvf; apply/Fadjoin_polyP. exists (map_poly iota (rVpoly x)). by apply/polyOverP=> i; rewrite coef_map memvZ ?mem1v. -apply: (can_inj (@rVpolyK _ _)). -by rewrite q_z modp_small // -Dn ltnS size_poly. +by apply/(can_inj rVpolyK); rewrite q_z modp_small // -Dn ltnS size_poly. Qed. *) diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 252868d..fb96ffe 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -1634,6 +1634,9 @@ End FundamentalTheoremOfGaloisTheory. End GaloisTheory. +Prenex Implicits gal_repr gal gal_reprK. +Arguments gal_repr_inj {F L V} [x1 x2]. + Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope. Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope. -- cgit v1.2.3