(Joint Center)Library MathComp.perm

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype.
Require Import tuple finfun bigop finset binomial fingroup.

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 TT}) & 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 : TT) : injective finjectiveb (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").

Notation Local fun_of_perm_def := (fun T (u : perm_type T) ⇒ val u : TT).
Notation Local perm_def := (fun T f injfPerm (@perm_proof T f injf)).

Module Type PermDefSig.
Parameter fun_of_perm : T, perm_type TTT.
Parameter perm : (T : finType) (f : TT), 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 :> (TT).

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

Lemma perm_inj s : injective s.

Implicit Arguments perm_inj [].
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 sperm_on H tperm_on H (s × t).

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

Lemma im_perm_on u S : perm_on S uu @: 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 : TType :=
  | 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 != zy != ztperm 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 : TT') x y z :
  injective ff (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].
Implicit Arguments dpair [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 tsodd_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.
Implicit Arguments dpair [eT].

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.