# Library mathcomp.fingroup.perm

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

Require Import mathcomp.ssreflect.ssreflect.

This file contains the definition and properties associated to the group of permutations of an arbitrary finite type. {perm T} == the type of permutations of a finite type T, i.e., injective (finite) functions from T to T. Permutations coerce to CiC functions. 'S_n == the set of all permutations of 'I_n, i.e., of {0,.., n-1} perm_on A u == u is a permutation with support A, i.e., u only displaces elements of A (u x != x implies x \in A). tperm x y == the transposition of x, y. aperm x s == the image of x under the action of the permutation s. := s x pcycle s x == the set of all elements that are in the same cycle of the permutation s as x, i.e., {x, s x, (s ^+ 2) x, ...}. pcycles s == the set of all the cycles of the permutation s. (s : bool) == s is an odd permutation (the coercion is called odd_perm). dpair u == u is a pair (x, y) of distinct objects (i.e., x != y). lift_perm i j s == the permutation obtained by lifting s : 'S_n.-1 over (i |-> j), that maps i to j and lift i k to lift j (s k). Canonical structures are defined allowing permutations to be an eqType, choiceType, countType, finType, subType, finGroupType; permutations with composition form a group, therefore inherit all generic group notations: 1 == identity permutation, * == composition, ^-1 == inverse permutation.

Set Implicit Arguments.

Import GroupScope.

Section PermDefSection.

Variable T : finType.

Inductive perm_type : predArgType :=
Perm (pval : {ffun T T}) & injectiveb pval.
Definition pval p := let: Perm f _ := p in f.
Definition perm_of of phant T := perm_type.
Identity Coercion type_of_perm : perm_of >-> perm_type.

Notation pT := (perm_of (Phant T)).

Canonical perm_subType := Eval hnf in [subType for pval].
Definition perm_eqMixin := Eval hnf in [eqMixin of perm_type by <:].
Canonical perm_eqType := Eval hnf in EqType perm_type perm_eqMixin.
Definition perm_choiceMixin := [choiceMixin of perm_type by <:].
Canonical perm_choiceType := Eval hnf in ChoiceType perm_type perm_choiceMixin.
Definition perm_countMixin := [countMixin of perm_type by <:].
Canonical perm_countType := Eval hnf in CountType perm_type perm_countMixin.
Canonical perm_subCountType := Eval hnf in [subCountType of perm_type].
Definition perm_finMixin := [finMixin of perm_type by <:].
Canonical perm_finType := Eval hnf in FinType perm_type perm_finMixin.
Canonical perm_subFinType := Eval hnf in [subFinType of perm_type].

Canonical perm_for_subType := Eval hnf in [subType of pT].
Canonical perm_for_eqType := Eval hnf in [eqType of pT].
Canonical perm_for_choiceType := Eval hnf in [choiceType of pT].
Canonical perm_for_countType := Eval hnf in [countType of pT].
Canonical perm_for_subCountType := Eval hnf in [subCountType of pT].
Canonical perm_for_finType := Eval hnf in [finType of pT].
Canonical perm_for_subFinType := Eval hnf in [subFinType of pT].

Lemma perm_proof (f : T T) : injective f injectiveb (finfun f).

End PermDefSection.

Notation "{ 'perm' T }" := (perm_of (Phant T))
(at level 0, format "{ 'perm' T }") : type_scope.

