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

diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 6a28884..2d576c4 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -240,8 +240,8 @@ without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x.
 have /dvdp_prod_XsubC[m Dq]: q ^ FtoL %| p_ I by rewrite DpI dvdp_map.
 pose B := [set j in mask m (enum I)]; have{Dq} Dq: q ^ FtoL = p_ B.
   apply/eqP; rewrite -eqp_monic ?monic_map ?monic_prod_XsubC //.
-  congr (_ %= _): Dq; apply: eq_big_perm => //.
-  by rewrite uniq_perm_eq ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE.
+  congr (_ %= _): Dq; apply: perm_big => //.
+  by rewrite uniq_perm ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE.
 rewrite -!(size_map_poly FtoL) Dq -DpI (minI B) // -?Dq ?FpxF //.
 by apply/subsetP=> j; rewrite inE => /mem_mask; rewrite mem_enum.
 Qed.
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index 00a7bad..cb499b3 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -651,10 +651,10 @@ have prod_aq m: m %| n -> \prod_(d < n.+1 | d %| m) aq d = (q ^ m - 1)%:R.
     by rewrite !hornerE hornerXn -natrX natrB ?expn_gt0 ?prime_gt0.
   rewrite (prod_cyclotomic (dvdn_prim_root z_prim m_dv_n)).
   have def_divm: perm_eq (divisors m) [seq d <- index_iota 0 n.+1 | d %| m].
-    rewrite uniq_perm_eq ?divisors_uniq ?filter_uniq ?iota_uniq // => d.
+    rewrite uniq_perm ?divisors_uniq ?filter_uniq ?iota_uniq // => d.
     rewrite -dvdn_divisors ?(dvdn_gt0 n_gt0) // mem_filter mem_iota ltnS /=.
     by apply/esym/andb_idr=> d_dv_m; rewrite dvdn_leq ?(dvdn_trans d_dv_m).
-  rewrite (eq_big_perm _ def_divm) big_filter big_mkord horner_prod.
+  rewrite (perm_big _ def_divm) big_filter big_mkord horner_prod.
   by apply: eq_bigr => d d_dv_m; rewrite -exprM muln_divA ?divnK.
 have /rpredBl<-: (aq n %| #|G|%:R)%C.
   rewrite oG -prod_aq // (bigD1 ord_max) //= dvdC_mulr //.
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index ae54fa1..30bef47 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -1329,12 +1329,12 @@ rewrite -fixedKE; apply/polyOverP => i; apply/fixedFieldP=> [|x galEx].
   rewrite (polyOverP _) // big_map rpred_prod // => b _.
   by rewrite polyOverXsubC memv_gal.
 rewrite -coef_map rmorph_prod; congr (_ : {poly _})`_i.
-symmetry; rewrite (eq_big_perm (map x r)) /= ?(big_map x).
+symmetry; rewrite (perm_big (map x r)) /= ?(big_map x).
   by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC.
 have Uxr: uniq (map x r) by rewrite map_inj_uniq //; apply: fmorph_inj.
 have /uniq_min_size: {subset map x r <= r}.
   by rewrite -map_comp => _ /codomP[b ->] /=; rewrite -galM // r_xa ?groupM.
-by rewrite (size_map x) perm_eq_sym; case=> // _ /uniq_perm_eq->.
+by rewrite (size_map x) perm_sym; case=> // _ /uniq_perm->.
 Qed.
 
 Lemma mem_galTrace K E a : galois K E -> a \in E -> galTrace K E a \in K.