Mercurial > hg > Members > kono > Proof > galois
annotate src/sym4.agda @ 274:691b2ee844ef
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 26 Jan 2023 01:16:38 +0900 |
| parents | 6d1619d9f880 |
| children | 77f01da94c4e |
| rev | line source |
|---|---|
| 68 | 1 open import Level hiding ( suc ; zero ) |
| 2 open import Algebra | |
| 88 | 3 module sym4 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 | |
| 88 | 20 open import Data.Fin.Permutation hiding (_∘ₚ_) |
| 68 | 21 |
| 88 | 22 infixr 200 _∘ₚ_ |
| 23 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_ | |
| 24 | |
| 25 sym4solvable : solvable (Symmetric 4) | |
| 26 solvable.dervied-length sym4solvable = 3 | |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
27 solvable.end sym4solvable x d = solved1 x d where |
| 68 | 28 |
| 70 | 29 open import Data.List using ( List ; [] ; _∷_ ) |
| 88 | 30 open Solvable (Symmetric 4) |
| 31 | |
| 32 -- Klien | |
| 33 -- | |
| 34 -- 1 (1,2),(3,4) (1,3),(2,4) (1,4),(2,3) | |
| 35 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] , 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] , 2 ∷ 3 ∷ 0 ∷ 1 ∷ [] , 3 ∷ 2 ∷ 1 ∷ 0 ∷ [] , | |
| 36 | |
| 37 a0 = pid {4} | |
| 38 a1 = pswap (pswap (pid {0})) | |
| 39 a2 = pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) | |
| 40 a3 = pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2}) | |
| 41 | |
| 42 k3 = plist (a1 ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3) ∷ plist (a2 ∘ₚ a1 ) ∷ [] | |
| 111 | 43 |
| 153 | 44 open import FLutil |
| 45 open import Data.List.Fresh hiding ([_]) | |
| 46 open import Relation.Nary using (⌊_⌋) | |
| 47 | |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
48 p0id : FL→perm ((# 0) :: (# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid |
| 111 | 49 p0id = pleq _ _ refl |
| 50 | |
| 127 | 51 |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
52 open import Data.List.Fresh.Relation.Unary.Any |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
53 open import FLComm |
| 111 | 54 |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
55 stage3FList : CommFListN 4 3 ≡ cons (zero :: zero :: zero :: zero :: f0) [] (Level.lift tt) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
56 stage3FList = refl |
| 251 | 57 |
| 58 st3 = proj₁ (toList ( CommFListN 4 2 )) | |
| 59 -- st4 = {!!} | |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
60 |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
61 solved1 : (x : Permutation 4 4) → deriving 3 x → x =p= pid |
| 184 | 62 solved1 x dr = CommSolved 4 x ( CommFListN 4 3 ) stage3FList p0id solved2 where |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
63 -- p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
64 solved2 : Any (perm→FL x ≡_) ( CommFListN 4 3 ) |
|
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
65 solved2 = CommStage→ 4 3 x dr |