From a6d8fa56652b0a66f0ef525d7b8af53874e1e113 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Thu, 9 Apr 2020 16:39:37 +0200
Subject: [PATCH] reworking new proofs in perm and action and adding missing
 ones

---
 CHANGELOG_UNRELEASED.md    |  5 +++--
 mathcomp/fingroup/action.v | 19 ++++++++-----------
 mathcomp/fingroup/perm.v   | 28 ++++++++++++++++------------
 3 files changed, 27 insertions(+), 25 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 373e80a2e7..b37ba43b97 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -37,8 +37,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Added definition `cast_perm` with a group morphism canonical
   structure, and lemmas `permX_fix`, `imset_perm1`, `permS0`,
   `permS1`, `cast_perm_id`, `cast_ord_permE`, `cast_permE`,
-  `cast_permK`, `cast_permKV`, `cast_perm_inj`, `cast_perm_morphM`,
-  and `isom_cast_perm` in `perm` and `restr_perm_commute` in `action`
+  `cast_perm_comp`, `cast_permK`, `cast_permKV`, `cast_perm_inj`,
+  `cast_perm_sym`,`cast_perm_morphM`, and `isom_cast_perm` in `perm`
+  and `restr_perm_commute` in `action`.
 
 - Added `card_porbit_neq0`, `porbitP`, and `porbitPmin` in `perm`
 
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index 9631d28ea3..2d1b6e6b10 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -1682,13 +1682,11 @@ Proof. exact: im_perm_on (restr_perm_on p). Qed.
 
 Lemma restr_perm_commute s : commute (restr_perm s) s.
 Proof.
-case: (boolP (s \in 'N(S | 'P))) =>
-    [HC | /triv_restr_perm ->]; last exact: (commute_sym (commute1 _)).
-apply/permP => x; case: (boolP (x \in S)) => Hx; rewrite !permM.
-- by rewrite !restr_permE //; move: HC => /astabsP/(_ x)/= ->.
-- have:= restr_perm_on s => /out_perm Hout.
-  rewrite (Hout _ Hx) {}Hout //.
-  by move: Hx; apply contra; move: HC => /astabsP/(_ x)/= ->.
+have [sC|/triv_restr_perm->] := boolP (s \in 'N(S | 'P)); last first.
+  exact: (commute_sym (commute1 _)).
+apply/permP => x; have /= xsS := astabsP sC x; rewrite !permM.
+have [xS|xNS] := boolP (x \in S); first by rewrite ?(restr_permE) ?xsS.
+by rewrite !(out_perm (restr_perm_on _)) ?xsS.
 Qed.
 
 End RestrictPerm.
@@ -1699,10 +1697,9 @@ Variables (T : finType) (S : {set T}).
 
 Lemma SymE : Sym S = 'C(~: S | 'P).
 Proof.
-apply/setP => s; rewrite inE; apply/idP/astabP => [Hperm x | Hstab].
-- by rewrite inE /= apermE => /out_perm; apply.
-- apply/subsetP => x; rewrite unfold_in; apply contraR => H.
-  by move/(_ x): Hstab; rewrite inE /= apermE => ->.
+apply/setP => s; rewrite inE; apply/idP/astabP => [sS x|/= S_id].
+  by rewrite inE /= apermE => /out_perm->.
+by apply/subsetP => x; move=> /(contra_neqN (S_id _)); rewrite inE negbK.
 Qed.
 
 End Symmetry.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index cb770787c0..b670c15b62 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -634,14 +634,12 @@ End LiftPerm.
 
 Prenex Implicits lift_perm lift_permK.
 
-Lemma permS0 (g : 'S_0) : g = 1%g.
-Proof. by apply permP => x; case x. Qed.
+Lemma permS0 (g : 'S_0) : g = 1%g. Proof. by apply/permP => - []. Qed.
 
 Lemma permS1 (g : 'S_1) : g = 1%g.
 Proof.
-apply/permP => i; rewrite perm1.
-case: (g i) => a Ha; case: i => b Hb.
-by apply val_inj => /=; case: a b Ha Hb => [|a] [|b].
+apply/permP => i; apply: val_inj.
+by case: (X in val X) (X in val X) => [[]//= _] [[]//= _].
 Qed.
 
 Section CastSn.
@@ -657,9 +655,13 @@ Lemma cast_ord_permE m n eq_m_n (s : 'S_m) i :
 Proof. by subst m; rewrite cast_perm_id !cast_ord_id. Qed.
 
 Lemma cast_permE m n (eq_m_n : m = n) (s : 'S_m) (i : 'I_n) :
-  cast_ord eq_m_n (s (cast_ord (esym eq_m_n) i)) = cast_perm eq_m_n s i.
+  cast_perm eq_m_n s i = cast_ord eq_m_n (s (cast_ord (esym eq_m_n) i)).
 Proof. by rewrite cast_ord_permE cast_ordKV. Qed.
 
+Lemma cast_perm_comp m n p (eq_m_n : m = n) (eq_n_p : n = p) s :
+  cast_perm eq_n_p (cast_perm eq_m_n s) = cast_perm (etrans eq_m_n eq_n_p) s.
+Proof. by case: _ / eq_n_p. Qed.
+
 Lemma cast_permK m n eq_m_n :
   cancel (@cast_perm m n eq_m_n) (cast_perm (esym eq_m_n)).
 Proof. by subst m. Qed.
@@ -668,6 +670,10 @@ Lemma cast_permKV m n eq_m_n :
   cancel (cast_perm (esym eq_m_n)) (@cast_perm m n eq_m_n).
 Proof. by subst m. Qed.
 
+Lemma cast_perm_sym m n (eq_m_n : m = n) s t :
+  s = cast_perm eq_m_n t -> t = cast_perm (esym eq_m_n) s.
+Proof. by move/(canLR (cast_permK _)). Qed.
+
 Lemma cast_perm_inj m n eq_m_n : injective (@cast_perm m n eq_m_n).
 Proof. exact: can_inj (cast_permK eq_m_n). Qed.
 
@@ -675,15 +681,13 @@ Lemma cast_perm_morphM m n eq_m_n :
   {morph @cast_perm m n eq_m_n : x y / x * y >-> x * y}.
 Proof. by subst m. Qed.
 Canonical morph_of_cast_perm m n eq_m_n :=
-  Morphism (D := setT) (in2W (@cast_perm_morphM m n eq_m_n)).
+  @Morphism _ _ setT (cast_perm eq_m_n) (in2W (@cast_perm_morphM m n eq_m_n)).
 
 Lemma isom_cast_perm m n eq_m_n : isom setT setT (@cast_perm m n eq_m_n).
 Proof.
-subst m.
-apply/isomP; split.
-- apply/injmP=> i j _ _; exact: cast_perm_inj.
-- apply/setP => /= s; rewrite !inE.
-  by apply/imsetP; exists s; rewrite ?inE.
+case: {n} _ / eq_m_n; apply/isomP; split.
+  exact/injmP/(in2W (@cast_perm_inj _ _ _)).
+by apply/setP => /= s; rewrite !inE; apply/imsetP; exists s; rewrite ?inE.
 Qed.
 
 End CastSn.