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/solvable/abelian.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'mathcomp/solvable/abelian.v') diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index ad12189..a51cbf2 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -1713,11 +1713,11 @@ rewrite orderXdiv ?pfactor_dvdn ?leq_subr // -(dvdn_pmul2r m_gt0). by rewrite -expnS -subSn // subSS divnK pfactor_dvdn ?leq_subr. Qed. -Lemma perm_eq_abelian_type p b G : +Lemma abelian_type_pgroup p b G : p.-group G -> \big[dprod/1]_(x <- b) <[x]> = G -> 1 \notin b -> - perm_eq (map order b) (abelian_type G). + perm_eq (abelian_type G) (map order b). Proof. -move: b => b1 pG defG1 ntb1. +rewrite perm_sym; move: b => b1 pG defG1 ntb1. have cGG: abelian G. elim: (b1) {pG}G defG1 => [_ <-|x b IHb G]; first by rewrite big_nil abelian1. rewrite big_cons; case/dprodP=> [[_ H _ defH]] <-; rewrite defH => cxH _. @@ -1992,8 +1992,8 @@ suffices def_atG: abelian_type K ++ abelian_type H =i abelian_type G. by rewrite size_abelian_type // -abelian_type_homocyclic. have [bK defK atK] := abelian_structure cKK. have [bH defH atH] := abelian_structure cHH. -apply: perm_eq_mem; rewrite -atK -atH -map_cat. -apply: (perm_eq_abelian_type pG); first by rewrite big_cat defK defH. +apply/perm_mem; rewrite perm_sym -atK -atH -map_cat. +apply: (abelian_type_pgroup pG); first by rewrite big_cat defK defH. have: all [pred m | m > 1] (map order (bK ++ bH)). by rewrite map_cat all_cat atK atH !abelian_type_gt1. by rewrite all_map (eq_all (@order_gt1 _)) all_predC has_pred1. -- cgit v1.2.3