Merge Arguments and Prenex Implicits

See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114

1 files changed, 71 insertions, 77 deletions

diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index ed8e6c0..af18125 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -227,16 +227,14 @@ Fact submx_key : unit. Proof. by []. Qed.
 Definition submx := locked_with submx_key submx_def.
 Canonical submx_unlockable := [unlockable fun submx].
 
-Arguments submx _%N _%N _%N _%MS _%MS.
-Prenex Implicits submx.
+Arguments submx {_%N _%N _%N} _%MS _%MS.
 Local Notation "A <= B" := (submx A B) : matrix_set_scope.
 Local Notation "A <= B <= C" := ((A <= B) && (B <= C))%MS : matrix_set_scope.
 Local Notation "A == B" := (A <= B <= A)%MS : matrix_set_scope.
 
 Definition ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
   (A <= B)%MS && ~~ (B <= A)%MS.
-Arguments ltmx _%N _%N _%N _%MS _%MS.
-Prenex Implicits ltmx.
+Arguments ltmx {_%N _%N _%N} _%MS _%MS.
 Local Notation "A < B" := (ltmx A B) : matrix_set_scope.
 
 Definition eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :=
@@ -298,8 +296,7 @@ Definition addsmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) =>
 Fact addsmx_key : unit. Proof. by []. Qed.
 Definition addsmx := locked_with addsmx_key addsmx_def.
 Canonical addsmx_unlockable := [unlockable fun addsmx].
-Arguments addsmx _%N _%N _%N _%MS _%MS.
-Prenex Implicits addsmx.
+Arguments addsmx {_%N _%N _%N} _%MS _%MS.
 Local Notation "A + B" := (addsmx A B) : matrix_set_scope.
 Local Notation "\sum_ ( i | P ) B" := (\big[addsmx/0]_(i | P) B%MS)
   : matrix_set_scope.
@@ -344,8 +341,7 @@ Definition diffmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) =>
 Fact diffmx_key : unit. Proof. by []. Qed.
 Definition diffmx := locked_with diffmx_key diffmx_def.
 Canonical diffmx_unlockable := [unlockable fun diffmx].
