Mercurial > hg > Members > kono > Proof > galois
annotate sym5n.agda @ 251:d782dd481a26
compile
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 12 Dec 2020 20:28:29 +0900 |
| parents | 59d12d02dfa8 |
| children | e937bf565bf8 |
| rev | line source |
|---|---|
| 68 | 1 open import Level hiding ( suc ; zero ) |
| 2 open import Algebra | |
| 184 | 3 module sym5n 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 | |
| 251 | 25 -- open import IO |
| 26 open import Data.String hiding (toList) | |
| 27 open import Data.Unit | |
| 28 open import Agda.Builtin.String | |
| 29 | |
| 30 sym5solvable : (n : ℕ) → String -- ¬ solvable (Symmetric 5) | |
| 31 sym5solvable n = FListtoStr (CommFListN 5 n) where | |
| 68 | 32 |
| 70 | 33 open import Data.List using ( List ; [] ; _∷_ ) |
| 184 | 34 open Solvable (Symmetric 5) |
| 111 | 35 |
| 153 | 36 open import FLutil |
| 37 open import Data.List.Fresh hiding ([_]) | |
| 38 open import Relation.Nary using (⌊_⌋) | |
| 39 | |
| 184 | 40 p0id : FL→perm (zero :: zero :: zero :: (zero :: (zero :: f0))) =p= pid |
| 111 | 41 p0id = pleq _ _ refl |
| 42 | |
|
182
eb94265d2a39
Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
162
diff
changeset
|
43 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
|
44 open import FLComm |
| 111 | 45 |
| 251 | 46 |
| 47 stage4FList = CommFListN 5 0 | |
| 48 stage6FList = CommFListN 5 3 | |
| 49 | |
| 50 -- stage5FList = {!!} | |
| 51 -- s2=s3 : CommFListN 5 2 ≡ CommFListN 5 3 | |
| 52 -- s2=s3 = refl | |
| 53 | |
| 54 FLtoStr : {n : ℕ} → (x : FL n) → String | |
| 55 FLtoStr f0 = "f0" | |
| 56 FLtoStr (x :: y) = primStringAppend ( primStringAppend (primShowNat (toℕ x)) " :: " ) (FLtoStr y) | |
| 57 | |
| 58 FListtoStr : {n : ℕ} → (x : FList n) → String | |
| 59 FListtoStr [] = "" | |
| 60 FListtoStr (cons a x x₁) = primStringAppend (FLtoStr a) (primStringAppend "\n" (FListtoStr x)) | |
| 61 | |
| 62 open import IO -- using (IO) | |
| 63 | |
| 64 main = run ( putStrLn $ sym5solvable 4) | |
| 65 |