Mercurial > hg > Members > kono > Proof > galois

annotate sym3.agda @ 111:d3da6e2c0d90

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 Tue, 01 Sep 2020 21:58:15 +0900
parents 405c1f727ffe
children 2dae51792e1a
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
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
3 module sym3 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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 open import Data.Fin.Permutation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
22 sym3solvable : solvable (Symmetric 3)
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
23 solvable.dervied-length sym3solvable = 2
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
24 solvable.end sym3solvable x d = solved1 x d where
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 open import Data.List using ( List ; [] ; _∷_ )
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
27
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
28 open Solvable (Symmetric 3)
111
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
29
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
30 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
31 p0id = pleq _ _ refl
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
111
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
33 p0 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
34 p1 = FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
35 p2 = FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
36 p3 = FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
37 p4 = FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
38 p5 = FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
39 t0 = plist p0 ∷ plist p1 ∷ plist p2 ∷ plist p3 ∷ plist p4 ∷ plist p5 ∷ []
88
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
40
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
41 open _=p=_
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
42
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
43 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
44 solved1 = {!!}