Library perm

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
This file contains the definition and properties  associated to the    
group of permutations.                                                 
  {perm T} == the permutation of a finite type T                       
                       (i.e. an injective function from T to T)        
  'S_n == the permutations of {0,.., n-1}                              
  perm_on A u <=> u is a permutation on T where only the elements of a 
                                a subset A of T are affected           
  tperm x y == the transposition of x, y                               
  aperm x s == s(x)                                                    
  pcycle s x == the set of all elements that are in the same cycle     
                of permutation s as x                                  
  pcycles s == the set of cycles of permutation s                      
  odd_perm s <=> s is an odd permutation                               
  dpair x <=> x is a pair of distinct objects                          
Permutations are coerced to the underlying function.                   
Canonical structures are defined allowing permutations to be an eqType,
choiceType, countType, finType, subType, finGroupType (permutations    
with the composition form a group, therefore all generic group         
notations are inherited: 1 == identity permutation, * == composition,  
^-1 == inverse permutation).                                           
Lemmas are given to establish the common properties for permutations.  

Import Prenex Implicits.

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

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

Lemma perm_proof : forall 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").

Notation Local fun_of_perm_def := (fun T (u : perm_type T) => val u : T -> T).
Notation Local perm_def := (fun T f injf => Perm (@perm_proof T f injf)).

Module Type PermDefSig.
Parameter fun_of_perm : forall T, perm_type T -> T -> T.
Coercion fun_of_perm : perm_type >-> Funclass.
Parameter perm : forall (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. Qed.

Lemma permE : perm = perm_def. Qed.

End PermDef.

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

Section Theory.

Variable T : finType.

Notation pT := {perm T}.

Lemma permP : forall u v : pT, u =1 v <-> u = v.

Lemma pvalE : forall u : pT, pval u = u :> (T -> T).

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

Lemma perm_inj : forall u : pT, injective u.

Implicit Arguments perm_inj [].

Hint Resolve perm_inj.

Lemma perm_onto : forall u : pT, codom u =i predT.

Definition perm_one := perm (@inj_id T).

Lemma perm_invK : forall u : pT, cancel (fun x => iinv (perm_onto u x)) u.

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

Definition perm_mul u v := perm (inj_comp (perm_inj v) (perm_inj u)).

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 Structure perm_baseFinGroupType :=
  Eval hnf in BaseFinGroupType perm_of_baseFinGroupMixin.
Canonical Structure perm_finGroupType :=
  @FinGroupType perm_baseFinGroupType perm_invP.

Canonical Structure perm_of_baseFinGroupType :=
  Eval hnf in [baseFinGroupType of pT].
Canonical Structure perm_of_finGroupType :=
  Eval hnf in [finGroupType of pT].

Lemma perm1 : forall x, (1 : pT) x = x.

Lemma permM : forall (s1 s2 : pT) x, (s1 * s2) x = s2 (s1 x).

Lemma permK : forall s : pT, cancel s s^-1.

Lemma permKV : forall s : pT, cancel s^-1 s.

Lemma permJ : forall (s t : pT) x, (s ^ t) (t x) = t (s x).

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

Definition perm_on (A : {set T}) : pred pT :=
  fun u => [pred x | u x != x] \subset A.

Lemma perm_closed : forall A u x, perm_on A u -> (u x \in A) = (x \in A).

Lemma perm_on1 : forall H, perm_on H 1.

Lemma perm_onM : forall H f g,
  perm_on H f -> perm_on H g -> perm_on H (f * g).

Lemma out_perm : forall H f x, perm_on H f -> x \notin H -> f x = x.

Lemma tperm_proof : forall x y : T,
  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) : 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 : forall x y z, tperm_spec x y z (tperm x y z).

Lemma tpermL : forall x y : T, tperm x y x = y.

Lemma tpermR : forall x y : T, tperm x y y = x.

Lemma tpermD : forall x y z : T, x != z -> y != z -> tperm x y z = z.

Lemma tpermC : forall x y : T, tperm x y = tperm y x.

Lemma tperm1 : forall x : T, tperm x x = 1.

Lemma tpermK : forall x y : T, involutive (tperm x y).

Lemma tpermKg : forall x y : T, involutive (mulg (tperm x y)).

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

Lemma tperm2 : forall x y : T, tperm x y * tperm x y = 1.

Lemma card_perm : forall A : {set T}, #|perm_on A| = fact #|A|.

End Theory.

Lemma inj_tperm : forall (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 : forall (T : finType) x y (s : {perm T}),
  (tperm x y) ^ s = tperm (s x) (s y).

Section PermutationParity.

Variable T : finType.

Implicit Type s : {perm T}.
Implicit Types x y z : 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 : forall x a, aperm x a = a x. Qed.

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

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

Lemma pcycle_traject : forall s x, pcycle s x =i traject s x #[s].

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

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

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

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

Lemma odd_perm1 : odd_perm 1 = false.

Lemma odd_mul_tperm : forall x y s,
  odd_perm (tperm x y * s) = (x != y) (+) odd_perm s.

Lemma odd_tperm : forall 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 : forall s : {perm T},
  {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.

Lemma odd_perm_prod : forall 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 : forall s, odd_perm s^-1 = odd_perm s.

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

End PermutationParity.

Coercion odd_perm : perm_type >-> bool.
Implicit Arguments dpair [eT].