diff options
46 files changed, 481 insertions, 536 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 4c5ad4d..933bfcb 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -340,14 +340,14 @@ apply: (iffP dvdnP) => [] [q Dm]; last by exists `|q|%N; rewrite Dm abszM. exists ((-1) ^+ (m < 0)%R * q%:Z * (-1) ^+ (d < 0)%R). by rewrite -!mulrA -abszEsign -PoszM -Dm -intEsign. Qed. -Arguments dvdzP [d m]. +Arguments dvdzP {d m}. Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z. Proof. apply: (iffP dvdzP) => [[q ->] | md0]; first by rewrite modzMl. by rewrite (divz_eq m d) md0 addr0; exists (m %/ d)%Z. Qed. -Arguments dvdz_mod0P [d m]. +Arguments dvdz_mod0P {d m}. Lemma dvdz_eq d m : (d %| m)%Z = ((m %/ d)%Z * d == m). Proof. by rewrite (sameP dvdz_mod0P eqP) subr_eq0 eq_sym. Qed. diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 80f1b5d..1ca3414 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -134,7 +134,7 @@ Lemma itv_dec : forall (x : R) (i : interval R), reflect (itv_decompose i x) (x \in i). Proof. by move=> x [[[] a|] [[] b|]]; apply: (iffP andP); case. Qed. -Arguments itv_dec [x i]. +Arguments itv_dec {x i}. Definition lersif (x y : R) b := if b then x < y else x <= y. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 2a701a2..2501117 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -911,14 +911,13 @@ End VecMatrix. End MatrixStructural. -Arguments const_mx [R m n]. -Arguments row_mxA [R m n1 n2 n3 A1 A2 A3]. -Arguments col_mxA [R m1 m2 m3 n A1 A2 A3]. +Arguments const_mx {R m n}. +Arguments row_mxA {R m n1 n2 n3 A1 A2 A3}. +Arguments col_mxA {R m1 m2 m3 n A1 A2 A3}. Arguments block_mxA - [R m1 m2 m3 n1 n2 n3 A11 A12 A13 A21 A22 A23 A31 A32 A33]. -Prenex Implicits const_mx castmx trmx lsubmx rsubmx usubmx dsubmx row_mx col_mx. + {R m1 m2 m3 n1 n2 n3 A11 A12 A13 A21 A22 A23 A31 A32 A33}. +Prenex Implicits castmx trmx lsubmx rsubmx usubmx dsubmx row_mx col_mx. Prenex Implicits block_mx ulsubmx ursubmx dlsubmx drsubmx. -Prenex Implicits row_mxA col_mxA block_mxA. Prenex Implicits mxvec vec_mx mxvec_indexP mxvecK vec_mxK. Notation "A ^T" := (trmx A) : ring_scope. @@ -2042,20 +2041,18 @@ Definition adjugate n (A : 'M_n) := \matrix[adjugate_key]_(i, j) cofactor A j i. End MatrixAlgebra. -Arguments delta_mx [R m n]. -Arguments scalar_mx [R n]. -Arguments perm_mx [R n]. -Arguments tperm_mx [R n]. -Arguments pid_mx [R m n]. -Arguments copid_mx [R n]. -Arguments lin_mulmxr [R m n p]. -Prenex Implicits delta_mx diag_mx scalar_mx is_scalar_mx perm_mx tperm_mx. -Prenex Implicits pid_mx copid_mx mulmx lin_mulmxr. -Prenex Implicits mxtrace determinant cofactor adjugate. - -Arguments is_scalar_mxP [R n A]. -Arguments mul_delta_mx [R m n p]. -Prenex Implicits mul_delta_mx. +Arguments delta_mx {R m n}. +Arguments scalar_mx {R n}. +Arguments perm_mx {R n}. +Arguments tperm_mx {R n}. +Arguments pid_mx {R m n}. +Arguments copid_mx {R n}. +Arguments lin_mulmxr {R m n p}. +Prenex Implicits diag_mx is_scalar_mx. +Prenex Implicits mulmx mxtrace determinant cofactor adjugate. + +Arguments is_scalar_mxP {R n A}. +Arguments mul_delta_mx {R m n p}. Notation "a %:M" := (scalar_mx a) : ring_scope. Notation "A *m B" := (mulmx A B) : ring_scope. @@ -2500,9 +2497,8 @@ Proof. by rewrite -det_tr tr_block_mx trmx0 det_ublock !det_tr. Qed. End ComMatrix. -Arguments lin_mul_row [R m n]. -Arguments lin_mulmx [R m n p]. -Prenex Implicits lin_mul_row lin_mulmx. +Arguments lin_mul_row {R m n}. +Arguments lin_mulmx {R m n p}. Canonical matrix_finAlgType (R : finComRingType) n' := [finAlgType R of 'M[R]_n'.+1]. @@ -2667,8 +2663,7 @@ Coercion GLval ph (u : GLtype ph) : 'M[R]_n.-1.+1 := End FinUnitMatrix. Bind Scope group_scope with GLtype. -Arguments GLval _%N _ _ _%g. -Prenex Implicits GLval. +Arguments GLval {_%N _ _} _%g. Notation "{ ''GL_' n [ R ] }" := (GLtype n (Phant R)) (at level 0, n at level 2, format "{ ''GL_' n [ R ] }") : type_scope. @@ -2786,7 +2781,7 @@ Qed. End MatrixDomain. -Arguments det0P [R n A]. +Arguments det0P {R n A}. (* Parametricity at the field level (mx_is_scalar, unit and inverse are only *) (* mapped at this level). *) 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. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 7bcd7ed..fe5de6d 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -116,8 +116,8 @@ Canonical rVpoly_linear := Linear rVpoly_is_linear. End RowPoly. -Arguments poly_rV [R d]. -Prenex Implicits rVpoly poly_rV. +Arguments poly_rV {R d}. +Prenex Implicits rVpoly. Section Resultant. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 040b3a8..34174bf 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1688,11 +1688,11 @@ Notation "a ^` ()" := (deriv a) : ring_scope. Notation "a ^` ( n )" := (derivn n a) : ring_scope. Notation "a ^`N ( n )" := (nderivn n a) : ring_scope. -Arguments monicP [R p]. -Arguments rootP [R p x]. -Arguments rootPf [R p x]. -Arguments rootPt [R p x]. -Arguments unity_rootP [R n z]. +Arguments monicP {R p}. +Arguments rootP {R p x}. +Arguments rootPf {R p x}. +Arguments rootPt {R p x}. +Arguments unity_rootP {R n z}. Arguments polyOverP {R S0 addS kS p}. Canonical polynomial_countZmodType (R : countRingType) := @@ -2611,7 +2611,7 @@ Open Scope unity_root_scope. Definition unity_rootE := unity_rootE. Definition unity_rootP := @unity_rootP. -Arguments unity_rootP [R n z]. +Arguments unity_rootP {R n z}. Definition prim_order_exists := prim_order_exists. Notation prim_order_gt0 := prim_order_gt0. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 9ccb92f..854335d 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -3727,24 +3727,23 @@ End TermDef. Bind Scope term_scope with term. Bind Scope term_scope with formula. -Arguments Add _ _%T _%T. -Arguments Opp _ _%T. -Arguments NatMul _ _%T _%N. -Arguments Mul _ _%T _%T. -Arguments Inv _ _%T. -Arguments Exp _ _%T _%N. -Arguments Equal _ _%T _%T. -Arguments Unit _ _%T. -Arguments And _ _%T _%T. -Arguments Or _ _%T _%T. -Arguments Implies _ _%T _%T. -Arguments Not _ _%T. -Arguments Exists _ _%N _%T. -Arguments Forall _ _%N _%T. - -Arguments Bool [R]. -Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not. -Prenex Implicits Exists Forall. +Arguments Add {_} _%T _%T. +Arguments Opp {_} _%T. +Arguments NatMul {_} _%T _%N. +Arguments Mul {_} _%T _%T. +Arguments Inv {_} _%T. +Arguments Exp {_} _%T _%N. +Arguments Equal {_} _%T _%T. +Arguments Unit {_} _%T. +Arguments And {_} _%T _%T. +Arguments Or {_} _%T _%T. +Arguments Implies {_} _%T _%T. +Arguments Not {_} _%T. +Arguments Exists {_} _%N _%T. +Arguments Forall {_} _%N _%T. + +Arguments Bool {R}. +Arguments Const {R}. Notation True := (Bool true). Notation False := (Bool false). diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 8d4d3e7..5c6f098 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1251,11 +1251,11 @@ Definition normrE x := (normr_id, normr0, normr1, normrN1, normr_ge0, normr_eq0, End NumIntegralDomainTheory. -Arguments ler01 [R]. -Arguments ltr01 [R]. -Arguments normr_idP [R x]. -Arguments normr0P [R x]. -Arguments lerifP [R x y C]. +Arguments ler01 {R}. +Arguments ltr01 {R}. +Arguments normr_idP {R x}. +Arguments normr0P {R x}. +Arguments lerifP {R x y C}. Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0. Section NumIntegralDomainMonotonyTheory. @@ -2680,7 +2680,7 @@ Lemma real_ler_normlP x y : Proof. by move=> Rx; rewrite real_ler_norml // ler_oppl; apply: (iffP andP) => [] []. Qed. -Arguments real_ler_normlP [x y]. +Arguments real_ler_normlP {x y}. Lemma real_eqr_norml x y : x \is real -> (`|x| == y) = ((x == y) || (x == -y)) && (0 <= y). @@ -2716,7 +2716,7 @@ Proof. move=> Rx; rewrite real_ltr_norml // ltr_oppl. by apply: (iffP (@andP _ _)); case. Qed. -Arguments real_ltr_normlP [x y]. +Arguments real_ltr_normlP {x y}. Lemma real_ler_normr x y : y \is real -> (x <= `|y|) = (x <= y) || (x <= - y). Proof. @@ -3141,9 +3141,9 @@ Hint Resolve ler_opp2 ltr_opp2 real0 real1 normr_real. Arguments ler_sqr {R} [x y]. Arguments ltr_sqr {R} [x y]. Arguments signr_inj {R} [x1 x2]. -Arguments real_ler_normlP [R x y]. -Arguments real_ltr_normlP [R x y]. -Arguments lerif_refl [R x C]. +Arguments real_ler_normlP {R x y}. +Arguments real_ltr_normlP {R x y}. +Arguments lerif_refl {R x C}. Arguments mono_in_lerif [R A f C]. Arguments nmono_in_lerif [R A f C]. Arguments mono_lerif [R f C]. @@ -3631,7 +3631,7 @@ Proof. exact: real_ler_norml. Qed. Lemma ler_normlP x y : reflect ((- x <= y) * (x <= y)) (`|x| <= y). Proof. exact: real_ler_normlP. Qed. -Arguments ler_normlP [x y]. +Arguments ler_normlP {x y}. Lemma eqr_norml x y : (`|x| == y) = ((x == y) || (x == -y)) && (0 <= y). Proof. exact: real_eqr_norml. Qed. @@ -3646,7 +3646,7 @@ Definition lter_norml := (ler_norml, ltr_norml). Lemma ltr_normlP x y : reflect ((-x < y) * (x < y)) (`|x| < y). Proof. exact: real_ltr_normlP. Qed. -Arguments ltr_normlP [x y]. +Arguments ltr_normlP {x y}. Lemma ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y). Proof. by rewrite lerNgt ltr_norml negb_and -!lerNgt orbC ler_oppr. Qed. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index cda2876..aef9a9f 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1223,27 +1223,27 @@ End BigSumBasis. End VectorTheory. Hint Resolve subvv. -Arguments subvP [K vT U V]. -Arguments addv_idPl [K vT U V]. -Arguments addv_idPr [K vT U V]. -Arguments memv_addP [K vT w U V ]. +Arguments subvP {K vT U V}. +Arguments addv_idPl {K vT U V}. +Arguments addv_idPr {K vT U V}. +Arguments memv_addP {K vT w U V }. Arguments sumv_sup [K vT I] i0 [P U Vs]. -Arguments memv_sumP [K vT I P Us v]. -Arguments subv_sumP [K vT I P Us V]. -Arguments capv_idPl [K vT U V]. -Arguments capv_idPr [K vT U V]. -Arguments memv_capP [K vT w U V]. +Arguments memv_sumP {K vT I P Us v}. +Arguments subv_sumP {K vT I P Us V}. +Arguments capv_idPl {K vT U V}. +Arguments capv_idPr {K vT U V}. +Arguments memv_capP {K vT w U V}. Arguments bigcapv_inf [K vT I] i0 [P Us V]. -Arguments subv_bigcapP [K vT I P U Vs]. -Arguments directvP [K vT S]. -Arguments directv_addP [K vT U V]. -Arguments directv_add_unique [K vT U V]. -Arguments directv_sumP [K vT I P Us]. -Arguments directv_sumE [K vT I P Ss]. -Arguments directv_sum_independent [K vT I P Us]. -Arguments directv_sum_unique [K vT I P Us]. -Arguments span_subvP [K vT X U]. -Arguments freeP [K vT n X]. +Arguments subv_bigcapP {K vT I P U Vs}. +Arguments directvP {K vT S}. +Arguments directv_addP {K vT U V}. +Arguments directv_add_unique {K vT U V}. +Arguments directv_sumP {K vT I P Us}. +Arguments directv_sumE {K vT I P Ss}. +Arguments directv_sum_independent {K vT I P Us}. +Arguments directv_sum_unique {K vT I P Us}. +Arguments span_subvP {K vT X U}. +Arguments freeP {K vT n X}. Prenex Implicits coord. Notation directv S := (directv_def (Phantom _ S%VS)). @@ -1598,11 +1598,11 @@ Proof. by move/lker0_lfunK=> fK; apply/lfunP=> u; rewrite !lfunE /= fK. Qed. End LinearImage. -Arguments memv_imgP [K aT rT f w U]. -Arguments lfunPn [K aT rT f g]. -Arguments lker0P [K aT rT f]. -Arguments eqlfunP [K aT rT f g v]. -Arguments eqlfun_inP [K aT rT V f g]. +Arguments memv_imgP {K aT rT f w U}. +Arguments lfunPn {K aT rT f g}. +Arguments lker0P {K aT rT f}. +Arguments eqlfunP {K aT rT f g v}. +Arguments eqlfun_inP {K aT rT V f g}. Section FixedSpace. @@ -1632,8 +1632,8 @@ Qed. End FixedSpace. -Arguments fixedSpaceP [K vT f a]. -Arguments fixedSpacesP [K vT f U]. +Arguments fixedSpaceP {K vT f a}. +Arguments fixedSpacesP {K vT f U}. Section LinAut. diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index e522924..6752623 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -390,8 +390,8 @@ Qed. End StandardRepresentation. -Arguments grepr0 [R gT G]. -Prenex Implicits grepr0 dadd_grepr. +Arguments grepr0 {R gT G}. +Prenex Implicits dadd_grepr. Section Char. @@ -924,7 +924,7 @@ Canonical char_semiringPred := SemiringPred mul_char. End IsChar. Prenex Implicits character. -Arguments char_reprP [gT G phi]. +Arguments char_reprP {gT G phi}. Section AutChar. @@ -2554,7 +2554,7 @@ Qed. End DerivedGroup. -Arguments irr_prime_injP [gT G i]. +Arguments irr_prime_injP {gT G i}. (* Determinant characters and determinential order. *) Section DetOrder. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 7a0e538..ac3e5bc 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -557,7 +557,7 @@ rewrite big1 ?addr0 // => _ /andP[/imsetP[y Gy ->]]; apply: contraNeq. rewrite cfunE cfun_repr cfun_classE Gy mulf_eq0 => /norP[_]. by rewrite pnatr_eq0 -lt0n lt0b => /class_eqP->. Qed. -Arguments cfun_onP [A phi]. +Arguments cfun_onP {A phi}. Lemma cfun_on0 A phi x : phi \in 'CF(G, A) -> x \notin A -> phi x = 0. Proof. by move/cfun_onP; apply. Qed. @@ -759,7 +759,7 @@ End ClassFun. Arguments classfun_on _ _%g _%g. Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope. -Arguments cfun_onP [gT G A phi]. +Arguments cfun_onP {gT G A phi}. Hint Resolve cfun_onT. Section DotProduct. @@ -1009,7 +1009,7 @@ Lemma orthoPl phi S : Proof. by rewrite [orthogonal _ S]andbT /=; apply: (iffP allP) => ophiS ? /ophiS/eqP. Qed. -Arguments orthoPl [phi S]. +Arguments orthoPl {phi S}. Lemma orthogonal_sym : symmetric (@orthogonal _ G). Proof. @@ -1242,12 +1242,12 @@ Qed. End DotProduct. -Arguments orthoP [gT G phi psi]. -Arguments orthoPl [gT G phi S]. -Arguments orthoPr [gT G S psi]. -Arguments orthogonalP [gT G S R]. -Arguments pairwise_orthogonalP [gT G S]. -Arguments orthonormalP [gT G S]. +Arguments orthoP {gT G phi psi}. +Arguments orthoPl {gT G phi S}. +Arguments orthoPr {gT G S psi}. +Arguments orthogonalP {gT G S R}. +Arguments pairwise_orthogonalP {gT G S}. +Arguments orthonormalP {gT G S}. Section CfunOrder. @@ -1273,7 +1273,7 @@ Proof. by apply/eqP; rewrite -dvdn_cforder. Qed. End CfunOrder. -Arguments dvdn_cforderP [gT G phi n]. +Arguments dvdn_cforderP {gT G phi n}. Section MorphOrder. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index c8d7ab1..6859168 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -427,7 +427,7 @@ Qed. End OneRepresentation. -Arguments rkerP [gT G n rG x]. +Arguments rkerP {gT G n rG x}. Section Proper. @@ -819,8 +819,8 @@ Arguments mx_repr _ _ _%g _%N _. Arguments group_ring _ _ _%g. Arguments regular_repr _ _ _%g. -Arguments centgmxP [R gT G n rG f]. -Arguments rkerP [R gT G n rG x]. +Arguments centgmxP {R gT G n rG f}. +Arguments rkerP {R gT G n rG x}. Prenex Implicits gring_mxK. Section ChangeOfRing. @@ -933,7 +933,7 @@ by apply: (iffP subsetP) => modU x Gx; have:= modU x Gx; rewrite !inE ?Gx. Qed. End Stabilisers. -Arguments mxmoduleP [m U]. +Arguments mxmoduleP {m U}. Lemma rstabS m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) : (U <= V)%MS -> rstab rG V \subset rstab rG U. @@ -1288,7 +1288,7 @@ apply/sub_kermxP; rewrite mul_rV_lin1 /=; apply: (canLR vec_mxK). apply/row_matrixP=> j; rewrite !row_mul rowK mul_vec_lin /= mul_vec_lin_row. by rewrite -!row_mul mulmxBr !mulmxA cGf ?enum_valP // subrr !linear0. Qed. -Arguments hom_mxP [m f W]. +Arguments hom_mxP {m f W}. Lemma hom_envelop_mxC m f (W : 'M_(m, n)) A : (W <= dom_hom_mx f -> A \in E_G -> W *m A *m f = W *m f *m A)%MS. @@ -1366,7 +1366,7 @@ apply/sub_kermxP; rewrite mul_rV_lin1 /=; apply: (canLR vec_mxK). apply/row_matrixP=> i; rewrite row_mul rowK mul_vec_lin_row -row_mul. by rewrite mulmxBr mulmx1 cHW ?enum_valP // subrr !linear0. Qed. -Arguments rfix_mxP [m W]. +Arguments rfix_mxP {m W}. Lemma rfix_mx_id (H : {set gT}) x : x \in H -> rfix_mx H *m rG x = rfix_mx H. Proof. exact/rfix_mxP. Qed. @@ -1428,7 +1428,7 @@ rewrite genmxE; apply: (iffP submxP) => [[a] | [A /submxP[a defA]]] -> {v}. by rewrite vec_mxK submxMl. by exists a; rewrite mulmxA mul_rV_lin1 /= -defA mxvecK. Qed. -Arguments cyclic_mxP [u v]. +Arguments cyclic_mxP {u v}. Lemma cyclic_mx_id u : (u <= cyclic_mx u)%MS. Proof. by apply/cyclic_mxP; exists 1%:M; rewrite ?mulmx1 ?envelop_mx1. Qed. @@ -2366,21 +2366,19 @@ Qed. End OneRepresentation. -Arguments mxmoduleP [gT G n rG m U]. -Arguments envelop_mxP [gT G n rG A]. -Arguments hom_mxP [gT G n rG m f W]. -Arguments rfix_mxP [gT G n rG m W]. -Arguments cyclic_mxP [gT G n rG u v]. -Arguments annihilator_mxP [gT G n rG u A]. -Arguments row_hom_mxP [gT G n rG u v]. -Arguments mxsimple_isoP [gT G n rG U V]. -Arguments socleP [gT G n rG sG0 W W']. -Arguments mx_abs_irrP [gT G n rG]. +Arguments mxmoduleP {gT G n rG m U}. +Arguments envelop_mxP {gT G n rG A}. +Arguments hom_mxP {gT G n rG m f W}. +Arguments rfix_mxP {gT G n rG m W}. +Arguments cyclic_mxP {gT G n rG u v}. +Arguments annihilator_mxP {gT G n rG u A}. +Arguments row_hom_mxP {gT G n rG u v}. +Arguments mxsimple_isoP {gT G n rG U V}. +Arguments socleP {gT G n rG sG0 W W'}. +Arguments mx_abs_irrP {gT G n rG}. -Arguments val_submod_inj [n U m]. -Arguments val_factmod_inj [n U m]. - -Prenex Implicits val_submod_inj val_factmod_inj. +Arguments val_submod_inj {n U m}. +Arguments val_factmod_inj {n U m}. Section Proper. @@ -4659,23 +4657,22 @@ Arguments gset_mx _ _ _%g _%g. Arguments classg_base _ _ _%g _%g : extra scopes. Arguments irrType _ _ _%g _%g : extra scopes. -Arguments mxmoduleP [F gT G n rG m U]. -Arguments envelop_mxP [F gT G n rG A]. -Arguments hom_mxP [F gT G n rG m f W]. +Arguments mxmoduleP {F gT G n rG m U}. +Arguments envelop_mxP {F gT G n rG A}. +Arguments hom_mxP {F gT G n rG m f W}. Arguments mx_Maschke [F gT G n] rG _ [U]. -Arguments rfix_mxP [F gT G n rG m W]. -Arguments cyclic_mxP [F gT G n rG u v]. -Arguments annihilator_mxP [F gT G n rG u A]. -Arguments row_hom_mxP [F gT G n rG u v]. -Arguments mxsimple_isoP [F gT G n rG U V]. +Arguments rfix_mxP {F gT G n rG m W}. +Arguments cyclic_mxP {F gT G n rG u v}. +Arguments annihilator_mxP {F gT G n rG u A}. +Arguments row_hom_mxP {F gT G n rG u v}. +Arguments mxsimple_isoP {F gT G n rG U V}. Arguments socle_exists [F gT G n]. -Arguments socleP [F gT G n rG sG0 W W']. -Arguments mx_abs_irrP [F gT G n rG]. -Arguments socle_rsimP [F gT G n rG sG W1 W2]. +Arguments socleP {F gT G n rG sG0 W W'}. +Arguments mx_abs_irrP {F gT G n rG}. +Arguments socle_rsimP {F gT G n rG sG W1 W2}. -Arguments val_submod_inj [F n U m]. -Arguments val_factmod_inj [F n U m]. -Prenex Implicits val_submod_inj val_factmod_inj. +Arguments val_submod_inj {F n U m}. +Arguments val_factmod_inj {F n U m}. Notation "'Cl" := (Clifford_action _) : action_scope. diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index ada61bc..0410e55 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -641,12 +641,12 @@ Notation "[ 'aspace' 'of' U ]" := (@clone_aspace _ _ U _ _ id) Notation "[ 'aspace' 'of' U 'for' A ]" := (@clone_aspace _ _ U A _ idfun) (at level 0, format "[ 'aspace' 'of' U 'for' A ]") : form_scope. -Arguments prodvP [K aT U V W]. -Arguments cent1vP [K aT u v]. -Arguments centvP [K aT u V]. -Arguments centvsP [K aT U V]. -Arguments has_algidP [K aT U]. -Arguments polyOver1P [K aT p]. +Arguments prodvP {K aT U V W}. +Arguments cent1vP {K aT u v}. +Arguments centvP {K aT u V}. +Arguments centvsP {K aT U V}. +Arguments has_algidP {K aT U}. +Arguments polyOver1P {K aT p}. Section AspaceTheory. @@ -856,8 +856,8 @@ Notation "'C [ u ]" := (centraliser1_aspace u) : aspace_scope. Notation "'C ( V )" := (centraliser_aspace V) : aspace_scope. Notation "'Z ( A )" := (center_aspace A) : aspace_scope. -Arguments adim1P [K aT A]. -Arguments memv_cosetP [K aT U v w]. +Arguments adim1P {K aT A}. +Arguments memv_cosetP {K aT U v w}. Section Closure. @@ -1118,8 +1118,8 @@ Canonical linfun_ahom f := AHom (linfun_is_ahom f). End Class_Def. Arguments ahom_in [aT rT]. -Arguments ahom_inP [aT rT f U]. -Arguments ahomP [aT rT f]. +Arguments ahom_inP {aT rT f U}. +Arguments ahomP {aT rT f}. Section LRMorphism. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 2a905e9..881b888 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -696,7 +696,7 @@ move=> sKE; apply: minPoly_dvdp; last exact: root_minPoly. by apply: (polyOverSv sKE); rewrite minPolyOver. Qed. -Arguments Fadjoin_polyP [K x v]. +Arguments Fadjoin_polyP {K x v}. Lemma Fadjoin1_polyP x v : reflect (exists p, v = (map_poly (in_alg L) p).[x]) (v \in <<1; x>>%VS). Proof. @@ -737,13 +737,13 @@ Notation "'C_ ( E ) ( V )" := (capv_aspace E 'C(V)) Notation "E * F" := (prodv_aspace E F) : aspace_scope. Notation "f @: E" := (aimg_aspace f E) : aspace_scope. -Arguments Fadjoin_idP [F0 L K x]. -Arguments FadjoinP [F0 L K x E]. -Arguments Fadjoin_seqP [F0 L K rs E]. -Arguments polyOver_subvs [F0 L K p]. -Arguments Fadjoin_polyP [F0 L K x v]. -Arguments Fadjoin1_polyP [F0 L x v]. -Arguments minPoly_XsubC [F0 L K x]. +Arguments Fadjoin_idP {F0 L K x}. +Arguments FadjoinP {F0 L K x E}. +Arguments Fadjoin_seqP {F0 L K rs E}. +Arguments polyOver_subvs {F0 L K p}. +Arguments Fadjoin_polyP {F0 L K x v}. +Arguments Fadjoin1_polyP {F0 L x v}. +Arguments minPoly_XsubC {F0 L K x}. Section MapMinPoly. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 7e2fa17..2ed40e1 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -329,9 +329,9 @@ End kHom. Notation "f ^-1" := (inv_ahom f) : lrfun_scope. -Arguments kHomP [F L K V f]. -Arguments kAHomP [F L U V f]. -Arguments kHom_lrmorphism [F L f]. +Arguments kHomP {F L K V f}. +Arguments kAHomP {F L U V f}. +Arguments kHom_lrmorphism {F L f}. Module SplittingField. @@ -1205,7 +1205,7 @@ have [x galEx Df] := kHom_to_gal sK_Ka_E nKE homKa_f; exists x => //. by rewrite -Df ?memv_adjoin // (kHomExtend_val (kHom1 K K)) ?lfun1_poly. Qed. -Arguments normalFieldP [K E]. +Arguments normalFieldP {K E}. Lemma normalField_factors K E : (K <= E)%VS -> @@ -1637,7 +1637,7 @@ End GaloisTheory. Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope. Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope. -Arguments fixedFieldP [F L E A a]. -Arguments normalFieldP [F L K E]. -Arguments splitting_galoisField [F L K E]. -Arguments galois_fixedField [F L K E]. +Arguments fixedFieldP {F L E A a}. +Arguments normalFieldP {F L K E}. +Arguments splitting_galoisField {F L K E}. +Arguments galois_fixedField {F L K E}. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index 8185314..528b314 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -170,7 +170,7 @@ Qed. End SeparablePoly. -Arguments separable_polyP [R p]. +Arguments separable_polyP {R p}. Lemma separable_map (F : fieldType) (R : idomainType) (f : {rmorphism F -> R}) (p : {poly F}) : @@ -544,7 +544,7 @@ Qed. End SeparableElement. -Arguments separable_elementP [K x]. +Arguments separable_elementP {K x}. Lemma separable_elementS K E x : (K <= E)%VS -> separable_element K x -> separable_element E x. @@ -992,10 +992,10 @@ Qed. End Separable. -Arguments separable_elementP [F L K x]. -Arguments separablePn [F L K x]. -Arguments Derivation_separableP [F L K x]. -Arguments adjoin_separableP [F L K x]. -Arguments purely_inseparable_elementP [F L K x]. -Arguments separableP [F L K E]. -Arguments purely_inseparableP [F L K E]. +Arguments separable_elementP {F L K x}. +Arguments separablePn {F L K x}. +Arguments Derivation_separableP {F L K x}. +Arguments adjoin_separableP {F L K x}. +Arguments purely_inseparable_elementP {F L K x}. +Arguments separableP {F L K E}. +Arguments purely_inseparableP {F L K E}. diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 5c5dcdc..ffea847 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -488,10 +488,9 @@ Arguments act_inj {aT D rT} to _ [x1 x2]. Notation "to ^*" := (set_action to) : action_scope. -Arguments orbitP [aT D rT to A x y]. -Arguments afixP [aT D rT to A x]. -Arguments afix1P [aT D rT to a x]. -Prenex Implicits orbitP afixP afix1P. +Arguments orbitP {aT D rT to A x y}. +Arguments afixP {aT D rT to A x}. +Arguments afix1P {aT D rT to a x}. Arguments reindex_astabs [aT D rT] to [vT idx op S] a [F]. Arguments reindex_acts [aT D rT] to [vT idx op S A a F]. @@ -876,10 +875,9 @@ Qed. End PartialAction. Arguments orbit_transversal _ _%g _ _%act _%g _%g. -Arguments orbit_in_eqP [aT D rT to G x y]. -Arguments orbit1P [aT D rT to G x]. +Arguments orbit_in_eqP {aT D rT to G x y}. +Arguments orbit1P {aT D rT to G x}. Arguments contra_orbit [aT D rT] to G [x y]. -Prenex Implicits orbit_in_eqP orbit1P. Notation "''C' ( S | to )" := (astab_group to S) : Group_scope. Notation "''C_' A ( S | to )" := (setI_group A 'C(S | to)) : Group_scope. @@ -1005,7 +1003,7 @@ Proof. apply: (iffP idP) => [nSA x|nSA]; first exact: acts_act. by apply/subsetP=> a Aa; rewrite !inE; apply/subsetP=> x; rewrite inE nSA. Qed. -Arguments actsP [A S]. +Arguments actsP {A S}. Lemma setact_orbit A x b : to^* (orbit to A x) b = orbit to (A :^ b) (to x b). Proof. @@ -1134,14 +1132,13 @@ Qed. End TotalActions. -Arguments astabP [aT rT to S a]. -Arguments orbit_eqP [aT rT to G x y]. -Arguments astab1P [aT rT to x a]. -Arguments astabsP [aT rT to S a]. -Arguments atransP [aT rT to G S]. -Arguments actsP [aT rT to A S]. -Arguments faithfulP [aT rT to A S]. -Prenex Implicits astabP orbit_eqP astab1P astabsP atransP actsP faithfulP. +Arguments astabP {aT rT to S a}. +Arguments orbit_eqP {aT rT to G x y}. +Arguments astab1P {aT rT to x a}. +Arguments astabsP {aT rT to S a}. +Arguments atransP {aT rT to G S}. +Arguments actsP {aT rT to A S}. +Arguments faithfulP {aT rT to A S}. Section Restrict. @@ -1634,8 +1631,7 @@ Proof. by apply/permP=> x; rewrite permE. Qed. End PermAction. -Arguments perm_act1P [rT a]. -Prenex Implicits perm_act1P. +Arguments perm_act1P {rT a}. Notation "'P" := (perm_action _) (at level 8) : action_scope. diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index b1c9d94..320331c 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.v @@ -198,8 +198,8 @@ Qed. End MakeAut. -Arguments morphim_fixP [gT G f]. -Prenex Implicits aut morphim_fixP. +Arguments morphim_fixP {gT G f}. +Prenex Implicits aut. Section AutIsom. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 959eea1..1165a33 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -493,8 +493,8 @@ Qed. End PreGroupIdentities. Hint Resolve commute1. -Arguments invg_inj [T]. -Prenex Implicits commute invgK invg_inj. +Arguments invg_inj {T}. +Prenex Implicits commute invgK. Section GroupIdentities. @@ -644,9 +644,8 @@ Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))). Arguments mulgI [T]. Arguments mulIg [T]. Arguments conjg_inj [T]. -Arguments commgP [T x y]. -Arguments conjg_fixP [T x y]. -Prenex Implicits conjg_fixP commgP. +Arguments commgP {T x y}. +Arguments conjg_fixP {T x y}. Section Repr. (* Plucking a set representative. *) @@ -945,9 +944,9 @@ Proof. by apply/setP=> y; rewrite !inE inv_eq //; apply: invgK. Qed. End BaseSetMulProp. -Arguments set1gP [gT x]. -Arguments mulsgP [gT A B x]. -Arguments prodsgP [gT I P A x]. +Arguments set1gP {gT x}. +Arguments mulsgP {gT A B x}. +Arguments prodsgP {gT I P A x}. Section GroupSetMulProp. (* Constructs that need a finGroupType *) @@ -1303,13 +1302,12 @@ Definition order x := #|cycle x|. End GroupSetMulProp. -Arguments lcosetP [gT A x y]. -Arguments lcosetsP [gT A B C]. -Arguments rcosetP [gT A x y]. -Arguments rcosetsP [gT A B C]. -Arguments group_setP [gT A]. +Arguments lcosetP {gT A x y}. +Arguments lcosetsP {gT A B C}. +Arguments rcosetP {gT A x y}. +Arguments rcosetsP {gT A B C}. +Arguments group_setP {gT A}. Prenex Implicits group_set mulsgP set1gP. -Prenex Implicits lcosetP lcosetsP rcosetP rcosetsP group_setP. Arguments commutator _ _%g _%g. Arguments joing _ _%g _%g. @@ -1857,16 +1855,15 @@ Notation "[ 'subg' G ]" := [set: subg_of G]%G : Group_scope. Prenex Implicits subg sgval subg_of. Bind Scope group_scope with subg_of. -Arguments trivgP [gT G]. -Arguments trivGP [gT G]. -Arguments lcoset_eqP [gT G x y]. -Arguments rcoset_eqP [gT G x y]. +Arguments trivgP {gT G}. +Arguments trivGP {gT G}. +Arguments lcoset_eqP {gT G x y}. +Arguments rcoset_eqP {gT G x y}. Arguments mulGidPl [gT G H]. Arguments mulGidPr [gT G H]. -Arguments comm_group_setP [gT G H]. -Arguments class_eqP [gT G x y]. -Arguments repr_classesP [gT G xG]. -Prenex Implicits trivgP trivGP lcoset_eqP rcoset_eqP comm_group_setP class_eqP. +Arguments comm_group_setP {gT G H}. +Arguments class_eqP {gT G x y}. +Arguments repr_classesP {gT G xG}. Section GroupInter. @@ -2395,11 +2392,11 @@ Qed. End GeneratedGroup. -Arguments gen_prodgP [gT A x]. -Arguments joing_idPl [gT G A]. -Arguments joing_idPr [gT A G]. -Arguments mulGsubP [gT K H G]. -Arguments joing_subP [gT A B G]. +Arguments gen_prodgP {gT A x}. +Arguments joing_idPl {gT G A}. +Arguments joing_idPr {gT A G}. +Arguments mulGsubP {gT K H G}. +Arguments joing_subP {gT A B G}. Section Cycles. @@ -2523,7 +2520,7 @@ Proof. suffices ->: (x \in 'N(A)) = (A :^ x == A) by apply: eqP. by rewrite eqEcard cardJg leqnn andbT inE. Qed. -Arguments normP [x A]. +Arguments normP {x A}. Lemma group_set_normaliser A : group_set 'N(A). Proof. @@ -2538,7 +2535,7 @@ Proof. apply: (iffP subsetP) => nBA x Ax; last by rewrite inE nBA //. by apply/normP; apply: nBA. Qed. -Arguments normsP [A B]. +Arguments normsP {A B}. Lemma memJ_norm x y A : x \in 'N(A) -> (y ^ x \in A) = (y \in A). Proof. by move=> Nx; rewrite -{1}(normP Nx) memJ_conjg. Qed. @@ -2986,15 +2983,13 @@ End SubAbelian. End Normaliser. -Arguments normP [gT x A]. -Arguments centP [gT A x]. -Arguments normsP [gT A B]. -Arguments cent1P [gT x y]. -Arguments normalP [gT A B]. -Arguments centsP [gT A B]. -Arguments commG1P [gT A B]. - -Prenex Implicits normP normsP cent1P normalP centP centsP commG1P. +Arguments normP {gT x A}. +Arguments centP {gT A x}. +Arguments normsP {gT A B}. +Arguments cent1P {gT x y}. +Arguments normalP {gT A B}. +Arguments centsP {gT A B}. +Arguments commG1P {gT A B}. Arguments normaliser_group _ _%g. Arguments centraliser_group _ _%g. @@ -3090,6 +3085,5 @@ Notation "[ 'min' A 'of' G | gP & gQ ]" := [min A of G | gP && gQ] : group_scope. Notation "[ 'min' G | gP & gQ ]" := [min G | gP && gQ] : group_scope. -Arguments mingroupP [gT gP G]. -Arguments maxgroupP [gT gP G]. -Prenex Implicits mingroupP maxgroupP. +Arguments mingroupP {gT gP G}. +Arguments maxgroupP {gT gP G}. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 986489b..22c19d4 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -867,11 +867,11 @@ Qed. End InternalProd. -Arguments complP [gT H A B]. -Arguments splitsP [gT B A]. -Arguments sdprod_normal_complP [gT G K H]. -Arguments dprodYP [gT K H]. -Arguments bigdprodYP [gT I P F]. +Arguments complP {gT H A B}. +Arguments splitsP {gT B A}. +Arguments sdprod_normal_complP {gT G K H}. +Arguments dprodYP {gT K H}. +Arguments bigdprodYP {gT I P F}. Section MorphimInternalProd. @@ -1700,5 +1700,5 @@ Qed. End DirprodIsom. -Arguments mulgmP [gT H1 H2 G]. -Prenex Implicits mulgm mulgmP. +Arguments mulgmP {gT H1 H2 G}. +Prenex Implicits mulgm. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 3c23921..4b2d863 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -118,9 +118,8 @@ Notation "[ 'morphism' D 'of' f ]" := Notation "[ 'morphism' 'of' f ]" := (clone_morphism (@Morphism _ _ _ f)) (at level 0, format "[ 'morphism' 'of' f ]") : form_scope. -Arguments morphimP [aT rT D A y f]. -Arguments morphpreP [aT rT D R x f]. -Prenex Implicits morphimP morphpreP. +Arguments morphimP {aT rT D A y f}. +Arguments morphpreP {aT rT D R x f}. (* Domain, image, preimage, kernel, using phantom types to infer the domain. *) @@ -873,7 +872,7 @@ Notation "f @* G" := (morphim_group (MorPhantom f) G) : Group_scope. Notation "f @*^-1 M" := (morphpre_group (MorPhantom f) M) : Group_scope. Notation "f @: D" := (morph_dom_group f D) : Group_scope. -Arguments injmP [aT rT D f]. +Arguments injmP {aT rT D f}. Section IdentityMorphism. @@ -908,8 +907,7 @@ Proof. exact: morphim_idm. Qed. End IdentityMorphism. -Arguments idm _ _%g _%g. -Prenex Implicits idm. +Arguments idm {_} _%g _%g. Section RestrictedMorphism. @@ -967,10 +965,9 @@ Proof. by move <-; exists f. Qed. End RestrictedMorphism. -Arguments restrm _ _ _%g _%g _ _%g. -Prenex Implicits restrm. -Arguments restrmP [aT rT A D]. -Arguments domP [aT rT A D]. +Arguments restrm {_ _ _%g _%g} _ _%g. +Arguments restrmP {aT rT A D}. +Arguments domP {aT rT A D}. Section TrivMorphism. @@ -1324,17 +1321,17 @@ Proof. exact: restr_isom_to. Qed. End ReflectProp. -Arguments isom _ _ _%g _%g _. -Arguments morphic _ _ _%g _. +Arguments isom {_ _} _%g _%g _. +Arguments morphic {_ _} _%g _. Arguments misom _ _ _%g _%g _. -Arguments isog _ _ _%g _%g. +Arguments isog {_ _} _%g _%g. -Arguments morphicP [aT rT A f]. -Arguments misomP [aT rT A B f]. +Arguments morphicP {aT rT A f}. +Arguments misomP {aT rT A B f}. Arguments isom_isog [aT rT A B D]. -Arguments isomP [aT rT G H f]. -Arguments isogP [aT rT G H]. -Prenex Implicits morphic morphicP morphm isom isog isomP misomP isogP. +Arguments isomP {aT rT G H f}. +Arguments isogP {aT rT G H}. +Prenex Implicits morphm. Notation "x \isog y":= (isog x y). Section Isomorphisms. @@ -1482,7 +1479,7 @@ Arguments homg _ _ _%g _%g. Notation "G \homg H" := (homg G H) (at level 70, no associativity) : group_scope. -Arguments homgP [rT aT C D]. +Arguments homgP {rT aT C D}. (* Isomorphism between a group and its subtype. *) diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 3edcfed..01ef08e 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -461,7 +461,7 @@ Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y). Proof. by rewrite -[_ y]mulg1 odd_mul_tperm odd_perm1 addbF. Qed. Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT]. -Arguments dpair [eT]. +Arguments dpair {eT}. Lemma prod_tpermP s : {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}. @@ -503,7 +503,7 @@ Proof. by rewrite !odd_permM odd_permV addbC addbK. Qed. End PermutationParity. Coercion odd_perm : perm_type >-> bool. -Arguments dpair [eT]. +Arguments dpair {eT}. Prenex Implicits pcycle dpair pcycles aperm. Section LiftPerm. diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 03c55b3..322fc4e 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.v @@ -198,10 +198,9 @@ Lemma quotientE : quotient = coset @* Q. Proof. by []. Qed. End Cosets. -Arguments coset_of _ _%g. -Arguments coset _ _%g _%g. +Arguments coset_of {_} _%g. +Arguments coset {_} _%g _%g. Arguments quotient _ _%g _%g. -Prenex Implicits coset_of coset. Bind Scope group_scope with coset_of. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 7ca0bdb..5f1a013 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -196,7 +196,7 @@ Arguments Ohm _%N _ _%g. Arguments Ohm_group _%N _ _%g. Arguments Mho _%N _ _%g. Arguments Mho_group _%N _ _%g. -Arguments OhmPredP [n gT x]. +Arguments OhmPredP {n gT x}. Notation "''Ohm_' n ( G )" := (Ohm n G) (at level 8, n at level 2, format "''Ohm_' n ( G )") : group_scope. @@ -233,7 +233,7 @@ apply: (iffP (dvdn_biglcmP _ _ _)) => eAn x Ax. by apply/eqP; rewrite -order_dvdn eAn. by rewrite order_dvdn eAn. Qed. -Arguments exponentP [A n]. +Arguments exponentP {A n}. Lemma trivg_exponent G : (G :==: 1) = (exponent G %| 1). Proof. @@ -495,7 +495,7 @@ Qed. Lemma pElemP p A E : reflect (E \subset A /\ p.-abelem E) (E \in 'E_p(A)). Proof. by rewrite inE; apply: andP. Qed. -Arguments pElemP [p A E]. +Arguments pElemP {p A E}. Lemma pElemS p A B : A \subset B -> 'E_p(A) \subset 'E_p(B). Proof. @@ -511,7 +511,7 @@ Proof. by rewrite !inE conjSg abelemJ. Qed. Lemma pnElemP p n A E : reflect [/\ E \subset A, p.-abelem E & logn p #|E| = n] (E \in 'E_p^n(A)). Proof. by rewrite !inE -andbA; apply: (iffP and3P) => [] [-> -> /eqP]. Qed. -Arguments pnElemP [p n A E]. +Arguments pnElemP {p n A E}. Lemma pnElemPcard p n A E : E \in 'E_p^n(A) -> [/\ E \subset A, p.-abelem E & #|E| = p ^ n]%N. @@ -636,7 +636,7 @@ have:= EpnE; rewrite pnElemE ?(pnElem_prime EpnE) // !inE -andbA ltnS. case/and3P=> sEG _ oE; rewrite dvdn_leq // (dvdn_trans _ (cardSg sEG)) //. by rewrite (eqP oE) dvdn_exp. Qed. -Arguments nElemP [n G E]. +Arguments nElemP {n G E}. Lemma nElem0 G : 'E^0(G) = [set 1%G]. Proof. @@ -899,18 +899,18 @@ Qed. End ExponentAbelem. -Arguments LdivP [gT A n x]. -Arguments exponentP [gT A n]. -Arguments abelemP [gT p G]. -Arguments is_abelemP [gT G]. -Arguments pElemP [gT p A E]. -Arguments pnElemP [gT p n A E]. -Arguments nElemP [gT n G E]. -Arguments nElem1P [gT G E]. -Arguments pmaxElemP [gT p A E]. -Arguments pmaxElem_LdivP [gT p G E]. -Arguments p_rank_geP [gT p n G]. -Arguments rank_geP [gT n G]. +Arguments LdivP {gT A n x}. +Arguments exponentP {gT A n}. +Arguments abelemP {gT p G}. +Arguments is_abelemP {gT G}. +Arguments pElemP {gT p A E}. +Arguments pnElemP {gT p n A E}. +Arguments nElemP {gT n G E}. +Arguments nElem1P {gT G E}. +Arguments pmaxElemP {gT p A E}. +Arguments pmaxElem_LdivP {gT p G E}. +Arguments p_rank_geP {gT p n G}. +Arguments rank_geP {gT n G}. Section MorphAbelem. @@ -2023,9 +2023,8 @@ Qed. End AbelianStructure. -Arguments abelian_type _ _%g. -Arguments homocyclic _ _%g. -Prenex Implicits abelian_type homocyclic. +Arguments abelian_type {_} _%g. +Arguments homocyclic {_} _%g. Section IsogAbelian. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index f984960..98434ba 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -187,7 +187,7 @@ End Injm. End Center. -Arguments center_idP [gT A]. +Arguments center_idP {gT A}. Lemma isog_center (aT rT : finGroupType) (G : {group aT}) (H : {group rT}) : G \isog H -> 'Z(G) \isog 'Z(H). diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index ffb07d2..dcd53ce 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -352,7 +352,7 @@ Proof. exact: commG1P. Qed. End Commutator_properties. -Arguments derG1P [gT G]. +Arguments derG1P {gT G}. Lemma der_cont n : GFunctor.continuous (derived_at n). Proof. by move=> aT rT G f; rewrite morphim_der. Qed. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index bed8c5c..046f4a2 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -289,11 +289,11 @@ Proof. by rewrite /order => /(<[a]> =P _)->. Qed. End Cyclic. -Arguments cyclic _ _%g. -Arguments generator _ _%g _%g. -Arguments expg_invn _ _%g _%N. -Arguments cyclicP [gT A]. -Prenex Implicits cyclic Zpm generator expg_invn. +Arguments cyclic {_} _%g. +Arguments generator {_}_%g _%g. +Arguments expg_invn {_} _%g _%N. +Arguments cyclicP {gT A}. +Prenex Implicits cyclic Zpm. (* Euler's theorem *) Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n = 1 %[mod n]. @@ -556,9 +556,8 @@ Qed. End Metacyclic. -Arguments metacyclic _ _%g. -Prenex Implicits metacyclic. -Arguments metacyclicP [gT A]. +Arguments metacyclic {_} _%g. +Arguments metacyclicP {gT A}. (* Automorphisms of cyclic groups. *) Section CyclicAutomorphism. diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index 98657b4..f7edfc9 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -244,7 +244,7 @@ have Gg: g \in G by rewrite groupMl ?groupV. rewrite -conjIg (inj_eq (act_inj 'Js x)) (eq_sym A) (sameP eqP normP). by rewrite -cards_eq0 cardJg cards_eq0 setI_eq0 => /tiAG/(subsetP nAL)->. Qed. -Arguments normedTI_P [A G L]. +Arguments normedTI_P {A G L}. Lemma normedTI_memJ_P A G L : reflect [/\ A != set0, L \subset G @@ -620,9 +620,9 @@ Qed. End FrobeniusBasics. -Arguments normedTI_P [gT A G L]. -Arguments normedTI_memJ_P [gT A G L]. -Arguments Frobenius_kerP [gT G K]. +Arguments normedTI_P {gT A G L}. +Arguments normedTI_memJ_P {gT A G L}. +Arguments Frobenius_kerP {gT G K}. Lemma Frobenius_coprime_quotient (gT : finGroupType) (G K H N : {group gT}) : K ><| H = G -> N <| G -> coprime #|K| #|H| /\ H :!=: 1%g -> diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index c5b5c0c..a1830b9 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -71,17 +71,16 @@ Definition simple A := minnormal A A. Definition chief_factor A V U := maxnormal V U A && (U <| A). End GroupDefs. -Arguments subnormal _ _%g _%g. +Arguments subnormal {_} _%g _%g. Arguments invariant_factor _ _%g _%g _%g. Arguments stable_factor _ _%g _%g _%g. Arguments central_factor _ _%g _%g _%g. -Arguments maximal _ _%g _%g. +Arguments maximal {_} _%g _%g. Arguments maximal_eq _ _%g _%g. Arguments maxnormal _ _%g _%g _%g. Arguments minnormal _ _%g _%g. -Arguments simple _ _%g. +Arguments simple {_} _%g. Arguments chief_factor _ _%g _%g _%g. -Prenex Implicits subnormal maximal simple. Notation "H <|<| G" := (subnormal H G) (at level 70, no associativity) : group_scope. @@ -212,8 +211,7 @@ Qed. End Subnormal. -Arguments subnormalP [gT H G]. -Prenex Implicits subnormalP. +Arguments subnormalP {gT H G}. Section MorphSubNormal. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index c1a2eb5..5f7a9ed 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1649,4 +1649,4 @@ Qed. End SCN. -Arguments SCN_P [gT G A].
\ No newline at end of file +Arguments SCN_P {gT G A}.
\ No newline at end of file diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index 387ce34..d631919 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -75,10 +75,9 @@ Definition solvable := End PropertiesDefs. -Arguments nilpotent _ _%g. -Arguments nil_class _ _%g. -Arguments solvable _ _%g. -Prenex Implicits nil_class nilpotent solvable. +Arguments nilpotent {_} _%g. +Arguments nil_class {_} _%g. +Arguments solvable {_} _%g. Section NilpotentProps. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index 6507160..6c02e7b 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -83,16 +83,15 @@ Definition Sylow A B := p_group B && Hall A B. End PgroupDefs. -Arguments pgroup _ _%N _%g. +Arguments pgroup {_} _%N _%g. Arguments psubgroup _ _%N _%g _%g. Arguments p_group _ _%g. Arguments p_elt _ _%N. Arguments constt _ _%g _%N. -Arguments Hall _ _%g _%g. +Arguments Hall {_} _%g _%g. Arguments pHall _ _%N _%g _%g. Arguments Syl _ _%N _%g. -Arguments Sylow _ _%g _%g. -Prenex Implicits p_group Hall Sylow. +Arguments Sylow {_} _%g _%g. Notation "pi .-group" := (pgroup pi) (at level 2, format "pi .-group") : group_scope. @@ -170,7 +169,7 @@ Proof. exact: partn_eq1 (cardG_gt0 G). Qed. Lemma pgroupP pi G : reflect (forall p, prime p -> p %| #|G| -> p \in pi) (pi.-group G). Proof. exact: pnatP. Qed. -Arguments pgroupP [pi G]. +Arguments pgroupP {pi G}. Lemma pgroup1 pi : pi.-group [1 gT]. Proof. by rewrite /pgroup cards1. Qed. @@ -679,9 +678,8 @@ Qed. End PgroupProps. -Arguments pgroupP [gT pi G]. -Arguments constt1P [gT pi x]. -Prenex Implicits pgroupP constt1P. +Arguments pgroupP {gT pi G}. +Arguments constt1P {gT pi x}. Section NormalHall. @@ -1302,8 +1300,8 @@ Qed. End EqPcore. -Arguments sdprod_Hall_pcoreP [pi gT H G]. -Arguments sdprod_Hall_p'coreP [gT pi H G]. +Arguments sdprod_Hall_pcoreP {pi gT H G}. +Arguments sdprod_Hall_p'coreP {gT pi H G}. Section Injm. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index dd45afa..f940ec9 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -535,8 +535,7 @@ Qed. End Zgroups. -Arguments Zgroup _ _%g. -Prenex Implicits Zgroup. +Arguments Zgroup {_} _%g. Section NilPGroups. diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index 9e7c77f..baa7231 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -562,8 +562,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 unpickle. +Arguments unpickle {T}. +Prenex Implicits pickle. Section CountableTheory. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 6565ddf..ed1eedf 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -302,8 +302,7 @@ Proof. apply: (iffP eqP) => [md0 | [k ->]]; last by rewrite modnMl. by exists (m %/ d); rewrite {1}(divn_eq m d) md0 addn0. Qed. -Arguments dvdnP [d m]. -Prenex Implicits dvdnP. +Arguments dvdnP {d m}. Lemma dvdn0 d : d %| 0. Proof. by case: d. Qed. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 76b0521..4487ab4 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -171,7 +171,7 @@ Proof. by []. Qed. Lemma eqP T : Equality.axiom (@eq_op T). Proof. by case: T => ? []. Qed. -Arguments eqP [T x y]. +Arguments eqP {T x y}. Delimit Scope eq_scope with EQ. Open Scope eq_scope. @@ -254,8 +254,8 @@ Proof. by rewrite eq_sym; apply: ifN. Qed. End Contrapositives. -Arguments memPn [T1 A x]. -Arguments memPnC [T1 A x]. +Arguments memPn {T1 A x}. +Arguments memPnC {T1 A x}. Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2. Proof. @@ -363,10 +363,10 @@ Proof. by case: eqP; [left | right]. Qed. End EqPred. -Arguments predU1P [T x y b]. -Arguments pred2P [T T2 x y z u]. -Arguments predD1P [T x y b]. -Prenex Implicits pred1 pred2 pred3 pred4 predU1 predC1 predD1 predU1P. +Arguments predU1P {T x y b}. +Arguments pred2P {T T2 x y z u}. +Arguments predD1P {T x y b}. +Prenex Implicits pred1 pred2 pred3 pred4 predU1 predC1 predD1. Notation "[ 'predU1' x & A ]" := (predU1 x [mem A]) (at level 0, format "[ 'predU1' x & A ]") : fun_scope. @@ -597,14 +597,14 @@ Qed. End SubType. Arguments SubType [T P]. -Arguments Sub [T P s]. -Arguments vrefl [T P]. -Arguments vrefl_rect [T P]. +Arguments Sub {T P s}. +Arguments vrefl {T P}. +Arguments vrefl_rect {T P}. Arguments clone_subType [T P] U v [sT] _ [c Urec cK]. -Arguments insub [T P sT]. +Arguments insub {T P sT}. Arguments insubT [T] P [sT x]. -Arguments val_inj [T P sT]. -Prenex Implicits val Sub vrefl vrefl_rect insub insubd val_inj. +Arguments val_inj {T P sT}. +Prenex Implicits val insubd. Local Notation inlined_sub_rect := (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px). @@ -646,8 +646,7 @@ Notation "[ 'newType' 'for' v 'by' rec ]" := (NewType v _ rec vrefl) (at level 0, format "[ 'newType' 'for' v 'by' rec ]") : form_scope. Definition innew T nT x := @Sub T predT nT x (erefl true). -Arguments innew [T nT]. -Prenex Implicits innew. +Arguments innew {T nT}. Lemma innew_val T nT : cancel val (@innew T nT). Proof. by move=> u; apply: val_inj; apply: SubK. Qed. @@ -737,8 +736,7 @@ Proof. by []. Qed. End SubEqType. -Arguments val_eqP [T P sT x y]. -Prenex Implicits val_eqP. +Arguments val_eqP {T P sT x y}. Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T) (at level 0, format "[ 'eqMixin' 'of' T 'by' <: ]") : form_scope. diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 8b85320..9929e82 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -147,8 +147,8 @@ End PlainTheory. Notation family F := (family_mem (fun_of_simpl (fmem F))). Notation ffun_on R := (ffun_on_mem _ (mem R)). -Arguments familyP [aT rT pT F f]. -Arguments ffun_onP [aT rT R f]. +Arguments familyP {aT rT pT F f}. +Arguments ffun_onP {aT rT R f}. (*****************************************************************************) @@ -213,7 +213,7 @@ Qed. End EqTheory. -Arguments supportP [aT rT y D g]. +Arguments supportP {aT rT y D g}. Notation pfamily y D F := (pfamily_mem y (mem D) (fun_of_simpl (fmem F))). Notation pffun_on y D R := (pffun_on_mem y (mem D) (mem R)). diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index baf5efe..c534b7b 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -224,9 +224,9 @@ Notation closure e a := (closure_mem e (mem a)). Prenex Implicits connect root roots. -Arguments dfsP [T g x y]. -Arguments connectP [T e x y]. -Arguments rootP [T e] _ [x y]. +Arguments dfsP {T g x y}. +Arguments connectP {T e x y}. +Arguments rootP [T e] _ {x y}. Notation fconnect f := (connect (coerced_frel f)). Notation froot f := (root (coerced_frel f)). diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 6cff46e..3fd10fa 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -243,8 +243,7 @@ End BasicSetTheory. Definition inE := (in_set, inE). -Arguments set0 [T]. -Prenex Implicits set0. +Arguments set0 {T}. Hint Resolve in_setT. Notation "[ 'set' : T ]" := (setTfor (Phant T)) @@ -827,7 +826,7 @@ Proof. apply: (iffP subsetP) => [sAB | <- x /setIP[] //]. by apply/setP=> x; rewrite inE; apply/andb_idr/sAB. Qed. -Arguments setIidPl [A B]. +Arguments setIidPl {A B}. Lemma setIidPr A B : reflect (A :&: B = B) (B \subset A). Proof. by rewrite setIC; apply: setIidPl. Qed. @@ -955,29 +954,27 @@ Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed. End setOps. -Arguments set1P [T x a]. -Arguments set1_inj [T]. -Arguments set2P [T x a b]. -Arguments setIdP [T x pA pB]. -Arguments setIP [T x A B]. -Arguments setU1P [T x a B]. -Arguments setD1P [T x A b]. -Arguments setUP [T x A B]. -Arguments setDP [T A B x]. -Arguments cards1P [T A]. -Arguments setCP [T x A]. -Arguments setIidPl [T A B]. -Arguments setIidPr [T A B]. -Arguments setUidPl [T A B]. -Arguments setUidPr [T A B]. -Arguments setDidPl [T A B]. -Arguments subsetIP [T A B C]. -Arguments subUsetP [T A B C]. -Arguments subsetDP [T A B C]. -Arguments subsetD1P [T A B x]. -Prenex Implicits set1 set1_inj. -Prenex Implicits set1P set2P setU1P setD1P setIdP setIP setUP setDP. -Prenex Implicits cards1P setCP setIidPl setIidPr setUidPl setUidPr setDidPl. +Arguments set1P {T x a}. +Arguments set1_inj {T}. +Arguments set2P {T x a b}. +Arguments setIdP {T x pA pB}. +Arguments setIP {T x A B}. +Arguments setU1P {T x a B}. +Arguments setD1P {T x A b}. +Arguments setUP {T x A B}. +Arguments setDP {T A B x}. +Arguments cards1P {T A}. +Arguments setCP {T x A}. +Arguments setIidPl {T A B}. +Arguments setIidPr {T A B}. +Arguments setUidPl {T A B}. +Arguments setUidPr {T A B}. +Arguments setDidPl {T A B}. +Arguments subsetIP {T A B C}. +Arguments subUsetP {T A B C}. +Arguments subsetDP {T A B C}. +Arguments subsetD1P {T A B x}. +Prenex Implicits set1. Hint Resolve subsetT_hint. Section setOpsAlgebra. @@ -1018,8 +1015,7 @@ Proof. by rewrite cardsE cardX. Qed. End CartesianProd. -Arguments setXP [fT1 fT2 A1 A2 x1 x2]. -Prenex Implicits setXP. +Arguments setXP {fT1 fT2 A1 A2 x1 x2}. Local Notation imset_def := (fun (aT rT : finType) f mD => [set y in @image_mem aT rT f mD]). @@ -1365,9 +1361,8 @@ Proof. by move=> sAB1 sAB2; rewrite -!imset2_pair imset2S. Qed. End FunImage. -Arguments imsetP [aT rT f D y]. -Arguments imset2P [aT aT2 rT f2 D1 D2 y]. -Prenex Implicits imsetP imset2P. +Arguments imsetP {aT rT f D y}. +Arguments imset2P {aT aT2 rT f2 D1 D2 y}. Section BigOps. @@ -1499,7 +1494,7 @@ Proof. by move=> fK gK; apply: can2_in_imset_pre; apply: in1W. Qed. End CardFunImage. -Arguments imset_injP [aT rT f D]. +Arguments imset_injP {aT rT f D}. Lemma on_card_preimset (aT rT : finType) (f : aT -> rT) (R : pred rT) : {on R, bijective f} -> #|f @^-1: R| = #|R|. @@ -1703,13 +1698,12 @@ End BigSetOps. Arguments bigcup_sup [T I] j [P F]. Arguments bigcup_max [T I] j [U P F]. -Arguments bigcupP [T I x P F]. -Arguments bigcupsP [T I U P F]. +Arguments bigcupP {T I x P F}. +Arguments bigcupsP {T I U P F}. Arguments bigcap_inf [T I] j [P F]. Arguments bigcap_min [T I] j [U P F]. -Arguments bigcapP [T I x P F]. -Arguments bigcapsP [T I U P F]. -Prenex Implicits bigcupP bigcupsP bigcapP bigcapsP. +Arguments bigcapP {T I x P F}. +Arguments bigcapsP {T I U P F}. Section ImsetCurry. @@ -2088,13 +2082,13 @@ End Transversals. End Partitions. -Arguments trivIsetP [T P]. +Arguments trivIsetP {T P}. Arguments big_trivIset_cond [T R idx op] P [K E]. Arguments set_partition_big_cond [T R idx op] P [D K E]. Arguments big_trivIset [T R idx op] P [E]. Arguments set_partition_big [T R idx op] P [D E]. -Prenex Implicits cover trivIset partition pblock trivIsetP. +Prenex Implicits cover trivIset partition pblock. Lemma partition_partition (T : finType) (D : {set T}) P Q : partition P D -> partition Q P -> @@ -2141,7 +2135,7 @@ apply: (iffP forallP) => [minA | [PA minA] B]. by move=> B PB sBA; have:= minA B; rewrite PB sBA /= eqb_id => /eqP. by apply/implyP=> sBA; apply/eqP; apply/eqP/idP=> [-> // | /minA]; apply. Qed. -Arguments minsetP [P A]. +Arguments minsetP {P A}. Lemma minsetp P A : minset P A -> P A. Proof. by case/minsetP. Qed. @@ -2212,7 +2206,7 @@ Qed. End MaxSetMinSet. -Arguments minsetP [T P A]. -Arguments maxsetP [T P A]. -Prenex Implicits minset maxset minsetP maxsetP. +Arguments minsetP {T P A}. +Arguments maxsetP {T P A}. +Prenex Implicits minset maxset. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 8848999..4b2952f 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -820,14 +820,13 @@ End OpsTheory. Hint Resolve subxx_hint. -Arguments pred0P [T P]. -Arguments pred0Pn [T P]. -Arguments subsetP [T A B]. -Arguments subsetPn [T A B]. -Arguments subset_eqP [T A B]. -Arguments card_uniqP [T s]. -Arguments properP [T A B]. -Prenex Implicits pred0P pred0Pn subsetP subsetPn subset_eqP card_uniqP. +Arguments pred0P {T P}. +Arguments pred0Pn {T P}. +Arguments subsetP {T A B}. +Arguments subsetPn {T A B}. +Arguments subset_eqP {T A B}. +Arguments card_uniqP {T s}. +Arguments properP {T A B}. (**********************************************************************) (* *) @@ -927,14 +926,14 @@ Proof. by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if. Qed. End Quantifiers. -Arguments forallP [T P]. -Arguments eqfunP [T rT f1 f2]. -Arguments forall_inP [T D P]. -Arguments eqfun_inP [T rT D f1 f2]. -Arguments existsP [T P]. -Arguments exists_eqP [T rT f1 f2]. -Arguments exists_inP [T D P]. -Arguments exists_eq_inP [T rT D f1 f2]. +Arguments forallP {T P}. +Arguments eqfunP {T rT f1 f2}. +Arguments forall_inP {T D P}. +Arguments eqfun_inP {T rT D f1 f2}. +Arguments existsP {T P}. +Arguments exists_eqP {T rT f1 f2}. +Arguments exists_inP {T D P}. +Arguments exists_eq_inP {T rT D f1 f2}. Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view)) (at level 4, right associativity, format "''exists_in_' view"). @@ -1197,15 +1196,15 @@ Qed. End Image. Prenex Implicits codom iinv. -Arguments imageP [T T' f A y]. -Arguments codomP [T T' f y]. +Arguments imageP {T T' f A y}. +Arguments codomP {T T' f y}. Lemma flatten_imageP (aT : finType) (rT : eqType) A (P : pred aT) (y : rT) : reflect (exists2 x, x \in P & y \in A x) (y \in flatten [seq A x | x in P]). Proof. by apply: (iffP flatten_mapP) => [][x Px]; exists x; rewrite ?mem_enum in Px *. Qed. -Arguments flatten_imageP [aT rT A P y]. +Arguments flatten_imageP {aT rT A P y}. Section CardFunImage. @@ -1253,7 +1252,7 @@ Qed. End CardFunImage. -Arguments image_injP [T T' f A]. +Arguments image_injP {T T' f A}. Section FinCancel. diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index 16709ee..1475d55 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -198,8 +198,7 @@ Notation QuotType Q m := (@QuotType_pack _ Q m). Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id) (at level 0, format "[ 'quotType' 'of' Q ]") : form_scope. -Arguments repr [T qT]. -Prenex Implicits repr. +Arguments repr {T qT}. (************************) (* Exporting the theory *) @@ -248,8 +247,7 @@ Notation piE := (@equal_toE _ _). Canonical equal_to_pi T (qT : quotType T) (x : T) := @EqualTo _ (\pi_qT x) (\pi x) (erefl _). -Arguments EqualTo [T x equal_val]. -Prenex Implicits EqualTo. +Arguments EqualTo {T x equal_val}. Section Morphism. @@ -276,12 +274,11 @@ Lemma pi_morph11 : \pi (h a) = hq (equal_val x). Proof. by rewrite !piE. Qed. End Morphism. -Arguments pi_morph1 [T qT f fq]. -Arguments pi_morph2 [T qT g gq]. -Arguments pi_mono1 [T U qT p pq]. -Arguments pi_mono2 [T U qT r rq]. -Arguments pi_morph11 [T U qT qU h hq]. -Prenex Implicits pi_morph1 pi_morph2 pi_mono1 pi_mono2 pi_morph11. +Arguments pi_morph1 {T qT f fq}. +Arguments pi_morph2 {T qT g gq}. +Arguments pi_mono1 {T U qT p pq}. +Arguments pi_mono2 {T U qT r rq}. +Arguments pi_morph11 {T U qT qU h hq}. Notation "{pi_ Q a }" := (equal_to (\pi_Q a)) : quotient_scope. Notation "{pi a }" := (equal_to (\pi a)) : quotient_scope. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 94873a8..dd67256 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -159,8 +159,7 @@ Qed. End Paths. -Arguments pathP [T e x p]. -Prenex Implicits pathP. +Arguments pathP {T e x p}. Section EqPath. @@ -687,10 +686,10 @@ Qed. End EqTrajectory. -Arguments fpathP [T f x p]. -Arguments loopingP [T f x n]. -Arguments trajectP [T f x n y]. -Prenex Implicits traject fpathP loopingP trajectP. +Arguments fpathP {T f x p}. +Arguments loopingP {T f x n}. +Arguments trajectP {T f x n y}. +Prenex Implicits traject. Section UniqCycle. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 4bbea2a..02064c3 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -349,9 +349,8 @@ case/primeP=> _ min_p d_neq1; apply: (iffP idP) => [/min_p|-> //]. by rewrite (negPf d_neq1) /= => /eqP. Qed. -Arguments primeP [p]. -Arguments primePn [n]. -Prenex Implicits primePn primeP. +Arguments primeP {p}. +Arguments primePn {n}. Lemma prime_gt1 p : prime p -> 1 < p. Proof. by case/primeP. Qed. @@ -541,8 +540,7 @@ exists (pdiv n); rewrite pdiv_dvd pdiv_prime //; split=> //. by case: leqP npr_p => //; move/ltn_pdiv2_prime->; auto. Qed. -Arguments primePns [n]. -Prenex Implicits primePns. +Arguments primePns {n}. Lemma pdivP n : n > 1 -> {p | prime p & p %| n}. Proof. by move=> lt1n; exists (pdiv n); rewrite ?pdiv_dvd ?pdiv_prime. Qed. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 9c13df3..ba1f969 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -786,12 +786,12 @@ End Sequences. Definition rev T (s : seq T) := nosimpl (catrev s [::]). -Arguments nilP [T s]. -Arguments all_filterP [T a s]. +Arguments nilP {T s}. +Arguments all_filterP {T a s}. -Prenex Implicits size nilP head ohead behead last rcons belast. +Prenex Implicits size head ohead behead last rcons belast. Prenex Implicits cat take drop rev rot rotr. -Prenex Implicits find count nth all has filter all_filterP. +Prenex Implicits find count nth all has filter. Notation count_mem x := (count (pred_of_simpl (pred1 x))). @@ -1354,10 +1354,9 @@ Proof. by elim: s n => [|y s' IHs] [|n] /=; auto. Qed. Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x). Proof. by case: s. Qed. -Arguments nthP [T s x]. -Arguments has_nthP [T a s]. -Arguments all_nthP [T a s]. -Prenex Implicits nthP has_nthP all_nthP. +Arguments nthP {T s x}. +Arguments has_nthP {T a s}. +Arguments all_nthP {T a s}. Definition bitseq := seq bool. Canonical bitseq_eqType := Eval hnf in [eqType of bitseq]. @@ -1598,10 +1597,10 @@ End PermSeq. Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2). Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2). -Arguments perm_eqP [T s1 s2]. -Arguments perm_eqlP [T s1 s2]. -Arguments perm_eqrP [T s1 s2]. -Prenex Implicits perm_eq perm_eqP perm_eqlP perm_eqrP. +Arguments perm_eqP {T s1 s2}. +Arguments perm_eqlP {T s1 s2}. +Arguments perm_eqrP {T s1 s2}. +Prenex Implicits perm_eq. Hint Resolve perm_eq_refl. Section RotrLemmas. @@ -1875,7 +1874,7 @@ Proof. by case/subseqP=> m _ -> Us2; apply: mask_uniq. Qed. End Subseq. Prenex Implicits subseq. -Arguments subseqP [T s1 s2]. +Arguments subseqP {T s1 s2}. Hint Resolve subseq_refl. @@ -2119,8 +2118,7 @@ Proof. by apply: map_inj_in_uniq; apply: in2W. Qed. End EqMap. -Arguments mapP [T1 T2 f s y]. -Prenex Implicits mapP. +Arguments mapP {T1 T2 f s y}. Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) : {f | uniq s -> size fs = size s -> map f s = fs}. @@ -2685,7 +2683,7 @@ elim: A => /= [|s A /iffP IH_A]; [by right; case | rewrite mem_cat]. have [s_x|s'x] := @idP (x \in s); first by left; exists s; rewrite ?mem_head. by apply: IH_A => [[t] | [t /predU1P[->|]]]; exists t; rewrite // mem_behead. Qed. -Arguments flattenP [A x]. +Arguments flattenP {A x}. Lemma flatten_mapP (A : S -> seq T) s y : reflect (exists2 x, x \in s & y \in A x) (y \in flatten (map A s)). @@ -2696,8 +2694,8 @@ Qed. End EqFlatten. -Arguments flattenP [T A x]. -Arguments flatten_mapP [S T A s y]. +Arguments flattenP {T A x}. +Arguments flatten_mapP {S T A s y}. Lemma perm_undup_count (T : eqType) (s : seq T) : perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 78d50b6..b24da11 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -394,7 +394,7 @@ apply: (iffP idP); last by elim: n / => // n _ /leq_trans->. elim: n => [|n IHn]; first by case: m. by rewrite leq_eqVlt ltnS => /predU1P[<- // | /IHn]; right. Qed. -Arguments leP [m n]. +Arguments leP {m n}. Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat. Proof. @@ -411,7 +411,7 @@ Qed. Lemma ltP m n : reflect (m < n)%coq_nat (m < n). Proof. exact leP. Qed. -Arguments ltP [m n]. +Arguments ltP {m n}. Lemma lt_irrelevance m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat. Proof. exact: (@le_irrelevance m.+1). Qed. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 38e3dbe..9154eb5 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -266,8 +266,8 @@ Proof. by rewrite -existsb_tnth; apply: existsP. Qed. End TupleQuantifiers. -Arguments all_tnthP [n T a t]. -Arguments has_tnthP [n T a t]. +Arguments all_tnthP {n T a t}. +Arguments has_tnthP {n T a t}. Section EqTuple. |