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