|
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
|
|
|
32 p0 = record { peq = p00 } where
|
|
|
33 p00 : (q : Fin 2) → (FL→perm ((# 0) :: ((# 0) :: f0)) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
|
|
|
34 p00 zero = refl
|
|
|
35 p00 (suc zero) = refl
|
|
|
36
|
|
|
37 p1 : Permutation 2 2
|
|
|
38 p1 = FL→perm ((# 1) :: ((# 0 ) :: f0))
|
|
|
39
|
|
|
40 p1rev : (p1 ∘ₚ p1 ) =p= pid
|
|
|
41 p1rev = record { peq = p01 } where
|
|
|
42 p01 : (q : Fin 2) → ((p1 ∘ₚ p1) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
|
|
|
43 p01 zero = refl
|
|
|
44 p01 (suc zero) = refl
|
|
68
|
45
|
|
70
|
46 open _=p=_
|
|
|
47
|
|
68
|
48 sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
|
|
70
|
49 sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g
|
|
|
50 sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} = begin
|
|
|
51 [ g , h ] ⟨$⟩ʳ q
|
|
|
52 ≡⟨⟩
|
|
|
53 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
54 ≡⟨ cong (λ k → h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ k))) ((peqˡ sym2lem1 _ )) ⟩
|
|
|
55 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q )))
|
|
|
56 ≡⟨ cong (λ k → h ⟨$⟩ʳ k ) (peq sym2lem1 _ ) ⟩
|
|
|
57 h ⟨$⟩ʳ (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q )))
|
|
|
58 ≡⟨⟩
|
|
|
59 [ pid , h ] ⟨$⟩ʳ q
|
|
|
60 ≡⟨ peq (idcomtl h) q ⟩
|
|
|
61 q
|
|
|
62 ∎ where
|
|
|
63 open ≡-Reasoning
|
|
|
64 postulate sym2lem1 : g =p= pid
|
|
|
65 -- it works but very slow
|
|
|
66 -- sym2lem1 = ptrans (psym ( FL←iso g )) (subst (λ k → FL→perm k =p= pid) (sym g=00) p0 )
|
|
|
67 sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} = begin
|
|
69
|
68 [ g , h ] ⟨$⟩ʳ q
|
|
70
|
69 ≡⟨⟩
|
|
|
70 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
71 ≡⟨ peq sym2lem2 _ ⟩
|
|
|
72 pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
73 ≡⟨ cong (λ k → pid ⟨$⟩ʳ (g ⟨$⟩ʳ k)) ((peqˡ sym2lem2 _ )) ⟩
|
|
|
74 pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
75 ≡⟨⟩
|
|
|
76 [ g , pid ] ⟨$⟩ʳ q
|
|
|
77 ≡⟨ peq (idcomtr g) q ⟩
|
|
69
|
78 q
|
|
70
|
79 ∎ where
|
|
|
80 open ≡-Reasoning
|
|
|
81 postulate sym2lem2 : h =p= pid
|
|
|
82 sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | _ = begin
|
|
|
83 [ g , h ] ⟨$⟩ʳ q
|
|
|
84 ≡⟨⟩
|
|
|
85 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
86 ≡⟨ peq sym2lem3 _ ⟩
|
|
|
87 pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))
|
|
|
88 ≡⟨ cong (λ k → pid ⟨$⟩ʳ k) (peq sym2lem4 _ )⟩
|
|
|
89 pid ⟨$⟩ʳ ( pid ⟨$⟩ˡ q )
|
|
|
90 ≡⟨⟩
|
|
|
91 q
|
|
|
92 ∎ where
|
|
|
93 open ≡-Reasoning
|
|
|
94 postulate
|
|
|
95 sym2lem3 : (g ∘ₚ h ) =p= pid
|
|
|
96 sym2lem4 : (pinv g ∘ₚ pinv h ) =p= pid
|
|
68
|
97 solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
|
|
|
98 solved x uni = prefl
|
|
|
99 solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h }
|
|
|
100 solved x (gen {f} {g} d d₁) with solved f d | solved g d₁
|
|
|
101 ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
|
|
|
102 genlem : ( q : Fin 2 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
|
|
|
103 genlem q = begin
|
|
|
104 g ⟨$⟩ʳ ( f ⟨$⟩ʳ q )
|
|
|
105 ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩
|
|
|
106 f ⟨$⟩ʳ q
|
|
|
107 ≡⟨ f=e q ⟩
|
|
|
108 q
|
|
|
109 ∎ where open ≡-Reasoning
|
|
|
110 solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d
|
|
|
111 ... | record { peq = f=e } = record { peq = λ q → cc q } where
|
|
|
112 cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q
|
|
|
113 cc q = begin
|
|
|
114 x ⟨$⟩ʳ q
|
|
|
115 ≡⟨ sym (f=g q) ⟩
|
|
|
116 f ⟨$⟩ʳ q
|
|
|
117 ≡⟨ f=e q ⟩
|
|
|
118 q
|
|
|
119 ∎ where open ≡-Reasoning
|
|
|
120
|
|
70
|
121 -- ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
|
|
|
122 -- ¬sym5solvable sol = {!!}
|
|
68
|
123
|
|
|
124
|
|
|
125
|
