module Perms where

{-
This file develops the basic definitions and properties
pertaining to permutations
-}

open import Basics
open import Atoms

--------------------------------------------------------------------------------------------------------------
--Definition of Perm
-------------------------------------------------------------------------------------------------------------

Perm = List (Atom × Atom)

------------------------------------------------------------------------------------------------------------
--Identity permutation
------------------------------------------------------------------------------------------------------------

ι : Perm
ι = []

---------------------------------------------------------------------------------------------------------
--Permutation action on atoms and relation representing intensional similarilty
--------------------------------------------------------------------------------------------------------

PermAct : Perm  Atom  Atom
PermAct [] a = a
PermAct (aa :: the_rest) a = PermAct the_rest (swap aa a)

pEquiv : Perm  Perm  Set
pEquiv p₁ p₂ =  {x}  (PermAct p₁ x)  (PermAct p₂ x)

-------------------------------------------------------------------------------------------------------
--The relation is an equivalence relation and so we have a setoid
------------------------------------------------------------------------------------------------------

P≡≈ : (π : Perm)  pEquiv π π
P≡≈ π = λ {x}  refl

p≈p : Reflexive Perm pEquiv
p≈p = refl

≈Sym : Symmetric Perm pEquiv
≈Sym = λ {p q}   (p≈q : pEquiv p q)   {x}  (sym (p≈q {x}))))

≈Trans : Transitive Perm pEquiv
≈Trans = λ {p q r}   (p≈q : pEquiv p q)   (q≈r : pEquiv q r)   {x}  (PermAct p x ≡< p≈q {x} > q≈r {x}))))

pEquiv≡ : isEquivalence Perm pEquiv
pEquiv≡ = record { Reflex = λ {p}  p≈p {p}
; Symm =  λ {p q}   ≈Sym {p} {q}
; Trans = λ {p q r}  ≈Trans {p}{q}{r}
}

PermSetoid : Setoid
PermSetoid = record { Carrier = Perm
;  ≈ₛ = pEquiv
; Eqv = pEquiv≡
}

-----------------------------------------------------------------------------------------------------------
--Inverse of permutation
-----------------------------------------------------------------------------------------------------------

invPerm : Perm  Perm
invPerm []  = []
invPerm ((a , b) :: the_rest) =  (invPerm (the_rest)) ++ [ (a , b) ]

---------------------------------------------------------------------------------------------------------
--Lemmas to prove that Perm is a group
--------------------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------------------
--Associativity
----------------------------------------------------------------------------------------------------

PermAssoc : (p₁ p₂ p₃ : Perm)  (p₁ ++ (p₂ ++ p₃))  ((p₁ ++ p₂) ++ p₃)
PermAssoc [] p₂ p₃ = refl
PermAssoc (p :: ps) p₂ p₃ rewrite PermAssoc ps p₂ p₃ = refl

PermAssoc≈ : assoc {Perm} {_++_} {pEquiv}
PermAssoc≈ = λ p₁ p₂ p₃   {x}  (cong   y  PermAct y x) (PermAssoc p₁ p₂ p₃)))

-------------------------------------------------------------------------------------------------------
--Identity axioms
------------------------------------------------------------------------------------------------------

p++[]≡p : (p : Perm)  (p ++ [])  p
p++[]≡p [] = refl
p++[]≡p (x :: xs) rewrite p++[]≡p xs = refl

p₁++p₂≡p₂p₁ :  {a}  (p₁ p₂ : Perm)  PermAct (p₁ ++ p₂) a  PermAct p₂ (PermAct p₁ a)
p₁++p₂≡p₂p₁ [] p₂ = refl
p₁++p₂≡p₂p₁ {a} ((p , q) :: ps) p₂ with AtEqDec a p
p₁++p₂≡p₂p₁ {a} ((.a , q) :: ps) p₂ | yes refl rewrite p₁++p₂≡p₂p₁ {q} ps p₂ = refl
... | no _  with AtEqDec a q
p₁++p₂≡p₂p₁ {a} ((p , .a) :: ps) p₂ | no _ | yes refl rewrite p₁++p₂≡p₂p₁ {p} ps p₂ = refl
p₁++p₂≡p₂p₁ {a} ((p , q) :: ps) p₂ | no _ | no _ rewrite p₁++p₂≡p₂p₁ {a} ps p₂ = refl

