module Perms where
open import Basics
open import Atoms
Perm = List (Atom × Atom)
ι : Perm
ι = []
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)
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≡
}
invPerm : Perm → Perm
invPerm [] = []
invPerm ((a , b) :: the_rest) = (invPerm (the_rest)) ++ [ (a , b) ]
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₃)))
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 ▪))
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) ▪ ))))
PPAct : Perm → Perm → Perm
PPAct p p' = (invPerm p) ++ (p' ++ p)
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) ▪ )))))))))))
ιp : (p : Perm) → pEquiv (PPAct ι p) p
ιp p = λ {x} → ( PermAct (p ++ ι) x ≡< cong (λ z → PermAct z x) (p++[]≡p p) >
((PermAct p x) ▪))
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