Mercurial > hg > Members > kono > Proof > galois
annotate src/sym5a.agda @ 320:8fb16f9a882a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 19 Sep 2023 11:11:38 +0900 |
| parents | fff18d4a063b |
| children |
| rev | line source |
|---|---|
|
318
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
292
diff
changeset
|
1 {-# OPTIONS --cubical-compatible --safe #-} |
|
fff18d4a063b
use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
292
diff
changeset
|
2 |
| 292 | 3 -- |
| 4 -- checking does not terminate, sorry | |
| 5 -- | |
| 68 | 6 open import Level hiding ( suc ; zero ) |
| 7 open import Algebra | |
| 251 | 8 module sym5a where |
| 68 | 9 |
| 10 open import Symmetric | |
| 75 | 11 open import Data.Unit using (⊤ ; tt ) |
| 68 | 12 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) |
| 75 | 13 open import Function hiding (flip) |
| 68 | 14 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) |
| 75 | 15 open import Data.Nat.Properties |
| 68 | 16 open import Relation.Nullary |
| 17 open import Data.Empty | |
| 18 open import Data.Product | |
| 19 | |
| 20 open import Gutil | |
| 21 open import Putil | |
| 22 open import Solvable using (solvable) | |
| 23 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 24 | |
| 75 | 25 open import Data.Fin hiding (_<_ ; _≤_ ; lift ) |
|
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
26 open import Data.Fin.Permutation hiding (_∘ₚ_) |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
27 |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
28 infixr 200 _∘ₚ_ |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
29 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_ |
|
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
30 |
| 73 | 31 open import Data.List hiding ( [_] ) |
| 75 | 32 open import nat |
| 77 | 33 open import fin |
| 84 | 34 open import logic |
| 35 | |
| 36 open _∧_ | |
| 68 | 37 |
| 38 ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) | |
| 251 | 39 ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (any3de (dervied-length sol) 3rot 0<3 0<4 ) ) where |
| 73 | 40 -- |
| 41 -- dba 1320 d → b → a → d | |
| 42 -- (dba)⁻¹ 3021 a → b → d → a | |
| 43 -- aec 21430 | |
| 44 -- (aec)⁻¹ 41032 | |
|
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
45 -- [ 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
|
46 -- so commutator always contains abc, dba and aec |
| 73 | 47 |
| 112 | 48 open ≡-Reasoning |
| 49 | |
| 73 | 50 open solvable |
| 112 | 51 open Solvable ( Symmetric 5) |
| 73 | 52 end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid |
| 53 end5 x der = end sol x der | |
| 54 | |
| 74 | 55 0<4 : 0 < 4 |
| 75 | 56 0<4 = s≤s z≤n |
| 74 | 57 |
| 58 0<3 : 0 < 3 | |
| 75 | 59 0<3 = s≤s z≤n |
| 74 | 60 |
| 79 | 61 --- 1 ∷ 2 ∷ 0 ∷ [] abc |
| 74 | 62 3rot : Permutation 3 3 |
| 79 | 63 3rot = pid {3} ∘ₚ pins (n≤ 2) |
| 64 | |
| 85 | 65 save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 |
| 66 save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) | |
| 67 | |
| 251 | 68 -- Permutation 5 5 include any Permutation 3 3 |
| 69 any3 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 | |
| 70 any3 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) | |
| 74 | 71 |
| 251 | 72 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 |
| 73 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
|
74 (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl |
| 112 | 75 |
| 76 open _=p=_ | |
| 77 | |
| 251 | 78 -- derving n includes any Permutation 3 3, |
| 79 any3de : {i j : ℕ } → (n : ℕ) → (abc : Permutation 3 3) → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (any3 abc i<3 j<4) | |
| 80 any3de {i} {j} zero abc i<3 j<4 = Level.lift tt | |
| 81 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 | |
| 82 i0 : ℕ | |
| 83 i0 = ? | |
| 84 j0 : ℕ | |
| 85 j0 = ? | |
| 86 i0<3 : i0 ≤ 3 | |
| 87 i0<3 = {!!} | |
| 88 j0<4 : j0 ≤ 4 | |
| 89 j0<4 = {!!} | |
| 90 abc-from-comm : [ any3 (abc ∘ₚ abc) i<3 j0<4 , any3 (abc ∘ₚ abc) i0<3 j<4 ] =p= any3 abc i<3 j<4 | |
| 91 abc-from-comm = {!!} | |
| 92 | |
| 75 | 93 abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 |
| 251 | 94 abc i<3 j<4 = any3 3rot i<3 j<4 |
| 74 | 95 |
| 184 | 96 counter-example : ¬ (abc 0<3 0<4 =p= pid ) |
| 97 counter-example eq with ←pleq _ _ eq | |
| 98 ... | () | |
| 99 |