p∘p⁻¹Act : (p : Perm)   {a}   PermAct (p ++ (invPerm p)) a  a
p∘p⁻¹Act  []  = refl
p∘p⁻¹Act  ((p , q) :: xs) {a}  rewrite PermAssoc xs (invPerm xs) [ (p , q)]  with AtEqDec a p
p∘p⁻¹Act  ((p , q) :: xs)  {.p} | yes refl rewrite p₁++p₂≡p₂p₁ {q} (xs ++ (invPerm xs)) [ (p , q) ] |  p∘p⁻¹Act xs {q} = swapabb≡a p q
p∘p⁻¹Act  ((p , q) :: xs)  {a} | no _ with AtEqDec a q
p∘p⁻¹Act ((p , q) :: xs) {.q} | no _ | yes refl rewrite p₁++p₂≡p₂p₁ {p} (xs ++ (invPerm xs)) [ (p , q) ] | p∘p⁻¹Act  xs {p} = swapaba≡b p q
p∘p⁻¹Act  ((p , q) :: xs) {a} | no f | no g  rewrite p₁++p₂≡p₂p₁ {a} (xs ++ (invPerm xs)) [ (p , q) ] | p∘p⁻¹Act xs {a} = swapabc≡c p q a f g

invTail :  {aa}  (p : Perm)  (invPerm (p ++ ([ aa ]) ))  (aa :: (invPerm p))
invTail [] = refl
invTail {aa} (x :: xs) rewrite invTail {aa} xs =  refl

p⁻¹⁻¹≡p : (p : Perm)  invPerm (invPerm p)  p
p⁻¹⁻¹≡p [] = refl
p⁻¹⁻¹≡p (x :: xs) rewrite invTail {x} (invPerm xs) | p⁻¹⁻¹≡p xs = refl

p⁻¹∘pAct : (p : Perm)   {a}  PermAct ((invPerm p) ++ p) a  a
p⁻¹∘pAct p {a} = (PermAct ((invPerm p) ++ p) a) ≡< congf (cong PermAct ( cong  x  (invPerm p) ++ x) (sym (p⁻¹⁻¹≡p p)))) a  > (p∘p⁻¹Act (invPerm p) {a})

pp⁻¹≡ι : (p : Perm)  pEquiv (p ++ (invPerm p)) ι
pp⁻¹≡ι p = λ {x}  (PermAct (p ++ (invPerm p)) x ) ≡< p∘p⁻¹Act p {x} > ((PermAct ι x) )

p⁻¹p≡ι : (p : Perm)  pEquiv ((invPerm p) ++ p) ι
p⁻¹p≡ι p = λ {x}  (PermAct ((invPerm p) ++ p) x ) ≡< p⁻¹∘pAct p {x} > ((PermAct ι x) )

pp⁻¹a≡a : (p : Perm)  (a : Atom)  (PermAct p (PermAct (invPerm p) a))  a
pp⁻¹a≡a p a = (PermAct p (PermAct (invPerm p) a))  ≡< sym (p₁++p₂≡p₂p₁ {a} (invPerm p) p) >
((PermAct ((invPerm p) ++ p) a)          ≡< p⁻¹∘pAct p {a} >
(a ))

-------------------------------------------------------------------------------------------------------------------------------------------------------------------
--Relation preserving operations
-------------------------------------------------------------------------------------------------------------------------------------------------------------------

