|
68
|
1 open import Level hiding ( suc ; zero )
|
|
|
2 open import Algebra
|
|
153
|
3 module sym3n 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)
|
|
153
|
33 open import FLutil
|
|
|
34 open import Data.List.Fresh hiding ([_])
|
|
|
35 open import Relation.Nary using (⌊_⌋)
|
|
111
|
36
|
|
|
37 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
|
|
153
|
38 p0id = pleq _ _ refl
|
|
|
39
|
|
|
40 t1 : FList 3 → FList 3
|
|
|
41 t1 x = tl2 x x [] where
|
|
|
42 tl3 : (FL 3) → ( z : FList 3) → FList 3 → FList 3
|
|
|
43 tl3 h [] w = w
|
|
|
44 tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
|
|
|
45 tl2 : ( x z : FList 3) → FList 3 → FList 3
|
|
|
46 tl2 [] _ x = x
|
|
|
47 tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
|
|
|
48
|
|
|
49 stage10 : FList 3
|
|
162
|
50 stage10 = {!!} -- t1 (Flist (fmax ))
|
|
68
|
51
|
|
111
|
52 p0 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))
|
|
|
53 p1 = FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0)))
|
|
|
54 p2 = FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0)))
|
|
|
55 p3 = FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0)))
|
|
|
56 p4 = FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0)))
|
|
|
57 p5 = FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0)))
|
|
|
58 t0 = plist p0 ∷ plist p1 ∷ plist p2 ∷ plist p3 ∷ plist p4 ∷ plist p5 ∷ []
|
|
88
|
59
|
|
153
|
60 tt4 = plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷ plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷ plist [ p5 , p1 ] ∷
|
|
125
|
61 plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷ plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷ plist [ p5 , p1 ] ∷
|
|
|
62 plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷ plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷ plist [ p5 , p2 ] ∷
|
|
|
63 plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷ plist [ p5 , p3 ] ∷
|
|
|
64 plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p4 ] ∷
|
|
|
65 plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p5 ] ∷
|
|
|
66 []
|
|
119
|
67
|
|
70
|
68 open _=p=_
|
|
|
69
|
|
119
|
70 stage1 : (x : Permutation 3 3) → Set (Level.suc Level.zero)
|
|
|
71 stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x
|
|
|
72
|
|
|
73 open import logic
|
|
121
|
74
|
|
122
|
75 pFL : ( g : Permutation 3 3) → { x : FL 3 } → perm→FL g ≡ x → g =p= FL→perm x
|
|
|
76 pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl )
|
|
|
77
|
|
121
|
78 open ≡-Reasoning
|
|
|
79
|
|
123
|
80 -- st01 : ( x y : Permutation 3 3) → x =p= p3 → y =p= p3 → x ∘ₚ y =p= p4
|
|
|
81 -- st01 x y s t = record { peq = λ q → ( begin
|
|
|
82 -- (x ∘ₚ y) ⟨$⟩ʳ q
|
|
|
83 -- ≡⟨ peq ( presp s t ) q ⟩
|
|
|
84 -- ( p3 ∘ₚ p3 ) ⟨$⟩ʳ q
|
|
|
85 -- ≡⟨ peq p33=4 q ⟩
|
|
|
86 -- p4 ⟨$⟩ʳ q
|
|
|
87 -- ∎ ) }
|
|
121
|
88
|
|
125
|
89 st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) ]
|
|
|
90
|
|
119
|
91
|
|
|
92 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
|
|
153
|
93 stage12 = {!!}
|
|
123
|
94
|
|
119
|
95
|
|
70
|
96 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
|
|
123
|
97 solved1 _ uni = prefl
|
|
|
98 solved1 x (gen {f} {g} d d₁) with solved1 f d | solved1 g d₁
|
|
|
99 ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
|
|
|
100 genlem : ( q : Fin 3 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
|
|
|
101 genlem q = begin
|
|
|
102 g ⟨$⟩ʳ ( f ⟨$⟩ʳ q )
|
|
|
103 ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩
|
|
|
104 f ⟨$⟩ʳ q
|
|
|
105 ≡⟨ f=e q ⟩
|
|
|
106 q
|
|
|
107 ∎
|
|
|
108 solved1 x (ccong {f} {g} (record {peq = f=g}) d) with solved1 f d
|
|
|
109 ... | record { peq = f=e } = record { peq = λ q → cc q } where
|
|
|
110 cc : ( q : Fin 3 ) → x ⟨$⟩ʳ q ≡ q
|
|
|
111 cc q = begin
|
|
|
112 x ⟨$⟩ʳ q
|
|
|
113 ≡⟨ sym (f=g q) ⟩
|
|
|
114 f ⟨$⟩ʳ q
|
|
|
115 ≡⟨ f=e q ⟩
|
|
|
116 q
|
|
|
117 ∎
|
|
153
|
118 solved1 _ (comm {g} {h} x y) = {!!}
|
|
123
|
119
|
