module PermProp where

{-
This file provides some lemmas for low-level manipulations. It also proves some
useful properties of permutations.
-}


open import Basics
open import Atoms
open import Perms

------------------------------------------------------------------------------------------------------------
--Some lemmas for low-level manipulations
------------------------------------------------------------------------------------------------------------

des≠ : {a b : Atom}{as : List Atom}  a  (b :: as)  b  a 
des≠ (a∉as a∉aas b≠a) = b≠a

des∉ : {a b : Atom}{as : List Atom}  a  (b :: as)  a  as
des∉ (a∉as a∉aas b≠a) = a∉aas

ba=ba : {a a' : Atom}  (b : Atom)  a  a'  pEquiv [(b , a)] [(b , a')]
ba=ba {a}{.a} b refl {x} with AtEqDec x b | AtEqDec x a
ba=ba {a}{.a} b refl {.b} | yes refl | _ = refl
ba=ba {a}{.a} b refl {.a} | no _ | yes refl = refl
ba=ba {a}{.a} b refl {x} | no _ | no _ = refl


bc+cb=ι : (b c : Atom)  pEquiv ([(b , c)] ++ [(c , b)]) ι
bc+cb=ι b c {x} with AtEqDec x b | AtEqDec x c 
bc+cb=ι b c {.b} | yes refl | _ = swapaba≡b c b
bc+cb=ι b c {.c} | no _ | yes refl = swapabb≡a c b
bc+cb=ι b c {x} | no x≠b | no x≠c = swapabc≡c c b x x≠c x≠b


bc+bc=ι : (b c : Atom)  pEquiv ([(b , c)] ++ [(b , c)]) ι
bc+bc=ι b c {x} with AtEqDec x b | AtEqDec x c 
bc+bc=ι b c {.b} | yes refl | _ = swapabb≡a b c
bc+bc=ι b c {.c} | no _ | yes refl = swapaba≡b b c
bc+bc=ι b c {x} | no x≠b | no x≠c = swapabc≡c b c x x≠b x≠c


aa≈ι : (a : Atom)  pEquiv [ (a , a) ] ι
aa≈ι a {x} with AtEqDec x a
aa≈ι a {.a} | yes refl = refl
aa≈ι a {x} | no _ = refl


ab=ba : (a b : Atom)  pEquiv [(a , b)] [(b , a)]
ab=ba a b {x} with AtEqDec x a | AtEqDec x b
ab=ba a .a {.a} | yes refl | yes refl = refl
ab=ba a b {.a} | yes refl | no _ = refl
ab=ba a b {.b} | no _ | yes refl = refl
ab=ba a b {x} | no _ | no _ = refl


∉⊆₁ : {aℓ₁ aℓ₂ : List Atom}  (b : Atom)  b  (aℓ₁ ++ aℓ₂)  b  aℓ₁
∉⊆₁ {[]} {aℓ₂} b b∉aℓ = a∉[]
∉⊆₁ {(c :: cs)} {aℓ₂} b (a∉as b∉cs b≠c) = a∉as (∉⊆₁ {cs} {aℓ₂} b b∉cs) b≠c

∉⊆₂ : {aℓ₁ aℓ₂ : List Atom}  (b : Atom)  b  (aℓ₁ ++ aℓ₂)  b  aℓ₂
∉⊆₂ {[]} {aℓ₂} b b∉aℓ = b∉aℓ
∉⊆₂ {c :: cs} {aℓ₂} b (a∉as b∉cs b≠c) = ∉⊆₂ {cs} {aℓ₂} b b∉cs   


----------------------------------------------------------------------------------------------------------------
--Properties of permutations
----------------------------------------------------------------------------------------------------------------

flatten : Perm  List Atom
flatten [] = []
flatten (p :: ps) = (proj₁ p) :: ((proj₂ p) :: (flatten ps))

syma≡b⊥ : {A : Set}{a b : A}  (a  b  )  (b  a  )
syma≡b⊥ f = λ r  (f (sym r))

pa≡a : (p : Perm)  (a : Atom)  (a  (flatten p))  PermAct p a  a
pa≡a [] a a∉p = refl
pa≡a (p :: ps) a (a∉as (a∉as a∉ps a≠p₂) a≠p₁)  =  PermAct (p :: ps) a ≡< cong  x  PermAct ps x)  
                                                    (swapabc≡c  (proj₁ p) (proj₂ p) a  (syma≡b⊥ a≠p₁) (syma≡b⊥ a≠p₂)) >
                                                                                  (PermAct ps a ≡< pa≡a ps a a∉ps > (a ))



lemu : (a b : Atom)  (p : Perm)  (a  (flatten p))  (b  a  )  ((PermAct p b)  a)  
lemu a b [] a∉p b≠a = b≠a
lemu a b (p :: ps) (a∉as (a∉as a∉ps p₂≠a) p₁≠a) b≠a  with AtEqDec b (proj₁ p) | AtEqDec b (proj₂ p)
lemu a .(proj₁ p) (p :: ps) (a∉as (a∉as a∉ps p₂≠a) p₁≠a) b≠a  | yes refl | _ = λ x  lemu a (proj₂ p) ps a∉ps p₂≠a x
lemu a .(proj₂ p) (p :: ps) (a∉as (a∉as a∉ps p₂≠a) p₁≠a) b≠a | no _ | yes refl = λ x  lemu a (proj₁ p) ps a∉ps p₁≠a x
lemu a b (p :: ps) (a∉as (a∉as a∉ps p₂≠a) p₁≠a) b≠a | no _ | no _ = λ x  lemu a b ps a∉ps b≠a x 
                                                                                                                                      

 
πsuppAx : (p : Perm)  (b c : Atom)  (b  (flatten p))  (c  (flatten p))  (a : Atom)  PermAct ([ ( b , c) ] ++ (p ++ [ ( b , c ) ])) a  PermAct p a
πsuppAx p b c b∉p c∉p a with AtEqDec a b | AtEqDec a c
πsuppAx p b c b∉p c∉p .b | yes refl | _ = PermAct (p ++ [ ( b , c ) ]) c ≡< p₁++p₂≡p₂p₁ {c} p ( [ ( b , c ) ] ) >
                           (PermAct ( [ ( b , c ) ] ) (PermAct p c) ≡< cong  w  PermAct ( [ ( b , c ) ] ) w) (pa≡a p c c∉p) >
                           (PermAct [ ( b , c ) ] c ≡< swapabb≡a b c > (b ≡< sym (pa≡a p b b∉p) >
                           (PermAct p b)  )))
πsuppAx p b c b∉p c∉p .c | no _ | yes refl = PermAct (p ++ [ ( b , c ) ]) b ≡< p₁++p₂≡p₂p₁ {b} p ( [ ( b , c ) ] ) >
                           (PermAct ( [ ( b , c ) ] ) (PermAct p b) ≡< cong  w  PermAct ( [ ( b , c ) ] ) w) (pa≡a p b b∉p) >
                           (PermAct [ ( b , c ) ] b ≡< swapaba≡b b c > (c ≡< sym (pa≡a p c c∉p) >
                           (PermAct p c)  )))
