Mercurial > hg > Members > kono > Proof > galois
view sym5.agda @ 83:f2edc816740b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 26 Aug 2020 19:53:24 +0900 |
| parents | fcb9e29d1894 |
| children | 7e36bd8916a9 |
line wrap: on
line source
open import Level hiding ( suc ; zero ) open import Algebra module sym5 where open import Symmetric open import Data.Unit using (⊤ ; tt ) open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) open import Function hiding (flip) open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) open import Data.Nat.Properties open import Relation.Nullary open import Data.Empty open import Data.Product open import Gutil open import Putil open import Solvable using (solvable) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Data.Fin hiding (_<_ ; _≤_ ; lift ) open import Data.Fin.Permutation open import Data.List hiding ( [_] ) open import nat open import fin ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) ) where -- -- dba 1320 d → b → a → d -- (dba)⁻¹ 3021 a → b → d → a -- aec 21430 -- (aec)⁻¹ 41032 -- (abd)(cea)(dba)(aec) -- open solvable open Solvable (Symmetric 5) end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid end5 x der = end sol x der 0<4 : 0 < 4 0<4 = s≤s z≤n 0<3 : 0 < 3 0<3 = s≤s z≤n --- 1 ∷ 2 ∷ 0 ∷ [] abc 3rot : Permutation 3 3 3rot = pid {3} ∘ₚ pins (n≤ 2) ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 ins2 abc i<3 j<4 = (save2 ∘ₚ (pprep (pprep abc))) ∘ₚ flip save2 where save2 : Permutation 5 5 save2 = ( (( pid {5} ∘ₚ flip (pins (s≤s i<3) ) )) ∘ₚ flip (pins j<4)) abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 abc i<3 j<4 = ins2 3rot i<3 j<4 dba : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4 aec : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 aec i<3 j<4 = ins2 (pinv 3rot) i<3 j<4 record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where field dba0<3 : Fin 4 dba1<4 : Fin 5 aec0<3 : Fin 4 aec1<4 : Fin 5 abc= : abc i<3 j<4 =p= [ dba (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , aec (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] open Triple -- d e a b c t1 = plist ( abc (n≤ 0) (n≤ 0) ) -- ( ∷ ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ no 4 on top ∷ plist ( abc (n≤ 0) (n≤ 1) ) -- ( ∷ ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ 342 043 312 ∷ plist ( abc (n≤ 0) (n≤ 2) ) -- (3 ∷ ∷ ∷ 4 ∷ 0 ∷ []) ∷ ∷ plist ( abc (n≤ 0) (n≤ 3) ) -- (2 ∷ ∷ 4 ∷ ∷ 0 ∷ []) ∷ ∷ plist ( abc (n≤ 0) (n≤ 4) ) -- (2 ∷ ∷ 3 ∷ 0 ∷ ∷ []) ∷ ∷ plist ( abc (n≤ 1) (n≤ 0) ) -- ( ∷ 3 ∷ ∷ 4 ∷ 1 ∷ []) ∷ ∷ plist ( abc (n≤ 1) (n≤ 1) ) -- ( ∷ 3 ∷ ∷ 4 ∷ 1 ∷ []) ∷ ∷ plist ( abc (n≤ 1) (n≤ 2) ) -- (3 ∷ ∷ ∷ 4 ∷ 0 ∷ []) ∷ ∷ plist ( abc (n≤ 1) (n≤ 3) ) -- (1 ∷ 4 ∷ ∷ ∷ 0 ∷ []) ∷ ∷ plist ( abc (n≤ 1) (n≤ 4) ) -- (1 ∷ 3 ∷ ∷ 0 ∷ ∷ []) ∷ ∷ plist ( abc (n≤ 2) (n≤ 0) ) -- ( ∷ 2 ∷ 4 ∷ ∷ 1 ∷ []) ∷ ∷ plist ( abc (n≤ 2) (n≤ 1) ) -- ( ∷ 2 ∷ 4 ∷ ∷ 1 ∷ []) ∷ ∷ plist ( abc (n≤ 2) (n≤ 2) ) -- (2 ∷ ∷ 4 ∷ ∷ 0 ∷ []) ∷ ∷ plist ( abc (n≤ 2) (n≤ 3) ) -- (1 ∷ 4 ∷ ∷ ∷ 0 ∷ []) ∷ ∷ plist ( abc (n≤ 2) (n≤ 4) ) -- (1 ∷ 2 ∷ 0 ∷ ∷ ∷ []) ∷ ∷ plist ( abc (n≤ 3) (n≤ 0) ) -- ( ∷ 2 ∷ 3 ∷ 1 ∷ ∷ []) ∷ ∷ plist ( abc (n≤ 3) (n≤ 1) ) -- ( ∷ 2 ∷ 3 ∷ 1 ∷ ∷ []) ∷ ∷ plist ( abc (n≤ 3) (n≤ 2) ) -- (2 ∷ ∷ 3 ∷ 0 ∷ ∷ []) ∷ ∷ plist ( abc (n≤ 3) (n≤ 3) ) -- (1 ∷ 3 ∷ ∷ 0 ∷ ∷ []) ∷ ∷ plist ( abc (n≤ 3) (n≤ 4) ) -- (1 ∷ 2 ∷ 0 ∷ ∷ ∷ []) ∷ [] ∷ [] td = plist ( dba (n≤ 0) (n≤ 0) ) -- ( ∷ ∷ 4 ∷ 2 ∷ 3 ∷ []) ∷ ∷ plist ( dba (n≤ 0) (n≤ 1) ) -- ( ∷ ∷ 4 ∷ 2 ∷ 3 ∷ []) ∷ ∷ plist ( dba (n≤ 0) (n≤ 2) ) -- (4 ∷ ∷ ∷ 0 ∷ 3 ∷ []) ∷ ∷ plist ( dba (n≤ 0) (n≤ 3) ) -- (4 ∷ ∷ 0 ∷ ∷ 2 ∷ []) ∷ ∷ plist ( dba (n≤ 0) (n≤ 4) ) -- (3 ∷ ∷ 0 ∷ 2 ∷ ∷ []) ∷ ∷ plist ( dba (n≤ 1) (n≤ 0) ) -- ( ∷ 4 ∷ ∷ 1 ∷ 3 ∷ []) ∷ ∷ plist ( dba (n≤ 1) (n≤ 1) ) -- ( ∷ 4 ∷ ∷ 1 ∷ 3 ∷ []) ∷ ∷ plist ( dba (n≤ 1) (n≤ 2) ) -- (4 ∷ ∷ ∷ 0 ∷ 3 ∷ []) ∷ ∷ plist ( dba (n≤ 1) (n≤ 3) ) -- (4 ∷ 0 ∷ ∷ ∷ 1 ∷ []) ∷ ∷ plist ( dba (n≤ 1) (n≤ 4) ) -- (3 ∷ 0 ∷ ∷ 1 ∷ ∷ []) ∷ ∷ plist ( dba (n≤ 2) (n≤ 0) ) -- ( ∷ 4 ∷ 1 ∷ ∷ 2 ∷ []) ∷ ∷ plist ( dba (n≤ 2) (n≤ 1) ) -- ( ∷ 4 ∷ 1 ∷ ∷ 2 ∷ []) ∷ ∷ plist ( dba (n≤ 2) (n≤ 2) ) -- (4 ∷ ∷ 0 ∷ ∷ 2 ∷ []) ∷ ∷ plist ( dba (n≤ 2) (n≤ 3) ) -- (4 ∷ 0 ∷ ∷ ∷ 1 ∷ []) ∷ ∷ plist ( dba (n≤ 2) (n≤ 4) ) -- (2 ∷ 0 ∷ 1 ∷ ∷ ∷ []) ∷ ∷ plist ( dba (n≤ 3) (n≤ 0) ) -- ( ∷ 3 ∷ 1 ∷ 2 ∷ ∷ []) ∷ ∷ plist ( dba (n≤ 3) (n≤ 1) ) -- ( ∷ 3 ∷ 1 ∷ 2 ∷ ∷ []) ∷ ∷ plist ( dba (n≤ 3) (n≤ 2) ) -- (3 ∷ ∷ 0 ∷ 2 ∷ ∷ []) ∷ ∷ plist ( dba (n≤ 3) (n≤ 3) ) -- (3 ∷ 0 ∷ ∷ 1 ∷ ∷ []) ∷ ∷ plist ( dba (n≤ 3) (n≤ 4) ) -- (2 ∷ 0 ∷ 1 ∷ ∷ ∷ []) ∷ [] ∷ [] --- 1 ∷ 2 ∷ 0 ∷ ∷ ∷ [] abc -- abc (n≤ 3) (n≤ 4) --- 3 ∷ 0 ∷ ∷ 1 ∷ ∷ [] dba dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 2) --- 4 ∷ ∷ 0 ∷ ∷ 2 ∷ [] aec aec99 = ins2 (pinv 3rot) (n≤ 1) (n≤ 4) tt1 = plist dba99 ∷ plist (pinv dba99) ∷ [] tt2 = plist aec99 ∷ plist (pinv aec99) ∷ [] tt5 = plist [ dba99 , aec99 ] -- =p= abc triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 triple z≤n z≤n = record { dba0<3 = {!!} ; dba1<4 = {!!} ; aec0<3 = {!!} ; aec1<4 = {!!} ; abc= = {!!} } triple z≤n (s≤s z≤n) = {!!} triple z≤n (s≤s (s≤s z≤n)) = {!!} triple z≤n (s≤s (s≤s (s≤s z≤n))) = {!!} triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!} triple (s≤s z≤n) z≤n = {!!} triple (s≤s z≤n) (s≤s z≤n) = {!!} triple (s≤s z≤n) (s≤s (s≤s z≤n)) = {!!} triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = {!!} triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!} triple (s≤s (s≤s z≤n)) z≤n = {!!} triple (s≤s (s≤s z≤n)) (s≤s z≤n) = {!!} triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = {!!} triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = {!!} triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = {!!} triple (s≤s (s≤s (s≤s z≤n))) z≤n = {!!} triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = {!!} triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = {!!} triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = {!!} triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 ) dervie-any-3rot 0 i<3 j<4 = lift tt dervie-any-3rot (suc i) i<3 j<4 = {!!} -- ccong {deriving i} ( abc= (triple i<3 j<4 ) ) ( -- comm {deriving i} {dba} {aec} -- ( dervie-any-3rot i (fin<n {3} {dba0<3 tc}) (fin<n {4} {dba1<4 tc}) ) -- ( dervie-any-3rot i (fin<n {3} {aec0<3 tc}) (fin<n {4} {aec1<4 tc}) )) where -- tc : Triple i<3 j<4 -- tc = triple i<3 j<4 -- dba : Permutation 5 5 -- dba = abc (fin<n {3} {dba0<3 tc}) (fin<n {4} {dba1<4 tc}) -- aec : Permutation 5 5 -- aec = abc (fin<n {3} {aec0<3 tc}) (fin<n {4} {aec1<4 tc}) open _=p=_ counter-example : ¬ (abc 0<3 0<4 =p= pid ) counter-example = {!!} -- p with peq p (# 1) -- ... | ()