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.

1 files changed, 5 insertions, 4 deletions

diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 929c313..702dfc4 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -142,8 +142,8 @@ Definition coefp_head h i (p : poly_of (Phant R)) := let: tt := h in p`_i.
 
 End Polynomial.
 
-(* We need to break off the section here to let the argument scope *)
-(* directives take effect.                                         *)
+(* We need to break off the section here to let the Bind Scope directives     *)
+(* take effect.                                                               *)
 Bind Scope ring_scope with poly_of.
 Bind Scope ring_scope with polynomial.
 Arguments polyseq {R} p%R.
@@ -1675,7 +1675,7 @@ Qed.
 
 End PolynomialTheory.
 
-Prenex Implicits polyC Poly lead_coef root horner polyOver.
+Prenex Implicits polyC polyCK Poly polyseqK lead_coef root horner polyOver.
 Arguments monic {R}.
 Notation "\poly_ ( i < n ) E" := (poly n (fun i => E)) : ring_scope.
 Notation "c %:P" := (polyC c) : ring_scope.
@@ -1694,6 +1694,7 @@ Arguments rootPf {R p x}.
 Arguments rootPt {R p x}.
 Arguments unity_rootP {R n z}.
 Arguments polyOverP {R S0 addS kS p}.
+Arguments polyC_inj {R} [x1 x2] eq_x12P.
 
 Canonical polynomial_countZmodType (R : countRingType) :=
   [countZmodType of polynomial R].
@@ -1947,7 +1948,7 @@ Definition comp_poly q p := p^:P.[q].
 Local Notation "p \Po q" := (comp_poly q p) : ring_scope.
 
 Lemma size_map_polyC p : size p^:P = size p.
-Proof. exact: size_map_inj_poly (@polyC_inj R) _ _. Qed.
+Proof. exact/(size_map_inj_poly polyC_inj). Qed.
 
 Lemma map_polyC_eq0 p : (p^:P == 0) = (p == 0).
 Proof. by rewrite -!size_poly_eq0 size_map_polyC. Qed.