Mercurial > hg > Members > kono > Proof > galois

comparison src/sym5a.agda @ 255:6d1619d9f880

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
library
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Jan 2021 10:18:08 +0900
parents sym5a.agda@d782dd481a26
children f59a9f4cfd78
comparison
equal deleted inserted replaced
254:a5b3061f15ee 255:6d1619d9f880
1 open import Level hiding ( suc ; zero )
2 open import Algebra
3 module sym5a where
4
5 open import Symmetric
6 open import Data.Unit using (⊤ ; tt )
7 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
8 open import Function hiding (flip)
9 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
10 open import Data.Nat.Properties
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
20 open import Data.Fin hiding (_<_ ; _≤_ ; lift )
21 open import Data.Fin.Permutation hiding (_∘ₚ_)
22
23 infixr 200 _∘ₚ_
24 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
25
26 open import Data.List hiding ( [_] )
27 open import nat
28 open import fin
29 open import logic
30
31 open _∧_
32
33 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
34 ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (any3de (dervied-length sol) 3rot 0<3 0<4 ) ) where
35 --
36 -- dba 1320 d → b → a → d
37 -- (dba)⁻¹ 3021 a → b → d → a
38 -- aec 21430
39 -- (aec)⁻¹ 41032
40 -- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc
41 -- so commutator always contains abc, dba and aec
42
43 open ≡-Reasoning
44
45 open solvable
46 open Solvable ( Symmetric 5)
47 end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid
48 end5 x der = end sol x der
49
50 0<4 : 0 < 4
51 0<4 = s≤s z≤n
52
53 0<3 : 0 < 3
54 0<3 = s≤s z≤n
55
56 --- 1 ∷ 2 ∷ 0 ∷ [] abc
57 3rot : Permutation 3 3
58 3rot = pid {3} ∘ₚ pins (n≤ 2)
59
60 save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
61 save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4)
62
63 -- Permutation 5 5 include any Permutation 3 3
64 any3 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
65 any3 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 )
66
67 any3cong : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → any3 x i<3 j<4 =p= any3 y i<3 j<4
68 any3cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )}
69 (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl
70
71 open _=p=_
72
73 -- derving n includes any Permutation 3 3,
74 any3de : {i j : ℕ } → (n : ℕ) → (abc : Permutation 3 3) → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (any3 abc i<3 j<4)
75 any3de {i} {j} zero abc i<3 j<4 = Level.lift tt
76 any3de {i} {j} (suc n) abc i<3 j<4 = ccong abc-from-comm (comm (any3de n (abc ∘ₚ abc) i<3 j0<4 ) (any3de n (abc ∘ₚ abc) i0<3 j<4 )) where
77 i0 : ℕ
78 i0 = ?
79 j0 : ℕ
80 j0 = ?
81 i0<3 : i0 ≤ 3
82 i0<3 = {!!}
83 j0<4 : j0 ≤ 4
84 j0<4 = {!!}
85 abc-from-comm : [ any3 (abc ∘ₚ abc) i<3 j0<4 , any3 (abc ∘ₚ abc) i0<3 j<4 ] =p= any3 abc i<3 j<4
86 abc-from-comm = {!!}
87
88 abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5
89 abc i<3 j<4 = any3 3rot i<3 j<4
90
91 counter-example : ¬ (abc 0<3 0<4 =p= pid )
92 counter-example eq with ←pleq _ _ eq
93 ... | ()
94