Notation "''S_' n" := {perm 'I_n}
(at level 8, n at level 2, format "''S_' n").

Module Type PermDefSig.
Parameter fun_of_perm : T, perm_type T T T.
Parameter perm : (T : finType) (f : T T), injective f {perm T}.
Axiom fun_of_permE : fun_of_perm = fun_of_perm_def.
Axiom permE : perm = perm_def.
End PermDefSig.

Module PermDef : PermDefSig.
Definition fun_of_perm := fun_of_perm_def.
Definition perm := perm_def.
Lemma fun_of_permE : fun_of_perm = fun_of_perm_def.
Lemma permE : perm = perm_def.
End PermDef.

Notation fun_of_perm := PermDef.fun_of_perm.
Notation "@ 'perm'" := (@PermDef.perm) (at level 10, format "@ 'perm'").
Notation perm := (@PermDef.perm _ _).
Canonical fun_of_perm_unlock := Unlockable PermDef.fun_of_permE.
Canonical perm_unlock := Unlockable PermDef.permE.
Coercion fun_of_perm : perm_type >-> Funclass.

Section Theory.

Variable T : finType.
Implicit Types (x y : T) (s t : {perm T}) (S : {set T}).

Lemma permP s t : s =1 t s = t.

Lemma pvalE s : pval s = s :> (T T).

Lemma permE f f_inj : @perm T f f_inj =1 f.

Lemma perm_inj s : injective s.

Hint Resolve perm_inj.

Lemma perm_onto s : codom s =i predT.

Definition perm_one := perm (@inj_id T).

Lemma perm_invK s : cancel (fun xiinv (perm_onto s x)) s.

Definition perm_inv s := perm (can_inj (perm_invK s)).

Definition perm_mul s t := perm (inj_comp (perm_inj t) (perm_inj s)).

Lemma perm_oneP : left_id perm_one perm_mul.

Lemma perm_invP : left_inverse perm_one perm_inv perm_mul.

Lemma perm_mulP : associative perm_mul.

Definition perm_of_baseFinGroupMixin : FinGroup.mixin_of (perm_type T) :=
FinGroup.Mixin perm_mulP perm_oneP perm_invP.
Canonical perm_baseFinGroupType :=
Eval hnf in BaseFinGroupType (perm_type T) perm_of_baseFinGroupMixin.
Canonical perm_finGroupType := @FinGroupType perm_baseFinGroupType perm_invP.

Canonical perm_of_baseFinGroupType :=
Eval hnf in [baseFinGroupType of {perm T}].
Canonical perm_of_finGroupType := Eval hnf in [finGroupType of {perm T} ].

Lemma perm1 x : (1 : {perm T}) x = x.

Lemma permM s t x : (s × t) x = t (s x).

Lemma permK s : cancel s s^-1.

Lemma permKV s : cancel s^-1 s.

Lemma permJ s t x : (s ^ t) (t x) = t (s x).

Lemma permX s x n : (s ^+ n) x = iter n s x.

Lemma im_permV s S : s^-1 @: S = s @^-1: S.

Lemma preim_permV s S : s^-1 @^-1: S = s @: S.

Definition perm_on S : pred {perm T} := fun s[pred x | s x != x] \subset S.

Lemma perm_closed S s x : perm_on S s (s x \in S) = (x \in S).

Lemma perm_on1 H : perm_on H 1.

Lemma perm_onM H s t : perm_on H s perm_on H t perm_on H (s × t).

Lemma out_perm S u x : perm_on S u x \notin S u x = x.

Lemma im_perm_on u S : perm_on S u u @: S = S.

Lemma tperm_proof x y : involutive [fun z z with x |-> y, y |-> x].

Definition tperm x y := perm (can_inj (tperm_proof x y)).

CoInductive tperm_spec x y z : T Type :=
| TpermFirst of z = x : tperm_spec x y z y
| TpermSecond of z = y : tperm_spec x y z x
| TpermNone of z x & z y : tperm_spec x y z z.

Lemma tpermP x y z : tperm_spec x y z (tperm x y z).

Lemma tpermL x y : tperm x y x = y.

Lemma tpermR x y : tperm x y y = x.

Lemma tpermD x y z : x != z y != z tperm x y z = z.

Lemma tpermC x y : tperm x y = tperm y x.

Lemma tperm1 x : tperm x x = 1.

Lemma tpermK x y : involutive (tperm x y).

Lemma tpermKg x y : involutive (mulg (tperm x y)).

Lemma tpermV x y : (tperm x y)^-1 = tperm x y.

Lemma tperm2 x y : tperm x y × tperm x y = 1.

Lemma card_perm A : #|perm_on A| = (#|A|)`!.

End Theory.

Lemma inj_tperm (T T' : finType) (f : T T') x y z :
injective f f (tperm x y z) = tperm (f x) (f y) (f z).

Lemma tpermJ (T : finType) x y (s : {perm T}) :
(tperm x y) ^ s = tperm (s x) (s y).

Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
reflect ( p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t).

Section PermutationParity.

Variable T : finType.

Implicit Types (s t u v : {perm T}) (x y z a b : T).

Note that pcycle s x is the orbit of x by < [s]> under the action aperm. Hence, the pcycle lemmas below are special cases of more general lemmas on orbits that will be stated in action.v. Defining pcycle directly here avoids a dependency of matrix.v on action.v and hence morphism.v.

Definition aperm x s := s x.
Definition pcycle s x := aperm x @: <[s]>.
Definition pcycles s := pcycle s @: T.
Definition odd_perm (s : perm_type T) := odd #|T| (+) odd #|pcycles s|.

Lemma apermE x s : aperm x s = s x.

Lemma mem_pcycle s i x : (s ^+ i) x \in pcycle s x.

Lemma pcycle_id s x : x \in pcycle s x.

Lemma uniq_traject_pcycle s x : uniq (traject s x #|pcycle s x|).

Lemma pcycle_traject s x : pcycle s x =i traject s x #|pcycle s x|.

Lemma iter_pcycle s x : iter #|pcycle s x| s x = x.

Lemma eq_pcycle_mem s x y : (pcycle s x == pcycle s y) = (x \in pcycle s y).

Lemma pcycle_sym s x y : (x \in pcycle s y) = (y \in pcycle s x).

Lemma pcycle_perm s i x : pcycle s ((s ^+ i) x) = pcycle s x.

Lemma ncycles_mul_tperm s x y : let t := tperm x y in
#|pcycles (t × s)| + (x \notin pcycle s y).*2 = #|pcycles s| + (x != y).

Lemma odd_perm1 : odd_perm 1 = false.

Lemma odd_mul_tperm x y s : odd_perm (tperm x y × s) = (x != y) (+) odd_perm s.

Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y).

Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT].

