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