πsuppAx p b c b∉p c∉p a | no f | no g = PermAct (p ++ [ ( b , c ) ]) a ≡< p₁++p₂≡p₂p₁ {a} p ( [ ( b , c ) ] ) >
                           (PermAct ( [ ( b , c ) ] ) (PermAct p a) ≡< swapabc≡c b c (PermAct p a) (lemu b a p b∉p f) (lemu c a p c∉p g) >
                           (PermAct p a)  ) 



ab∉pcom : (a b : Atom)  (p : Perm)  (a  (flatten p))  (b  (flatten p))  pEquiv ( [ ( a , b ) ] ++ p) (p ++ [ ( a , b ) ] )
ab∉pcom a b p a∉p b∉p {x} with AtEqDec x a | AtEqDec x b
ab∉pcom a b p a∉p b∉p {.a} | yes refl | _ = PermAct p b ≡< pa≡a p b b∉p >
                                                                         (sym (PermAct (p ++ [ ( a , b ) ] ) a ≡< p₁++p₂≡p₂p₁ {a} p [ ( a , b ) ] >
                                                                         (PermAct [ ( a , b ) ] (PermAct p a) ≡< cong  w  PermAct [ ( a , b ) ] w) (pa≡a p a a∉p) >
                                                                         (PermAct [ ( a , b ) ] a ≡< swapaba≡b a b > (b ) ))))
ab∉pcom a b p a∉p b∉p {.b} | no _ |  yes refl = PermAct p a ≡< pa≡a p a a∉p >
                                                                         (sym (PermAct (p ++ [ ( a , b ) ] ) b ≡< p₁++p₂≡p₂p₁ {b} p [ ( a , b ) ] >
                                                                         (PermAct [ ( a , b ) ] (PermAct p b) ≡< cong  w  PermAct [ ( a , b ) ] w) (pa≡a p b b∉p) >
                                                                         (PermAct [ ( a , b ) ] b ≡< swapabb≡a a b > (a ) ))))
