|
68
|
1 open import Level hiding ( suc ; zero )
|
|
|
2 open import Algebra
|
|
70
|
3 module sym2 where
|
|
68
|
4
|
|
|
5 open import Symmetric
|
|
|
6 open import Data.Unit
|
|
|
7 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
|
|
|
8 open import Function
|
|
|
9 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
|
|
|
10 open import Relation.Nullary
|
|
|
11 open import Data.Empty
|
|
|
12 open import Data.Product
|
|
|
13
|
|
|
14 open import Gutil
|
|
|
15 open import Putil
|
|
|
16 open import Solvable using (solvable)
|
|
|
17 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
18
|
|
|
19 open import Data.Fin
|
|
|
20 open import Data.Fin.Permutation
|
|
|
21
|
|
70
|
22 sym2solvable : solvable (Symmetric 2)
|
|
|
23 solvable.dervied-length sym2solvable = 1
|
|
|
24 solvable.end sym2solvable x d = solved x d where
|
|
|
25
|
|
|
26 open import Data.List using ( List ; [] ; _∷_ )
|
|
68
|
27
|
|
|
28 open Solvable (Symmetric 2)
|
|
|
29 -- open Group (Symmetric 2) using (_⁻¹)
|
|
|
30
|
|
70
|
31 p0 : FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid
|
|
90
|
32 p0 = pleq _ _ refl
|
|
70
|
33
|
|
90
|
34 p0r : (p : Permutation 2 2 ) → perm→FL p ≡ ((# 0) :: ((# 0 ) :: f0)) → p =p= pid
|
|
|
35 p0r p eq = {!!}
|
|
70
|
36
|
|
90
|
37 p1 : FL→perm ((# 1) :: ((# 0 ) :: f0)) =p= pswap pid
|
|
|
38 p1 = pleq _ _ refl
|
|
68
|
39
|
|
70
|
40 open _=p=_
|
|
|
41
|
|
68
|
42 sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
|
|
70
|
43 sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g
|
|
|
44 sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} = begin
|
|
|
45 [ g , h ] ⟨$⟩ʳ q
|
|
|
46 ≡⟨⟩
|
|
|
47 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
48 ≡⟨ cong (λ k → h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ k))) ((peqˡ sym2lem1 _ )) ⟩
|
|
|
49 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q )))
|
|
|
50 ≡⟨ cong (λ k → h ⟨$⟩ʳ k ) (peq sym2lem1 _ ) ⟩
|
|
|
51 h ⟨$⟩ʳ (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q )))
|
|
|
52 ≡⟨⟩
|
|
|
53 [ pid , h ] ⟨$⟩ʳ q
|
|
|
54 ≡⟨ peq (idcomtl h) q ⟩
|
|
|
55 q
|
|
|
56 ∎ where
|
|
|
57 open ≡-Reasoning
|
|
88
|
58 sym2lem1 : g =p= pid
|
|
90
|
59 sym2lem1 = pleq _ _ {!!}
|
|
70
|
60 -- it works but very slow
|
|
|
61 -- sym2lem1 = ptrans (psym ( FL←iso g )) (subst (λ k → FL→perm k =p= pid) (sym g=00) p0 )
|
|
|
62 sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} = begin
|
|
69
|
63 [ g , h ] ⟨$⟩ʳ q
|
|
70
|
64 ≡⟨⟩
|
|
|
65 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
66 ≡⟨ peq sym2lem2 _ ⟩
|
|
|
67 pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
68 ≡⟨ cong (λ k → pid ⟨$⟩ʳ (g ⟨$⟩ʳ k)) ((peqˡ sym2lem2 _ )) ⟩
|
|
|
69 pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
70 ≡⟨⟩
|
|
|
71 [ g , pid ] ⟨$⟩ʳ q
|
|
|
72 ≡⟨ peq (idcomtr g) q ⟩
|
|
69
|
73 q
|
|
70
|
74 ∎ where
|
|
|
75 open ≡-Reasoning
|
|
|
76 postulate sym2lem2 : h =p= pid
|
|
|
77 sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | _ = begin
|
|
|
78 [ g , h ] ⟨$⟩ʳ q
|
|
|
79 ≡⟨⟩
|
|
|
80 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
81 ≡⟨ peq sym2lem3 _ ⟩
|
|
|
82 pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))
|
|
|
83 ≡⟨ cong (λ k → pid ⟨$⟩ʳ k) (peq sym2lem4 _ )⟩
|
|
|
84 pid ⟨$⟩ʳ ( pid ⟨$⟩ˡ q )
|
|
|
85 ≡⟨⟩
|
|
|
86 q
|
|
|
87 ∎ where
|
|
|
88 open ≡-Reasoning
|
|
|
89 postulate
|
|
|
90 sym2lem3 : (g ∘ₚ h ) =p= pid
|
|
|
91 sym2lem4 : (pinv g ∘ₚ pinv h ) =p= pid
|
|
68
|
92 solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
|
|
|
93 solved x uni = prefl
|
|
|
94 solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h }
|
|
|
95 solved x (gen {f} {g} d d₁) with solved f d | solved g d₁
|
|
|
96 ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
|
|
|
97 genlem : ( q : Fin 2 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
|
|
|
98 genlem q = begin
|
|
|
99 g ⟨$⟩ʳ ( f ⟨$⟩ʳ q )
|
|
|
100 ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩
|
|
|
101 f ⟨$⟩ʳ q
|
|
|
102 ≡⟨ f=e q ⟩
|
|
|
103 q
|
|
|
104 ∎ where open ≡-Reasoning
|
|
|
105 solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d
|
|
|
106 ... | record { peq = f=e } = record { peq = λ q → cc q } where
|
|
|
107 cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q
|
|
|
108 cc q = begin
|
|
|
109 x ⟨$⟩ʳ q
|
|
|
110 ≡⟨ sym (f=g q) ⟩
|
|
|
111 f ⟨$⟩ʳ q
|
|
|
112 ≡⟨ f=e q ⟩
|
|
|
113 q
|
|
|
114 ∎ where open ≡-Reasoning
|
|
|
115
|
|
|
116
|
|
|
117
|
|
|
118
|
