Mercurial > hg > Members > kono > Proof > galois

annotate sym5n.agda @ 205:0525f4dabdbc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 02 Dec 2020 11:35:54 +0900
parents 59d12d02dfa8
children d782dd481a26
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level hiding ( suc ; zero )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Algebra
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
3 module sym5n where
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Symmetric
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.Unit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Function
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Nullary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Empty
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Data.Product
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import Gutil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import Putil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open import Solvable using (solvable)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open import Relation.Binary.PropositionalEquality hiding ( [_] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 open import Data.Fin
88
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
20 open import Data.Fin.Permutation hiding (_∘ₚ_)
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
88
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
22 infixr 200 _∘ₚ_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
23 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
24
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
25 sym5solvable : ¬ solvable (Symmetric 5)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
26 sym5solvable = {!!} where
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
28 open import Data.List using ( List ; [] ; _∷_ )
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
29 open Solvable (Symmetric 5)
111
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
30
153
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
31 open import FLutil
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
32 open import Data.List.Fresh hiding ([_])
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
33 open import Relation.Nary using (⌊_⌋)
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
34
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
35 p0id : FL→perm (zero :: zero :: zero :: (zero :: (zero :: f0))) =p= pid
111
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
36 p0id = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
37
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
38 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
39 open import FLComm
111
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
40
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
41 stage4FList = CommFListN 5 2
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
42