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, 59 insertions, 20 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 9a61ebe..783c46f 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -817,7 +817,9 @@ Qed.
 End IrrClass.
 
 Arguments cfReg {gT} B%g.
-Prenex Implicits cfIirr.
+Prenex Implicits cfIirr irrK.
+Arguments irrP {gT G xi}.
+Arguments irr_reprP {gT G xi}.
 Arguments irr_inj {gT G} [x1 x2].
 
 Section IsChar.
@@ -1334,6 +1336,8 @@ Qed.
 
 End OrthogonalityRelations.
 
+Prenex Implicits irr_class class_Iirr irr_classK.
+Arguments class_IirrK {gT G%G} [xG%g] GxG : rename.
 Arguments character_table {gT} G%g.
 
 Section InnerProduct.
@@ -1353,7 +1357,7 @@ Lemma irr_orthonormal : orthonormal (irr G).
 Proof.
 apply/orthonormalP; split; first exact: free_uniq (irr_free G).
 move=> _ _ /irrP[i ->] /irrP[j ->].
-by rewrite cfdot_irr (inj_eq (@irr_inj _ G)).
+by rewrite cfdot_irr (inj_eq irr_inj).
 Qed.
 
 Lemma coord_cfdot phi i : coord (irr G) i phi = '[phi, 'chi_i].
@@ -1436,7 +1440,7 @@ Qed.
 
 Lemma eq_signed_irr (s t : bool) i j :
   ((-1) ^+ s *: 'chi[G]_i == (-1) ^+ t *: 'chi_j) = (s == t) && (i == j).
-Proof. by rewrite eq_scaled_irr signr_eq0 (inj_eq (@signr_inj _)). Qed.
+Proof. by rewrite eq_scaled_irr signr_eq0 (inj_eq signr_inj). Qed.
 
 Lemma eq_scale_irr a (i j : Iirr G) :
   (a *: 'chi_i == a *: 'chi_j) = (a == 0) || (i == j).
@@ -2258,6 +2262,7 @@ Qed.
 End Aut.
 
 Arguments aut_Iirr_inj {gT G} u [i1 i2] : rename.
+Arguments conjC_IirrK {gT G} i : rename.
 
 Section Coset.
 
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index a4ecd2c..2048868 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -759,6 +759,7 @@ Arguments classfun_on {gT} B%g A%g.
 Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.
 
 Arguments cfun_onP {gT G A phi}.
+Arguments cfConjCK {gT G} phi : rename.
 Hint Resolve cfun_onT : core.
 
 Section DotProduct.
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index 22ab389..1d8f785 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -755,6 +755,8 @@ End SubGroup.
 
 End AbelemRepr.
 
+Arguments rVabelem_inj {p%N gT E%G} abelE ntE [v1%R v2%R] : rename.
+
 Section ModularRepresentation.
 
 Variables (F : fieldType) (p : nat) (gT : finGroupType).
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index 560b61d..0968347 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -300,13 +300,13 @@ Lemma repr_mxM : {in G &, {morph rG : x y / (x * y)%g >-> x *m y}}.
 Proof. by case: rG => r []. Qed.
 
 Lemma repr_mxK m x :
