Mercurial > hg > Members > kono > Proof > galois
annotate src/sym5n.agda @ 290:c870095531ef
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 29 Jan 2023 21:05:55 +0900 |
| parents | 6d1619d9f880 |
| children | f59a9f4cfd78 |
| 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 | |
| 253 | 62 open import Codata.Musical.Notation |
| 252 | 63 open import Data.Maybe hiding (_>>=_) |
| 253 | 64 open import Data.List |
| 65 open import Data.Char | |
| 252 | 66 open import IO.Primitive |
| 67 open import Codata.Musical.Costring | |
| 68 | |
| 69 postulate | |
| 253 | 70 getArgs : IO (List (List Char)) |
| 71 {-# FOREIGN GHC import qualified System.Environment #-} | |
| 252 | 72 {-# COMPILE GHC getArgs = System.Environment.getArgs #-} |
| 251 | 73 |
| 253 | 74 charToDigit : Char → Maybe ℕ |
| 75 charToDigit '0' = just ( 0) | |
| 76 charToDigit '1' = just ( 1) | |
| 77 charToDigit '2' = just ( 2) | |
| 78 charToDigit '3' = just ( 3) | |
| 79 charToDigit '4' = just ( 4) | |
| 80 charToDigit '5' = just ( 5) | |
| 81 charToDigit '6' = just ( 6) | |
| 82 charToDigit '7' = just ( 7) | |
| 83 charToDigit '8' = just ( 8) | |
| 84 charToDigit '9' = just ( 9) | |
| 252 | 85 charToDigit _ = nothing |
| 251 | 86 |
| 253 | 87 getNumArg1 : (List (List Char)) → ℕ |
| 252 | 88 getNumArg1 [] = 0 |
| 253 | 89 getNumArg1 ([] ∷ y) = 0 |
| 90 getNumArg1 ((x ∷ _) ∷ y) with charToDigit x | |
| 252 | 91 ... | just n = n |
| 92 ... | nothing = 0 | |
| 93 | |
| 254 | 94 |
| 95 -- | |
| 96 -- CommFListN 5 x is too slow use compiler | |
| 97 -- agda --compile sym5n.agda | |
| 98 -- | |
| 253 | 99 |
| 252 | 100 main : IO ⊤ |
| 253 | 101 main = getArgs >>= (λ x → putStrLn $ toCostring $ sym5solvable $ getNumArg1 x ) |
| 252 | 102 |
| 253 | 103 |