Mercurial > hg > Members > kono > Proof > galois

annotate sym3n.agda @ 193:f9aa8bb5fb1d

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 Sun, 29 Nov 2020 09:36:16 +0900
parents 59d12d02dfa8
children
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
153
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
3 module sym3n 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
121
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
20 open import Data.Fin.Permutation hiding (_∘ₚ_)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
21
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
22 infixr 200 _∘ₚ_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
23 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
24
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
26 sym3solvable : solvable (Symmetric 3)
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
27 solvable.dervied-length sym3solvable = 2
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
28 solvable.end sym3solvable x d = solved1 x d where
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
30 open import Data.List using ( List ; [] ; _∷_ )
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
31
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
32 open Solvable (Symmetric 3)
153
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
33 open import FLutil
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
34 open import Data.List.Fresh hiding ([_])
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
35 open import Relation.Nary using (⌊_⌋)
111
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
36
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
37 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
153
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
38 p0id = pleq _ _ refl
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
39
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
40 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
41 open import FLComm
153
d880595eae30 FLinsert-mb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
42
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
43 stage3FList : CommFListN 3 2 ≡ cons (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
44 stage3FList = refl
88
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
45
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
46 solved1 : (x : Permutation 3 3) → deriving 2 x → x =p= pid
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
47 solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
48 solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 )
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
49 solved2 = CommStage→ 3 2 x dr
123
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
50
119
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
51