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, 6 insertions, 2 deletions

diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 40a1f83..47cee1f 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -875,6 +875,7 @@ End ZmoduleTheory.
 
 Arguments addrI {V} y [x1 x2].
 Arguments addIr {V} x [x1 x2].
+Arguments opprK {V}.
 Arguments oppr_inj {V} [x1 x2].
 
 Module Ring.
@@ -3031,6 +3032,7 @@ End ClosedPredicates.
 
 End UnitRingTheory.
 
+Arguments invrK {R}.
 Arguments invr_inj {R} [x1 x2].
 
 Section UnitRingMorphism.
@@ -5370,7 +5372,8 @@ Arguments addrI {V} y [x1 x2].
 Arguments addIr {V} x [x1 x2].
 Arguments subrI {V} y [x1 x2].
 Arguments subIr {V} x [x1 x2].
-Definition opprK := opprK.
+Definition opprK := @opprK.
+Arguments opprK {V}.
 Definition oppr_inj := @oppr_inj.
 Arguments oppr_inj {V} [x1 x2].
 Definition oppr0 := oppr0.
@@ -5554,7 +5557,8 @@ Definition divIr := divIr.
 Definition telescope_prodr := telescope_prodr.
 Definition commrV := commrV.
 Definition unitrE := unitrE.
-Definition invrK := invrK.
+Definition invrK := @invrK.
+Arguments invrK {R}.
 Definition invr_inj := @invr_inj.
 Arguments invr_inj {R} [x1 x2].
 Definition unitrV := unitrV.