Lemma prod_tpermP s :
{ts : seq (T × T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.

Lemma odd_perm_prod ts :
all dpair ts odd_perm (\prod_(t <- ts) tperm t.1 t.2) = odd (size ts).

Lemma odd_permM : {morph odd_perm : s1 s2 / s1 × s2 >-> s1 (+) s2}.

Lemma odd_permV s : odd_perm s^-1 = odd_perm s.

Lemma odd_permJ s1 s2 : odd_perm (s1 ^ s2) = odd_perm s1.

End PermutationParity.

Coercion odd_perm : perm_type >-> bool.

Section LiftPerm.
Somewhat more specialised constructs for permutations on ordinals.

Variable n : nat.
Implicit Types i j : 'I_n.+1.
Implicit Types s t : 'S_n.

Definition lift_perm_fun i j s k :=
if unlift i k is Some k' then lift j (s k') else j.

Lemma lift_permK i j s :
cancel (lift_perm_fun i j s) (lift_perm_fun j i s^-1).

Definition lift_perm i j s := perm (can_inj (lift_permK i j s)).

Lemma lift_perm_id i j s : lift_perm i j s i = j.

Lemma lift_perm_lift i j s k' :
lift_perm i j s (lift i k') = lift j (s k') :> 'I_n.+1.

Lemma lift_permM i j k s t :
lift_perm i j s × lift_perm j k t = lift_perm i k (s × t).

Lemma lift_perm1 i : lift_perm i i 1 = 1.

Lemma lift_permV i j s : (lift_perm i j s)^-1 = lift_perm j i s^-1.

Lemma odd_lift_perm i j s : lift_perm i j s = odd i (+) odd j (+) s :> bool.

End LiftPerm.