cong++ : _++_ Preserves₂  pEquiv   pEquiv  pEquiv
cong++ = λ {p₁ p₂ q₁ q₂}   (p₁≈p₂ : pEquiv p₁ p₂)   (q₁≈q₂ : pEquiv q₁ q₂)
{x}
(PermAct (p₁ ++ q₁) x)                                              ≡< p₁++p₂≡p₂p₁ {x} p₁ q₁ >
(PermAct q₁ (PermAct p₁ x)                                       ≡< q₁≈q₂ {PermAct p₁ x} >
((PermAct q₂ (PermAct p₁ x))                                     ≡< cong  z  PermAct q₂ z) (p₁≈p₂ {x}) >
(sym (p₁++p₂≡p₂p₁ {x} p₂ q₂)))))))

p≈q⇒p⁻¹≈q⁻¹ : (p q : Perm)  (pEquiv p q)  (pEquiv (invPerm p) (invPerm q))
p≈q⇒p⁻¹≈q⁻¹ p q p≈q = λ {x}  ( PermAct (invPerm p) x ≡< sym (PermAct (invPerm p) (PermAct p (PermAct (invPerm q) x)) ≡< cong  y  PermAct (invPerm p) y)
(PermAct p (PermAct (invPerm q) x) ≡< p≈q {PermAct (invPerm q) x} >
(PermAct q (PermAct (invPerm q) x) ≡< sym (p₁++p₂≡p₂p₁ {x} (invPerm q) q) >
(PermAct ((invPerm q) ++ q) x ≡< p⁻¹∘pAct q {x} >
(x )))) > ((PermAct (invPerm p) x) )) >
( PermAct (invPerm p) (PermAct p (PermAct (invPerm q) x)) ≡< sym (p₁++p₂≡p₂p₁ {PermAct (invPerm q) x} p (invPerm p)) >
( PermAct (p ++ (invPerm p)) (PermAct (invPerm q) x)  ≡< p∘p⁻¹Act p {(PermAct (invPerm q) x)} >
( ( PermAct (invPerm q) x)  ))))

-----------------------------------------------------------------------------------------------------------------------------------------------------------
--Lemmas to prove that Perm is a Perm-Set with conjugation action
-----------------------------------------------------------------------------------------------------------------------------------------------------------

--------------------------------------------------------------------------------------------------------------------------------------------------------------
--conjugation action
--------------------------------------------------------------------------------------------------------------------------------------------------------------
PPAct : Perm  Perm  Perm
PPAct p p' = (invPerm p) ++ (p' ++ p)

----------------------------------------------------------------------------------------------------------------------------------------------------------
--associativity axiom for group action
----------------------------------------------------------------------------------------------------------------------------------------------------------

