diff options
| author | Cyril Cohen | 2020-11-19 18:33:21 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-19 21:38:46 +0100 |
| commit | e565f8d9bebd4fd681c34086d5448dbaebc11976 (patch) | |
| tree | 3e74907bf8e310b6400b7c340357ad44fc44a83f | |
| parent | 0dbefe01e54a467b7932a514355f0435b4cfb978 (diff) | |
Removing duplicate clears and turning the warning into an error
52 files changed, 115 insertions, 115 deletions
diff --git a/mathcomp/Make b/mathcomp/Make index 3cb12dd..0ef0b23 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -96,7 +96,7 @@ ssreflect/tuple.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +non-primitive-record -arg -w -arg +undeclared-scope diff --git a/mathcomp/_CoqProject b/mathcomp/_CoqProject index c2aa374..ca863b3 100644 --- a/mathcomp/_CoqProject +++ b/mathcomp/_CoqProject @@ -4,6 +4,6 @@ -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg +non-primitive-record -arg -w -arg +undeclared-scope diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make index 8d89b59..0d0629f 100644 --- a/mathcomp/algebra/Make +++ b/mathcomp/algebra/Make @@ -23,6 +23,6 @@ zmodp.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +undeclared-scope diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 336b6df..3efe76d 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -934,7 +934,7 @@ wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first. do 2!rewrite /cofactor [row' _ _]mx11_scalar !mxE det_scalar1 /=. rewrite mulr1 mul1r mulN1r opprK -[_ + _](mulzK _ nz_b) mulrDl. by rewrite -!mulrA !divzK ?dvdz_gcdl ?dvdz_gcdr // Db divzz nz_b unitr1. - have{Db} Db: M1 i 0 = b. + have{} Db: M1 i 0 = b. rewrite /M1 -(lshift0 n 1) [U]block_mxEh mul_mx_row row_mxEl. rewrite -[M](@hsubmxK _ _ 2) (@mul_row_col _ _ 2) mulmx0 addr0 !mxE /=. rewrite big_ord_recl big_ord1 !mxE /= [lshift _ _]((_ =P 0) _) // Da. @@ -943,7 +943,7 @@ wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first. exists L => //; exists (R *m invmx U); last exists d => //. by rewrite unitmx_mul uR unitmx_inv. by rewrite mulmxA -dM1 mulmxK. -move=> {A leA IHa} IHa; wlog Di: i M Da / i = 0; last rewrite {i}Di in Da. +move=> {A leA}IHa; wlog Di: i M Da / i = 0; last rewrite {i}Di in Da. case/(_ 0 (xrow i 0 M)); rewrite ?mxE ?tpermR // => L uL [R uR [d dvD dM]]. exists (xrow i 0 L); first by rewrite xrowE unitmx_mul unitmx_perm. exists R => //; exists d; rewrite //= xrowE -!mulmxA (mulmxA L) -dM xrowE. @@ -982,7 +982,7 @@ without loss{nz_a a_dvM} a1: M a Da / a = 1. by rewrite !nth_default ?size_map ?mulr0. rewrite {a}a1 -[m.+1]/(1 + m)%N -[n.+1]/(1 + n)%N in M Da *. pose Mu := ursubmx M; pose Ml := dlsubmx M. -have{Da} Da: ulsubmx M = 1 by rewrite [_ M]mx11_scalar !mxE !lshift0 Da. +have{} Da: ulsubmx M = 1 by rewrite [_ M]mx11_scalar !mxE !lshift0 Da. pose M1 := - (Ml *m Mu) + drsubmx M. have [|L uL [R uR [d dvD dM1]]] := IHmn m n M1; first by rewrite -addnS ltnW. exists (block_mx 1 0 Ml L). @@ -1023,7 +1023,7 @@ have [L _ [G uG [D _ defK]]] := int_Smith_normal_form K. pose Gud := castmx (Dm, Em) G; pose G'lr := castmx (Em, Dm) (invmx G). have{K L D defK kerK} kerGu: map_mx intr (usubmx Gud) *m S = 0. pose Kl : 'M[rat]_k:= map_mx intr (lsubmx (castmx (Ek, Dm) (K *m invmx G))). - have{defK} defK: map_mx intr K = row_mx Kl 0 *m map_mx intr Gud. + have{} defK: map_mx intr K = row_mx Kl 0 *m map_mx intr Gud. rewrite -[K](mulmxKV uG) -{2}[G](castmxK Dm Em) -/Gud. rewrite -[K *m _](castmxK Ek Dm) map_mxM map_castmx. rewrite -(hsubmxK (castmx _ _)) map_row_mx -/Kl map_castmx /Em. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 77d2e4f..9b27ba7 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1650,7 +1650,7 @@ Lemma diagmx_ind (P : forall m n, 'M_(m, n) -> Type) : forall m n A, is_diag_mx A -> P m n A. Proof. move=> P0l P0r PS m n A Adiag; have Atrig := is_diag_mx_is_trig Adiag. -elim/trigmx_ind: Atrig Adiag => // {m n} m n r c {A}A _ PA. +elim/trigmx_ind: Atrig Adiag => // {}m {}n r c {}A _ PA. rewrite is_diag_block_mx => // /and4P[_ /eqP-> _ Adiag]. exact: PS (PA _). Qed. @@ -1660,7 +1660,7 @@ Lemma diagsqmx_ind (P : forall n, 'M[V]_n -> Type) : (forall n x c A, is_diag_mx A -> P n A -> P (1 + n)%N (block_mx x 0 c A)) -> forall n A, is_diag_mx A -> P n A. Proof. -move=> P0 PS n A; elim/sqmx_ind: A => {n} [|n x r c] A PA. +move=> P0 PS n A; elim/sqmx_ind: A => [|{}n x r c] A PA. by rewrite thinmx0; apply: P0. rewrite is_diag_block_mx => // /and4P[/eqP-> /eqP-> _ Adiag]. exact: PS (PA _). diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index cc3c6c6..dde8843 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -885,7 +885,7 @@ Lemma eq_genmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :=: B -> <<A>> = <<B>>)%MS. Proof. move=> eqAB; rewrite unlock. -have{eqAB} eqAB: equivmx A (row_full A) =1 equivmx B (row_full B). +have{} eqAB: equivmx A (row_full A) =1 equivmx B (row_full B). by move=> C; rewrite /row_full /equivmx !eqAB. rewrite (eq_choose eqAB) (choose_id _ (genmx_witnessP B)) //. by rewrite -eqAB genmx_witnessP. @@ -1379,7 +1379,7 @@ Let capmx_norm_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : qidmx A = qidmx B -> (A == B)%MS -> capmx_norm A = capmx_norm B. Proof. move=> eqABid /eqmxP eqAB. -have{eqABid eqAB} eqAB: equivmx A (qidmx A) =1 equivmx B (qidmx B). +have{eqABid} eqAB: equivmx A (qidmx A) =1 equivmx B (qidmx B). by move=> C; rewrite /equivmx eqABid !eqAB. rewrite {1}/capmx_norm (eq_choose eqAB). by apply: choose_id; first rewrite -eqAB; apply: capmx_witnessP. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 19a23e6..625be60 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -175,13 +175,13 @@ have{Ss u} ->: Ss = Ss_ dS. apply/matrixP=> i j; rewrite mxE [in X in _ = X]mxE; case: (j == j0) => {j}//. apply/polyP=> k; rewrite coef_poly Sylvester_mxE mxE. have [k_ge_dS | k_lt_dS] := leqP dS k. - case: (split i) => {i}i; rewrite !mxE coefMXn; + case: (split i) => {}i; rewrite !mxE coefMXn; case: ifP => // /negbT; rewrite -ltnNge ltnS => hi. apply: (leq_sizeP _ _ (leqnn (size p))); rewrite -(ltn_predK p_nc). by rewrite ltn_subRL (leq_trans _ k_ge_dS) // ltn_add2r. - apply: (leq_sizeP _ _ (leqnn (size q))); rewrite -(ltn_predK q_nc). by rewrite ltn_subRL (leq_trans _ k_ge_dS) // addnC ltn_add2l. - by rewrite insubdK //; case: (split i) => {i}i; + by rewrite insubdK //; case: (split i) => {}i; rewrite !mxE coefMXn; case: leqP. case: (ubnPgeq dS) (dS_gt0); elim=> // dj IHj ltjS _; pose j1 := Ordinal ltjS. pose rj0T (A : 'M[{poly R}]_dS) := row j0 A^T. @@ -253,7 +253,7 @@ have le_q'_dq: size q' <= dq. by rewrite /dq -(size_scale q nz_k) q'r size_mul // addnC -def_r leq_addl. exists (row_mx (- c *: poly_rV q') (k *: poly_rV p')). apply: contraNneq r_nz; rewrite -row_mx0; case/eq_row_mx=> q0 p0. - have{p0} p0: p = 0. + have{} p0: p = 0. apply/eqP; rewrite -size_poly_eq0 -(size_scale p nz_c) p'r. rewrite -(size_scale _ nz_k) scalerAl -(poly_rV_K le_p'_dp) -linearZ p0. by rewrite linear0 mul0r size_poly0. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index e3de209..c413171 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -2510,7 +2510,7 @@ have [|q' def_q] := factor_theorem q z _; last first. by exists q'; rewrite big_cons mulrA -def_q. rewrite {p}def_p in rpz. elim/last_ind: rs drs rpz => [|rs t IHrs] /=; first by rewrite big_nil mulr1. -rewrite all_rcons => /andP[/andP[/eqP czt Uzt] /IHrs {IHrs}IHrs]. +rewrite all_rcons => /andP[/andP[/eqP czt Uzt] /IHrs{}IHrs]. rewrite -cats1 big_cat big_seq1 /= mulrA rootE hornerM_comm; last first. by rewrite /comm_poly hornerXsubC mulrBl mulrBr czt. rewrite hornerXsubC -opprB mulrN oppr_eq0 -(mul0r (t - z)). diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 7945265..3db328d 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -294,7 +294,7 @@ Proof. by move=> x y /=; rewrite !ratz_frac mulq_frac // /= !mulr1. Qed. Fact invq_frac x : x.1 != 0 -> x.2 != 0 -> invq (fracq x) = fracq (invq_subdef x). Proof. -by rewrite /invq_subdef; case: fracqP => // k {x} x k0; rewrite fracqMM. +by rewrite /invq_subdef; case: fracqP => // k {}x k0; rewrite fracqMM. Qed. Fact mulqC : commutative mulq. @@ -357,7 +357,7 @@ Canonical rat_countFieldType := [countFieldType of rat]. Lemma numq_eq0 x : (numq x == 0) = (x == 0). Proof. -rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {x} x k0]. +rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {}x k0]. by rewrite eqxx orbT. by rewrite !mulf_eq0 (negPf k0) /= denq_eq0 orbF. Qed. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 455a79e..fa952bb 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -4233,22 +4233,22 @@ Proof. suffices eq0_ring t1: rformula (eq0_rform t1) by elim: f => //= => f1 ->. rewrite /eq0_rform; move: (ub_var t1) => m; set tr := _ m. suffices: all rterm (tr.1 :: tr.2). - case: tr => {t1} t1 r /= /andP[t1_r]. + case: tr => {}t1 r /= /andP[t1_r]. by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr. have: all rterm [::] by []. rewrite {}/tr; elim: t1 [::] => //=. - move=> t1 IHt1 t2 IHt2 r. - move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r]. - move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r]. + move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. + move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. - by move=> t1 IHt1 r /IHt1; case: to_rterm. - by move=> t1 IHt1 n r /IHt1; case: to_rterm. - move=> t1 IHt1 t2 IHt2 r. - move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r]. - move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r]. + move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. + move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. - move=> t1 IHt1 r. - by move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /=; rewrite all_rcons. + by move/IHt1; case: to_rterm => {r IHt1}t1 r /=; rewrite all_rcons. - by move=> t1 IHt1 n r /IHt1; case: to_rterm. Qed. @@ -4317,7 +4317,7 @@ elim: t r0 m => /=; try do [ by move=> n r m hlt hub; rewrite take_size (ltn_addr _ hlt) rsub_id | by move=> n r m hlt hub; rewrite leq0n take_size rsub_id | move=> t1 IHt1 t2 IHt2 r m; rewrite geq_max; case/andP=> hub1 hub2 hmr; - case: to_rterm {IHt1 hub1 hmr}(IHt1 r m hub1 hmr) => t1' r1; + case: to_rterm {hub1 hmr}(IHt1 r m hub1 hmr) => t1' r1; case=> htake1 hub1' hsub1 <-; case: to_rterm {IHt2 hub2 hsub1}(IHt2 r1 m hub2 hsub1) => t2' r2 /=; rewrite geq_max; case=> htake2 -> hsub2 /= <-; @@ -4327,8 +4327,8 @@ elim: t r0 m => /=; try do [ first by [rewrite takel_cat // -htake1 size_take geq_min leqnn orbT]; rewrite -(rsub_acc r1 r3 t1') {hub1'}// -{htake1}htake2 {r3}cat_take_drop; by elim: r2 m => //= u r2 IHr2 m; rewrite IHr2 -| do [ move=> t1 IHt1 r m; do 2!move/IHt1=> {IHt1}IHt1 - | move=> t1 IHt1 n r m; do 2!move/IHt1=> {IHt1}IHt1]; +| do [ move=> t1 IHt1 r m; do 2!move=> /IHt1{}IHt1 + | move=> t1 IHt1 n r m; do 2!move=> /IHt1{}IHt1]; case: to_rterm IHt1 => t1' r1 [-> -> hsub1 <-]; split=> {hsub1}//; by elim: r1 m => //= u r1 IHr1 m; rewrite IHr1]. move=> t1 IH r m letm /IH {IH} /(_ letm) {letm}. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index aa899b2..e234504 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -410,7 +410,7 @@ Proof. by case: m; first case. Qed. Lemma subz_ge0 m n : lez 0 (n - m) = lez m n. Proof. -case: (intP m); case: (intP n)=> // {m n} m n /=; +case: (intP m); case: (intP n)=> // {}m {}n /=; rewrite ?ltnS -?opprD ?opprB ?subzSS; case: leqP=> // hmn; by [ rewrite subzn // | rewrite -opprB subzn ?(ltnW hmn) //; diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 7da7ebc..4bb7a5a 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3468,7 +3468,7 @@ pose cmp_mu s := [pred i | s * mu < s * En i]. have{Enonconstant} has_cmp_mu e (s := (-1) ^+ e): {i | i \in A & cmp_mu s i}. apply/sig2W/exists_inP; apply: contraR Enonconstant => /exists_inPn-mu_s_A. have n_gt0 i: i \in A -> (0 < n)%N by rewrite [n](cardD1 i) => ->. - have{mu_s_A} mu_s_A i: i \in A -> s * En i <= s * mu. + have{} mu_s_A i: i \in A -> s * En i <= s * mu. move=> Ai; rewrite real_leNgt ?mu_s_A ?rpredMsign ?ger0_real ?Ege0 //. by rewrite -(pmulrn_lge0 _ (n_gt0 i Ai)) -sumrMnl sumr_ge0. have [_ /esym/eqfun_inP] := leif_sum (fun i Ai => leif_eq (mu_s_A i Ai)). @@ -4305,7 +4305,7 @@ Qed. Lemma sqrtrM a b : 0 <= a -> sqrt (a * b) = sqrt a * sqrt b. Proof. -case: (sqrtrP a) => // {a} a a_ge0 _; case: (sqrtrP b) => [b_lt0 | {b} b b_ge0]. +case: (sqrtrP a) => // {}a a_ge0 _; case: (sqrtrP b) => [b_lt0 | {}b b_ge0]. by rewrite mulr0 ler0_sqrtr // nmulr_lle0 ?mulr_ge0. by rewrite mulrACA sqrtr_sqr ger0_norm ?mulr_ge0. Qed. @@ -4415,7 +4415,7 @@ have sz_p: size p = n.+1. rewrite size_addl ?size_polyXn // ltnS size_opp size_polyC mulrn_eq0. by case: posnP => //; case: negP. pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted. -have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P). +have{} Dp: p = \prod_(z <- r) ('X - z%:P). rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb. by rewrite subr0 eqxx scale1r; apply/esym/perm_big; rewrite perm_sort. have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r). diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index e02aaef..76bec6f 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1101,7 +1101,7 @@ Lemma free_span X v (sumX := fun k => \sum_(x <- X) k x *: x) : Proof. rewrite -{2}[X]in_tupleE => freeX /coord_span def_v. pose k x := oapp (fun i => coord (in_tuple X) i v) 0 (insub (index x X)). -exists k => [|k1 {def_v}def_v _ /(nthP 0)[i ltiX <-]]. +exists k => [|k1 {}def_v _ /(nthP 0)[i ltiX <-]]. rewrite /sumX (big_nth 0) big_mkord def_v; apply: eq_bigr => i _. by rewrite /k index_uniq ?free_uniq // valK. rewrite /k /= index_uniq ?free_uniq // insubT //= def_v. @@ -1627,7 +1627,7 @@ Proof. by apply: (iffP subvP) => cUf x /cUf/fixedSpaceP. Qed. Lemma fixedSpace_limg f U : (U <= fixedSpace f -> f @: U = U)%VS. Proof. move/fixedSpacesP=> cUf; apply/vspaceP=> x. -by apply/memv_imgP/idP=> [[{x} x Ux ->] | Ux]; last exists x; rewrite ?cUf. +by apply/memv_imgP/idP=> [[{}x Ux ->] | Ux]; last exists x; rewrite ?cUf. Qed. Lemma fixedSpace_id : fixedSpace \1 = {:vT}%VS. @@ -1862,7 +1862,7 @@ Lemma sumv_pi_uniq_sum v : \sum_(i <- r0 | P i) sumv_pi_for defV i v = v. Proof. rewrite /sumv_pi_for defV -!(big_filter r0 P). -elim: (filter P r0) v => [|i r IHr] v /= => [_ | /andP[r'i /IHr{IHr}IHr]]. +elim: (filter P r0) v => [|i r IHr] v /= => [_ | /andP[r'i /IHr{}IHr]]. by rewrite !big_nil memv0 => /eqP. rewrite !big_cons eqxx => /addv_pi1_pi2; congr (_ + _ = v). rewrite -[_ v]IHr ?memv_pi2 //; apply: eq_big_seq => j /=. diff --git a/mathcomp/character/Make b/mathcomp/character/Make index 43790cd..b750b49 100644 --- a/mathcomp/character/Make +++ b/mathcomp/character/Make @@ -12,6 +12,6 @@ vcharacter.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +undeclared-scope diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index e7ea1e0..58a3688 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -1490,7 +1490,7 @@ Proof. move=> Gx; have [e [[B uB def_x] [_ e1] [-> _] _]] := repr_rsim_diag rG Gx. rewrite cfRepr1 -[n in n%:R]card_ord -sumr_const -(eq_bigr _ (in1W e1)). case/normC_sum_eq1=> [i _ | c /eqP norm_c_1 def_e]; first by rewrite e1. -have{def_e} def_e: e = const_mx c by apply/rowP=> i; rewrite mxE def_e ?andbT. +have{} def_e: e = const_mx c by apply/rowP=> i; rewrite mxE def_e ?andbT. by exists c => //; rewrite def_x def_e diag_const_mx scalar_mxC mulmxKV. Qed. @@ -1619,7 +1619,7 @@ apply: andb_id2l => Gx; rewrite {1 2}[chi]cfun_sum_constt !sum_cfunE. apply/eqP/bigcapP=> [Kx i Ci | Kx]; last first. by apply: eq_bigr => i /Kx Kx_i; rewrite !cfunE cfker1. rewrite cfkerEirr inE /= -(inj_eq (mulfI Ci)). -have:= (normC_sum_upper _ Kx) i; rewrite !cfunE => -> // {i Ci} i _. +have:= (normC_sum_upper _ Kx) i; rewrite !cfunE => -> // {Ci}i _. have chi_i_ge0: 0 <= '[chi, 'chi_i]. by rewrite Cnat_ge0 ?Cnat_cfdot_char_irr. by rewrite !cfunE normrM (normr_idP _) ?ler_wpmul2l ?char1_ge_norm ?irr_char. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index ccfc37b..2bea267 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -1093,7 +1093,7 @@ Lemma pairwise_orthogonalP S : Proof. rewrite /pairwise_orthogonal /=; case notS0: (~~ _); last by right; case. elim: S notS0 => [|phi S IH] /=; first by left. -rewrite inE eq_sym andbT => /norP[nz_phi /IH{IH}IH]. +rewrite inE eq_sym andbT => /norP[nz_phi /IH{}IH]. have [opS | not_opS] := allP; last first. right=> [[/andP[notSp _] opS]]; case: not_opS => psi Spsi /=. by rewrite opS ?mem_head 1?mem_behead // (memPnC notSp). @@ -1306,7 +1306,7 @@ Lemma isometry_of_free S f : Proof. move=> freeS If; have defS := free_span freeS. have [tau /(_ freeS (size_map f S))Dtau] := linear_of_free S (map f S). -have{Dtau} Dtau: {in S, tau =1 f}. +have{} Dtau: {in S, tau =1 f}. by move=> _ /(nthP 0)[i ltiS <-]; rewrite -!(nth_map 0 0) ?Dtau. exists tau => // _ _ /defS[a -> _] /defS[b -> _]. rewrite !{1}linear_sum !{1}cfdot_suml; apply/eq_big_seq=> xi1 Sxi1. @@ -2229,7 +2229,7 @@ rewrite (set_partition_big _ (rcosets_partition_mul H K)) ?big_imset /=. apply: eq_bigr => y Hy; rewrite rcosetE norm_rlcoset ?(subsetP nKH) //. rewrite -lcosetE mulr_natl big_imset /=; last exact: in2W (mulgI _). by rewrite -sumr_const; apply: eq_bigr => z Kz; rewrite conjgM cfunJ. -have [{nKH}nKH /isomP[injf _]] := sdprod_isom defG. +have [{}nKH /isomP[injf _]] := sdprod_isom defG. apply: can_in_inj (fun Ky => invm injf (coset K (repr Ky))) _ => y Hy. by rewrite rcosetE -val_coset ?(subsetP nKH) // coset_reprK invmE. Qed. @@ -2410,7 +2410,7 @@ Lemma map_cfAut_free S : cfAut_closed u S -> free S -> free (map (cfAut u) S). Proof. set Su := map _ S => sSuS freeS; have uniqS := free_uniq freeS. have uniqSu: uniq Su by rewrite (map_inj_uniq cfAut_inj). -have{sSuS} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS. +have{} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS. have [|_ eqSuS] := uniq_min_size uniqSu sSuS; first by rewrite size_map. by rewrite (perm_free (uniq_perm uniqSu uniqS eqSuS)). Qed. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index 29d7162..e7f80dc 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -1140,7 +1140,7 @@ have [defKT | ltKT_K] := eqVneq (K :&: T) K; last first. by have /cfclassP[y _ ->] := mem_tnth i phiKt; rewrite cfConjg_irr ?mem_irr. constructor 3; exists p => [i j /(congr1 (tnth (irr L)))/eqP| ]. by apply: contraTeq; rewrite !pK !nth_uniq ?t_cast ?cfclass_uniq. - have{DthL} DthL: 'Res theta = e%:R *: \sum_(i < t) (phi ^: K)%CF`_i. + have{} DthL: 'Res theta = e%:R *: \sum_(i < t) (phi ^: K)%CF`_i. by rewrite DthL (big_nth 0) big_mkord t_cast. suffices /eqP e1: e == 1%N by rewrite DthL e1 scale1r; apply: eq_bigr. have Dth1: theta 1%g = e%:R * t%:R * phi 1%g. @@ -1153,7 +1153,7 @@ have [defKT | ltKT_K] := eqVneq (K :&: T) K; last first. rewrite mul1r -Dth1 -cfInd1 //. by rewrite char1_ge_constt ?cfInd_char ?irr_char ?constt_Ind_Res. have IKphi: 'I_K[phi] = K by rewrite -{1}(setIidPl sKG) -setIA. -have{DthL} DthL: 'Res[L] theta = e%:R *: phi. +have{} DthL: 'Res[L] theta = e%:R *: phi. by rewrite DthL -[rhs in (_ ^: rhs)%CF]IKphi cfclass_inertia big_seq1. pose mmLth := @mul_mod_Iirr K L s. have linKbar := char_abelianP _ abKbar. @@ -1295,7 +1295,7 @@ exists c => // c2 c2Nth det_c2_mu; apply: irr_inj. have [irrMc _ imMc _] := constt_Ind_ext nsNG chiN. have /codomP[s2 Dc2]: c2 \in codom (@mul_mod_Iirr G N c). by rewrite -imMc constt_Ind_Res c2Nth constt_irr ?inE. -have{Dc2} Dc2: 'chi_c2 = ('chi_s2 %% N)%CF * 'chi_c. +have{} Dc2: 'chi_c2 = ('chi_s2 %% N)%CF * 'chi_c. by rewrite Dc2 cfIirrE // mod_IirrE. have s2_lin: 'chi_s2 \is a linear_char. rewrite qualifE irr_char; apply/eqP/(mulIf (irr1_neq0 c)). diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index c82202b..8911134 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -376,7 +376,7 @@ rewrite ltnS => leGn piGle2; have [simpleG | ] := boolP (simple G); last first. rewrite groupP /= genGid normG andbT eqb_id negbK => /eqP->. exact: solvable1. rewrite [N == G]eqEproper sNG eqbF_neg !negbK => ltNG /and3P[grN]. - case/isgroupP: grN => {N}N -> in sNG ltNG *; rewrite /= genGid => ntN nNG. + case/isgroupP: grN => {}N -> in sNG ltNG *; rewrite /= genGid => ntN nNG. have nsNG: N <| G by apply/andP. have dv_le_pi m: (m %| #|G| -> size (primes m) <= 2)%N. move=> m_dv_G; apply: leq_trans piGle2. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 8575d58..2a9eb19 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -955,7 +955,7 @@ have rphi_fful i: mx_faithful (rphi i). have rphi_z i: rphi i z = (w ^+ i.+1)%:M. by rewrite /rphi [phi]lock /= /morphim_mx autmE alpha_i_z -lock phi_ze. pose iphi i := irr_comp sS (rphi i); pose phi_ i := irr_repr (iphi i). -have{phi_ze} phi_ze i e: phi_ i (z ^+ e)%g = (w ^+ (e * i.+1)%N)%:M. +have{} phi_ze i e: phi_ i (z ^+ e)%g = (w ^+ (e * i.+1)%N)%:M. rewrite /phi_ !{1}irr_center_scalar ?groupX ?irr_modeX //. suffices ->: irr_mode (iphi i) z = w ^+ i.+1 by rewrite mulnC exprM. have:= mx_rsim_sym (rsim_irr_comp sS F'S (rphi_irr i)). diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 6885ec7..ea93ab2 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -3114,7 +3114,7 @@ Proof. move=> addUV dxUV. have eqUV: \rank U = \rank (cokermx V). by rewrite mxrank_coker -{3}(mxrank1 F n) -addUV (mxdirectP dxUV) addnK. -have{dxUV} dxUV: (U :&: V = 0)%MS by apply/mxdirect_addsP. +have{} dxUV: (U :&: V = 0)%MS by apply/mxdirect_addsP. exists (in_submod U (val_factmod 1%:M *m proj_mx U V)) => // [|x Gx]. rewrite /row_free -{6}eqUV -[_ == _]sub1mx -val_submodS val_submod1. rewrite in_submodK ?proj_mx_sub // -{1}[U](proj_mx_id dxUV) //. @@ -3407,7 +3407,7 @@ Proof. rewrite -{9}(mxrank1 F n) -Clifford_Socle1. rewrite (mxdirectP (Socle_direct sH)) /= -sum_nat_const. apply: eq_bigr => W1 _; have [W0 _ W0G] := imsetP Clifford_atrans. -have{W0G} W0G W': W' \in orbit 'Cl G W0 by rewrite -W0G inE. +have{} W0G W': W' \in orbit 'Cl G W0 by rewrite -W0G inE. have [/orbitP[x Gx <-] /orbitP[y Gy <-]] := (W0G W, W0G W1). by rewrite !{1}val_Clifford_act // !mxrankMfree // !repr_mx_free. Qed. @@ -4299,7 +4299,7 @@ have simM: mxsimple aG M. rewrite (eqmx_module _ (genmxE _)); apply/mxmoduleP=> x Gx. by rewrite -mulmxA -homf // mulmxA submxMr // (mxmoduleP modU). pose i := PackSocle (component_socle sG simM). -have{modM rsimM} rsimM: mx_rsim rG (socle_repr i). +have{modM} rsimM: mx_rsim rG (socle_repr i). apply: mx_rsim_trans rsimM (mx_rsim_sym _); apply/mx_rsim_iso. apply: (component_mx_iso (socle_simple _)) => //. by rewrite [component_mx _ _]PackSocleK component_mx_id. @@ -4812,7 +4812,7 @@ Lemma dec_mx_reducible_semisimple U : Proof. have [m] := ubnP (\rank U); elim: m U => // m IHm U leUm modU redU. have [U0 | nzU] := eqVneq U 0. - have{U0} U0: (\sum_(i < 0) 0 :=: U)%MS by rewrite big_ord0 U0. + have{} U0: (\sum_(i < 0) 0 :=: U)%MS by rewrite big_ord0 U0. by apply: (intro_mxsemisimple U0); case. have [V simV sVU] := dec_mxsimple_exists modU nzU; have [modV nzV _] := simV. have [W modW defVW dxVW] := redU V modV sVU. @@ -5035,7 +5035,7 @@ have compUf: mx_composition_series (regular_repr rF G) Uf. rewrite -{2}(map_mx0 f) -map_cons !(nth_map 0) ?leqW //. by rewrite map_submx // ltmxW // (pathP _ (mx_series_lt compU)). have [[i ltiU] simUi] := rsim_regular_series irrG compUf lastUf. -have{simUi} simUi: mx_rsim rG (subseries_repr i modUf). +have{} simUi: mx_rsim rG (subseries_repr i modUf). by apply: mx_rsim_trans simUi _; apply: section_eqmx. by rewrite (mx_rsim_abs_irr simUi) absUf; rewrite size_map in ltiU. Qed. @@ -5693,7 +5693,7 @@ elim: t => //=. - move=> t1 IH1 n1 rt1; rewrite eval_mulmx eval_mx_term mul_scalar_mx. by rewrite scaler_nat {}IH1 //; elim: n1 => //= n1 IHn1; rewrite !mulrS IHn1. - by move=> t1 IH1 t2 IH2 /andP[rt1 rt2]; rewrite eval_mulT IH1 ?IH2. -move=> t1 IH1 n1 /IH1 {IH1}IH1. +move=> t1 + n1 => /[apply] IH1. elim: n1 => [|n1 IHn1] /=; first by rewrite eval_mx_term. by rewrite eval_mulT exprS IH1 IHn1. Qed. diff --git a/mathcomp/field/Make b/mathcomp/field/Make index c906bd9..93795e9 100644 --- a/mathcomp/field/Make +++ b/mathcomp/field/Make @@ -15,6 +15,6 @@ separable.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +undeclared-scope
\ No newline at end of file diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index 815bfba..68e1ba7 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -71,14 +71,14 @@ have nz2: 2%:R != 0 :> L. apply/eqP=> char2; apply: conj_nt => e; apply/eqP/idPn=> eJ. have opp_id x: - x = x :> L. by apply/esym/eqP; rewrite -addr_eq0 -mulr2n -mulr_natl char2 mul0r. - have{char2} char2: 2 \in [char L] by apply/eqP. + have{} char2: 2 \in [char L] by apply/eqP. without loss{eJ} eJ: e / conj e = e + 1. move/(_ (e / (e + conj e))); apply. rewrite fmorph_div rmorphD conjK -{1}[conj e](addNKr e) mulrDl. by rewrite opp_id (addrC e) divff // addr_eq0 opp_id. pose a := e * conj e; have aJ: conj a = a by rewrite rmorphM conjK mulrC. have [w Dw] := @solve_monicpoly _ 2 (nth 0 [:: e * a; - 1]) isT. - have{Dw} Dw: w ^+ 2 + w = e * a. + have{} Dw: w ^+ 2 + w = e * a. by rewrite Dw !big_ord_recl big_ord0 /= mulr1 mulN1r addr0 subrK. pose b := w + conj w; have bJ: conj b = b by rewrite rmorphD conjK addrC. have Db2: b ^+ 2 + b = a. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index a950ecc..c956047 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -239,7 +239,7 @@ without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x. rewrite -(subnn (size q1)) {1}IHq1 ?Dp ?dvdp_mulr // polySpred ?monic_neq0 //. by rewrite eqSS size_monicM ?monic_neq0 // -!subn1 subnAC addKn. have /dvdp_prod_XsubC[m Dq]: q ^ FtoL %| p_ I by rewrite DpI dvdp_map. -pose B := [set j in mask m (enum I)]; have{Dq} Dq: q ^ FtoL = p_ B. +pose B := [set j in mask m (enum I)]; have{} Dq: q ^ FtoL = p_ B. apply/eqP; rewrite -eqp_monic ?monic_map ?monic_prod_XsubC //. congr (_ %= _): Dq; apply: perm_big => //. by rewrite uniq_perm ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE. @@ -372,7 +372,7 @@ pose root_in (xR : realC) p := exists2 w, w \in sQ (tag xR) & root p w. pose extendsR (xR yR : realC) := tag xR \in sQ (tag yR). have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. rewrite {}/extendsR; case: (has_Rroot xR p c) / and4P; last by exists xR. - case: xR => x [R QxR] /= [/inQpK <-]; move: (p ^ _) => {p}p mon_p /inQ_K<- Dc. + case: xR => x [R QxR] /= [/inQpK <-]; move: (p ^ _) => {}p mon_p /inQ_K<- Dc. have{c Dc} p0_le0: (p ^ QxR).[0] <= 0. rewrite horner_coef0 coef_map -[p`_0]ofQ_K -coef_map -horner_coef0 (eqP Dc). by rewrite -rmorphX -rmorphN ofQ_K /= rmorphN rmorphX oppr_le0 sqr_ge0. @@ -417,7 +417,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. exists u => {s s_y}//; set y := ofQ z (t_ u); set p1 := minPoly Qx u in Dp. have /QtoQ[Qyz QyzE]: y \in sQ z := sQof z (t_ u). pose q1_ v := Fadjoin_poly Qx u (Qyz v). - have{QyzE} QyzE v: Qyz v = (q1_ v).[u]. + have{} QyzE v: Qyz v = (q1_ v).[u]. by rewrite Fadjoin_poly_eq // -Dt -sQof2 QyzE sQof. have /all_sig2[q_ coqp Dq] v: {q | v != 0 -> coprimep p q & q ^ Qxz = q1_ v}. have /pQwx[q Dq]: q1_ v \is a polyOver Qx by apply: Fadjoin_polyOver. @@ -572,7 +572,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}. have /(find_root ((d * e)^-1 *: r ^ QxR))[N ub_rp] := xab0. pose f := d * e * h2; apply/posP; exists (maxn N (maxn m n)), f => [|k]. by rewrite !mulr_gt0 ?invr_gt0 ?ltr0n. - rewrite !geq_max => /and3P[/ab_le/ub_rp{ub_rp}ub_rp le_mk le_nk]. + rewrite !geq_max => /and3P[/ab_le/ub_rp{}ub_rp le_mk le_nk]. rewrite -(ltr_add2r f) -mulr2n -mulr_natr divfK // /nlim /lim Dqvw. rewrite rmorphD hornerD /= -addrA -ltr_subl_addl ler_lt_add //. by rewrite rmorphM hornerM ler_pmul ?ltW ?v_gtd ?w_gte. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index bed8e71..0b1e892 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -392,7 +392,7 @@ have ext1 mu0 x: {mu1 | exists y, x = Sinj mu1 y suffices in01M: lrmorphism in01 by exists (LRMorphism in01M). pose rwM := (=^~ Din01, SinjZ, rmorph1, rmorphB, rmorphM). by do 3?split; try move=> ? ?; apply: (fmorph_inj QrC); rewrite !rwM. - have {z zz Dz px Dx} Dx: exists xx, x = QrC xx. + have {z zz Dz px} Dx: exists xx, x = QrC xx. exists (map_poly (in_alg Qr) px).[zz]. by rewrite -horner_map Dz Sinj_poly Dx. pose lin01 := linfun in01; pose K := (lin01 @: fullv)%VS. @@ -637,7 +637,7 @@ Proof. have ZP_C c: (ZtoC c)%:P \is a polyOver Cint by rewrite raddfMz rpred_int. move=> mulS S_P x Sx; pose v := \row_(i < n) Y`_i. have [v0 | nz_v] := eqVneq v 0. - case/S_P: Sx => {x}x ->; rewrite big1 ?isAlgInt0 // => i _. + case/S_P: Sx => {}x ->; rewrite big1 ?isAlgInt0 // => i _. by have /rowP/(_ i) := v0; rewrite !mxE => ->; rewrite mul0rz. have sYS (i : 'I_n): x * Y`_i \in S. by rewrite rpredM //; apply/S_P/Cint_spanP/mem_Cint_span/memt_nth. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 266788c..24b764b 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -538,7 +538,7 @@ elim: t; do ?[ by move=> * //=; do ?case: (_ == _)]. - by move=> t irt /= n rt; rewrite rpoly_map_mul ?irt //. - move=> t irt s irs /=; case/andP=> rt rs. by apply: rmulpT; rewrite ?irt ?irs //. -- move=> t irt /= n rt; move: (irt rt)=> {rt} rt; elim: n => [|n ihn] //=. +- move=> t irt /= n rt; move: (irt rt) => {}rt; elim: n => [|n ihn] //=. exact: rmulpT. Qed. @@ -886,7 +886,7 @@ suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}. pose Kdec := DecFieldType Kfield (closed_field_QEMixin Kclosed). pose KclosedField := ClosedFieldType Kdec Kclosed. by exists [countClosedFieldType of CountType KclosedField cntK]. -exists (EtoKM 0%N) => /= z; have [i [{z}z ->]] := KtoE z. +exists (EtoKM 0%N) => /= z; have [i [{}z ->]] := KtoE z. suffices{z} /(_ z)[p mon_p]: integralRange (toE 0%N i isT). by rewrite -(fmorph_root (EtoKM i)) -map_poly_comp toEtoKp; exists p. rewrite /toE /E; clear - minXp_gt1 ext1root ext1gen. diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 5359cce..a6ba3bc 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -234,7 +234,7 @@ without loss{nz_af} [mon_f mon_g]: af f g Df Dfg / f \is monic /\ g \is monic. - by rewrite rmorphMz -scalerMzr scalerMzl -mulrzA cfg1. - by rewrite mulrzAl mulrzAr -mulrzA cfg1. by rewrite !(intz, =^~ scaler_int) !monicE !lead_coefZ mulrC cfg1. -have{af Df} Df: pQtoC pf = pZtoC f. +have{af} Df: pQtoC pf = pZtoC f. have:= congr1 lead_coef Df. rewrite lead_coefZ lead_coef_map_inj //; last exact: intr_inj. rewrite !(monicP _) // mulr1 Df => <-; rewrite scale1r -map_poly_comp. @@ -289,7 +289,7 @@ suffices: coprimep (pZtoC f) (pZtoC (g \Po 'X^p)). suffices: coprimep f (g \Po 'X^p). case/Bezout_coprimepP=> [[u v]]; rewrite -size_poly_eq1. rewrite -(size_map_inj_poly (can_inj intCK)) // rmorphD !rmorphM /=. - rewrite size_poly_eq1 => {co_fg}co_fg; apply/Bezout_coprimepP. + rewrite size_poly_eq1 => {}co_fg; apply/Bezout_coprimepP. by exists (pZtoC u, pZtoC v). apply: contraLR co_fg => /coprimepPn[|d]; first exact: monic_neq0. rewrite andbC -size_poly_eq1 dvdp_gcd => /and3P[sz_d]. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index d99b69b..9091dd8 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -680,7 +680,7 @@ rewrite rootM => pqx0 szpq. have [nzq nzp]: q != 0 /\ p != 0. by apply/norP; rewrite -mulf_eq0 -size_poly_eq0 szpq. without loss{pqx0} qx0: q p Kp Kq nzp nzq szpq / root q x. - move=> IH; case/orP: pqx0 => /IH{IH}IH; first exact: IH. + move=> IH; case/orP: pqx0 => /IH{}IH; first exact: IH. have{IH} /orP[]: (q %= p * q) || (q %= 1) by apply: IH => //; rewrite mulrC. by rewrite orbC -{1}[q]mul1r eqp_mul2r // eqp_sym => ->. by rewrite -{1}[p]mul1r eqp_sym eqp_mul2r // => ->. @@ -875,7 +875,7 @@ Implicit Types (V : {vspace L}) (E : {subfield L}). Lemma trivial_fieldOver : (1%VS : {vspace L_F}) =i F. Proof. -move=> x; apply/vlineP/idP=> [[{x}x ->] | Fx]. +move=> x; apply/vlineP/idP=> [[{}x ->] | Fx]. by rewrite fieldOver_scaleE mulr1 (valP x). by exists (vsproj F x); rewrite fieldOver_scaleE mulr1 vsprojK. Qed. @@ -912,7 +912,7 @@ suff: basis_of (vspaceOver M) b by apply: size_basis. apply/andP; split. rewrite eqEsubv; apply/andP; split; apply/span_subvP=> u. by rewrite mem_vspaceOver field_module_eq // => /Mb. - move/(@vbasis_mem _ _ _ M); rewrite -defM => /memv_sumP[{u}u Fu ->]. + move/(@vbasis_mem _ _ _ M); rewrite -defM => /memv_sumP[{}u Fu ->]. apply: memv_suml => i _; have /memv_cosetP[a Fa ->] := Fu i isT. by apply: (memvZ (Subvs Fa)); rewrite memv_span ?memt_nth. apply/freeP=> a /(directv_sum_independent dx_b) a_0 i. @@ -1109,7 +1109,7 @@ move=> v; rewrite -{1}(field_module_eq modM0) -(mem_vspaceOver M0) {}/V. move: (vspaceOver F1 M0) => M. apply/idP/idP=> [/coord_vbasis|/coord_span]->; apply/memv_suml=> i _. rewrite /(_ *: _) /= /fieldOver_scale; case: (coord _ i _) => /= x. - rewrite {1}[F1]unlock mem_baseVspace => /vlineP[{x}x ->]. + rewrite {1}[F1]unlock mem_baseVspace => /vlineP[{}x ->]. by rewrite -(@scalerAl F L) mul1r memvZ ?memv_span ?memt_nth. move: (coord _ i _) => x; rewrite -[_`_i]mul1r scalerAl -tnth_nth. have F1x: x%:A \in F1. diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index 492aed8..19684dc 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -405,7 +405,7 @@ have fZ: linear f. have /kAut_to_gal[alpha galLalpha Dalpha]: kAut 1 {:L} (linfun (Linear fZ)). rewrite kAutfE; apply/kHomP; split=> [x y _ _ | x /idfP]; rewrite !lfunE //=. exact: (rmorphM (RMorphism fM)). -have{Dalpha} Dalpha: alpha =1 f by move=> a; rewrite -Dalpha ?memvf ?lfunE. +have{} Dalpha: alpha =1 f by move=> a; rewrite -Dalpha ?memvf ?lfunE. suffices <-: fixedField [set alpha] = 1%AS. by rewrite gal_generated /generator; exists alpha. apply/vspaceP=> x; apply/fixedFieldP/idfP; rewrite ?memvf // => id_x. @@ -442,7 +442,7 @@ End FinGalois. Lemma Fermat's_little_theorem (L : fieldExtType F) (K : {subfield L}) a : (a \in K) = (a ^+ order K == a). Proof. -move: K a; wlog [{L}L -> K a]: L / exists galL : splittingFieldType F, L = galL. +move: K a; wlog [{}L -> K a]: L / exists galL : splittingFieldType F, L = galL. by pose galL := (FinSplittingFieldType F L) => /(_ galL); apply; exists galL. have /galois_fixedField fixLK := finField_galois (subvf K). have [alpha defGalLK Dalpha] := finField_galois_generator (subvf K). diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 82c4819..f41ec06 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -158,7 +158,7 @@ Definition kHom_rmorphism K E f homKEf := Lemma kHom_horner K E f p x : kHom K E f -> p \is a polyOver E -> x \in E -> f p.[x] = (map_poly f p).[f x]. Proof. -move=> homKf /polyOver_subvs[{p}p -> Ex]; pose fRM := kHom_rmorphism homKf. +move=> homKf /polyOver_subvs[{}p -> Ex]; pose fRM := kHom_rmorphism homKf. by rewrite (horner_map _ _ (Subvs Ex)) -[f _](horner_map fRM) map_poly_comp. Qed. @@ -632,7 +632,7 @@ have [f homLf fxz]: exists2 f : 'End(Lz), kHom 1 imL f & f (inLz x) = z. pose f0 := kHomExtend 1 \1 (inLz x) z. have{map1q1z_z} hom_f0 : kHom 1 <<1; inLz x>> f0. by apply: kHomExtendP map1q1z_z => //; apply: kHom1. - have{splitLpz} splitLpz: splittingFieldFor <<1; inLz x>> pz imL. + have{} splitLpz: splittingFieldFor <<1; inLz x>> pz imL. have [r def_pz defLz] := splitLpz; exists r => //. apply/eqP; rewrite eqEsubv -{2}defLz adjoin_seqSl ?sub1v // andbT. apply/Fadjoin_seqP; split; last first. @@ -1230,7 +1230,7 @@ exists (pmap f r). rewrite splitKa; have{splitKa}: all (root (minPoly K a)) r. by apply/allP => b; rewrite splitKa root_prod_XsubC. elim: r Er => /= [|b r IHr]; first by rewrite !big_nil. -case/andP=> Eb Er /andP[pKa_b_0 /(IHr Er){IHr Er}IHr]. +case/andP=> Eb Er /andP[pKa_b_0 /(IHr Er){Er}IHr]. have [x galE /eqP xa_b] := normalField_root_minPoly sKE nKE Ea pKa_b_0. rewrite /(f b); case: (pickP _) => [y /andP[_ /eqP<-]|/(_ x)/andP[]//]. by rewrite !big_cons IHr. @@ -1587,7 +1587,7 @@ Proof. by rewrite -normalField_ker ker_normal. Qed. Lemma normalField_img : normalField_cast @* 'Gal(E / K) = 'Gal(M / K). Proof. have [[sKM sME] [sKE _ nKE]] := (andP sKME, and3P galKE). -apply/setP=> x; apply/idP/idP=> [/morphimP[{x}x galEx _ ->] | galMx]. +apply/setP=> x; apply/idP/idP=> [/morphimP[{}x galEx _ ->] | galMx]. rewrite gal_kHom //; apply/kAHomP=> a Ka; have Ma := subvP sKM a Ka. by rewrite normalField_cast_eq // (fixed_gal sKE). have /(kHom_to_gal sKME nKE)[y galEy eq_xy]: kHom K M x by rewrite -gal_kHom. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index e51a660..6320343 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -414,7 +414,7 @@ exists p => //; exists (\poly_(i < r.+1) f`_(i * p)). rewrite comp_polyE size_poly_eq -?Dn ?fn1 ?oner_eq0 //. have pr_p := charf_prime charLp; have p_gt0 := prime_gt0 pr_p. apply/polyP=> i; rewrite coef_sum. -have [[{i} i ->] | p'i] := altP (@dvdnP p i); last first. +have [[{}i ->] | p'i] := altP (@dvdnP p i); last first. rewrite big1 => [|j _]; last first. rewrite coefZ -exprM coefXn [_ == _](contraNF _ p'i) ?mulr0 // => /eqP->. by rewrite dvdn_mulr. @@ -512,7 +512,7 @@ Lemma Derivation_separableP : (separable_element K x). Proof. apply: (iffP idP) => [sepKx D derD /subvP DK_0 | derKx_0]. - have{DK_0} DK_0 q: q \is a polyOver K -> map_poly D q = 0. + have{} DK_0 q: q \is a polyOver K -> map_poly D q = 0. move=> /polyOverP Kq; apply/polyP=> i; apply/eqP. by rewrite coef0 coef_map -memv_ker DK_0. apply/subvP=> _ /Fadjoin_polyP[p Kp ->]; rewrite memv_ker. @@ -771,7 +771,7 @@ have sep_pKy: separable_poly (minPoly K y). have{sep_pKy} sep_q: separable_poly q by rewrite Dq separable_map in sep_pKy. have [r nz_r PETr] := large_field_PET nz_p px0 qy0 sep_q. have [[s [Us Ks /ltnW leNs]] | //] := finite_PET (size r). -have{s Us leNs} /allPn[t {Ks}/Ks Kt nz_rt]: ~~ all (root r) s. +have{s Us leNs} /allPn[t {}/Ks Kt nz_rt]: ~~ all (root r) s. by apply: contraTN leNs; rewrite -ltnNge => /max_poly_roots->. have{PETr} [/= [p1 Dx] [q1 Dy]] := PETr (Subvs Kt) nz_rt. set z := t * y - x in Dx Dy; exists z; apply/eqP. diff --git a/mathcomp/fingroup/Make b/mathcomp/fingroup/Make index a765cd3..0f25f14 100644 --- a/mathcomp/fingroup/Make +++ b/mathcomp/fingroup/Make @@ -13,6 +13,6 @@ quotient.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +undeclared-scope
\ No newline at end of file diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index b9ed8e1..a2cda05 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.v @@ -432,7 +432,7 @@ Lemma lone_subgroup_char G H : H \char G. Proof. move=> sHG Huniq; apply/charP; split=> // f injf Gf; apply/eqP. -have{injf} injf: {in H &, injective f}. +have{} injf: {in H &, injective f}. by move/injmP: injf; apply: sub_in2; apply/subsetP. have fH: f @* H = f @: H by rewrite /morphim (setIidPr sHG). rewrite eqEcard {2}fH card_in_imset ?{}Huniq //=. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 21e1e49..914c332 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -866,7 +866,7 @@ suffices{big_r} IHr: reflect (exists2 c, inA c r & x = \prod_(i <- r) c i) piAx. apply: (iffP IHr) => -[c inAc ->]; do [exists c; last by rewrite big_r]. by move=> i Pi; rewrite (allP inAc) ?mem_r. by apply/allP=> i; rewrite mem_r => /inAc. -elim: {P mem_r}r x @piAx Ur => /= [x _ | i r IHr x /andP[r'i /IHr{IHr}IHr]]. +elim: {P mem_r}r x @piAx Ur => /= [x _ | i r IHr x /andP[r'i /IHr{}IHr]]. by rewrite unlock; apply: (iffP set1P) => [-> | [] //]; exists (fun=> x). rewrite big_cons; apply: (iffP idP) => [|[c /andP[Aci Ac] ->]]; last first. by rewrite big_cons mem_mulg //; apply/IHr=> //; exists c. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index cdd68fd..47f9353 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -393,7 +393,7 @@ have [/= f inj_f im_f] := third_isom (joing_subl K M) nsKG nsKMG. rewrite quotientYidl //= -imKH -(restrm_quotientE nKH sMH) in f inj_f im_f. have /domP[h [_ ker_h _ im_h]]: 'dom (f \o quotm _ nsMH) = H / M. by rewrite ['dom _]morphpre_quotm injmK. -have{im_h} im_h L: L \subset H -> h @* (L / M) = K <*> L / (K <*> M). +have{} im_h L: L \subset H -> h @* (L / M) = K <*> L / (K <*> M). move=> sLH; have [sLG sKKM] := (subset_trans sLH sHG, joing_subl K M). rewrite im_h morphim_comp morphim_quotm [_ @* L]restrm_quotientE ?im_f //. rewrite quotientY ?(normsG sKKM) ?(subset_trans sLG) ?normal_norm //. @@ -811,7 +811,7 @@ Proof. elim: r G => [|i r IHr]; rewrite !(big_nil, big_cons) //; case: ifP => _ // G. case/cprodP=> [[K H -> defH]]; rewrite defH => <- cKH leKH_G. have /implyP := leq_trans leKH_G (dvdn_leq _ (dvdn_cardMg K H)). -rewrite muln_gt0 leq_pmul2l !cardG_gt0 //= => /(IHr H defH){defH}defH. +rewrite muln_gt0 leq_pmul2l !cardG_gt0 //= => /(IHr H defH){}defH. by rewrite defH dprodE // cardMg_TI // -(bigdprod_card defH). Qed. @@ -825,7 +825,7 @@ have [m leQm] := ubnP #|Q|; elim: m => // m IHm in (Q) leQm G defG sQP *. have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0 in defG *. move: defG; rewrite !(bigD1 i Qi) /= => /cprodP[[Hi Gi defAi defGi] <-]. rewrite defAi defGi => cHGi. -have{defGi} defGi: \big[dprod/1]_(j | Q j && (j != i)) A j = Gi. +have{} defGi: \big[dprod/1]_(j | Q j && (j != i)) A j = Gi. by apply: IHm => [||j /andP[/sQP]] //; rewrite (cardD1x Qi) in leQm. rewrite defGi dprodE // coprime_TIg // -defAi -(bigdprod_card defGi). elim/big_rec: _ => [|j n /andP[neq_ji Qj] IHn]; first exact: coprimen1. diff --git a/mathcomp/solvable/Make b/mathcomp/solvable/Make index fd00057..2f5aac3 100644 --- a/mathcomp/solvable/Make +++ b/mathcomp/solvable/Make @@ -24,6 +24,6 @@ sylow.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +undeclared-scope
\ No newline at end of file diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index ba26ab6..2163b7d 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -299,7 +299,7 @@ rewrite partn_dvd ?exponentS ?exponent_gt0 //=; apply/dvdn_partP=> // p. rewrite pi_of_part ?exponent_gt0 // => /andP[_ /= pi_p]. have sppi: {subset (p : nat_pred) <= pi} by move=> q /eqnP->. have [P sylP] := Sylow_exists p H; have sPH := pHall_sub sylP. -have{sylP} sylP: p.-Sylow(G) P. +have{} sylP: p.-Sylow(G) P. rewrite pHallE (subset_trans sPH) //= (card_Hall sylP) eqn_dvd andbC. by rewrite -{1}(partn_part _ sppi) !partn_dvd ?cardSg ?cardG_gt0. rewrite partn_part ?partn_biglcm //. diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index e67a0f9..f95069a 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -270,7 +270,7 @@ have nSyl5: #|'Syl_5(H)| = 1%N. move: (dvdn_leq (isT: (0 < 20)%N) Hdiv). by move: (n) Hdiv; do 20 (case=> //). case: (Sylow_exists 5 H) => S; case/pHallP=> sSH oS. -have{oS} oS: #|S| = 5 by rewrite oS p_part Hcard20. +have{} oS: #|S| = 5 by rewrite oS p_part Hcard20. suff: 20 %| #|S| by rewrite oS. apply: FF => [|S1]; last by rewrite S1 cards1 in oS. apply: char_normal_trans Hnorm; apply: lone_subgroup_char => // Q sQH isoQS. diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 2dcb1d5..6d1a01f 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -538,7 +538,7 @@ elim: Es {+}G => [|E Es IHs] S in n oG expG p3Es defG *. by rewrite isog_cyclic_card prime_cyclic ?oZ ?card_pX1p2n //=. rewrite big_cons -cprodA in defG; rewrite /= -andbA in p3Es. have [[_ T _ defT] defET cTE] := cprodP defG; rewrite defT in defET cTE defG. -case/and3P: p3Es; move/eqP=> oE; move/eqP=> defZE; move/IHs=> {IHs}IHs. +move: p3Es => /and3P[/eqP oE /eqP defZE /IHs{}IHs]. have not_cEE: ~~ abelian E. by apply: contra not_le_p3_p => cEE; rewrite -oE -oZ -defZE (center_idP _). have sES: E \subset S by rewrite -defET mulG_subl. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index a0c40ee..8e6e002 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -862,7 +862,7 @@ Proof. move=> n_gt1; have [def2q _ ltqm _] := def2qr n_gt1. case/(isoGrpP _ (Grp_2dihedral n_gt1)); rewrite card_2dihedral // -/ m => oG. case/existsP=> -[x y] /=; rewrite -/q => /eqP[defG xq y2 xy]. -have{defG} defG: <[x]> * <[y]> = G. +have{} defG: <[x]> * <[y]> = G. by rewrite -norm_joinEr // norms_cycle xy groupV cycle_id. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. @@ -884,7 +884,7 @@ move=> n_gt3; have [def2q _ ltqm _] := def2qr (ltnW (ltnW n_gt3)). case/(isoGrpP _ (Grp_semidihedral n_gt3)). rewrite card_semidihedral // -/m => oG. case/existsP=> -[x y] /=; rewrite -/q -/r => /eqP[defG xq y2 xy]. -have{defG} defG: <[x]> * <[y]> = G. +have{} defG: <[x]> * <[y]> = G. by rewrite -norm_joinEr // norms_cycle xy mem_cycle. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. @@ -905,7 +905,7 @@ Proof. move=> n_gt2; have [def2q def2r ltqm _] := def2qr (ltnW n_gt2). case/(isoGrpP _ (Grp_quaternion n_gt2)); rewrite card_quaternion // -/m => oG. case/existsP=> -[x y] /=; rewrite -/q -/r => /eqP[defG xq y2 xy]. -have{defG} defG: <[x]> * <[y]> = G. +have{} defG: <[x]> * <[y]> = G. by rewrite -norm_joinEr // norms_cycle xy groupV cycle_id. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. @@ -1949,7 +1949,7 @@ have [a [fGa oa au n_gt01 cycGs]]: exists a, rewrite -(injm_p_rank injf) // p_rank_abelian 1?morphim_abelian //= p2 -/Gs. case: leqP => [|fGs1_gt1]; [by left | right]. split=> //; exists c; last by rewrite -def_m // m_c expg_zneg. - have{defA1} defA1: <[a]> \x <[c]> = 'Ohm_1(Aut U). + have{} defA1: <[a]> \x <[c]> = 'Ohm_1(Aut U). by rewrite -(Ohm_dprod 1 defA) defA1 (@Ohm_p_cycle 1 _ 2) /p_elt oc. have def_fGs1: 'Ohm_1(f @* Gs) = 'Ohm_1(A). apply/eqP; rewrite eqEcard OhmS // -(dprod_card defA1) -!orderE oa oc. @@ -2240,7 +2240,7 @@ have tiER: E :&: R = 'Z(E) by rewrite setIA (setIidPl (subset_trans sEH sHG)). have [cRR | not_cRR] := boolP (abelian R). exists E; [by right | exists [group of R]; split=> //; left]. by rewrite /= -(setIidPl (sub_abelian_cent cRR sUR)) scUR. -have{scUR} scUR: [group of U] \in 'SCN(R). +have{} scUR: [group of U] \in 'SCN(R). by apply/SCN_P; rewrite (normalS sUR (subsetIl _ _)) // char_normal. have pR: p.-group R := pgroupS (subsetIl _ _) pG. have [R_le_3 | R_gt_3] := leqP (logn p #|R|) 3. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index af0001c..7f36723 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1216,8 +1216,8 @@ set T := S; exists (logn p #|T|)./2. have [Es] := extraspecial_structure pS esS; rewrite -[in RHS]/T. elim: Es T => [_ _ <-| E s IHs T] /=. by rewrite big_nil cprod1g oZ (pfactorK 1). -rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oEp3; move/eqP=> defZE. -move/IHs=> {IHs}IHs; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU. +rewrite -andbA big_cons -cprodA => /and3P[/eqP oEp3 /eqP defZE]. +move=> /IHs{}IHs /cprodP[[_ U _ defU]]; rewrite defU => defT cEU. rewrite -(mulnK #|T| (cardG_gt0 (E :&: U))) -defT -mul_cardG /=. have ->: E :&: U = 'Z(S). apply/eqP; rewrite eqEsubset subsetI -{1 2}defZE subsetIl setIS //=. @@ -1385,7 +1385,7 @@ have{CAx GAx}: <[coset A x]> <| G / A. by rewrite /normal cycle_subG GAx cents_norm // centsC cycle_subG. case/(inv_quotientN nsAG)=> B /= defB sAB nBG. rewrite -cycle_subG defB (maxA B) ?trivg_quotient // nBG. -have{defB} defB : B :=: A * <[x]>. +have{} defB : B :=: A * <[x]>. rewrite -quotientK ?cycle_subG ?quotient_cycle // defB quotientGK //. exact: normalS (normal_sub nBG) nsAG. apply/setIidPl; rewrite ?defB -[_ :&: _]center_prod //=. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index 06f3152..cf6503a 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -424,7 +424,7 @@ have <-: 'Z(H / Z) * 'Z(K / Z) = 'Z(G / Z). by rewrite -mulHK quotientMl // center_prod ?quotient_cents. have ZquoZ (B A : {group gT}): B \subset 'C(A) -> 'Z_n(A) * 'Z_n(B) = Z -> 'Z(A / Z) = 'Z_n.+1(A) / Z. -- move=> cAB {defZ}defZ; have cAZnB: 'Z_n(B) \subset 'C(A) := gFsub_trans _ cAB. +- move=> cAB {}defZ; have cAZnB: 'Z_n(B) \subset 'C(A) := gFsub_trans _ cAB. have /second_isom[/=]: A \subset 'N(Z). by rewrite -defZ normsM ?gFnorm ?cents_norm // centsC. suffices ->: Z :&: A = 'Z_n(A). diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index 80005a4..27c0780 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -120,7 +120,7 @@ have [trG _] := andP primG; have [x Sx defS] := imsetP trG. move: primG; rewrite (trans_prim_astab Sx) // => /maximal_eqP[_]. case/(_ ('C_G[x | to] <*> H)%G) => /= [||cxH|]; first exact: joing_subl. - by rewrite join_subG subsetIl. -- have{cxH} cxH: H \subset 'C_G[x | to] by rewrite -cxH joing_subr. +- have{} cxH: H \subset 'C_G[x | to] by rewrite -cxH joing_subr. rewrite subsetI sHG /= in cxH; left; apply/subsetP=> a Ha. apply/astabP=> y Sy; have [b Gb ->] := atransP2 trG Sx Sy. rewrite actCJV [to x (a ^ _)](astab1P _) ?(subsetP cxH) //. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index fcbe7e8..3d2685b 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -148,7 +148,7 @@ have sylP: p.-Sylow(G) P. by rewrite p'natE // -indexgI -oSiN // /dvdn oS1. have eqS Q: maxp G Q = p.-Sylow(G) Q. apply/idP/idP=> [S_Q|]; last exact: Hall_max. - have{S_Q} S_Q: Q \in S by rewrite inE. + have{} S_Q: Q \in S by rewrite inE. rewrite pHallE -(card_Hall sylP); case: (S_pG Q) => // -> _ /=. by case: (atransP2 trS S_P S_Q) => x _ ->; rewrite cardJg. have ->: 'Syl_p(G) = S by apply/setP=> Q; rewrite 2!inE. @@ -568,7 +568,7 @@ Theorem Baer_Suzuki x G : x \in 'O_p(G). Proof. have [n] := ubnP #|G|; elim: n G x => // n IHn G x /ltnSE-leGn Gx pE. -set E := x ^: G; have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. +set E := x ^: G; have{} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. move=> _ _ /imsetP[y1 Gy1 ->] /imsetP[y2 Gy2 ->]. rewrite -(mulgKV y1 y2) conjgM -2!conjg_set1 -conjUg genJ pgroupJ. by rewrite pE // groupMl ?groupV. diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make index d6879a6..b909046 100644 --- a/mathcomp/ssreflect/Make +++ b/mathcomp/ssreflect/Make @@ -28,7 +28,7 @@ order.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +undeclared-scope -arg -w -arg -non-reversible-notation
\ No newline at end of file diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index cd3507a..7d8332c 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1770,7 +1770,7 @@ rewrite -{P mem_r}big_r; elim: r Ur => /= [_ | i r IHr]. rewrite (big_pred1 [ffun=> j0]) ?big_nil //= => f. apply/familyP/eqP=> /= [Df |->{f} i]; last by rewrite ffunE !inE. by apply/ffunP=> i; rewrite ffunE; apply/eqP/Df. -case/andP=> /negbTE nri; rewrite big_cons big_distrl => {IHr}/IHr <-. +case/andP=> /negbTE nri; rewrite big_cons big_distrl => {}/IHr<-. rewrite (partition_big (fun f : fIJ => f i) (Q i)) => [|f]; last first. by move/familyP/(_ i); rewrite /= inE /= eqxx. pose seti j (f : fIJ) := [ffun k => if k == i then j else f k]. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 4899ee3..ae46cd3 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -709,7 +709,7 @@ rewrite !natTrecE; set m := _ + r; set km := _ + kn; pose d := gcdn m n. have ->: gcdn n r = d by rewrite [d]gcdnC gcdnMDl. have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT. have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0. -move/IHq=> {IHq} IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d. +move=> {}/IHq IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d. by rewrite mulnDl leq_add // -mulnA leq_mul2l le_kr_n orbT. apply: (@addIn d); rewrite mulnDr -addnA addnACA -def_d addnACA mulnA. rewrite -!mulnDl -mulnDr -addnA [kr * _]mulnC; congr addn. diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 0218f6a..1fd1a83 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -175,7 +175,7 @@ Proof. suffices ffunK f g: (forall x, f x = g x) -> f = finfun g. by split=> [/ffunK|] -> //; apply/esym/ffunK. case: f => f Dg; rewrite unlock; congr FinfunOf. -have{Dg} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx. +have{} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx. by rewrite -Dg /= (bool_irrelevance (mem_enum _ _) aTx). elim: (enum aT) / f (enum_uniq aT) => //= x1 s y f IHf /andP[s'x1 Us] in Dg *. rewrite Dg ?eqxx //=; case: eqP => // /eq_axiomK-> /= _. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 3e60c2d..ef47cd2 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -1840,7 +1840,7 @@ Proof. have->: P = [set x in enum (mem P)] by apply/setP=> x; rewrite inE mem_enum. elim: {P}(enum _) (enum_uniq (mem P)) => [_ | A e IHe] /=. by rewrite /trivIset /cover !big_set0 cards0; left=> A; rewrite inE. -case/andP; rewrite set_cons -(in_set (fun B => B \in e)) => PA {IHe}/IHe. +case/andP; rewrite set_cons -(in_set (fun B => B \in e)) => PA {}/IHe. move: {e}[set x in e] PA => P PA IHP. rewrite /trivIset /cover !big_setU1 //= eq_sym. have:= leq_card_cover P; rewrite -(mono_leqif (leq_add2l #|A|)). @@ -2157,7 +2157,7 @@ move=> /and3P[/eqP defG tiP notP0] /and3P[/eqP defP tiQ notQ0]. have sQP E: E \in Q -> {subset E <= P}. by move=> Q_E; apply/subsetP; rewrite -defP (bigcup_max E). rewrite /partition cover_imset -(big_trivIset _ tiQ) defP -defG eqxx /= andbC. -have{notQ0} notQ0: set0 \notin cover @: Q. +have{} notQ0: set0 \notin cover @: Q. apply: contra notP0 => /imsetP[E Q_E E0]. have /set0Pn[/= A E_A] := memPn notQ0 E Q_E. congr (_ \in P): (sQP E Q_E A E_A). diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 7cd178d..3cf68d3 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -6968,7 +6968,7 @@ Lemma leEtprod n T (t1 t2 : n.-tuple T) : Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= lexx; symmetry; apply/forallP => []. -case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2]. +case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ <= _]le_cons [t1 <= t2 :> seq _]IHn. apply/idP/forallP => [/andP[lex12 /forallP/= let12 i]|lext12]. by case: (unliftP ord0 i) => [j ->|->]//; rewrite !tnthS. @@ -7278,7 +7278,7 @@ Lemma lexi_tupleP n T (t1 t2 : n.-tuple T) : Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= lexx; constructor; exists ord0 => -[]. -case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2]. +case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ <= _]lexi_cons; apply: (iffP idP) => [|[k leif_xt12]]. case: comparableP => //= [ltx12 _|-> /IHn[k kP]]. exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->. @@ -7299,7 +7299,7 @@ Lemma ltxi_tupleP n T (t1 t2 : n.-tuple T) : Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= ltxx; constructor => - [] []. -case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2]. +case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ < _]ltxi_cons; apply: (iffP idP) => [|[k leif_xt12]]. case: (comparableP x1 x2) => //= [ltx12 _|-> /IHn[k kP]]. exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 72c9719..fa66807 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -687,12 +687,12 @@ Proof. move=> e_p; have: x \in x :: p by apply: mem_head. elim: p x {1 3 5}x e_p => [|y2 p IHp] x y1. by rewrite mem_seq1 => _ /eqP->. -rewrite inE orbC /= => /andP[ey12 /IHp {IHp}IHp]. +rewrite inE orbC /= => /andP[ey12 {}/IHp IHp]. case: ifPn => [y2p_x _ | not_y2p_x /eqP def_x]. have [p' e_p' Up' p'p] := IHp _ y2p_x. by split=> // y /p'p; apply: predU1r. have [p' e_p' Up' p'p] := IHp y2 (mem_head y2 p). -have{p'p} p'p z: z \in y2 :: p' -> z \in y2 :: p. +have{} p'p z: z \in y2 :: p' -> z \in y2 :: p. by rewrite !inE; case: (z == y2) => // /p'p. rewrite -(last_cons y1) def_x; split=> //=; first by rewrite ey12. by rewrite (contra (p'p y1)) -?def_x. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 389b1c2..ab8edce 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -216,13 +216,13 @@ have eq_bc_0: (b == 0) && (c == 0) = (d == 0). have lt1p: 1 < p by rewrite ltnS double_gt0. have co_p_2: coprime p 2 by rewrite /coprime gcdnC gcdnE modn2 /= odd_double. have if_d0: d = 0 -> [/\ m = (p + a.*2) * p, lb_dvd p p & lb_dvd p (p + a.*2)]. - move=> d0; have{d0 def_m} def_m: m = (p + a.*2) * p. + move=> d0; have{d0} def_m: m = (p + a.*2) * p. by rewrite d0 addn0 -!mul2n mulnA -mulnDl in def_m *. split=> //; apply/hasPn=> r /(hasPn leppm); apply: contra => /= dv_r. by rewrite def_m dvdn_mull. by rewrite def_m dvdn_mulr. case def_a: a => [|a'] /= in le_a_n *; rewrite !natTrecE -/p {}eq_bc_0. - case: d if_d0 def_m => [[//| def_m {pr_p}pr_p pr_m'] _ | d _ def_m] /=. + case: d if_d0 def_m => [[//| def_m {}pr_p pr_m'] _ | d _ def_m] /=. rewrite def_m def_a addn0 mulnA -2!expnSr. by split; rewrite /pd_ord /pf_ok /= ?muln1 ?pr_p ?leqnn. apply: apd_ok; rewrite // /pd_ok /= /pfactor expn1 muln1 /pd_ord /= ltpm. @@ -256,11 +256,11 @@ have ltdp: d < p. move/eqP: def_b'; rewrite subn_eq0 -(@leq_pmul2r kb); last first. by rewrite -def_kb1. rewrite mulnBl -def_k2 ltnS -(leq_add2r c); move/leq_trans; apply. - have{ltc} ltc: c < k.*2. + have{} ltc: c < k.*2. by apply: (leq_trans ltc); rewrite leq_double /kb; case e. rewrite -{2}(subnK (ltnW ltc)) leq_add2r leq_sub2l //. by rewrite -def_kb1 mulnS leq_addr. -case def_d: d if_d0 => [|d'] => [[//|{def_m ltdp pr_p} def_m pr_p pr_m'] | _]. +case def_d: d if_d0 => [|d'] => [[//|{ltdp pr_p}def_m pr_p pr_m'] | _]. rewrite eqxx -doubleS -addnS -def_a doubleD -addSn -/p def_m. rewrite mulnCA mulnC -expnSr. apply: IHn => {n le_a_n}//; rewrite -/p -/kb; split. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index db53235..f32793f 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -349,7 +349,7 @@ Proof. case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (insubK _)). rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first. by rewrite isSome_insub; case: eqP=> // ->. -elim: n t t_n => [|m IHm] [|x t] //= {IHm}/IHm; move: (iter m _ _) => em IHm. +elim: n t t_n => [|m IHm] [|x t] //= {}/IHm; move: (iter m _ _) => em IHm. transitivity (x \in T : nat); rewrite // -mem_enum codomE. elim: (fintype.enum T) (enum_uniq T) => //= y e IHe /andP[/negPf ney]. rewrite count_cat count_map inE /preim /= [in LHS]/eq_op /= eq_sym => /IHe->. |