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