|
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
|
|
184
|
16 open import FLutil
|
|
68
|
17 open import Solvable using (solvable)
|
|
|
18 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
19
|
|
|
20 open import Data.Fin
|
|
|
21 open import Data.Fin.Permutation
|
|
|
22
|
|
70
|
23 sym2solvable : solvable (Symmetric 2)
|
|
|
24 solvable.dervied-length sym2solvable = 1
|
|
|
25 solvable.end sym2solvable x d = solved x d where
|
|
|
26
|
|
|
27 open import Data.List using ( List ; [] ; _∷_ )
|
|
68
|
28
|
|
|
29 open Solvable (Symmetric 2)
|
|
|
30 -- open Group (Symmetric 2) using (_⁻¹)
|
|
|
31
|
|
97
|
32
|
|
70
|
33 p0 : FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid
|
|
90
|
34 p0 = pleq _ _ refl
|
|
70
|
35
|
|
97
|
36 p0r : perm→FL pid ≡ ((# 0) :: ((# 0 ) :: f0))
|
|
|
37 p0r = refl
|
|
70
|
38
|
|
90
|
39 p1 : FL→perm ((# 1) :: ((# 0 ) :: f0)) =p= pswap pid
|
|
|
40 p1 = pleq _ _ refl
|
|
68
|
41
|
|
97
|
42 p1r : perm→FL (pswap pid) ≡ ((# 1) :: ((# 0 ) :: f0))
|
|
|
43 p1r = refl
|
|
|
44
|
|
111
|
45 -- FL→iso : (fl : FL 2 ) → perm→FL ( FL→perm fl ) ≡ fl
|
|
|
46 -- FL→iso (zero :: (zero :: f0)) = refl
|
|
|
47 -- FL→iso ((suc zero) :: (zero :: f0)) = refl
|
|
97
|
48
|
|
111
|
49 open _=p=_
|
|
|
50 open ≡-Reasoning
|
|
97
|
51
|
|
68
|
52 sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
|
|
111
|
53 sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
|
|
|
54 sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} | record { eq = h=00} = begin
|
|
70
|
55 [ g , h ] ⟨$⟩ʳ q
|
|
|
56 ≡⟨⟩
|
|
|
57 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
58 ≡⟨ cong (λ k → h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ k))) ((peqˡ sym2lem1 _ )) ⟩
|
|
|
59 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q )))
|
|
|
60 ≡⟨ cong (λ k → h ⟨$⟩ʳ k ) (peq sym2lem1 _ ) ⟩
|
|
|
61 h ⟨$⟩ʳ (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q )))
|
|
|
62 ≡⟨⟩
|
|
|
63 [ pid , h ] ⟨$⟩ʳ q
|
|
|
64 ≡⟨ peq (idcomtl h) q ⟩
|
|
|
65 q
|
|
111
|
66 ∎ where
|
|
|
67 sym2lem1 : g =p= pid
|
|
|
68 sym2lem1 = FL-inject g=00
|
|
|
69 sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00} = begin
|
|
69
|
70 [ g , h ] ⟨$⟩ʳ q
|
|
70
|
71 ≡⟨⟩
|
|
|
72 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
73 ≡⟨ peq sym2lem2 _ ⟩
|
|
|
74 pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
111
|
75 ≡⟨ cong (λ k → pid ⟨$⟩ʳ (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩
|
|
70
|
76 pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
77 ≡⟨⟩
|
|
|
78 [ g , pid ] ⟨$⟩ʳ q
|
|
|
79 ≡⟨ peq (idcomtr g) q ⟩
|
|
69
|
80 q
|
|
70
|
81 ∎ where
|
|
111
|
82 sym2lem2 : h =p= pid
|
|
|
83 sym2lem2 = FL-inject h=00
|
|
|
84 sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00}= begin
|
|
70
|
85 [ g , h ] ⟨$⟩ʳ q
|
|
|
86 ≡⟨⟩
|
|
|
87 h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
111
|
88 ≡⟨ peq (psym g=h ) _ ⟩
|
|
|
89 g ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
90 ≡⟨ cong (λ k → g ⟨$⟩ʳ (g ⟨$⟩ʳ k) ) (peqˡ (psym g=h) _) ⟩
|
|
|
91 g ⟨$⟩ʳ (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
|
|
|
92 ≡⟨ cong (λ k → g ⟨$⟩ʳ k) ( inverseʳ g ) ⟩
|
|
|
93 g ⟨$⟩ʳ ( g ⟨$⟩ˡ q )
|
|
|
94 ≡⟨ inverseʳ g ⟩
|
|
70
|
95 q
|
|
|
96 ∎ where
|
|
111
|
97 g=h : g =p= h
|
|
|
98 g=h = FL-inject (trans g=00 (sym h=00))
|
|
68
|
99 solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
|
|
|
100 solved x uni = prefl
|
|
|
101 solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h }
|
|
|
102 solved x (gen {f} {g} d d₁) with solved f d | solved g d₁
|
|
|
103 ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
|
|
|
104 genlem : ( q : Fin 2 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
|
|
|
105 genlem q = begin
|
|
|
106 g ⟨$⟩ʳ ( f ⟨$⟩ʳ q )
|
|
|
107 ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩
|
|
|
108 f ⟨$⟩ʳ q
|
|
|
109 ≡⟨ f=e q ⟩
|
|
|
110 q
|
|
|
111 ∎ where open ≡-Reasoning
|
|
|
112 solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d
|
|
|
113 ... | record { peq = f=e } = record { peq = λ q → cc q } where
|
|
|
114 cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q
|
|
|
115 cc q = begin
|
|
|
116 x ⟨$⟩ʳ q
|
|
|
117 ≡⟨ sym (f=g q) ⟩
|
|
|
118 f ⟨$⟩ʳ q
|
|
|
119 ≡⟨ f=e q ⟩
|
|
|
120 q
|
|
|
121 ∎ where open ≡-Reasoning
|
|
|
122
|
|
|
123
|
|
|
124
|
|
|
125
|
