Mercurial > hg > Members > kono > Proof > galois
annotate src/sym5a.agda @ 274:691b2ee844ef
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 26 Jan 2023 01:16:38 +0900 |
| parents | 6d1619d9f880 |
| children | f59a9f4cfd78 |
| rev | line source |
|---|---|
| 68 | 1 open import Level hiding ( suc ; zero ) |
| 2 open import Algebra | |
| 251 | 3 module sym5a 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 ) |
|
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
21 open import Data.Fin.Permutation hiding (_∘ₚ_) |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
22 |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
23 infixr 200 _∘ₚ_ |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
24 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_ |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
25 |
| 73 | 26 open import Data.List hiding ( [_] ) |
| 75 | 27 open import nat |
| 77 | 28 open import fin |
| 84 | 29 open import logic |
| 30 | |
| 31 open _∧_ | |
| 68 | 32 |
| 33 ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) | |
| 251 | 34 ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (any3de (dervied-length sol) 3rot 0<3 0<4 ) ) where |
| 73 | 35 -- |
| 36 -- dba 1320 d → b → a → d | |
| 37 -- (dba)⁻¹ 3021 a → b → d → a | |
| 38 -- aec 21430 | |
| 39 -- (aec)⁻¹ 41032 | |
|
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
40 -- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc |
|
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
41 -- so commutator always contains abc, dba and aec |
| 73 | 42 |
| 112 | 43 open ≡-Reasoning |
| 44 | |
| 73 | 45 open solvable |
| 112 | 46 open Solvable ( Symmetric 5) |
| 73 | 47 end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid |
| 48 end5 x der = end sol x der | |
| 49 | |
| 74 | 50 0<4 : 0 < 4 |
| 75 | 51 0<4 = s≤s z≤n |
| 74 | 52 |
| 53 0<3 : 0 < 3 | |
| 75 | 54 0<3 = s≤s z≤n |
| 74 | 55 |
| 79 | 56 --- 1 ∷ 2 ∷ 0 ∷ [] abc |
| 74 | 57 3rot : Permutation 3 3 |
| 79 | 58 3rot = pid {3} ∘ₚ pins (n≤ 2) |
| 59 | |
| 85 | 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 | |
| 251 | 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 ) | |
| 74 | 66 |
| 251 | 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 )} | |
|
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
69 (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl |
| 112 | 70 |
| 71 open _=p=_ | |
| 72 | |
| 251 | 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 | |
| 75 | 88 abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 |
| 251 | 89 abc i<3 j<4 = any3 3rot i<3 j<4 |
| 74 | 90 |
| 184 | 91 counter-example : ¬ (abc 0<3 0<4 =p= pid ) |
| 92 counter-example eq with ←pleq _ _ eq | |
| 93 ... | () | |
| 94 |