From a06d61a8e226eeabc52f1a22e469dca1e6077065 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 29 Nov 2019 01:19:33 +0900 Subject: Refactoring and linting especially polydiv - Replace `altP eqP` and `altP (_ =P _)` with `eqVneq`: The improved `eqVneq` lemma (#351) is redesigned as a comparison predicate and introduces a hypothesis in the form of `x != y` in the second case. Thus, `case: (altP eqP)`, `case: (altP (x =P _))` and `case: (altP (x =P y))` idioms can be replaced with `case: eqVneq`, `case: (eqVneq x)` and `case: (eqVneq x y)` respectively. This replacement slightly simplifies and reduces proof scripts. - use `have [] :=` rather than `case` if it is better. - `by apply:` -> `exact:`. - `apply/lem1; apply/lem2` or `apply: lem1; apply: lem2` -> `apply/lem1/lem2`. - `move/lem1; move/lem2` -> `move/lem1/lem2`. - Remove `GRing.` prefix if applicable. - `negbTE` -> `negPf`, `eq_refl` -> `eqxx` and `sym_equal` -> `esym`. --- mathcomp/character/character.v | 15 +++++++-------- mathcomp/character/classfun.v | 14 +++++++------- mathcomp/character/integral_char.v | 4 ++-- mathcomp/character/mxabelem.v | 2 +- mathcomp/character/mxrepresentation.v | 9 ++++----- 5 files changed, 21 insertions(+), 23 deletions(-) (limited to 'mathcomp/character') diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 78c5295..113ef8b 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -491,7 +491,7 @@ Proof. by rewrite cfunE cfuniE ?normal1 // inE mulr_natr. Qed. Lemma cfReprReg : cfRepr (regular_repr algCF G) = cfReg G. Proof. apply/cfun_inP=> x Gx; rewrite cfRegE. -have [-> | ntx] := altP (x =P 1%g); first by rewrite cfRepr1. +have [-> | ntx] := eqVneq x 1%g; first by rewrite cfRepr1. rewrite cfunE Gx [\tr _]big1 // => i _; rewrite 2!mxE /=. rewrite -(inj_eq enum_val_inj) gring_indexK ?groupM ?enum_valP //. by rewrite eq_mulVg1 mulKg (negbTE ntx). @@ -714,7 +714,7 @@ Qed. Lemma xcfun_id i j : ('chi_i).['e_j]%CF = 'chi_i 1%g *+ (i == j). Proof. -have [<-{j} | /xcfun_annihilate->//] := altP eqP; last exact: Wedderburn_id_mem. +have [<-{j} | /xcfun_annihilate->//] := eqVneq; last exact: Wedderburn_id_mem. by rewrite -xcfunG // repr_mx1 -(xcfun_mul_id _ (envelop_mx1 _)) mulmx1. Qed. @@ -1204,7 +1204,7 @@ transitivity (('chi_i).[e j *m aG y]%CF / 'chi_j 1%g). rewrite mulmx_suml raddf_sum big_distrl; apply: eq_bigr => x Gx /=. rewrite -scalemxAl xcfunZr -repr_mxM // xcfunG ?groupM // mulrAC mulrC. by congr (_ * _); rewrite mulrC mulKf ?irr1_neq0. -rewrite mulr_natl mulrb; have [<-{j} | neq_ij] := altP eqP. +rewrite mulr_natl mulrb; have [<-{j} | neq_ij] := eqVneq. by congr (_ / _); rewrite xcfun_mul_id ?envelop_mx_id ?xcfunG. rewrite (xcfun_annihilate neq_ij) ?mul0r //. case/andP: (Wedderburn_ideal (W j)) => _; apply: submx_trans. @@ -1284,7 +1284,7 @@ transitivity ((#|'C_G[repr (y ^: G)]|%:R *: (X' *m X)) i_y i_x). rewrite mulmx1C // !mxE -!divg_index !(index_cent1, =^~ indexgI). rewrite (class_eqP (mem_repr y _)) ?class_refl // mulr_natr. rewrite (can_in_eq class_IirrK) ?mem_classes //. -have [-> | not_yGx] := altP eqP; first by rewrite class_refl. +have [-> | not_yGx] := eqVneq; first by rewrite class_refl. by rewrite [x \in _](contraNF _ not_yGx) // => /class_eqP->. Qed. @@ -1450,7 +1450,7 @@ rewrite -!eq_scale_irr; apply/eqP/idP; last first. case/orP; first by case/andP=> /eqP-> /eqP->. case/orP=> /and3P[/eqP-> /eqP-> /eqP->]; first by rewrite addrC. by rewrite !scaleNr !addNr. -have [-> /addrI/eqP-> // | /= ] := altP eqP. +have [-> /addrI/eqP-> // | /=] := eqVneq. rewrite eq_scale_irr => /norP[/negP nz_a /negPf neq_ir]. move/(congr1 (cfdotr 'chi__))/esym/eqP => /= eq_cfdot. move: {eq_cfdot}(eq_cfdot i) (eq_cfdot r); rewrite eq_sym !cfdotDl !cfdotZl. @@ -2412,7 +2412,7 @@ Implicit Types G H : {group gT}. Lemma lin_irr_der1 G i : ('chi_i \is a linear_char) = (G^`(1)%g \subset cfker 'chi[G]_i). Proof. -apply/idP/idP=> [|sG'K]; first by apply: lin_char_der1. +apply/idP/idP=> [|sG'K]; first exact: lin_char_der1. have nsG'G: G^`(1) <| G := der_normal 1 G. rewrite qualifE irr_char -[i](quo_IirrK nsG'G) // mod_IirrE //=. by rewrite cfModE // morph1 lin_char1 //; apply/char_abelianP/der_abelian. @@ -2832,8 +2832,7 @@ Proof. apply/eqP; rewrite eqEsubset; rewrite cfcenter_subset_center ?irr_char //. apply/subsetP=> _ /setIP[/morphimP[x /= _ Gx ->] cGx]; rewrite mem_quotient //=. rewrite -irrRepr cfker_repr cfcenter_repr inE Gx in cGx *. -apply: mx_abs_irr_cent_scalar 'Chi_i _ _ _. - by apply: groupC; apply: socle_irr. +apply: mx_abs_irr_cent_scalar 'Chi_i _ _ _; first exact/groupC/socle_irr. have nKG: G \subset 'N(rker 'Chi_i) by apply: rker_norm. (* GG -- locking here is critical to prevent Coq kernel divergence. *) apply/centgmxP=> y Gy; rewrite [eq]lock -2?(quo_repr_coset (subxx _) nKG) //. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 295b77a..fc19eba 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -943,7 +943,7 @@ Lemma cfCauchySchwarz phi psi : `|'[phi, psi]| ^+ 2 <= '[phi] * '[psi] ?= iff ~~ free (phi :: psi). Proof. rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC. -have [-> | nz_psi] /= := altP (psi =P 0). +have [-> | nz_psi] /= := eqVneq psi 0. by apply/leifP; rewrite !cfdot0r normCK mul0r mulr0. without loss ophi: phi / '[phi, psi] = 0. move=> IHo; pose a := '[phi, psi] / '[psi]; pose phi1 := phi - a *: psi. @@ -978,7 +978,7 @@ rewrite (mono_leif (ler_pmul2r _)) ?ltr0n //. have:= leif_trans (leif_Re_Creal '[phi, psi]) (cfCauchySchwarz_sqrt phi psi). congr (_ <= _ ?= iff _); apply: andb_id2r. rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC. -have [-> | nz_psi] := altP (psi =P 0); first by rewrite cfdot0r coord0. +have [-> | nz_psi] := eqVneq psi 0; first by rewrite cfdot0r coord0. case/vlineP=> [x ->]; rewrite cfdotZl linearZ pmulr_lge0 ?cfnorm_gt0 //=. by rewrite (coord_free 0) ?seq1_free // eqxx mulr1. Qed. @@ -1186,7 +1186,7 @@ rewrite orthonormalE; have [/= normS | not_normS] := allP; last first. by right=> [[_ o1S]]; case: not_normS => phi Sphi; rewrite /= o1S ?eqxx. apply: (iffP (pairwise_orthogonalP S)) => [] [uniqS oSS]. split=> // [|phi psi]; first by case/andP: uniqS. - by have [-> _ /normS/eqP | /oSS] := altP eqP. + by have [-> _ /normS/eqP | /oSS] := eqVneq. split=> // [|phi psi Sphi Spsi /negbTE]; last by rewrite oSS // => ->. by rewrite /= (contra (normS _)) // cfdot0r eq_sym oner_eq0. Qed. @@ -1497,7 +1497,7 @@ by rewrite -!cfMorphE // eq_phi. Qed. Lemma cfMorph_eq1 phi : (cfMorph phi == 1) = (phi == 1). -Proof. by apply: rmorph_eq1; apply: cfMorph_inj. Qed. +Proof. exact/rmorph_eq1/cfMorph_inj. Qed. Lemma cfker_morph phi : cfker (cfMorph phi) = G :&: f @*^-1 (cfker phi). Proof. @@ -1526,7 +1526,7 @@ Lemma sub_morphim_cfker phi (A : {set aT}) : Proof. by move=> sAG; rewrite sub_cfker_morph ?sAG. Qed. Lemma cforder_morph phi : #[cfMorph phi]%CF = #[phi]%CF. -Proof. by apply: cforder_inj_rmorph; apply: cfMorph_inj. Qed. +Proof. exact/cforder_inj_rmorph/cfMorph_inj. Qed. End Main. @@ -1607,7 +1607,7 @@ Qed. Lemma cfIsom_inj : injective (cfIsom isoGR). Proof. exact: can_inj cfIsomK. Qed. Lemma cfIsom_eq1 phi : (cfIsom isoGR phi == 1) = (phi == 1). -Proof. by apply: rmorph_eq1; apply: cfIsom_inj. Qed. +Proof. exact/rmorph_eq1/cfIsom_inj. Qed. Lemma cforder_isom phi : #[cfIsom isoGR phi]%CF = #[phi]%CF. Proof. exact: cforder_inj_rmorph cfIsom_inj. Qed. @@ -1860,7 +1860,7 @@ by rewrite quotientK ?(subset_trans skerH) // -group_modr //= setIC tiKH mul1g. Qed. Lemma cforder_sdprod phi : #[cfSdprod phi]%CF = #[phi]%CF. -Proof. by apply: cforder_inj_rmorph cfSdprod_inj. Qed. +Proof. exact: cforder_inj_rmorph cfSdprod_inj. Qed. End SDproduct. diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index 1022afa..7e470b2 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -67,7 +67,7 @@ exists (SplittingFieldType _ _ Qn_ax). apply: separable_Xn_sub_1; rewrite -(fmorph_eq0 QnC) rmorph_nat. by rewrite pnatr_eq0 -lt0n cardG_gt0. exists QnC => [// nuQn|]. - by apply: (extend_algC_subfield_aut QnC [rmorphism of nuQn]). + exact: (extend_algC_subfield_aut QnC [rmorphism of nuQn]). rewrite span_seq1 in genQn. exists w => // hT H phi Nphi x x_dv_n. apply: sig_eqW; have [rH ->] := char_reprP Nphi. @@ -372,7 +372,7 @@ Proof. move: {2}_.+1 (ltnSn #|G|) => n; elim: n => // n IHn in gT G *. rewrite ltnS => leGn piGle2; have [simpleG | ] := boolP (simple G); last first. rewrite negb_forall_in => /exists_inP[N sNG]; rewrite eq_sym. - have [-> | ] := altP (N =P G). + have [->|] := eqVneq N G. rewrite groupP /= genGid normG andbT eqb_id negbK => /eqP->. exact: solvable1. rewrite [N == G]eqEproper sNG eqbF_neg !negbK => ltNG /and3P[grN]. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index f5755a3..1c3fe0b 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -199,7 +199,7 @@ move=> linL; apply/eqP; rewrite eqEsubset sub_rowg_mx andbT. apply/subsetP=> v; rewrite inE genmxE => /submxP[u ->{v}]. rewrite mulmx_sum_row group_prod // => i _. rewrite rowK; move: (enum_val i) (enum_valP i) => v Lv. -case: (eqVneq (u 0 i) 0) => [->|]; first by rewrite scale0r group1. +have [->|] := eqVneq (u 0 i) 0; first by rewrite scale0r group1. by rewrite -unitfE => aP; rewrite ((actsP linL) (FinRing.Unit _ aP)) ?inE. Qed. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index aff51bd..51d28f8 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -1592,7 +1592,7 @@ Lemma mxsimple_exists m (U : 'M_(m, n)) : Proof. move=> modU nzU [] // simU; move: {2}_.+1 (ltnSn (\rank U)) => r leUr. elim: r => // r IHr in m U leUr modU nzU simU. -have genU := genmxE U; apply simU; exists <>%MS; last by rewrite genU. +have genU := genmxE U; apply: (simU); exists <>%MS; last by rewrite genU. apply/mxsimpleP; split; rewrite ?(eqmx_eq0 genU) ?(eqmx_module genU) //. case=> V; rewrite !genU=> /and4P[modV sVU nzV ltVU]; case: notF. apply: IHr nzV _ => // [|[W simW sWV]]; first exact: leq_trans ltVU _. @@ -1891,7 +1891,7 @@ move=> modV redV [] // nssimV; have [r leVr] := ubnP (\rank V). elim: r => // r IHr in V leVr modV redV nssimV. have [V0 | nzV] := eqVneq V 0. by rewrite nssimV ?V0 //; apply: mxsemisimple0. -apply (mxsimple_exists modV nzV) => [[U simU sUV]]; have [modU nzU _] := simU. +apply: (mxsimple_exists modV nzV) => [[U simU sUV]]; have [modU nzU _] := simU. have [W modW defUW dxUW] := redV U modU sUV. have sWV: (W <= V)%MS by rewrite -defUW addsmxSr. apply: IHr (mx_reducibleS modW sWV redV) _ => // [|ssimW]. @@ -3492,8 +3492,7 @@ rewrite -defW; apply/sumsmx_subP=> j _; set x := x_ W j. have{Gx_} Gx: x \in G by rewrite Gx_. apply: submx_trans (submxMr _ sMU) _; apply: (mxmoduleP modU). rewrite inE -val_Clifford_act Gx //; set Wx := 'Cl%act W x. -have [-> //= | neWxW] := eqVneq Wx W. -case: (simM) => _ /negP[]; rewrite -submx0. +case: (eqVneq Wx W) (simM) => [-> //=|] neWxW [_ /negP[]]; rewrite -submx0. rewrite (canF_eq (actKin 'Cl Gx)) in neWxW. rewrite -(component_mx_disjoint _ _ neWxW); try exact: socle_simple. rewrite sub_capmx {1}(submx_trans sMU sUW) val_Clifford_act ?groupV //. @@ -5838,7 +5837,7 @@ have: mx_subseries (aG F) U /\ path ltmx 0 U by []. pose f : {rmorphism F0 -> F} := [rmorphism of idfun]. elim: m F U f => [|m IHm] F U f [modU ltU]. by rewrite addn0 (leq_trans (max_size_mx_series ltU)) ?rank_leq_row. -rewrite addnS ltnNge -implybF; apply/implyP=> le_nG_Um; apply nosplit. +rewrite addnS ltnNge -implybF; apply/implyP=> le_nG_Um; apply: nosplit. exists F => //; case=> [|n] rG irrG; first by case/mx_irrP: irrG. apply/idPn=> nabsG; pose cG := ('C(enveloping_algebra_mx rG))%MS. have{nabsG} [A]: exists2 A, (A \in cG)%MS & ~~ is_scalar_mx A. -- cgit v1.2.3