ab∉pcom a b p a∉p b∉p {x} | no x≠a | no x≠b = PermAct p x  ≡<
                                                                                                             sym (PermAct (p ++ [ ( a , b ) ] ) x ≡< p₁++p₂≡p₂p₁ {x} p [ ( a , b ) ] >
                                                                                                            (PermAct [ ( a , b ) ] (PermAct p x) ≡< swapabc≡c a b (PermAct p x) (lemu a x p a∉p x≠a) (lemu b x p b∉p x≠b) >
                                                                                                            (PermAct p x)  )) 
                                                                                                         >
                                                                         (PermAct (p ++ [ ( a , b ) ] ) x) 



a≠b⇒πa≠πb : (a b : Atom)  (p : Perm)  (a  b  )  ((PermAct p a  PermAct p b)  )
a≠b⇒πa≠πb a b [] a≠b = a≠b
a≠b⇒πa≠πb a b (p :: ps) a≠b with AtEqDec a (proj₁ p) | AtEqDec a (proj₂ p)
a≠b⇒πa≠πb a b ((.a , .a) :: ps) a≠b | yes refl | yes refl with AtEqDec b a | AtEqDec b a
a≠b⇒πa≠πb a .a ((.a , .a) :: ps) a≠b | yes refl | yes refl | yes refl | _ with a≠b refl
a≠b⇒πa≠πb a .a ((.a , .a) :: ps) a≠b | yes refl | yes refl | yes refl | _ | ()
a≠b⇒πa≠πb a .a ((.a , .a) :: ps) a≠b | yes refl | yes refl | no _ | yes refl with a≠b refl
a≠b⇒πa≠πb a .a ((.a , .a) :: ps) a≠b | yes refl | yes refl | no _ | yes refl | ()
a≠b⇒πa≠πb a b ((.a , .a) :: ps) a≠b | yes refl | yes refl | no f | no g = a≠b⇒πa≠πb a b ps (syma≡b⊥ f)
a≠b⇒πa≠πb a b ((.a , x) :: ps) a≠b | yes refl | no f with AtEqDec b a | AtEqDec b x
a≠b⇒πa≠πb a .a ((.a , x) :: ps) a≠b | yes refl | no _ | yes refl | _ with a≠b refl
a≠b⇒πa≠πb a .a ((.a , x) :: ps) a≠b | yes refl | no _ | yes refl | _ | ()
a≠b⇒πa≠πb a b ((.a , .b) :: ps) a≠b | yes refl | no _ | no _ | yes refl = a≠b⇒πa≠πb b a ps (syma≡b⊥ a≠b)
a≠b⇒πa≠πb a b ((.a , x) :: ps) a≠b | yes refl | no _ | no _ | no j = a≠b⇒πa≠πb x b ps (syma≡b⊥ j)
a≠b⇒πa≠πb a b ((x , .a) :: ps) a≠b | no f | yes refl with AtEqDec b x | AtEqDec b a
a≠b⇒πa≠πb a .a ((x , .a) :: ps) a≠b | no f | yes refl | _ | yes refl with a≠b refl
a≠b⇒πa≠πb a .a ((x , .a) :: ps) a≠b | no f | yes refl | _ | yes refl | ()
a≠b⇒πa≠πb a b ((.b , .a) :: ps) a≠b | no f | yes refl | yes refl | no _ = a≠b⇒πa≠πb b a ps (syma≡b⊥ a≠b)
a≠b⇒πa≠πb a b ((x , .a) :: ps) a≠b | no f | yes refl | no j | no _ = a≠b⇒πa≠πb x b ps (syma≡b⊥ j)
a≠b⇒πa≠πb a b ((x , y) :: ps) a≠b | no i | no j with AtEqDec b x | AtEqDec b y
a≠b⇒πa≠πb a b ((.b , x) :: ps) a≠b | no i | no j | yes refl | _ = a≠b⇒πa≠πb a x ps j
a≠b⇒πa≠πb a b ((x , .b) :: ps) a≠b | no i | no j | no _ | yes refl = a≠b⇒πa≠πb a x ps i
a≠b⇒πa≠πb a b ((x , y) :: ps) a≠b | no _ | no _ | no _ | no _ = a≠b⇒πa≠πb a b ps a≠b


