|
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
|
|
119
|
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 []
|
|
|
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
|
|
122
|
72 pFL : ( g : Permutation 3 3) → { x : FL 3 } → perm→FL g ≡ x → g =p= FL→perm x
|
|
|
73 pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl )
|
|
|
74
|
|
121
|
75 open ≡-Reasoning
|
|
|
76
|
|
|
77 st01 : ( x y : Permutation 3 3) → x =p= p3 → y =p= p3 → x ∘ₚ y =p= p4
|
|
|
78 st01 x y s t = record { peq = λ q → ( begin
|
|
|
79 (x ∘ₚ y) ⟨$⟩ʳ q
|
|
|
80 ≡⟨ peq ( presp s t ) q ⟩
|
|
|
81 ( p3 ∘ₚ p3 ) ⟨$⟩ʳ q
|
|
|
82 ≡⟨ peq p33=4 q ⟩
|
|
|
83 p4 ⟨$⟩ʳ q
|
|
|
84 ∎ ) }
|
|
|
85
|
|
|
86 st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
|
|
|
87 st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
|
|
122
|
88 ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
|
|
|
89 ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
|
|
|
90 ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
91 case1 (ptrans (comm-resp (pFL g ge) (pFL h he) ) (comm-refl {FL→perm (zero :: (suc zero) :: (zero :: f0 ))} prefl ))
|
|
|
92 ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
93 case1 (ptrans (comm-resp (pFL g ge) (pFL h he) ) (comm-refl {FL→perm ((suc zero) :: (zero :: (zero :: f0 )))} prefl ))
|
|
|
94 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
|
|
|
95 case1 (ptrans (comm-resp (pFL g ge) (pFL h he) ) (comm-refl {FL→perm ((suc zero) :: (suc zero :: (zero :: f0 )))} prefl ))
|
|
121
|
96 ... | (zero :: (suc zero) :: (zero :: f0 )) | t | se | te = {!!}
|
|
|
97 ... | (suc zero) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
|
|
|
98 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | t | se | te = {!!}
|
|
|
99 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
|
|
|
100 ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | t | se | te = {!!}
|
|
119
|
101
|
|
|
102 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
|
|
120
|
103 stage12 x uni = case1 prefl
|
|
121
|
104 stage12 x (comm {g} {h} x1 y1 ) = st02 g h
|
|
|
105 stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy
|
|
|
106 ... | case1 t | case1 s = case1 ( record { peq = λ q → peq (presp t s) q} )
|
|
|
107 ... | case1 t | case2 (case1 s) = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } ))
|
|
|
108 ... | case1 t | case2 (case2 s) = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } ))
|
|
|
109 ... | case2 (case1 t) | case1 s = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } ))
|
|
|
110 ... | case2 (case2 t) | case1 s = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } ))
|
|
|
111 ... | case2 (case1 s) | case2 (case1 t) = case2 (case2 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p33=4 q) } )
|
|
|
112 ... | case2 (case1 s) | case2 (case2 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p34=0 q) }
|
|
|
113 ... | case2 (case2 s) | case2 (case1 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p43=0 q) }
|
|
|
114 ... | case2 (case2 s) | case2 (case2 t) = case2 (case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p44=3 q) } )
|
|
120
|
115 stage12 _ (ccong {y} x=y sx) with stage12 y sx
|
|
|
116 ... | case1 id = case1 ( ptrans (psym x=y ) id )
|
|
|
117 ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ ))
|
|
|
118 ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ ))
|
|
119
|
119
|
|
70
|
120 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
|
|
|
121 solved1 = {!!}
|
