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.

5 files changed, 20 insertions, 17 deletions

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.