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, 5 deletions

diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index 97b2eba..61b0cd9 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.v
@@ -198,13 +198,14 @@ Lemma quotientE : quotient = coset @* Q. Proof. by []. Qed.
 
 End Cosets.
 
-Arguments coset_of {_} _%g.
-Arguments coset {_} _%g _%g.
-Arguments quotient _ _%g _%g.
+Arguments coset_of {gT} H%g : rename.
+Arguments coset {gT} H%g x%g : rename.
+Arguments quotient {gT} A%g H%g : rename.
+Arguments coset_reprK {gT H%g} xbar%g : rename.
 
 Bind Scope group_scope with coset_of.
 
-Notation "A / B" := (quotient A B) : group_scope.
+Notation "A / H" := (quotient A H) : group_scope.
 
 Section CosetOfGroupTheory.
 
@@ -454,7 +455,7 @@ Proof. by rewrite /normal -{1}ker_coset; apply: morphim_injG. Qed.
 
 Lemma quotient_inj G1 G2 :
    H <| G1 -> H <| G2 -> G1 / H = G2 / H -> G1 :=: G2.
-Proof. by rewrite /normal -{1 3}ker_coset; apply: morphim_inj. Qed.
+Proof. by rewrite /normal -[in mem H]ker_coset; apply: morphim_inj. Qed.
 
 Lemma quotient_neq1 A : H <| A -> (A / H != 1) = (H \proper A).
 Proof.