|
68
|
1 open import Level hiding ( suc ; zero )
|
|
|
2 open import Algebra
|
|
70
|
3 module sym3 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
|
|
162
|
16 open import FLutil
|
|
68
|
17 open import Solvable using (solvable)
|
|
|
18 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
19
|
|
|
20 open import Data.Fin
|
|
121
|
21 open import Data.Fin.Permutation hiding (_∘ₚ_)
|
|
|
22
|
|
|
23 infixr 200 _∘ₚ_
|
|
|
24 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
|
|
|
25
|
|
68
|
26
|
|
70
|
27 sym3solvable : solvable (Symmetric 3)
|
|
|
28 solvable.dervied-length sym3solvable = 2
|
|
|
29 solvable.end sym3solvable x d = solved1 x d where
|
|
68
|
30
|
|
70
|
31 open import Data.List using ( List ; [] ; _∷_ )
|
|
|
32
|
|
|
33 open Solvable (Symmetric 3)
|
|
111
|
34
|
|
|
35 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
|
|
|
36 p0id = pleq _ _ refl
|
|
68
|
37
|
|
111
|
38 p0 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))
|
|
|
39 p1 = FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0)))
|
|
|
40 p2 = FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0)))
|
|
|
41 p3 = FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0)))
|
|
|
42 p4 = FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0)))
|
|
|
43 p5 = FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0)))
|
|
|
44 t0 = plist p0 ∷ plist p1 ∷ plist p2 ∷ plist p3 ∷ plist p4 ∷ plist p5 ∷ []
|
|
88
|
45
|
|
125
|
46 t1 = plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷ plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷ plist [ p5 , p1 ] ∷
|
|
|
47 plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷ plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷ plist [ p5 , p1 ] ∷
|
|
|
48 plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷ plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷ plist [ p5 , p2 ] ∷
|
|
|
49 plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷ plist [ p5 , p3 ] ∷
|
|
|
50 plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p4 ] ∷
|
|
|
51 plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p5 ] ∷
|
|
|
52 []
|
|
119
|
53
|
|
70
|
54 open _=p=_
|
|
|
55
|
|
119
|
56 stage1 : (x : Permutation 3 3) → Set (Level.suc Level.zero)
|
|
|
57 stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x
|
|
|
58
|
|
|
59 open import logic
|
|
121
|
60
|
|
|
61 p33=4 : ( p3 ∘ₚ p3 ) =p= p4
|
|
|
62 p33=4 = pleq _ _ refl
|
|
|
63
|
|
|
64 p44=3 : ( p4 ∘ₚ p4 ) =p= p3
|
|
|
65 p44=3 = pleq _ _ refl
|
|
|
66
|
|
|
67 p34=0 : ( p3 ∘ₚ p4 ) =p= pid
|
|
|
68 p34=0 = pleq _ _ refl
|
|
|
69
|
|
|
70 p43=0 : ( p4 ∘ₚ p3 ) =p= pid
|
|
|
71 p43=0 = pleq _ _ refl
|
|
|
72
|
|
123
|
73 com33 : [ p3 , p3 ] =p= pid
|
|
|
74 com33 = pleq _ _ refl
|
|
|
75
|
|
|
76 com44 : [ p4 , p4 ] =p= pid
|
|
|
77 com44 = pleq _ _ refl
|
|
|
78
|
|
|
79 com34 : [ p3 , p4 ] =p= pid
|
|
|
80 com34 = pleq _ _ refl
|
|
|
81
|
|
|
82 com43 : [ p4 , p3 ] =p= pid
|
|
|
83 com43 = pleq _ _ refl
|
|
|
84
|
|
|
85
|
|
122
|
86 pFL : ( g : Permutation 3 3) → { x : FL 3 } → perm→FL g ≡ x → g =p= FL→perm x
|
|
|
87 pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl )
|
|
|
88
|
|
121
|
89 open ≡-Reasoning
|
|
|
90
|
|
123
|
91 -- st01 : ( x y : Permutation 3 3) → x =p= p3 → y =p= p3 → x ∘ₚ y =p= p4
|
|
|
92 -- st01 x y s t = record { peq = λ q → ( begin
|
|
|
93 -- (x ∘ₚ y) ⟨$⟩ʳ q
|
|
|
94 -- ≡⟨ peq ( presp s t ) q ⟩
|
|
|
95 -- ( p3 ∘ₚ p3 ) ⟨$⟩ʳ q
|
|
|
96 -- ≡⟨ peq p33=4 q ⟩
|
|
|
97 -- p4 ⟨$⟩ʳ q
|
|
|
98 -- ∎ ) }
|
|
121
|
99
|
|
125
|
100 st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) ]
|
|
|
101
|
|
121
|
102 st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
|
|
124
|
103 st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
|
|
|
104 ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
|
|
|
105 ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
|
|
|
106 ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
107 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
|
|
|
108 ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
109 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
|
|
|
110 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
111 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
|
|
|
112 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
113 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
|
|
|
114 ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } | record { eq = he } =
|
|
|
115 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
|
|
125
|
116
|
|
|
117 ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } =
|
|
|
118 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
119 ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
120 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
121 ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 ))| record { eq = ge } | record { eq = he } =
|
|
|
122 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
123 ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0))| record { eq = ge } | record { eq = he } =
|
|
|
124 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
125 ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
162
|
126 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
125
|
127 ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
128 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
129 ... | ((suc zero) :: (zero :: (zero :: f0 ))) | ((suc (suc zero)) :: (zero :: (zero :: f0 )))| record { eq = ge } | record { eq = he } =
|
|
|
130 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
131 ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } | record { eq = he } =
|
|
|
132 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
133 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
134 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
135 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } =
|
|
|
136 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
137 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc (suc zero)) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } =
|
|
|
138 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
|
|
|
139 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } | record { eq = he } =
|
|
|
140 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
141 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } | record { eq = he } =
|
|
|
142 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
143 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } =
|
|
|
144 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
145 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (suc zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } =
|
|
|
146 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
|
|
|
147 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } | record { eq = he } =
|
|
|
148 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
149 ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } | record { eq = he } =
|
|
|
150 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
151 ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } =
|
|
|
152 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
153 ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (suc zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } =
|
|
|
154 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
|
155 ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
156 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
|
|
119
|
157
|
|
|
158 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
|
|
125
|
159 stage12 x (comm {g} {h} x1 y1 ) = st02 g h
|
|
|
160 stage12 _ (ccong {y} x=y sx) with stage12 y sx
|
|
|
161 ... | case1 id = case1 ( ptrans (psym x=y ) id )
|
|
|
162 ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ ))
|
|
|
163 ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ ))
|
|
123
|
164
|
|
119
|
165
|
|
70
|
166 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
|
|
123
|
167 solved1 x (ccong {f} {g} (record {peq = f=g}) d) with solved1 f d
|
|
|
168 ... | record { peq = f=e } = record { peq = λ q → cc q } where
|
|
|
169 cc : ( q : Fin 3 ) → x ⟨$⟩ʳ q ≡ q
|
|
|
170 cc q = begin
|
|
|
171 x ⟨$⟩ʳ q
|
|
|
172 ≡⟨ sym (f=g q) ⟩
|
|
|
173 f ⟨$⟩ʳ q
|
|
|
174 ≡⟨ f=e q ⟩
|
|
|
175 q
|
|
|
176 ∎
|
|
125
|
177 solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y
|
|
|
178 ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
|
|
|
179 ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
|
|
|
180 ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g)
|
|
|
181 ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com33 q) }
|
|
|
182 ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com44 q) }
|
|
|
183 ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com34 q) }
|
|
|
184 ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com43 q) }
|
|
123
|
185
|
