From 5d7bd2ea2a0a28fb275da8ba2e2c0dc5a33d1034 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Wed, 8 May 2019 09:43:34 +0200
Subject: 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
---
 mathcomp/character/classfun.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/character/classfun.v')

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)).
-- 
cgit v1.2.3