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/closed_field.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index 76039d1..c338002 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -714,7 +714,7 @@ have EmulV: GRing.Field.axiom Einv.
   rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE.
   by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; apply: dvdp_mull.
 pose Efield := FieldType _ (FieldMixin EmulV Einv0).
-pose Ecount := CountType Efield (CanCountMixin (@reprK _ _)).
+pose Ecount := CountType Efield (CanCountMixin reprK).
 pose FtoE := [rmorphism of PtoE \o polyC]; pose w : E := PtoE 'X.
 have defPtoE q: (map_poly FtoE q).[w] = PtoE q.
   by rewrite map_poly_comp horner_map [_.['X]]comp_polyXr.
@@ -783,7 +783,7 @@ have eqKtrans : transitive eqKrep.
   do [rewrite -toEtrans ?le_max // -maxnA => lez2m] in lez3m *.
   by rewrite (toEtrans (maxn (tag z2) (tag z3))) // eq_z23 -toEtrans.
 pose K := {eq_quot (EquivRel _  eqKrefl eqKsym eqKtrans)}%qT.
-have cntK : Countable.mixin_of K := CanCountMixin (@reprK _ _).
+have cntK : Countable.mixin_of K := CanCountMixin reprK.
 pose EtoKrep i (x : E i) : K := \pi%qT (Tagged E x).
 have [EtoK piEtoK]: {EtoK | forall i, EtoKrep i =1 EtoK i} by exists EtoKrep.
 pose FtoK := EtoK 0%N; rewrite {}/EtoKrep in piEtoK.
-- 
cgit v1.2.3