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, 10 insertions, 10 deletions

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 :