From 0b1ea03dafcf36880657ba910eec28ab78ccd018 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Thu, 13 Dec 2018 12:55:43 +0100
Subject: 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.
---
 mathcomp/field/algC.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'mathcomp/field/algC.v')

diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index fc01763..ae60027 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -279,7 +279,7 @@ Canonical eqType := EqType type eqMixin.
 Definition choiceMixin : Choice.mixin_of type := EquivQuot.choiceMixin _.
 Canonical choiceType := ChoiceType type choiceMixin.
 
-Definition countMixin : Countable.mixin_of type := CanCountMixin (@reprK _ _).
+Definition countMixin : Countable.mixin_of type := CanCountMixin reprK.
 Canonical countType := CountType type countMixin.
 
 Definition CtoL (u : type) := rootQtoL (repr u).
@@ -607,7 +607,8 @@ Local Notation intrp := (map_poly intr).
 Local Notation pZtoQ := (map_poly ZtoQ).
 Local Notation pZtoC := (map_poly ZtoC).
 Local Notation pQtoC := (map_poly ratr).
-Local Hint Resolve (@intr_inj _ : injective ZtoC) : core.
+
+Local Hint Resolve (intr_inj : injective ZtoC) : core.
 
 (* Specialization of a few basic ssrnum order lemmas. *)
 
@@ -882,7 +883,7 @@ Lemma CintE x : (x \in Cint) = (x \in Cnat) || (- x \in Cnat).
 Proof.
 apply/idP/idP=> [/CintP[[n | n] ->] | ]; first by rewrite Cnat_nat.
   by rewrite NegzE opprK Cnat_nat orbT.
-by case/pred2P=> [<- | /(canLR (@opprK _)) <-]; rewrite ?rpredN rpred_nat.
+by case/pred2P=> [<- | /(canLR opprK) <-]; rewrite ?rpredN rpred_nat.
 Qed.
 
 Lemma Cnat_norm_Cint x : x \in Cint -> `|x| \in Cnat.
-- 
cgit v1.2.3