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, 23 insertions, 15 deletions

diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index f679828..710adc6 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -29,7 +29,7 @@ Require Import poly polydiv.
 (*   char_poly A  == the characteristic polynomial of A.                      *)
 (* char_poly_mx A == a matrix whose determinant is char_poly A.               *)
 (*  companionmx p == a matrix whose char_poly is p                            *)
-(*   mxminpoly A  == the minimal polynomial of A, i.e., the smallest monic     *)
+(*   mxminpoly A  == the minimal polynomial of A, i.e., the smallest monic    *)
 (*                   polynomial that annihilates A (A must be nontrivial).    *)
 (* degree_mxminpoly A == the (positive) degree of mxminpoly A.                *)
 (* mx_inv_horner A == the inverse of horner_mx A for polynomials of degree    *)
@@ -116,8 +116,9 @@ Canonical rVpoly_linear := Linear rVpoly_is_linear.
 
 End RowPoly.
 
+Prenex Implicits rVpoly rVpolyK.
 Arguments poly_rV {R d}.
-Prenex Implicits rVpoly.
+Arguments poly_rV_K {R d} [p] le_p_d.
 
 Section Resultant.
 
@@ -140,6 +141,8 @@ Definition resultant := \det Sylvester_mx.
 
 End Resultant.
 
+Prenex Implicits Sylvester_mx resultant.
+
 Lemma resultant_in_ideal (R : comRingType) (p q : {poly R}) :
     size p > 1 -> size q > 1 ->
   {uv : {poly R} * {poly R} | size uv.1 < size q /\ size uv.2 < size p
@@ -224,7 +227,7 @@ apply/det0P/idP=> [[uv nz_uv] | r_nonC].
   rewrite addrC addr_eq0 => /eqP vq_up.
   have nz_v: v != 0.
     apply: contraNneq nz_uv => v0; apply/eqP.
-    congr row_mx; apply: (can_inj (@rVpolyK _ _)); rewrite linear0 // -/u.
+    congr row_mx; apply: (can_inj rVpolyK); rewrite linear0 // -/u.
     by apply: contra_eq vq_up; rewrite v0 mul0r -addr_eq0 add0r => /mulf_neq0->.
   have r_nz: r != 0 := dvdpN0 r_p p_nz.
   have /dvdpP [[c w] /= nz_c wv]: v %| m by rewrite dvdp_gcd !dvdp_mulr.
@@ -298,6 +301,8 @@ Qed.
 
 End HornerMx.
 
+Prenex Implicits horner_mx powers_mx.
+
 Section CharPoly.
 
 Variables (R : ringType) (n : nat) (A : 'M[R]_n).
@@ -330,7 +335,7 @@ apply: leq_trans (_ : #|[pred j | s j == j]|.+1 <= n.-1).
   by rewrite sub0r size_opp size_polyC leq_b1.
 rewrite -{8}[n]card_ord -(cardC (pred2 (s i) i)) card2 nfix_i !ltnS.
 apply: subset_leq_card; apply/subsetP=> j; move/(_ =P j)=> fix_j.
-rewrite !inE -{1}fix_j (inj_eq (@perm_inj _ s)) orbb.
+rewrite !inE -{1}fix_j (inj_eq perm_inj) orbb.
 by apply: contraNneq nfix_i => <-; rewrite fix_j.
 Qed.
 
@@ -373,6 +378,8 @@ Qed.
 
 End CharPoly.
 
+Prenex Implicits char_poly_mx char_poly.
+
 Lemma mx_poly_ring_isom (R : ringType) n' (n := n'.+1) :
   exists phi : {rmorphism 'M[{poly R}]_n -> {poly 'M[R]_n}},
   [/\ bijective phi,
@@ -431,13 +438,11 @@ rewrite (big_morph _ (fun p q => hornerM p q a) (hornerC 1 a)).
 by apply: eq_bigr => i _; rewrite !mxE !(hornerE, hornerMn).
 Qed.
 
-Section Companion.
-
-Definition companionmx (R : ringType) (p : seq R) (d := (size p).-1) :=
+Definition companionmx {R : ringType} (p : seq R) (d := (size p).-1) :=
   \matrix_(i < d, j < d)
     if (i == d.-1 :> nat) then - p`_j else (i.+1 == j :> nat)%:R.
 
-Lemma companionmxK (R : comRingType) (p : {poly R}) :
+Lemma companionmxK {R : comRingType} (p : {poly R}) :
    p \is monic -> char_poly (companionmx p) = p.
 Proof.
 pose D n : 'M[{poly R}]_n := \matrix_(i, j)
@@ -487,8 +492,6 @@ rewrite ltn_eqF ?big1 ?addr0 1?eq_sym //; last first.
 by move=> k /negPf ki_eqF; rewrite !mxE eqxx ki_eqF mul0r.
 Qed.
 
-End Companion.
-
 Section MinPoly.
 
 Variables (F : fieldType) (n' : nat).
@@ -601,10 +604,10 @@ Qed.
 Lemma mxminpoly_min p : horner_mx A p = 0 -> p_A %| p.
 Proof. by move=> pA0; rewrite /dvdp -horner_mxK pA0 mx_inv_horner0. Qed.
 
-Lemma horner_rVpoly_inj : @injective 'M_n 'rV_d (horner_mx A \o rVpoly).
+Lemma horner_rVpoly_inj : injective (horner_mx A \o rVpoly : 'rV_d -> 'M_n).
 Proof.
-apply: can_inj (poly_rV \o mx_inv_horner) _ => u.
-by rewrite /= horner_rVpolyK rVpolyK.
+apply: can_inj (poly_rV \o mx_inv_horner) _ => u /=.
+by rewrite horner_rVpolyK rVpolyK.
 Qed.
 
 Lemma mxminpoly_linear_is_scalar : (d <= 1) = is_scalar_mx A.
@@ -639,6 +642,11 @@ Qed.
 
 End MinPoly.
 
+Prenex Implicits degree_mxminpoly mxminpoly mx_inv_horner.
+
+Arguments mx_inv_hornerK {F n' A} [B] AnB.
+Arguments horner_rVpoly_inj {F n' A} [u1 u2] eq_u12A : rename.
+          
 (* Parametricity. *)
 Section MapRingMatrix.
 
@@ -1044,9 +1052,9 @@ Local Notation holds := GRing.holds.
 Local Notation qf_form := GRing.qf_form.
 Local Notation qf_eval := GRing.qf_eval.
 
-Definition eval_mx (e : seq F) := map_mx (eval e).
+Definition eval_mx (e : seq F) := @map_mx term F (eval e).
 
-Definition mx_term := map_mx (@GRing.Const F).
+Definition mx_term := @map_mx F term GRing.Const.
 
 Lemma eval_mx_term e m n (A : 'M_(m, n)) : eval_mx e (mx_term A) = A.
 Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.