p₁p₂⁻¹≈p₂⁻¹p₁⁻¹ : (p₁ p₂ : Perm)  pEquiv (invPerm (p₁ ++ p₂))  ((invPerm p₂) ++ (invPerm p₁))
p₁p₂⁻¹≈p₂⁻¹p₁⁻¹ p₁ p₂ = λ {x}
( PermAct (invPerm (p₁ ++ p₂)) x
≡< sym ( (PermAct (invPerm p₁) (PermAct (invPerm p₂) x)) ≡< cong  y  PermAct (invPerm p₁) y)
(PermAct (invPerm p₂) x                                    ≡< cong  z  PermAct (invPerm p₂) z)
(x                                                                                             ≡< sym (p⁻¹∘pAct (p₁ ++ p₂) {x} ) >
(PermAct ((invPerm (p₁ ++ p₂)) ++ (p₁ ++ p₂)) x                  ≡< p₁++p₂≡p₂p₁ {x} (invPerm (p₁ ++ p₂)) (p₁ ++ p₂) >
((PermAct (p₁ ++ p₂) (PermAct (invPerm (p₁ ++ p₂)) x)) )))
>
(PermAct (invPerm p₂) (PermAct (p₁ ++ p₂) (PermAct (invPerm (p₁ ++ p₂)) x))               ≡< sym ( p₁++p₂≡p₂p₁ {PermAct (invPerm (p₁ ++ p₂)) x} (p₁ ++ p₂) (invPerm p₂)) >
( PermAct ((p₁ ++ p₂) ++ (invPerm p₂)) (PermAct (invPerm (p₁ ++ p₂)) x)                      ≡< cong  w  PermAct w (PermAct (invPerm (p₁ ++ p₂)) x))
(sym (PermAssoc p₁ p₂ (invPerm p₂))) >
( PermAct (p₁ ++ (p₂ ++ (invPerm p₂))) (PermAct (invPerm (p₁ ++ p₂)) x)                      ≡< p₁++p₂≡p₂p₁ {PermAct (invPerm (p₁ ++ p₂)) x} p₁ (p₂ ++ (invPerm p₂)) >
( PermAct (p₂ ++ (invPerm p₂)) (PermAct p₁ (PermAct (invPerm (p₁ ++ p₂)) x))              ≡< p∘p⁻¹Act p₂ {PermAct p₁ (PermAct (invPerm (p₁ ++ p₂)) x)} >
( (PermAct p₁ (PermAct (invPerm (p₁ ++ p₂)) x)) ))))))
>
(PermAct (invPerm p₁) (PermAct p₁ (PermAct (invPerm (p₁ ++ p₂)) x))                                ≡< sym (p₁++p₂≡p₂p₁ {PermAct (invPerm (p₁ ++ p₂)) x} p₁ (invPerm p₁)) >
(PermAct (p₁ ++ (invPerm p₁)) (PermAct (invPerm (p₁ ++ p₂)) x)                                        ≡< p∘p⁻¹Act p₁ {PermAct (invPerm (p₁ ++ p₂)) x} >
((PermAct (invPerm (p₁ ++ p₂)) x) )))
) >
(PermAct (invPerm p₁) (PermAct (invPerm p₂) x) ≡< sym (p₁++p₂≡p₂p₁ {x} (invPerm p₂) (invPerm p₁)) >
((PermAct ((invPerm p₂) ++ (invPerm p₁)) x) )))

