Mercurial > hg > Members > kono > Proof > galois

annotate src/sym2n.agda @ 274:691b2ee844ef

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 Thu, 26 Jan 2023 01:16:38 +0900
parents 6d1619d9f880
children 77f01da94c4e
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
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
3 module sym2n 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
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
26 sym2solvable : solvable (Symmetric 2)
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
27 solvable.dervied-length sym2solvable = 1
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
28 solvable.end sym2solvable 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
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
32 open Solvable (Symmetric 2)
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
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
37 p0id : FL→perm ((# 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 stage2FList : CommFListN 2 1 ≡ cons (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 stage2FList = 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 2 2) → deriving 1 x → x =p= pid
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
47 solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList p0id solved0 where
182
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
48 solved0 : Any (perm→FL x ≡_) ( CommFListN 2 1 )
eb94265d2a39 Any based proof computation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 162
diff changeset
49 solved0 = CommStage→ 2 1 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