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

2 files changed, 4 insertions, 5 deletions

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 97afdfb..12fcecb 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -4384,8 +4384,7 @@ have sz_p: size p = n.+1.
 pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted.
 have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P).
   rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb.
-  rewrite subr0 eqxx scale1r; apply: eq_big_perm.
-  by rewrite perm_eq_sym perm_sort.
+  by rewrite subr0 eqxx scale1r; apply/esym/perm_big; rewrite perm_sort.
 have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r).
   move=> n_gt0; rewrite -root_prod_XsubC -Dp rootE !hornerE hornerXn n_gt0.
   by rewrite subr_eq0; apply: eqP.
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index e73ca33..87ca0f4 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1004,7 +1004,7 @@ Proof. by rewrite /free span_seq1 dim_vline; case: (~~ _). Qed.
  
 Lemma perm_free X Y : perm_eq X Y -> free X = free Y.
 Proof.
-by move=> eqX; rewrite /free (perm_eq_size eqX) (eq_span (perm_eq_mem eqX)).
+by move=> eqXY; rewrite /free (perm_size eqXY) (eq_span (perm_mem eqXY)).
 Qed.
 
 Lemma free_directv X : free X = (0 \notin X) && directv (\sum_(v <- X) <[v]>).
@@ -1061,7 +1061,7 @@ Proof. by rewrite cat_free => /and3P[]. Qed.
 
 Lemma filter_free p X : free X -> free (filter p X).
 Proof.
-rewrite -(perm_free (etrans (perm_filterC p X _) (perm_eq_refl X))).
+rewrite -(perm_free (etrans (perm_filterC p X _) (perm_refl X))).
 exact: catl_free.
 Qed.
 
@@ -1170,7 +1170,7 @@ Qed.
 Lemma perm_basis X Y U : perm_eq X Y -> basis_of U X = basis_of U Y.
 Proof.
 move=> eqXY; congr ((_ == _) && _); last exact: perm_free.
-by apply/eq_span; apply: perm_eq_mem.
+by apply/eq_span; apply: perm_mem.
 Qed.
 
 Lemma vbasisP U : basis_of U (vbasis U).