p₁++p₂≡p₂p₁p : (p₁ p₂ : Perm)  (p : Perm)  pEquiv (PPAct (p₁ ++ p₂) p) (PPAct p₂ (PPAct p₁ p))
p₁++p₂≡p₂p₁p p₁ p₂ p = λ {x}  (PermAct ((invPerm (p₁ ++ p₂)) ++ (p ++ (p₁ ++ p₂))) x                                ≡< p₁++p₂≡p₂p₁ {x} (invPerm (p₁ ++ p₂)) (p ++ (p₁ ++ p₂)) >
( PermAct (p ++ (p₁ ++ p₂)) (PermAct (invPerm (p₁ ++ p₂)) x)                        ≡< cong  z  PermAct (p ++ (p₁ ++ p₂)) z)  ((p₁p₂⁻¹≈p₂⁻¹p₁⁻¹ p₁ p₂) {x}) >
( PermAct (p ++ (p₁ ++ p₂)) (PermAct ((invPerm p₂) ++ (invPerm p₁)) x)        ≡< sym (p₁++p₂≡p₂p₁ {x} ((invPerm p₂) ++ (invPerm p₁)) (p ++ (p₁ ++ p₂))) >
( PermAct (((invPerm p₂) ++ (invPerm p₁)) ++ (p ++ (p₁ ++ p₂))) x   ≡< sym (cong  w  PermAct w x) (PermAssoc (invPerm p₂) (invPerm p₁) (p ++ (p₁ ++ p₂)))) >
( PermAct ((invPerm p₂) ++ ((invPerm p₁) ++ (p ++ (p₁ ++ p₂)))) x                ≡< p₁++p₂≡p₂p₁ {x} (invPerm p₂) ((invPerm p₁) ++ (p ++ (p₁ ++ p₂))) >
( PermAct ((invPerm p₁) ++ (p ++ (p₁ ++ p₂))) (PermAct (invPerm p₂) x)          ≡< p₁++p₂≡p₂p₁ {PermAct (invPerm p₂) x} (invPerm p₁) (p ++ (p₁ ++ p₂)) >
( PermAct (p ++ (p₁ ++ p₂)) (PermAct (invPerm p₁) (PermAct (invPerm p₂) x))  ≡< cong  w  PermAct w (PermAct (invPerm p₁) (PermAct (invPerm p₂) x)))
(PermAssoc p p₁ p₂) >
( PermAct ((p ++ p₁) ++ p₂) (PermAct (invPerm p₁) (PermAct (invPerm p₂) x))  ≡< sym (p₁++p₂≡p₂p₁ {PermAct (invPerm p₂) x} (invPerm p₁) ((p ++ p₁) ++ p₂)) >
( PermAct ((invPerm p₁) ++ ((p ++ p₁) ++ p₂)) (PermAct (invPerm p₂) x)   ≡< cong  w  PermAct w (PermAct (invPerm p₂) x)) (PermAssoc (invPerm p₁) (p ++ p₁) p₂) >
( PermAct (((invPerm p₁) ++ (p ++ p₁)) ++ p₂) (PermAct (invPerm p₂) x)   ≡< sym (p₁++p₂≡p₂p₁ {x} (invPerm p₂) (((invPerm p₁) ++ (p ++ p₁)) ++ p₂)) >
( (PermAct ((invPerm p₂) ++ (((invPerm p₁) ++ (p ++ p₁)) ++ p₂)) x)  )))))))))))

---------------------------------------------------------------------------------------------------------------------------------------------------------
--identity axiom for group action
---------------------------------------------------------------------------------------------------------------------------------------------------------

ιp : (p : Perm)  pEquiv (PPAct ι p) p
ιp p = λ {x}  ( PermAct (p ++ ι) x         ≡< cong  z  PermAct z x) (p++[]≡p p) >
((PermAct p x) ))

--------------------------------------------------------------------------------------------------------------------------------------------------------
--Action respects equivalence relation
--------------------------------------------------------------------------------------------------------------------------------------------------------

resPP : (π₁ π₂ p₁ p₂ : Perm)  (π₁≈π₂ : pEquiv π₁ π₂)  (p₁≈p₂ : pEquiv p₁ p₂)  pEquiv (PPAct π₁ p₁) (PPAct π₂ p₂)
resPP π₁ π₂ p₁ p₂ π₁≈π₂ p₁≈p₂  = λ {x}  PermAct ((invPerm π₁) ++ (p₁ ++ π₁)) x ≡< p₁++p₂≡p₂p₁ {x} (invPerm π₁) (p₁ ++ π₁) >
( PermAct (p₁ ++ π₁) (PermAct (invPerm π₁) x) ≡< cong  w  PermAct (p₁ ++ π₁) w) ((p≈q⇒p⁻¹≈q⁻¹ π₁ π₂ π₁≈π₂) {x}) >
( PermAct (p₁ ++ π₁) (PermAct (invPerm π₂) x) ≡< (cong++ {p₁}{p₂}{π₁}{π₂} p₁≈p₂ π₁≈π₂) {PermAct (invPerm π₂) x} >
( PermAct (p₂ ++ π₂) (PermAct (invPerm π₂) x) ≡< sym (p₁++p₂≡p₂p₁ {x} (invPerm π₂) (p₂ ++ π₂)) >
( (PermAct ((invPerm π₂) ++ (p₂ ++ π₂)) x)  ))))

p≈≡ :  {p q}  p  q  pEquiv p q
p≈≡ refl = λ {x}  refl

-----------------------------------------------------------------------------------------------------------------------------------------------------