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, 16 insertions, 15 deletions

diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 676daf0..853ffb6 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -614,19 +614,19 @@ Lemma perm_bigcprod (I : eqType) r1 r2 (A : I -> {set gT}) G x :
   \prod_(i <- r1) x i = \prod_(i <- r2) x i.
 Proof.
 elim: r1 r2 G => [|i r1 IHr] r2 G defG Ax eq_r12.
-  by rewrite perm_eq_sym in eq_r12; rewrite (perm_eq_small _ eq_r12) ?big_nil.
-have /rot_to[n r3 Dr2]: i \in r2 by rewrite -(perm_eq_mem eq_r12) mem_head.
+  by rewrite perm_sym in eq_r12; rewrite (perm_small_eq _ eq_r12) ?big_nil.
+have /rot_to[n r3 Dr2]: i \in r2 by rewrite -(perm_mem eq_r12) mem_head.
 transitivity (\prod_(j <- rot n r2) x j).
   rewrite Dr2 !big_cons in defG Ax *; have [[_ G1 _ defG1] _ _] := cprodP defG.
   rewrite (IHr r3 G1) //; first by case/allP/andP: Ax => _ /allP.
-  by rewrite -(perm_cons i) -Dr2 perm_eq_sym perm_rot perm_eq_sym.
+  by rewrite -(perm_cons i) -Dr2 perm_sym perm_rot perm_sym.
 rewrite -{-2}(cat_take_drop n r2) in eq_r12 *.
-rewrite (eq_big_perm _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *.
+rewrite (perm_big _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *.
 have /cprodP[[G1 G2 defG1 defG2] _ /centsP-> //] := defG.
   rewrite defG2 -(bigcprodW defG2) mem_prodg // => k _; apply: Ax.
-  by rewrite (perm_eq_mem eq_r12) mem_cat orbC mem_nth.
+  by rewrite (perm_mem eq_r12) mem_cat orbC mem_nth.
 rewrite defG1 -(bigcprodW defG1) mem_prodg // => k _; apply: Ax.
-by rewrite (perm_eq_mem eq_r12) mem_cat mem_nth.
+by rewrite (perm_mem eq_r12) mem_cat mem_nth.
 Qed.
 
 Lemma reindex_bigcprod (I J : finType) (h : J -> I) P (A : I -> {set gT}) G x :
@@ -637,7 +637,7 @@ Proof.
 case=> h1 hK h1K; rewrite -!(big_filter _ P) filter_index_enum => defG Ax.
 rewrite -(big_map h P x) -(big_filter _ P) filter_map filter_index_enum.
 apply: perm_bigcprod defG _ _ => [i|]; first by rewrite mem_enum => /Ax.
-apply: uniq_perm_eq (enum_uniq P) _ _ => [|i].
+apply: uniq_perm (enum_uniq P) _ _ => [|i].
   by apply/dinjectiveP; apply: (can_in_inj hK).
 rewrite mem_enum; apply/idP/imageP=> [Pi | [j Phj ->//]].
 by exists (h1 i); rewrite ?inE h1K.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 33bf82c..b610c36 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -294,22 +294,22 @@ Proof.
 by apply/permP => z; rewrite -(permKV s z) permJ; apply/inj_tperm/perm_inj.
 Qed.
 
-Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
+Lemma tuple_permP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
   reflect (exists p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t).
 Proof.
 apply: (iffP idP) => [|[p ->]]; last first.
   rewrite /= (map_comp (tnth t)) -{1}(map_tnth_enum t) perm_map //.
-  apply: uniq_perm_eq => [||i]; rewrite ?enum_uniq //.
+  apply: uniq_perm => [||i]; rewrite ?enum_uniq //.
     by apply/injectiveP; apply: perm_inj.
   by rewrite mem_enum -[i](permKV p) image_f.
 case: n => [|n] in t *; last have x0 := tnth t ord0.
-  rewrite tuple0 => /perm_eq_small-> //.
+  rewrite tuple0 => /perm_small_eq-> //.
   by exists 1; rewrite [mktuple _]tuple0.
-case/(perm_eq_iotaP x0); rewrite size_tuple => Is eqIst ->{s}.
-have uniqIs: uniq Is by rewrite (perm_eq_uniq eqIst) iota_uniq.
-have szIs: size Is == n.+1 by rewrite (perm_eq_size eqIst) !size_tuple.
+case/(perm_iotaP x0); rewrite size_tuple => Is eqIst ->{s}.
+have uniqIs: uniq Is by rewrite (perm_uniq eqIst) iota_uniq.
+have szIs: size Is == n.+1 by rewrite (perm_size eqIst) !size_tuple.
 have pP i : tnth (Tuple szIs) i < n.+1.
-  by rewrite -[_ < _](mem_iota 0) -(perm_eq_mem eqIst) mem_tnth.
+  by rewrite -[_ < _](mem_iota 0) -(perm_mem eqIst) mem_tnth.
 have inj_p: injective (fun i => Ordinal (pP i)).
   by apply/injectiveP/(@map_uniq _ _ val); rewrite -map_comp map_tnth_enum.
 exists (perm inj_p); rewrite -[Is]/(tval (Tuple szIs)); congr (tval _).
@@ -577,5 +577,6 @@ End LiftPerm.
 
 Prenex Implicits lift_perm lift_permK.
 
-
+Notation tuple_perm_eqP :=
+  (deprecate tuple_perm_eqP tuple_permP) (only parsing).