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

3 files changed, 16 insertions, 16 deletions

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.
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index 65c186a..d236575 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -2322,7 +2322,7 @@ have{defZN2} strZN2: \big[dprod/1]_(z <- [:: xpn3; y]) <[z]> = 'Z('Ohm_2(N)).
   by rewrite unlock /= dprodg1.
 rewrite -size_abelian_type ?center_abelian //.
 have pZN2: p.-group 'Z('Ohm_2(N)) by rewrite (pgroupS _ pN) // subIset ?Ohm_sub.
-rewrite -(perm_eq_size (perm_eq_abelian_type pZN2 strZN2 _)) //= !inE.
+rewrite (perm_size (abelian_type_pgroup pZN2 strZN2 _)) //= !inE.
 rewrite !(eq_sym 1) -!order_eq1 oy orderE oX2.
 by rewrite (eqn_exp2l 2 0) // (eqn_exp2l 1 0).
 Qed.
diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v
index 1a32bce..d191e20 100644
--- a/mathcomp/solvable/jordanholder.v
+++ b/mathcomp/solvable/jordanholder.v
@@ -179,9 +179,9 @@ elim: {G}#|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => cs1 cs2.
 have [G1 | ntG] := boolP (G :==: 1).
   have -> : s1 = [::] by apply/eqP; rewrite -(trivg_comps cs1).
   have -> : s2 = [::] by apply/eqP; rewrite -(trivg_comps cs2).
-  by rewrite /= perm_eq_refl.
+  by rewrite /= perm_refl.
 have [sG | nsG] := boolP (simple G).
-  by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_eq_refl.
+  by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_refl.
 case es1: s1 cs1 => [|N1 st1] cs1.
   by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG.
 case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}.
@@ -228,9 +228,9 @@ have i3 : perm_eq fG1 fG2.
   rewrite (@perm_catCA _ [::_] [::_]) /mksrepr.
   rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1).
   rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2).
-  exact: perm_eq_refl.
-apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym.
-by apply: perm_eq_trans i2; apply: perm_eq_refl.
+  exact: perm_refl.
+apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym.
+by apply: perm_trans i2; apply: perm_refl.
 Qed.
 
 End CompositionSeries.
@@ -593,11 +593,11 @@ elim: {G} #|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => hsD cs1 cs2.
 case/orP: (orbN (G :==: 1)) => [tG | ntG].
   have -> : s1 = [::] by apply/eqP; rewrite -(trivg_acomps cs1).
   have -> : s2 = [::] by apply/eqP; rewrite -(trivg_acomps cs2).
-  by rewrite /= perm_eq_refl.
+  by rewrite /= perm_refl.
 case/orP: (orbN (asimple to G))=> [sG | nsG].
   have -> : s1 = [:: 1%G ] by apply/(asimple_acompsP cs1).
   have -> : s2 = [:: 1%G ] by apply/(asimple_acompsP cs2).
-  by rewrite /= perm_eq_refl.
+  by rewrite /= perm_refl.
 case es1: s1 cs1 => [|N1 st1] cs1.
   by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG.
 case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}.
@@ -667,9 +667,9 @@ have i3 : perm_eq fG1 fG2.
   rewrite (@perm_catCA _ [::_] [::_]) /mksrepr.
   rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1).
   rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2).
-  exact: perm_eq_refl.
-apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym.
-by apply: perm_eq_trans i2; apply: perm_eq_refl.
+  exact: perm_refl.
+apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym.
+by apply: perm_trans i2; apply: perm_refl.
 Qed.
 
 End StrongJordanHolder.