-Arguments diffmx _%N _%N _%N _%MS _%MS.
-Prenex Implicits diffmx.
+Arguments diffmx {_%N _%N _%N} _%MS _%MS.
 Local Notation "A :\: B" := (diffmx A B) : matrix_set_scope.
 
 Definition proj_mx n (U V : 'M_n) : 'M_n := pinvmx (col_mx U V) *m col_mx U 0.
@@ -505,7 +501,7 @@ Proof.
 apply: (iffP idP) => [/mulmxKpV | [D ->]]; first by exists (A *m pinvmx B).
 by rewrite submxE -mulmxA mulmx_coker mulmx0.
 Qed.
-Arguments submxP [m1 m2 n A B].
+Arguments submxP {m1 m2 n A B}.
 
 Lemma submx_refl m n (A : 'M_(m, n)) : (A <= A)%MS.
 Proof. by rewrite submxE mulmx_coker. Qed.
@@ -606,7 +602,7 @@ apply: (iffP idP) => [sAB i|sAB].
 rewrite submxE; apply/eqP/row_matrixP=> i; apply/eqP.
 by rewrite row_mul row0 -submxE.
 Qed.
-Arguments row_subP [m1 m2 n A B].
+Arguments row_subP {m1 m2 n A B}.
 
 Lemma rV_subP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   reflect (forall v : 'rV_n, v <= A -> v <= B)%MS (A <= B)%MS.
@@ -614,7 +610,7 @@ Proof.
 apply: (iffP idP) => [sAB v Av | sAB]; first exact: submx_trans sAB.
 by apply/row_subP=> i; rewrite sAB ?row_sub.
 Qed.
-Arguments rV_subP [m1 m2 n A B].
+Arguments rV_subP {m1 m2 n A B}.
 
 Lemma row_subPn m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   reflect (exists i, ~~ (row i A <= B)%MS) (~~ (A <= B)%MS).
@@ -662,7 +658,7 @@ apply: (iffP idP) => [Afull | [B kA]].
   by exists (1%:M *m pinvmx A); apply: mulmxKpV (submx_full _ Afull).
 by rewrite [_ A]eqn_leq rank_leq_col (mulmx1_min_rank B 1%:M) ?mulmx1.
 Qed.
-Arguments row_fullP [m n A].
+Arguments row_fullP {m n A}.
 
 Lemma row_full_inj m n p A : row_full A -> injective (@mulmx _ m n p A).
 Proof.
@@ -733,7 +729,7 @@ split=> [|m3 C]; first by apply/eqP; rewrite eqn_leq !mxrankS.
 split; first by apply/idP/idP; apply: submx_trans.
 by apply/idP/idP=> sC; apply: submx_trans sC _.
 Qed.
-Arguments eqmxP [m1 m2 n A B].
+Arguments eqmxP {m1 m2 n A B}.
 
 Lemma rV_eqP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   reflect (forall u : 'rV_n, (u <= A) = (u <= B))%MS (A == B)%MS.
@@ -854,7 +850,7 @@ Proof.
 apply: (iffP idP) => eqAB; first exact: eq_genmx (eqmxP _).
 by rewrite -!(genmxE A) eqAB !genmxE andbb.
 Qed.
-Arguments genmxP [m1 m2 n A B].
+Arguments genmxP {m1 m2 n A B}.
 
 Lemma genmx0 m n : <<0 : 'M_(m, n)>>%MS = 0.
 Proof. by apply/eqP; rewrite -submx0 genmxE sub0mx. Qed.
@@ -1060,7 +1056,7 @@ apply: (iffP idP) => [|[u ->]]; last by rewrite addmx_sub_adds ?submxMl.
 rewrite addsmxE; case/submxP=> u ->; exists (lsubmx u, rsubmx u).
 by rewrite -mul_row_col hsubmxK.
 Qed.
-Arguments sub_addsmxP [m1 m2 m3 n A B C].
+Arguments sub_addsmxP {m1 m2 m3 n A B C}.
 
 Variable I : finType.
 Implicit Type P : pred I.
@@ -1784,7 +1780,7 @@ Notation mxdirect A := (mxdirect_def (Phantom 'M_(_,_) A%MS)).
 Lemma mxdirectP n (S : proper_mxsum_expr n) :
   reflect (\rank S = proper_mxsum_rank S) (mxdirect S).
 Proof. exact: eqnP. Qed.
-Arguments mxdirectP [n S].
+Arguments mxdirectP {n S}.
 
 Lemma mxdirect_trivial m n A : mxdirect (unwrap (@trivial_mxsum m n A)).
 Proof. exact: eqxx. Qed.
@@ -1966,49 +1962,49 @@ End Eigenspace.
 End RowSpaceTheory.
 
 Hint Resolve submx_refl.
-Arguments submxP [F m1 m2 n A B].
+Arguments submxP {F m1 m2 n A B}.
 Arguments eq_row_sub [F m n v A].
-Arguments row_subP [F m1 m2 n A B].
-Arguments rV_subP [F m1 m2 n A B].
-Arguments row_subPn [F m1 m2 n A B].
-Arguments sub_rVP [F n u v].
-Arguments rV_eqP [F m1 m2 n A B].
-Arguments rowV0Pn [F m n A].
-Arguments rowV0P [F m n A].
-Arguments eqmx0P [F m n A].
-Arguments row_fullP [F m n A].
-Arguments row_freeP [F m n A].
-Arguments eqmxP [F m1 m2 n A B].
-Arguments genmxP [F m1 m2 n A B].
-Arguments addsmx_idPr [F m1 m2 n A B].
-Arguments addsmx_idPl [F m1 m2 n A B].
-Arguments sub_addsmxP [F m1 m2 m3 n A B C].
+Arguments row_subP {F m1 m2 n A B}.
+Arguments rV_subP {F m1 m2 n A B}.
+Arguments row_subPn {F m1 m2 n A B}.
+Arguments sub_rVP {F n u v}.
+Arguments rV_eqP {F m1 m2 n A B}.
+Arguments rowV0Pn {F m n A}.
+Arguments rowV0P {F m n A}.
+Arguments eqmx0P {F m n A}.
+Arguments row_fullP {F m n A}.
+Arguments row_freeP {F m n A}.
+Arguments eqmxP {F m1 m2 n A B}.
+Arguments genmxP {F m1 m2 n A B}.
+Arguments addsmx_idPr {F m1 m2 n A B}.
+Arguments addsmx_idPl {F m1 m2 n A B}.
+Arguments sub_addsmxP {F m1 m2 m3 n A B C}.
 Arguments sumsmx_sup [F I] i0 [P m n A B_].
-Arguments sumsmx_subP [F I P m n A_ B].
-Arguments sub_sumsmxP [F I P m n A B_].
-Arguments sub_kermxP [F p m n A B].
-Arguments capmx_idPr [F n m1 m2 A B].
-Arguments capmx_idPl [F n m1 m2 A B].
+Arguments sumsmx_subP {F I P m n A_ B}.
+Arguments sub_sumsmxP {F I P m n A B_}.
+Arguments sub_kermxP {F p m n A B}.
+Arguments capmx_idPr {F n m1 m2 A B}.
+Arguments capmx_idPl {F n m1 m2 A B}.
 Arguments bigcapmx_inf [F I] i0 [P m n A_ B].
-Arguments sub_bigcapmxP [F I P m n A B_].
-Arguments mxrank_injP [F m n] p [A f].
-Arguments mxdirectP [F n S].
-Arguments mxdirect_addsP [F m1 m2 n A B].
-Arguments mxdirect_sumsP [F I P n A_].
-Arguments mxdirect_sumsE [F I P n S_].
-Arguments eigenspaceP [F n g a m W].
-Arguments eigenvalueP [F n g a].
-
-Arguments mxrank _ _%N _%N _%MS.
-Arguments complmx _ _%N _%N _%MS.
+Arguments sub_bigcapmxP {F I P m n A B_}.
+Arguments mxrank_injP {F m n} p [A f].
+Arguments mxdirectP {F n S}.
+Arguments mxdirect_addsP {F m1 m2 n A B}.
+Arguments mxdirect_sumsP {F I P n A_}.
+Arguments mxdirect_sumsE {F I P n S_}.
+Arguments eigenspaceP {F n g a m W}.
+Arguments eigenvalueP {F n g a}.
+
+Arguments mxrank {_ _%N _%N} _%MS.
+Arguments complmx {_ _%N _%N} _%MS.
 Arguments row_full _ _%N _%N _%MS.
-Arguments submx _ _%N _%N _%N _%MS _%MS.
-Arguments ltmx _ _%N _%N _%N _%MS _%MS.
-Arguments eqmx _ _%N _%N _%N _%MS _%MS.
-Arguments addsmx _ _%N _%N _%N _%MS _%MS.
-Arguments capmx _ _%N _%N _%N _%MS _%MS.
+Arguments submx {_ _%N _%N _%N} _%MS _%MS.
+Arguments ltmx {_ _%N _%N _%N} _%MS _%MS.
+Arguments eqmx {_ _%N _%N _%N} _%MS _%MS.
+Arguments addsmx {_ _%N _%N _%N} _%MS _%MS.
+Arguments capmx {_ _%N _%N _%N} _%MS _%MS.
 Arguments diffmx _ _%N _%N _%N _%MS _%MS.
-Prenex Implicits mxrank genmx complmx submx ltmx addsmx capmx.
+Prenex Implicits genmx.
 Notation "\rank A" := (mxrank A) : nat_scope.
 Notation "<< A >>" := (genmx A) : matrix_set_scope.
 Notation "A ^C" := (complmx A) : matrix_set_scope.
@@ -2229,7 +2225,7 @@ Proof.
 apply: (iffP idP) => [sR12 A R1_A | sR12]; first exact: submx_trans sR12.
 by apply/rV_subP=> vA; rewrite -(vec_mxK vA); apply: sR12.
 Qed.
-Arguments memmx_subP [m1 m2 n R1 R2].
+Arguments memmx_subP {m1 m2 n R1 R2}.
 
 Lemma memmx_eqP m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
   reflect (forall A, (A \in R1) = (A \in R2)) (R1 == R2)%MS.
@@ -2237,7 +2233,7 @@ Proof.
 apply: (iffP eqmxP) => [eqR12 A | eqR12]; first by rewrite eqR12.
 by apply/eqmxP; apply/rV_eqP=> vA; rewrite -(vec_mxK vA) eqR12.
 Qed.
-Arguments memmx_eqP [m1 m2 n R1 R2].
+Arguments memmx_eqP {m1 m2 n R1 R2}.
 
 Lemma memmx_addsP m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
   reflect (exists D, [/\ D.1 \in R1, D.2 \in R2 & A = D.1 + D.2])
@@ -2249,7 +2245,7 @@ apply: (iffP sub_addsmxP) => [[u /(canRL mxvecK)->] | [D []]].
 case/submxP=> u1 defD1 /submxP[u2 defD2] ->.
 by exists (u1, u2); rewrite linearD /= defD1 defD2.
 Qed.
-Arguments memmx_addsP [m1 m2 n A R1 R2].
+Arguments memmx_addsP {m1 m2 n A R1 R2}.
 
 Lemma memmx_sumsP (I : finType) (P : pred I) n (A : 'M_n) R_ :
   reflect (exists2 A_, A = \sum_(i | P i) A_ i & forall i, A_ i \in R_ i)
@@ -2262,7 +2258,7 @@ apply: (iffP sub_sumsmxP) => [[C defA] | [A_ -> R_A] {A}].
 exists (fun i => mxvec (A_ i) *m pinvmx (R_ i)).
 by rewrite linear_sum; apply: eq_bigr => i _; rewrite mulmxKpV.
 Qed.
-Arguments memmx_sumsP [I P n A R_].
+Arguments memmx_sumsP {I P n A R_}.
 
 Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : 
     (1%:M \in R)%MS ->
@@ -2312,7 +2308,7 @@ case/memmx_sumsP=> A_ -> R_A; rewrite linear_sum summx_sub //= => j _.
 rewrite (submx_trans (R_A _)) // genmxE; apply/row_subP=> i.
 by rewrite row_mul mul_rV_lin sR12R ?vec_mxK ?row_sub.
 Qed.
-Arguments mulsmx_subP [m1 m2 m n R1 R2 R].
+Arguments mulsmx_subP {m1 m2 m n R1 R2 R}.
 
 Lemma mulsmxS m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n))
                             (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)) :
@@ -2347,7 +2343,7 @@ exists A2_ => [i|]; first by rewrite vec_mxK -(genmxE R2) row_sub.
 apply: eq_bigr => i _; rewrite -[_ *m _](mx_rV_lin (mulmxr_linear _ _)).
 by rewrite -mulmxA mulmxKpV ?mxvecK // -(genmxE (_ *m _)) R_A.
 Qed.
-Arguments mulsmxP [m1 m2 n A R1 R2].
+Arguments mulsmxP {m1 m2 n A R1 R2}.
 
 Lemma mulsmxA m1 m2 m3 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
   (R1 * (R2 * R3) = R1 * R2 * R3)%MS.
@@ -2437,7 +2433,7 @@ congr (row_mx 0 (row_mx (mxvec _) (mxvec _))); apply/row_matrixP=> i.
   by rewrite !row_mul !mul_rV_lin1 /= mxvecK ideR vec_mxK ?row_sub.
 by rewrite !row_mul !mul_rV_lin1 /= mxvecK idRe vec_mxK ?row_sub.
 Qed.
-Arguments mxring_idP [m n R].
+Arguments mxring_idP {m n R}.
 
 Section CentMxDef.
 
@@ -2473,7 +2469,7 @@ apply: (iffP sub_kermxP); rewrite mul_vec_lin => cBE.
 apply: (canLR vec_mxK); apply/row_matrixP=> i.
 by rewrite row_mul mul_rV_lin /= cBE subrr !linear0.
 Qed.
-Arguments cent_rowP [m n B R].
+Arguments cent_rowP {m n B R}.
 
 Lemma cent_mxP m n B (R : 'A_(m, n)) :
   reflect (forall A, A \in R -> A *m B = B *m A) (B \in 'C(R))%MS.
@@ -2484,7 +2480,7 @@ apply: (iffP cent_rowP) => cEB => [A sAE | i A].
   by rewrite !linearZ -scalemxAl /= cEB.
 by rewrite cEB // vec_mxK row_sub.
 Qed.
-Arguments cent_mxP [m n B R].
+Arguments cent_mxP {m n B R}.
 
 Lemma scalar_mx_cent m n a (R : 'A_(m, n)) : (a%:M \in 'C(R))%MS.
 Proof. by apply/cent_mxP=> A _; apply: scalar_mxC. Qed.
@@ -2499,7 +2495,7 @@ Proof.
 rewrite sub_capmx; case R_A: (A \in R); last by right; case.
 by apply: (iffP cent_mxP) => [cAR | [_ cAR]].
 Qed.
-Arguments center_mxP [m n A R].
+Arguments center_mxP {m n A R}.
 
 Lemma mxring_id_uniq m n (R : 'A_(m, n)) e1 e2 :
   mxring_id R e1 -> mxring_id R e2 -> e1 = e2.
@@ -2593,7 +2589,7 @@ Qed.
 
 End MatrixAlgebra.
 
-Arguments mulsmx _ _%N _%N _%N _%MS _%MS.
+Arguments mulsmx {_ _%N _%N _%N} _%MS _%MS.
 Arguments left_mx_ideal _ _%N _%N _%N _%MS _%MS.
 Arguments right_mx_ideal _ _%N _%N _%N _%MS _%MS.
 Arguments mx_ideal _ _%N _%N _%N _%MS _%MS.
@@ -2603,8 +2599,6 @@ Arguments mxring _ _%N _%N _%MS.
 Arguments cent_mx _ _%N _%N _%MS.
 Arguments center_mx _ _%N _%N _%MS.
 
-Prenex Implicits mulsmx.
-
 Notation "A \in R" := (submx (mxvec A) R) : matrix_set_scope.
 Notation "R * S" := (mulsmx R S) : matrix_set_scope.
 Notation "''C' ( R )" := (cent_mx R) : matrix_set_scope.
@@ -2612,16 +2606,16 @@ Notation "''C_' R ( S )" := (R :&: 'C(S))%MS : matrix_set_scope.
 Notation "''C_' ( R ) ( S )" := ('C_R(S))%MS (only parsing) : matrix_set_scope.
 Notation "''Z' ( R )" := (center_mx R) : matrix_set_scope.
 
-Arguments memmx_subP [F m1 m2 n R1 R2].
-Arguments memmx_eqP [F m1 m2 n R1 R2].
-Arguments memmx_addsP [F m1 m2 n] A [R1 R2].
-Arguments memmx_sumsP [F I P n A R_].
-Arguments mulsmx_subP [F m1 m2 m n R1 R2 R].
-Arguments mulsmxP [F m1 m2 n A R1 R2].
-Arguments mxring_idP F [m n R].
-Arguments cent_rowP [F m n B R].
-Arguments cent_mxP [F m n B R].
-Arguments center_mxP [F m n A R].
+Arguments memmx_subP {F m1 m2 n R1 R2}.
+Arguments memmx_eqP {F m1 m2 n R1 R2}.
+Arguments memmx_addsP {F m1 m2 n} A [R1 R2].
+Arguments memmx_sumsP {F I P n A R_}.
+Arguments mulsmx_subP {F m1 m2 m n R1 R2 R}.
+Arguments mulsmxP {F m1 m2 n A R1 R2}.
+Arguments mxring_idP F {m n R}.
+Arguments cent_rowP {F m n B R}.
+Arguments cent_mxP {F m n B R}.
+Arguments center_mxP {F m n A R}.
 
 (* Parametricity for the row-space/F-algebra theory.                         *)
 Section MapMatrixSpaces.