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

CHANGELOG.md

@@ -16,16 +16,51 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   warning for `old_id`; `Import Deprecation.Silent` turns off those warnings,
   `Import Deprecation.Reject` raises errors instead of only warning.
 
+- `filter_nseq`, `count_nseq`, `mem_nseq`,
+  `rcons_inj`, `rcons_injl`, `rcons_injr`, `nthK`, `sumn_rot`.
+
+- some `perm_eq` lemmas: `perm_cat[lr]`, `perm_nilP`,
+  `perm_consP`, `perm_has`, `perm_flatten`, `perm_sumn`.
+
+- computing (efficiently) (item, multiplicity) tallies of sequences over an
+  `eqType`: `tally s`, `incr_tally bs x`, `bs \is a wf_tally`, `tally_seq bs`.
+
 ### Changed
 
 - definition of `PredType` which now takes only a `P -> pred T` function;
   definition of `simpl_rel` to improve simplification by `inE`. Both these
   changes will be in the Coq 8.11 SSReflect core library.
 
+- definition of `permutations s` now uses an optimal algorithm (in space _and_
+  time) to generate all permutations of s back-to-front, using `tally s`.
+
 ### Renamed
 
+- `perm_eqP` -> `permP` (`seq.permP` if `perm.v` is also imported)
+- `perm_eqlP` -> `permPl`
+- `perm_eqrP` -> `permPr`
+- `perm_eqlE` -> `permEl`
+- `perm_eq_refl` -> `perm_refl`
+- `perm_eq_sym` -> `perm_sym`
+- `perm_eq_trans` -> `perm_trans`
+- `perm_eq_size` -> `perm_size`
+- `perm_eq_mem` -> `perm_mem`
+- `perm_eq_uniq` -> perm_uniq`
+- `perm_eq_rev` -> `perm_rev`
+- `perm_eq_flatten` -> `perm_flatten`
+- `perm_eq_all` -> `perm_all`
+- `perm_eq_small` -> `perm_small_eq`
+- `perm_eq_nilP` -> `perm_nilP`
+- `perm_eq_consP` -> `perm_consP`
 - `leq_size_perm` -> `uniq_min_size` (permuting conclusions)
 - `perm_uniq` -> `eq_uniq` (permuting assumptions)
+  --> beware `perm_uniq` now means `perm_eq_uniq`
+- `uniq_perm_eq` -> `uniq_perm`
+- `perm_eq_iotaP` -> `perm_iotaP`
+- `perm_undup_count` -> `perm_count_undup`
+- `tuple_perm_eqP` -> `tuple_permP`
+- `eq_big_perm` -> `perm_big`
+- `perm_eq_abelian_type` -> `abelian_type_pgroup`
 
 ### Misc
 

mathcomp/Make

@@ -95,3 +95,5 @@ test_suite/hierarchy_test.v
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overridden
+-arg -w -arg -duplicate-clear
+-arg -w -arg -ambiguous-paths

mathcomp/_CoqProject

@@ -4,3 +4,4 @@
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overridden
+-arg -w -arg -duplicate-clear

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.

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).

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)).

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.
 

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 :

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.

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 //.

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.

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.

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).
 

mathcomp/solvable/abelian.v

@@ -1713,11 +1713,11 @@ rewrite orderXdiv ?pfactor_dvdn ?leq_subr // -(dvdn_pmul2r m_gt0).
 by rewrite -expnS -subSn // subSS divnK pfactor_dvdn ?leq_subr.
 Qed.
 
-Lemma perm_eq_abelian_type p b G :
+Lemma abelian_type_pgroup p b G :
     p.-group G -> \big[dprod/1]_(x <- b) <[x]> = G -> 1 \notin b ->
-  perm_eq (map order b) (abelian_type G).
+  perm_eq (abelian_type G) (map order b).
 Proof.
-move: b => b1 pG defG1 ntb1.
+rewrite perm_sym; move: b => b1 pG defG1 ntb1.
 have cGG: abelian G.
   elim: (b1) {pG}G defG1 => [_ <-|x b IHb G]; first by rewrite big_nil abelian1.
   rewrite big_cons; case/dprodP=> [[_ H _ defH]] <-; rewrite defH => cxH _.
@@ -1992,8 +1992,8 @@ suffices def_atG: abelian_type K ++ abelian_type H =i abelian_type G.
   by rewrite size_abelian_type // -abelian_type_homocyclic.
 have [bK defK atK] := abelian_structure cKK.
 have [bH defH atH] := abelian_structure cHH.
-apply: perm_eq_mem; rewrite -atK -atH -map_cat.
-apply: (perm_eq_abelian_type pG); first by rewrite big_cat defK defH.
+apply/perm_mem; rewrite perm_sym -atK -atH -map_cat.
+apply: (abelian_type_pgroup pG); first by rewrite big_cat defK defH.
 have: all [pred m | m > 1] (map order (bK ++ bH)).
   by rewrite map_cat all_cat atK atH !abelian_type_gt1.
 by rewrite all_map (eq_all (@order_gt1 _)) all_predC has_pred1.

mathcomp/solvable/extremal.v

@@ -2322,7 +2322,7 @@ have{defZN2} strZN2: \big[dprod/1]_(z <- [:: xpn3; y]) <[z]> = 'Z('Ohm_2(N)).
   by rewrite unlock /= dprodg1.
 rewrite -size_abelian_type ?center_abelian //.
 have pZN2: p.-group 'Z('Ohm_2(N)) by rewrite (pgroupS _ pN) // subIset ?Ohm_sub.
-rewrite -(perm_eq_size (perm_eq_abelian_type pZN2 strZN2 _)) //= !inE.
+rewrite (perm_size (abelian_type_pgroup pZN2 strZN2 _)) //= !inE.
 rewrite !(eq_sym 1) -!order_eq1 oy orderE oX2.
 by rewrite (eqn_exp2l 2 0) // (eqn_exp2l 1 0).
 Qed.

mathcomp/solvable/jordanholder.v

@@ -179,9 +179,9 @@ elim: {G}#|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => cs1 cs2.
 have [G1 | ntG] := boolP (G :==: 1).
   have -> : s1 = [::] by apply/eqP; rewrite -(trivg_comps cs1).
   have -> : s2 = [::] by apply/eqP; rewrite -(trivg_comps cs2).
-  by rewrite /= perm_eq_refl.
+  by rewrite /= perm_refl.
 have [sG | nsG] := boolP (simple G).
-  by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_eq_refl.
+  by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_refl.
 case es1: s1 cs1 => [|N1 st1] cs1.
   by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG.
 case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}.
@@ -228,9 +228,9 @@ have i3 : perm_eq fG1 fG2.
   rewrite (@perm_catCA _ [::_] [::_]) /mksrepr.
   rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1).
   rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2).
-  exact: perm_eq_refl.
-apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym.
-by apply: perm_eq_trans i2; apply: perm_eq_refl.
+  exact: perm_refl.
+apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym.
+by apply: perm_trans i2; apply: perm_refl.
 Qed.
 
 End CompositionSeries.
@@ -593,11 +593,11 @@ elim: {G} #|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => hsD cs1 cs2.
 case/orP: (orbN (G :==: 1)) => [tG | ntG].
   have -> : s1 = [::] by apply/eqP; rewrite -(trivg_acomps cs1).
   have -> : s2 = [::] by apply/eqP; rewrite -(trivg_acomps cs2).
-  by rewrite /= perm_eq_refl.
+  by rewrite /= perm_refl.
 case/orP: (orbN (asimple to G))=> [sG | nsG].
   have -> : s1 = [:: 1%G ] by apply/(asimple_acompsP cs1).
   have -> : s2 = [:: 1%G ] by apply/(asimple_acompsP cs2).
-  by rewrite /= perm_eq_refl.
+  by rewrite /= perm_refl.
 case es1: s1 cs1 => [|N1 st1] cs1.
   by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG.
 case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}.
@@ -667,9 +667,9 @@ have i3 : perm_eq fG1 fG2.
   rewrite (@perm_catCA _ [::_] [::_]) /mksrepr.
   rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1).
   rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2).
-  exact: perm_eq_refl.
-apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym.
-by apply: perm_eq_trans i2; apply: perm_eq_refl.
+  exact: perm_refl.
+apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym.
+by apply: perm_trans i2; apply: perm_refl.
 Qed.
 
 End StrongJordanHolder.