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, 12 insertions, 9 deletions

diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index b1a7dd7..8c97ab1 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -125,10 +125,8 @@ Proof. by rewrite [@fun_of_perm]unlock. Qed.
 Lemma permE f f_inj : @perm T f f_inj =1 f.
 Proof. by move=> x; rewrite -pvalE [@perm]unlock ffunE. Qed.
 
-Lemma perm_inj s : injective s.
+Lemma perm_inj {s} : injective s.
 Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed.
-
-Arguments perm_inj : clear implicits.
 Hint Resolve perm_inj : core.
 
 Lemma perm_onto s : codom s =i predT.
@@ -141,7 +139,7 @@ Proof. by move=> x /=; rewrite f_iinv. Qed.
 
 Definition perm_inv s := perm (can_inj (perm_invK s)).
 
-Definition perm_mul s t := perm (inj_comp (perm_inj t) (perm_inj s)).
+Definition perm_mul s t := perm (inj_comp (@perm_inj t) (@perm_inj s)).
 
 Lemma perm_oneP : left_id perm_one perm_mul.
 Proof. by move=> s; apply/permP => x; rewrite permE /= permE. Qed.
@@ -191,7 +189,7 @@ Definition perm_on S : pred {perm T} := fun s => [pred x | s x != x] \subset S.
 Lemma perm_closed S s x : perm_on S s -> (s x \in S) = (x \in S).
 Proof.
 move/subsetP=> s_on_S; have [-> // | nfix_s_x] := eqVneq (s x) x.
-by rewrite !s_on_S // inE /= ?(inj_eq (perm_inj s)).
+by rewrite !s_on_S // inE /= ?(inj_eq perm_inj).
 Qed.
 
 Lemma perm_on1 H : perm_on H 1.
@@ -282,7 +280,11 @@ Qed.
 
 End Theory.
 
-Prenex Implicits tperm.
+Prenex Implicits tperm permK permKV tpermK.
+Arguments perm_inj {T s} [x1 x2] eq_sx12.
+
+(* Shorthand for using a permutation to reindex a bigop. *)
+Notation reindex_perm s := (reindex_inj (@perm_inj _ s)).
 
 Lemma inj_tperm (T T' : finType) (f : T -> T') x y z :
   injective f -> f (tperm x y z) = tperm (f x) (f y) (f z).
@@ -291,8 +293,7 @@ Proof. by move=> injf; rewrite !permE /= !(inj_eq injf) !(fun_if f). Qed.
 Lemma tpermJ (T : finType) x y (s : {perm T}) :
   (tperm x y) ^ s = tperm (s x) (s y).
 Proof.
-apply/permP => z; rewrite -(permKV s z) permJ; apply: inj_tperm.
-exact: perm_inj.
+by apply/permP => z; rewrite -(permKV s z) permJ; apply/inj_tperm/perm_inj.
 Qed.
 
 Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
@@ -554,7 +555,7 @@ congr (_ (+) _); last first.
   elim: ts => [|t ts IHts] /=; first by rewrite big_nil lift_perm1 !odd_perm1.
   rewrite big_cons odd_mul_tperm -(lift_permM _ j) odd_permM {}IHts //.
   congr (_ (+) _); transitivity (tperm (lift j t.1) (lift j t.2)); last first.
-    by rewrite odd_tperm (inj_eq (@lift_inj _ _)).
+     by rewrite odd_tperm (inj_eq (pcan_inj (liftK j))).
   congr odd_perm; apply/permP=> k; case: (unliftP j k) => [k'|] ->.
     by rewrite lift_perm_lift inj_tperm //; apply: lift_inj.
   by rewrite lift_perm_id tpermD // eq_sym neq_lift.
@@ -576,5 +577,7 @@ Qed.
 
 End LiftPerm.
 
+Prenex Implicits lift_perm lift_permK.
+