```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

-----------------------------------------------------------------------------------------------------------------------------------------------------
```