-  x \in G ->  cancel ((@mulmx _ m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).
+  x \in G ->  cancel ((@mulmx R m n n)^~ (rG x)) (mulmx^~ (rG x^-1)).
 Proof.
 by move=> Gx U; rewrite -mulmxA -repr_mxM ?groupV // mulgV repr_mx1 mulmx1.
 Qed.
 
 Lemma repr_mxKV m x :
-  x \in G -> cancel ((@mulmx _ m n n)^~ (rG x^-1)) (mulmx^~ (rG x)).
+  x \in G -> cancel ((@mulmx R m n n)^~ (rG x^-1)) (mulmx^~ (rG x)).
 Proof. by rewrite -groupV -{3}[x]invgK; apply: repr_mxK. Qed.
 
 Lemma repr_mx_unit x : x \in G -> rG x \in unitmx.
@@ -821,7 +821,11 @@ Arguments regular_repr R {gT} G%g.
 
 Arguments centgmxP {R gT G n rG f}.
 Arguments rkerP {R gT G n rG x}.
-Prenex Implicits gring_mxK.
+Arguments repr_mxK {R gT G%G n%N} rG {m%N} [x%g] Gx.
+Arguments repr_mxKV {R gT G%G n%N} rG {m%N} [x%g] Gx.
+Arguments gring_valK {gT G%G} i%R : rename.
+Arguments gring_indexK {gT G%G} x%g.
+Arguments gring_mxK {R gT G%G} v%R : rename.
 
 Section ChangeOfRing.
 
@@ -2377,7 +2381,16 @@ Arguments mxsimple_isoP {gT G n rG U V}.
 Arguments socleP {gT G n rG sG0 W W'}.
 Arguments mx_abs_irrP {gT G n rG}.
 
+Arguments val_submod {n U m} W.
+Arguments in_submod {n} U {m} W.
+Arguments val_submodK {n U m} W : rename.
+Arguments in_submodK {n U m} [W] sWU.
 Arguments val_submod_inj {n U m} [W1 W2] : rename.
+
+Arguments val_factmod {n U m} W.
+Arguments in_factmod {n} U {m} W.
+Arguments val_factmodK {n U m} W : rename.
+Arguments in_factmodK {n} U {m} [W] sWU.
 Arguments val_factmod_inj {n U m} [W1 W2] : rename.
 
 Section Proper.
@@ -3797,7 +3810,7 @@ rewrite !permM; case: (unliftP i_m i) => [j {simWUm}|] ->{i}; last first.
 apply: rsimT (rsimC _) {pUW}(rsimT (pUW j) _).
   by rewrite lift_max; apply: rsim_rcons.
 rewrite lift_perm_lift; case: (unliftP j_m (pU j)) => [k|] ->{j pU}.
-  rewrite tpermD ?(inj_eq (@lift_inj _ _)) ?neq_lift //.
+  rewrite tpermD ?(inj_eq lift_inj) ?neq_lift //.
   rewrite lift_perm_lift !lift_max; set j := lift j_m k.
   have ltjW: j < size W by have:= ltn_ord k; rewrite -(lift_max k) /= {1 3}szW.
   apply: rsimT (rsimT (pWV j) _); last by apply: rsim_rcons; rewrite -szV.
@@ -4671,16 +4684,28 @@ Arguments socleP {F gT G n rG sG0 W W'}.
 Arguments mx_abs_irrP {F gT G n rG}.
 Arguments socle_rsimP {F gT G n rG sG W1 W2}.
 
+Arguments val_submod {F n U m} W.
+Arguments in_submod {F n} U {m} W.
+Arguments val_submodK {F n U m} W : rename.
+Arguments in_submodK {F n U m} [W] sWU.
 Arguments val_submod_inj {F n U m} [W1 W2] : rename.
+
+Arguments val_factmod {F n U m} W.
+Arguments in_factmod {F n} U {m} W.
+Arguments val_factmodK {F n U m} W : rename.
+Arguments in_factmodK {F n} U {m} [W] sWU.
 Arguments val_factmod_inj {F n U m} [W1 W2] : rename.
 
 Notation "'Cl" := (Clifford_action _) : action_scope.
 
+Arguments gring_row {R gT G} A.
+Arguments gring_rowK {F gT G} [A] RG_A.
+
 Bind Scope irrType_scope with socle_sort.
 Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope.
 Arguments irr_degree {F gT G%G sG} i%irr.
-Arguments irr_repr [F gT G%G sG] i%irr _%g : extra scopes.
-Arguments irr_mode [F gT G%G sG] i%irr z%g : rename.
+Arguments irr_repr {F gT G%G sG} i%irr _%g : extra scopes.
+Arguments irr_mode {F gT G%G sG} i%irr z%g : rename.
 Notation "''n_' i" := (irr_degree i) : group_ring_scope.
 Notation "''R_' i" := (Wedderburn_subring i) : group_ring_scope.
 Notation "''e_' i" := (Wedderburn_id i) : group_ring_scope.
@@ -4973,7 +4998,7 @@ Proof.
 move=> splitG n rG irrG.
 have modU0: all ((mxmodule (regular_repr aF G)) #|G|) [::] by [].
 apply: (mx_Schreier modU0 _) => // [[U [compU lastU _]]]; have [modU _]:= compU.
-pose Uf := map ((map_mx f) _ _) U.
+pose Uf := map (map_mx f) U.
 have{lastU} lastUf: (last 0 Uf :=: 1%:M)%MS.
   by rewrite -(map_mx0 f) -(map_mx1 f) last_map; apply/map_eqmx.
 have modUf: mx_subseries (regular_repr rF G) Uf.
@@ -5062,7 +5087,7 @@ by rewrite /mxval [pval _]poly_rV_K ?horner_mx_C // size_polyC; case: (x != 0).
 Qed.
 
 Lemma mxval_inj : injective mxval.
-Proof. exact: inj_comp (@horner_rVpoly_inj _ _ A) val_inj. Qed.
+Proof. exact: inj_comp horner_rVpoly_inj val_inj. Qed.
 
 Lemma mxval0 : mxval 0 = 0.
 Proof. by rewrite /mxval [pval _]raddf0 rmorph0. Qed.
@@ -5557,6 +5582,11 @@ Proof. by rewrite /mx_faithful rker_gen. Qed.
 
 End GenField.
 
+Arguments in_gen {F gT G n' rG A} irrG cGA {m1} W.
+Arguments val_gen {F gT G n' rG A} irrG cGA {m1} W.
+Arguments in_genK {F gT G n' rG A} irrG cGA {m1} W : rename.
+Arguments val_genK {F gT G n' rG A} irrG cGA {m1} W : rename.
+
 Section DecideGenField.
 
 Import MatrixFormula.
@@ -5596,7 +5626,7 @@ Lemma eval_mulT e u v :
   eval_mx e (mulT u v) = val (inFA (eval_mx e u) * inFA (eval_mx e v)).
 Proof.
 rewrite !(eval_mulmx, eval_mxvec) !eval_mxT eval_mx_term.
-by apply: (can_inj (@rVpolyK _ _)); rewrite -mxvalM [rVpoly _]horner_rVpolyK.
+by apply: (can_inj rVpolyK); rewrite -mxvalM [rVpoly _]horner_rVpolyK.
 Qed.
 
 Fixpoint gen_term t := match t with
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 5c9ca9b..246e955 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -749,7 +749,7 @@ Lemma cfdot_dirr f g : f \in dirr G -> g \in dirr G ->
 Proof.
 case/dirrP=> [b1 [i1 ->]] /dirrP[b2 [i2 ->]].
 rewrite cfdotZl cfdotZr rmorph_sign mulrA -signr_addb cfdot_irr.
-rewrite -scaleNr -signrN !eq_scaled_irr signr_eq0 !(inj_eq (@signr_inj _)) /=.
+rewrite -scaleNr -signrN !eq_scaled_irr signr_eq0 !(inj_eq signr_inj) /=.
 by rewrite -!negb_add addbN mulr_sign -mulNrn mulrb; case: ifP.
 Qed.
 
@@ -799,7 +799,7 @@ Lemma cfdot_dchi (i j : dIirr G) :
   '[dchi i, dchi j] = (i == j)%:R - (i == ndirr j)%:R.
 Proof.
 case: i => bi i; case: j => bj j; rewrite cfdot_dirr ?dirr_dchi // !xpair_eqE.
-rewrite -dchi_ndirrE !eq_scaled_irr signr_eq0 !(inj_eq (@signr_inj _)) /=.
+rewrite -dchi_ndirrE !eq_scaled_irr signr_eq0 !(inj_eq signr_inj) /=.
 by rewrite -!negb_add addbN negbK; case: andP => [[->]|]; rewrite ?subr0 ?add0r.
 Qed.
 
@@ -811,7 +811,7 @@ Proof.  by case: i => b i; rewrite cfnorm_sign cfnorm_irr. Qed.
 
 Lemma dirr_inj : injective (@dchi G).
 Proof.
-case=> b1 i1 [b2 i2] /eqP; rewrite eq_scaled_irr (inj_eq (@signr_inj _)) /=.
+case=> b1 i1 [b2 i2] /eqP; rewrite eq_scaled_irr (inj_eq signr_inj) /=.
 by rewrite signr_eq0 -xpair_eqE => /eqP.
 Qed.
 
@@ -890,15 +890,13 @@ Lemma cfdot_todirrE (phi: 'CF(G)) i (phi_i := dchi (to_dirr phi i)) :
 Proof. by rewrite cfdotZr rmorph_sign mulrC -scalerA signrZK. Qed.
 
 Lemma cfun_sum_dconstt (phi : 'CF(G)) :
-  phi \in 'Z[irr G] ->
+    phi \in 'Z[irr G] ->
   phi = \sum_(i in dirr_constt phi) '[phi, dchi i] *: dchi i.
 Proof.
-(* GG -- rewrite pattern fails in trunk
-  move=> PiZ; rewrite [X in X = _]cfun_sum_constt. *)
-move=> PiZ; rewrite {1}[phi]cfun_sum_constt.
+move=> PiZ; rewrite [LHS]cfun_sum_constt.
 rewrite (reindex (to_dirr phi))=> [/= |]; last first.
   by exists (@of_irr _)=> //; apply: of_irrK .
-by apply: eq_big=> i; rewrite ?irr_constt_to_dirr // cfdot_todirrE.
+by apply: eq_big => i; rewrite ?irr_constt_to_dirr // cfdot_todirrE.
 Qed.
 
 Lemma cnorm_dconstt (phi : 'CF(G)) :
@@ -981,3 +979,6 @@ by case: (i1 == j) eq_phi_psi; case: (i2 == j); do 2!case: (_ (+) c).
 Qed.
 
 End Norm1vchar.
+
+Prenex Implicits ndirr ndirrK to_dirr to_dirrK of_irr.
+Arguments of_irrK {gT G phi} [i] phi_i : rename.