Mercurial > hg > Members > kono > Proof > galois

comparison src/sym5n.agda @ 255:6d1619d9f880

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
library
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Jan 2021 10:18:08 +0900
parents sym5n.agda@a5b3061f15ee
children f59a9f4cfd78
comparison
equal deleted inserted replaced
254:a5b3061f15ee 255:6d1619d9f880
1 open import Level hiding ( suc ; zero )
2 open import Algebra
3 module sym5n where
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
20 open import Data.Fin.Permutation hiding (_∘ₚ_)
21
22 infixr 200 _∘ₚ_
23 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
24
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
32
33 open import Data.List using ( List ; [] ; _∷_ )
34 open Solvable (Symmetric 5)
35
36 open import FLutil
37 open import Data.List.Fresh hiding ([_])
38 open import Relation.Nary using (⌊_⌋)
39
40 p0id : FL→perm (zero :: zero :: zero :: (zero :: (zero :: f0))) =p= pid
41 p0id = pleq _ _ refl
42
43 open import Data.List.Fresh.Relation.Unary.Any
44 open import FLComm
45
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 Codata.Musical.Notation
63 open import Data.Maybe hiding (_>>=_)
64 open import Data.List
65 open import Data.Char
66 open import IO.Primitive
67 open import Codata.Musical.Costring
68
69 postulate
70 getArgs : IO (List (List Char))
71 {-# FOREIGN GHC import qualified System.Environment #-}
72 {-# COMPILE GHC getArgs = System.Environment.getArgs #-}
73
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)
85 charToDigit _ = nothing
86
87 getNumArg1 : (List (List Char)) → ℕ
88 getNumArg1 [] = 0
89 getNumArg1 ([] ∷ y) = 0
90 getNumArg1 ((x ∷ _) ∷ y) with charToDigit x
91 ... | just n = n
92 ... | nothing = 0
93
94
95 --
96 -- CommFListN 5 x is too slow use compiler
97 -- agda --compile sym5n.agda
98 --
99
100 main : IO ⊤
101 main = getArgs >>= (λ x → putStrLn $ toCostring $ sym5solvable $ getNumArg1 x )
102
103