Mercurial > hg > Members > kono > Proof > galois

comparison sym3.agda @ 121:54035eed6b9b

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 Fri, 04 Sep 2020 12:37:54 +0900
parents 77cb357b81a9
children 61310d395c1b
comparison
equal deleted inserted replaced
120:77cb357b81a9 121:54035eed6b9b
15 open import Putil 15 open import Putil
16 open import Solvable using (solvable) 16 open import Solvable using (solvable)
17 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 17 open import Relation.Binary.PropositionalEquality hiding ( [_] )
18 18
19 open import Data.Fin 19 open import Data.Fin
20 open import Data.Fin.Permutation 20 open import Data.Fin.Permutation hiding (_∘ₚ_)
21
22 infixr 200 _∘ₚ_
23 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
24
21 25
22 sym3solvable : solvable (Symmetric 3) 26 sym3solvable : solvable (Symmetric 3)
23 solvable.dervied-length sym3solvable = 2 27 solvable.dervied-length sym3solvable = 2
24 solvable.end sym3solvable x d = solved1 x d where 28 solvable.end sym3solvable x d = solved1 x d where
25 29
50 54
51 stage1 : (x : Permutation 3 3) → Set (Level.suc Level.zero) 55 stage1 : (x : Permutation 3 3) → Set (Level.suc Level.zero)
52 stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x 56 stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x
53 57
54 open import logic 58 open import logic
59
60 p33=4 : ( p3 ∘ₚ p3 ) =p= p4
61 p33=4 = pleq _ _ refl
62
63 p44=3 : ( p4 ∘ₚ p4 ) =p= p3
64 p44=3 = pleq _ _ refl
65
66 p34=0 : ( p3 ∘ₚ p4 ) =p= pid
67 p34=0 = pleq _ _ refl
68
69 p43=0 : ( p4 ∘ₚ p3 ) =p= pid
70 p43=0 = pleq _ _ refl
71
72 open ≡-Reasoning
73
74 st01 : ( x y : Permutation 3 3) → x =p= p3 → y =p= p3 → x ∘ₚ y =p= p4
75 st01 x y s t = record { peq = λ q → ( begin
76 (x ∘ₚ y) ⟨$⟩ʳ q
77 ≡⟨ peq ( presp s t ) q ⟩
78 ( p3 ∘ₚ p3 ) ⟨$⟩ʳ q
79 ≡⟨ peq p33=4 q ⟩
80 p4 ⟨$⟩ʳ q
81 ∎ ) }
82
83 st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
84 st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
85 ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (record { peq = λ q → begin (
86 [ g , h ] ⟨$⟩ʳ q
87 ≡⟨ ( peq (comm-cong-l {h} {g} {pid} (FL-inject ge )) ) q ⟩
88 [ pid , h ] ⟨$⟩ʳ q
89 ≡⟨ peq (idcomtl h) q ⟩
90 q
91 ∎ ) } )
92 ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } =
93 case1 (record { peq = λ q → trans (( peq (comm-cong-r {h} {g} {pid} (FL-inject he )) ) q) (peq (idcomtr g) q) } )
94 ... | (zero :: (suc zero) :: (zero :: f0 )) | t | se | te = {!!}
95 ... | (suc zero) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
96 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | t | se | te = {!!}
97 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
98 ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | t | se | te = {!!}
55 99
56 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 ) 100 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
57 stage12 x uni = case1 prefl 101 stage12 x uni = case1 prefl
58 stage12 x (comm x1 y1 ) = {!!} 102 stage12 x (comm {g} {h} x1 y1 ) = st02 g h
59 stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy -- x =p= pid : t , y =p= pid : s 103 stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy
60 ... | case1 t | case1 s = case1 ( {!!} ) 104 ... | case1 t | case1 s = case1 ( record { peq = λ q → peq (presp t s) q} )
61 ... | case1 t | case2 (case1 x₁) = {!!} 105 ... | case1 t | case2 (case1 s) = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } ))
62 ... | case1 t | case2 (case2 x₁) = {!!} 106 ... | case1 t | case2 (case2 s) = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } ))
63 ... | case2 t | case1 s = {!!} 107 ... | case2 (case1 t) | case1 s = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } ))
64 ... | case2 (case1 s) | case2 (case1 t) = case2 (case2 (pleq _ _ {!!} )) 108 ... | case2 (case2 t) | case1 s = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } ))
65 ... | case2 (case1 s) | case2 (case2 t) = {!!} 109 ... | case2 (case1 s) | case2 (case1 t) = case2 (case2 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p33=4 q) } )
66 ... | case2 (case2 s) | case2 (case1 t) = {!!} 110 ... | case2 (case1 s) | case2 (case2 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p34=0 q) }
67 ... | case2 (case2 s) | case2 (case2 t) = {!!} 111 ... | case2 (case2 s) | case2 (case1 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p43=0 q) }
112 ... | case2 (case2 s) | case2 (case2 t) = case2 (case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p44=3 q) } )
68 stage12 _ (ccong {y} x=y sx) with stage12 y sx 113 stage12 _ (ccong {y} x=y sx) with stage12 y sx
69 ... | case1 id = case1 ( ptrans (psym x=y ) id ) 114 ... | case1 id = case1 ( ptrans (psym x=y ) id )
70 ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ )) 115 ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ ))
71 ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ )) 116 ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ ))
72 117