a=b≠c : {a b c : Atom}  a  b  (b  c  )  a  c  
a=b≠c {a}{b}{c} a=b b≠c a=c = b≠c (b ≡< sym a=b > a=c) 


abbcab=ac : (a b c : Atom)  (x : Atom)  (c  a  )  (c  b  )  PermAct [ (a , b) ] (PermAct [ (b , c) ] (PermAct [ (a , b) ] x))  PermAct [ (a , c) ] x
abbcab=ac a b c x c≠a c≠b with AtEqDec x a | AtEqDec x b
abbcab=ac a b c .a c≠a c≠b | yes refl | _ with AtEqDec c a | AtEqDec c b
abbcab=ac a b .a .a c≠a c≠b | yes refl | _ | yes refl | _ with c≠a refl
abbcab=ac a b .a .a c≠a c≠b | yes refl | _ | yes refl | _ | ()
abbcab=ac a b .b .a c≠a c≠b | yes refl | _ | no _ | yes refl with c≠b refl
abbcab=ac a b .b .a c≠a c≠b | yes refl | _ | no _ | yes refl | ()
abbcab=ac a b c .a c≠a c≠b | yes refl | _ | no _ | no _ = PermAct [ (a , b) ] (PermAct [ (b , c) ] b) ≡< cong  w  PermAct [ (a , b) ] w) (swapaba≡b b c) > 
                                                                                                                         (PermAct [ (a , b) ] c ≡< swapabc≡c a b c c≠a c≠b  > (c ))  
abbcab=ac a b c .b c≠a c≠b | no x≠a | yes refl with AtEqDec a b | AtEqDec a c
abbcab=ac a .a c .a c≠a c≠b | no x≠a | yes refl | yes refl | no _ with x≠a refl
abbcab=ac a .a c .a c≠a c≠b | no x≠a | yes refl | yes refl | no _ | ()
abbcab=ac a b .a .b c≠a c≠b | no x≠a | yes refl | _ | yes refl  with c≠a refl
abbcab=ac a b .a .b c≠a c≠b | no x≠a | yes refl | _ | yes refl | ()
abbcab=ac a b c .b c≠a c≠b | no x≠a | yes refl | no a≠b | no a≠c with AtEqDec b c 
abbcab=ac a b .b .b c≠a c≠b | no x≠a | yes refl | no a≠b | no a≠c | yes refl with c≠b refl
abbcab=ac a b .b .b c≠a c≠b | no x≠a | yes refl | no a≠b | no a≠c | yes refl | ()
abbcab=ac a b c .b c≠a c≠b | no x≠a | yes refl | no a≠b | no a≠c | no b≠c = swapaba≡b a b
abbcab=ac a b c x c≠a c≠b | no _ | no _ with AtEqDec x b | AtEqDec x c
abbcab=ac a b c .b c≠a c≠b | no _ | no x≠b | yes refl | _ with x≠b refl
abbcab=ac a b c .c c≠a c≠b | no _ | no _ | yes refl | _ | ()  
abbcab=ac a b c .c c≠a c≠b | no _ | no _ | no _ | yes refl = swapabb≡a a b 
abbcab=ac a b c x c≠a c≠b | no x≠a | no x≠b | no _ | no x≠c = swapabc≡c a b x x≠a x≠b 



ac≈ab+bc+ab : (a b c : Atom)  (c  a  )  (c  b  )  pEquiv ([ (a , c) ]) ([ (a , b) ] ++ ([ (b , c ) ] ++ [ (a , b) ]))
ac≈ab+bc+ab a b c c≠a c≠b = λ {x}  PermAct [ (a , c) ] x ≡< sym (abbcab=ac a b c x c≠a c≠b) >
                                                   ((PermAct [ (a , b) ] (PermAct [ (b , c) ] (PermAct [ (a , b) ] x))) ≡< sym (p₁++p₂≡p₂p₁ {PermAct [ (a , b) ] x} [ (b , c) ] [ (a , b) ]) >
                                                   ((PermAct ([ (b , c) ] ++ [ (a , b) ]) (PermAct [ (a , b) ] x))         ≡< sym (p₁++p₂≡p₂p₁ {x} [ (a , b) ] ([ (b , c) ] ++ [ (a , b) ])) >
                                                   ((PermAct ([ (a , b) ] ++ ([ (b , c) ] ++ [ (a , b) ])) x) )))



