module PermProp where
open import Basics
open import Atoms
open import Perms
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
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 ▪)))