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/solvable/jordanholder.v | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'mathcomp/solvable/jordanholder.v')

diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v
index 1a32bce..d191e20 100644
--- a/mathcomp/solvable/jordanholder.v
+++ b/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.
-- 
cgit v1.2.3