πabπ⟶πab : (π : Perm)  (a b : Atom)  (b  (flatten π))  (x : Atom)  PermAct [ ((PermAct π a) , b) ] (PermAct π x)  PermAct π (PermAct [ (a , b) ] x)
πabπ⟶πab π a b b∉π x with AtEqDec x a | AtEqDec x b
πabπ⟶πab π a b b∉π .a | yes refl | _ rewrite (pa≡a π b b∉π) = swapaba≡b (PermAct π a) b 
πabπ⟶πab π a b b∉π .b | no _ | yes refl rewrite (pa≡a π b b∉π) = swapabb≡a (PermAct π a) b
πabπ⟶πab π a b b∉π x | no x≠a | no x≠b = swapabc≡c (PermAct π a) b (PermAct π x) (a≠b⇒πa≠πb x a π x≠a) (lemu b x π b∉π x≠b)  



πabπ≈πab : (π : Perm)  (a b : Atom)  (b  (flatten π))  pEquiv (π ++ [((PermAct π a) , b)]) ([(a , b)] ++ π)
πabπ≈πab π a b b∉π {x} = PermAct (π ++ [((PermAct π a) , b)]) x ≡< p₁++p₂≡p₂p₁ π [((PermAct π a) , b)] >
                                           ((PermAct [((PermAct π a) , b) ] (PermAct π x)) ≡< πabπ⟶πab π a b b∉π x >
                                           ((PermAct π (PermAct [(a , b)] x))  ≡< sym (p₁++p₂≡p₂p₁ {x} [(a , b)] π) >
                                           ((PermAct ([(a , b)] ++ π) x) )))



bπaπ≈πab : (π : Perm)  (b a : Atom)  (b  (flatten π))  pEquiv (π ++ [(b , (PermAct π a))]) ([(b , a)] ++ π)
bπaπ≈πab π b a b∉π {x} = PermAct (π ++ [(b , (PermAct π a))]) x ≡< p₁++p₂≡p₂p₁ π [(b , (PermAct π a))] >
                                           ((PermAct [(b , (PermAct π a)) ] (PermAct π x)) ≡< ab=ba b (PermAct π a) {PermAct π x} > 
                                           ((PermAct [((PermAct π a) , b) ] (PermAct π x)) ≡< πabπ⟶πab π a b b∉π x >
                                           ((PermAct π (PermAct [(a , b)] x))                      ≡< cong  w  PermAct π w) (ab=ba a b {x}) >
                                           ((PermAct π (PermAct [(b , a)] x))                      ≡< sym (p₁++p₂≡p₂p₁ {x} [(b , a)] π) >
                                           ((PermAct ([(b , a)] ++ π) x) )))))




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



π+πab≈abπ : (π : Perm)  (a b : Atom)  pEquiv (π ++ [(PermAct π a) , (PermAct π b)]) ([(a , b)] ++ π)
π+πab≈abπ π a b {x} with AtEqDec x a | AtEqDec x b
π+πab≈abπ π a b {.a} | yes refl | _ = 
                                                           ((PermAct (π ++ [(PermAct π a) , (PermAct π b)]) a)
                                                                                           ≡< p₁++p₂≡p₂p₁ {a} π [(PermAct π a) , (PermAct π b)] >
                                                           ((PermAct [(PermAct π a) , (PermAct π b)] (PermAct π a))
                                                                                           ≡< swapaba≡b (PermAct π a) (PermAct π b) >
                                                           ((PermAct π b) )))
π+πab≈abπ π a b {.b} | no _ | yes refl = 
                                                            ((PermAct (π ++ [(PermAct π a) , (PermAct π b)]) b)
                                                                                           ≡< p₁++p₂≡p₂p₁ {b} π [(PermAct π a) , (PermAct π b)] >
                                                           ((PermAct [(PermAct π a) , (PermAct π b)] (PermAct π b))
                                                                                           ≡< swapabb≡a (PermAct π a) (PermAct π b) >
                                                           ((PermAct π a) )))
π+πab≈abπ π a b {x} | no x≠a | no x≠b = 
                                                            ((PermAct (π ++ [(PermAct π a) , (PermAct π b)]) x)
                                                                                           ≡< p₁++p₂≡p₂p₁ {x} π [(PermAct π a) , (PermAct π b)] >
                                                           ((PermAct [(PermAct π a) , (PermAct π b)] (PermAct π x))
                                                                                           ≡< swapabc≡c (PermAct π a) (PermAct π b) (PermAct π x) (a≠b⇒πa≠πb x a π x≠a) (a≠b⇒πa≠πb x b π x≠b)  >
                                                           ((PermAct π x) )))



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


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