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

diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index 6f46832..57b585e 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -141,6 +141,9 @@ Proof. by case. Qed.
 
 End OtherEncodings.
 
+Prenex Implicits seq_of_opt tag_of_pair pair_of_tag opair_of_sum sum_of_opair.
+Prenex Implicits seq_of_optK tag_of_pairK pair_of_tagK opair_of_sumK.
+
 (* Generic variable-arity tree type, providing an encoding target for         *)
 (* miscellaneous user datatypes. The GenTree.tree type can be combined with   *)
 (* a sigT type to model multi-sorted concrete datatypes.                      *)
@@ -562,8 +565,8 @@ Export Countable.Exports.
 
 Definition unpickle T := Countable.unpickle (Countable.class T).
 Definition pickle T := Countable.pickle (Countable.class T).
-Arguments unpickle {T}.
-Prenex Implicits pickle.
+Arguments unpickle {T} n.
+Arguments pickle {T} x.
 
 Section CountableTheory.
 
@@ -609,6 +612,11 @@ Notation "[ 'countMixin' 'of' T 'by' <: ]" :=
     (sub_countMixin _ : Countable.mixin_of T)
   (at level 0, format "[ 'countMixin'  'of'  T  'by'  <: ]") : form_scope.
 
+Arguments pickle_inv {T} n.
+Arguments pickleK {T} x.
+Arguments pickleK_inv {T} x.
+Arguments pickle_invK {T} n : rename.
+
 Section SubCountType.
 
 Variables (T : choiceType) (P : pred T).