|
68
|
1 open import Level hiding ( suc ; zero )
|
|
|
2 open import Algebra
|
|
73
|
3 module sym5 where
|
|
68
|
4
|
|
|
5 open import Symmetric
|
|
75
|
6 open import Data.Unit using (⊤ ; tt )
|
|
68
|
7 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
|
|
75
|
8 open import Function hiding (flip)
|
|
68
|
9 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
|
|
75
|
10 open import Data.Nat.Properties
|
|
68
|
11 open import Relation.Nullary
|
|
|
12 open import Data.Empty
|
|
|
13 open import Data.Product
|
|
|
14
|
|
|
15 open import Gutil
|
|
|
16 open import Putil
|
|
|
17 open import Solvable using (solvable)
|
|
|
18 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
19
|
|
75
|
20 open import Data.Fin hiding (_<_ ; _≤_ ; lift )
|
|
68
|
21 open import Data.Fin.Permutation
|
|
73
|
22 open import Data.List hiding ( [_] )
|
|
75
|
23 open import nat
|
|
77
|
24 open import fin
|
|
84
|
25 open import logic
|
|
|
26
|
|
|
27 open _∧_
|
|
68
|
28
|
|
|
29 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
|
|
84
|
30 ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (proj1 (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) )) where
|
|
73
|
31
|
|
|
32 --
|
|
|
33 -- dba 1320 d → b → a → d
|
|
|
34 -- (dba)⁻¹ 3021 a → b → d → a
|
|
|
35 -- aec 21430
|
|
|
36 -- (aec)⁻¹ 41032
|
|
|
37 -- (abd)(cea)(dba)(aec)
|
|
|
38 --
|
|
|
39
|
|
|
40 open solvable
|
|
|
41 open Solvable (Symmetric 5)
|
|
|
42 end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid
|
|
|
43 end5 x der = end sol x der
|
|
|
44
|
|
74
|
45 0<4 : 0 < 4
|
|
75
|
46 0<4 = s≤s z≤n
|
|
74
|
47
|
|
|
48 0<3 : 0 < 3
|
|
75
|
49 0<3 = s≤s z≤n
|
|
74
|
50
|
|
79
|
51 --- 1 ∷ 2 ∷ 0 ∷ [] abc
|
|
74
|
52 3rot : Permutation 3 3
|
|
79
|
53 3rot = pid {3} ∘ₚ pins (n≤ 2)
|
|
|
54
|
|
85
|
55 save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
|
|
|
56 save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4)
|
|
|
57
|
|
79
|
58 ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
|
|
85
|
59 ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 )
|
|
74
|
60
|
|
75
|
61 abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
|
|
79
|
62 abc i<3 j<4 = ins2 3rot i<3 j<4
|
|
|
63
|
|
|
64 dba : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
|
|
|
65 dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4
|
|
|
66 aec : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
|
|
|
67 aec i<3 j<4 = ins2 (pinv 3rot) i<3 j<4
|
|
74
|
68
|
|
85
|
69 import Relation.Binary.Reasoning.Setoid as EqReasoning
|
|
|
70 abc→dba : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p= dba i<3 j<4
|
|
|
71 abc→dba i<3 j<4 = lemma where
|
|
|
72 open EqReasoning (Algebra.Group.setoid (Symmetric 5))
|
|
87
|
73 S = Symmetric 5
|
|
|
74 open Group (Symmetric 5)
|
|
|
75 postulate lemma : (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p= dba i<3 j<4
|
|
|
76 -- some kind of functional extentionaly required?
|
|
|
77 -- lemma = begin
|
|
|
78 -- abc i<3 j<4 ∘ₚ abc i<3 j<4
|
|
|
79 -- ≈⟨ prefl ⟩
|
|
|
80 -- ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 )) ∘ₚ
|
|
|
81 -- ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 ))
|
|
|
82 -- ≈⟨ ∙-flatten (Symmetric 5) (((am (save2 i<3 j<4) o am (pprep (pprep 3rot))) o am (flip (save2 i<3 j<4 ))) o
|
|
|
83 -- ((am (save2 i<3 j<4) o am (pprep (pprep 3rot))) o am ( flip (save2 i<3 j<4 )))) ⟩
|
|
|
84 -- save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ (
|
|
|
85 -- save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ pid )))))
|
|
|
86 -- ≈⟨ ∙-cong prefl ( ∙-cong prefl (grm S (proj₁ inverse _))) ⟩
|
|
|
87 -- save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ pid )))
|
|
|
88 -- ≈⟨ ∙-cong prefl (grepl S (pprep-cong prefl ) ) ⟩
|
|
|
89 -- (save2 i<3 j<4 ∘ₚ (pprep (pprep (3rot ∘ₚ 3rot)))) ∘ₚ flip (save2 i<3 j<4 )
|
|
|
90 -- ≈⟨ prefl ⟩
|
|
|
91 -- dba i<3 j<4
|
|
|
92 -- ∎
|
|
85
|
93
|
|
87
|
94 postulate -- someday
|
|
|
95 dba→aec : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → (dba i<3 j<4 ∘ₚ dba i<3 j<4 ) =p= aec i<3 j<4
|
|
|
96 aec→abc : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → (aec i<3 j<4 ∘ₚ aec i<3 j<4 ) =p= abc i<3 j<4
|
|
85
|
97
|
|
87
|
98 record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
|
|
77
|
99 field
|
|
82
|
100 dba0<3 : Fin 4
|
|
|
101 dba1<4 : Fin 5
|
|
|
102 aec0<3 : Fin 4
|
|
|
103 aec1<4 : Fin 5
|
|
87
|
104 abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (pinv rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]
|
|
83
|
105
|
|
85
|
106 open Triple
|
|
87
|
107 triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot
|
|
84
|
108 triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
|
|
|
109 triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
|
|
|
110 triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
|
|
|
111 triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
|
|
|
112 triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
|
|
|
113 triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl }
|
|
|
114 triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl }
|
|
|
115 triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
|
|
|
116 triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
|
|
|
117 triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
|
|
|
118 triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
|
|
|
119 triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
|
|
|
120 triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
|
|
|
121 triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
|
|
|
122 triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
|
|
|
123 triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
|
|
|
124 triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
|
|
|
125 triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
|
|
|
126 triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
|
|
80
|
127 triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =
|
|
84
|
128 record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
|
|
79
|
129
|
|
87
|
130 dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot )
|
|
|
131 dba-triple = ?
|
|
|
132
|
|
|
133 aec-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (pinv 3rot )
|
|
|
134 aec-triple = ?
|
|
|
135
|
|
74
|
136
|
|
84
|
137 dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
|
|
|
138 → deriving n (abc i<3 j<4 ) ∧ deriving n (dba i<3 j<4 ) ∧ deriving n (aec i<3 j<4 )
|
|
|
139 dervie-any-3rot 0 i<3 j<4 = ⟪ lift tt , ⟪ lift tt , lift tt ⟫ ⟫
|
|
87
|
140 dervie-any-3rot (suc i) i<3 j<4 = ⟪ d0 , ⟪ d1 , d2 ⟫ ⟫ where
|
|
|
141 tc : Triple i<3 j<4 3rot
|
|
|
142 tc = triple i<3 j<4
|
|
|
143 abc0 = abc i<3 j<4
|
|
|
144 b<3 = fin≤n {3} (dba0<3 tc)
|
|
|
145 b<4 = fin≤n {4} (dba1<4 tc)
|
|
|
146 dba0 = dba b<3 b<4
|
|
|
147 c<3 = fin≤n {3} (aec0<3 tc)
|
|
|
148 c<4 = fin≤n {4} (aec1<4 tc)
|
|
|
149 aec0 = aec c<3 c<4
|
|
|
150 d0 : deriving (suc i) (abc i<3 j<4)
|
|
|
151 d0 =
|
|
|
152 ccong {deriving i} ( psym (abc= tc )) (
|
|
|
153 comm {deriving i} {dba0} {aec0}
|
|
|
154 (proj1 (proj2 ( dervie-any-3rot i b<3 b<4)))
|
|
|
155 (proj2 (proj2 ( dervie-any-3rot i c<3 c<4 ))))
|
|
|
156 d1 : deriving (suc i) (dba i<3 j<4)
|
|
|
157 d1 =
|
|
|
158 ccong {deriving i} ( psym {!!}) ( -- dba i<3 j<4 =p= [ aec0 , abc0 ] -- dba= : dba b<3 b<4 =p= [ aec0 , abc0 ] is not enough...
|
|
|
159 comm {deriving i} {aec0} {abc0}
|
|
|
160 (proj2 (proj2 ( dervie-any-3rot i c<3 c<4 )))
|
|
|
161 (proj1 ( dervie-any-3rot i i<3 j<4 )))
|
|
|
162 d2 : deriving (suc i) (aec i<3 j<4)
|
|
|
163 d2 =
|
|
|
164 ccong {deriving i} ( psym {!!}) (
|
|
|
165 comm {deriving i} {abc0} {dba0}
|
|
|
166 (proj1 ( dervie-any-3rot i i<3 j<4 ))
|
|
|
167 (proj1 (proj2 ( dervie-any-3rot i b<3 b<4 ) )))
|
|
74
|
168
|
|
|
169 open _=p=_
|
|
77
|
170 counter-example : ¬ (abc 0<3 0<4 =p= pid )
|
|
85
|
171 counter-example eq with ←pleq _ _ eq
|
|
|
172 ... | ()
|
|
74
|
173
|
|
|
174
|
