From 5d7bd2ea2a0a28fb275da8ba2e2c0dc5a33d1034 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Wed, 8 May 2019 09:43:34 +0200 Subject: refactor `seq` permutation theory - Change the naming of permutation lemmas so they conform to a consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`) prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq` using a property when there is also a lemma _using_ `perm_eq` for the same property. Lemmas that do not concern `perm_eq` do _not_ have `perm` in their name. - Change the definition of `permutations` for a time- and space- back-to-front generation algorithm. - Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and `tally_seq`, used by the improved `permutation` algorithm. - add deprecated aliases for renamed lemmas --- mathcomp/character/classfun.v | 4 ++-- mathcomp/character/inertia.v | 6 +++--- mathcomp/character/vcharacter.v | 10 +++++----- 3 files changed, 10 insertions(+), 10 deletions(-) (limited to 'mathcomp/character') diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 65167b5..c35cdd6 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -1173,7 +1173,7 @@ Qed. Lemma eq_orthonormal R S : perm_eq R S -> orthonormal R = orthonormal S. Proof. -move=> eqRS; rewrite !orthonormalE (eq_all_r (perm_eq_mem eqRS)). +move=> eqRS; rewrite !orthonormalE (eq_all_r (perm_mem eqRS)). by rewrite (eq_pairwise_orthogonal eqRS). Qed. @@ -2413,7 +2413,7 @@ 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 [|_ eqSuS] := uniq_min_size uniqSu sSuS; first by rewrite size_map. -by rewrite (perm_free (uniq_perm_eq uniqSu uniqS eqSuS)). +by rewrite (perm_free (uniq_perm uniqSu uniqS eqSuS)). Qed. Lemma cfAut_on A phi : (phi^u \in 'CF(G, A)) = (phi \in 'CF(G, A)). diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index 5350075..d3dfd38 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -465,14 +465,14 @@ Lemma im_cfclass_Iirr i : H <| G -> perm_eq [seq 'chi_j | j in cfclass_Iirr G i] ('chi_i ^: G)%CF. Proof. move=> nsHG; have UchiG := cfclass_uniq 'chi_i nsHG. -apply: uniq_perm_eq; rewrite ?(map_inj_uniq irr_inj) ?enum_uniq // => phi. +apply: uniq_perm; rewrite ?(map_inj_uniq irr_inj) ?enum_uniq // => phi. apply/imageP/idP=> [[j iGj ->] | /cfclassP[y]]; first by rewrite -cfclass_IirrE. by exists (conjg_Iirr i y); rewrite ?mem_imset ?conjg_IirrE. Qed. Lemma card_cfclass_Iirr i : H <| G -> #|cfclass_Iirr G i| = #|G : 'I_G['chi_i]|. Proof. -move=> nsHG; rewrite -size_cfclass -(perm_eq_size (im_cfclass_Iirr i nsHG)). +move=> nsHG; rewrite -size_cfclass -(perm_size (im_cfclass_Iirr i nsHG)). by rewrite size_map -cardE. Qed. @@ -481,7 +481,7 @@ Lemma reindex_cfclass R idx (op : Monoid.com_law idx) (F : 'CF(H) -> R) i : \big[op/idx]_(chi <- ('chi_i ^: G)%CF) F chi = \big[op/idx]_(j | 'chi_j \in ('chi_i ^: G)%CF) F 'chi_j. Proof. -move/im_cfclass_Iirr/(eq_big_perm _) <-; rewrite big_map big_filter /=. +move/im_cfclass_Iirr/(perm_big _) <-; rewrite big_map big_filter /=. by apply: eq_bigl => j; rewrite cfclass_IirrE. Qed. diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index 4212fbe..4a113b6 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -314,7 +314,7 @@ Lemma cfproj_sum_orthogonal P z phi : = if P phi then z phi * '[phi] else 0. Proof. move=> Sphi; have defS := perm_to_rem Sphi. -rewrite cfdot_suml (eq_big_perm _ defS) big_cons /= cfdotZl Inu ?Z_S //. +rewrite cfdot_suml (perm_big _ defS) big_cons /= cfdotZl Inu ?Z_S //. rewrite big1_seq ?addr0 // => xi; rewrite mem_rem_uniq ?inE //. by case/and3P=> _ neq_xi Sxi; rewrite cfdotZl Inu ?Z_S // dotSS ?mulr0. Qed. @@ -412,15 +412,15 @@ Lemma vchar_orthonormalP S : Proof. move=> vcS; apply: (equivP orthonormalP). split=> [[uniqS oSS] | [I [b defS]]]; last first. - split=> [|xi1 xi2]; rewrite ?(perm_eq_mem defS). - rewrite (perm_eq_uniq defS) map_inj_uniq ?enum_uniq // => i j /eqP. + split=> [|xi1 xi2]; rewrite ?(perm_mem defS). + rewrite (perm_uniq defS) map_inj_uniq ?enum_uniq // => i j /eqP. by rewrite eq_signed_irr => /andP[_ /eqP]. case/mapP=> [i _ ->] /mapP[j _ ->]; rewrite eq_signed_irr. rewrite cfdotZl cfdotZr rmorph_sign mulrA cfdot_irr -signr_addb mulr_natr. by rewrite mulrb andbC; case: eqP => //= ->; rewrite addbb eqxx. pose I := [set i | ('chi_i \in S) || (- 'chi_i \in S)]. pose b i := - 'chi_i \in S; exists I, b. -apply: uniq_perm_eq => // [|xi]. +apply: uniq_perm => // [|xi]. rewrite map_inj_uniq ?enum_uniq // => i j /eqP. by rewrite eq_signed_irr => /andP[_ /eqP]. apply/idP/mapP=> [Sxi | [i Ii ->{xi}]]; last first. @@ -453,7 +453,7 @@ move=> Zphi phiN1. have: orthonormal phi by rewrite /orthonormal/= phiN1 eqxx. case/vchar_orthonormalP=> [xi /predU1P[->|] // | I [b def_phi]]. have: phi \in (phi : seq _) := mem_head _ _. -by rewrite (perm_eq_mem def_phi) => /mapP[i _ ->]; exists (b i), i. +by rewrite (perm_mem def_phi) => /mapP[i _ ->]; exists (b i), i. Qed. Lemma zchar_small_norm phi n : -- cgit v1.2.3