Mercurial > hg > Members > kono > Proof > galois

comparison sym3.agda @ 122:61310d395c1b

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 17:05:15 +0900
parents 54035eed6b9b
children 465c42c9a99e
comparison
equal deleted inserted replaced
121:54035eed6b9b 122:61310d395c1b
67 p34=0 = pleq _ _ refl 67 p34=0 = pleq _ _ refl
68 68
69 p43=0 : ( p4 ∘ₚ p3 ) =p= pid 69 p43=0 : ( p4 ∘ₚ p3 ) =p= pid
70 p43=0 = pleq _ _ refl 70 p43=0 = pleq _ _ refl
71 71
72 pFL : ( g : Permutation 3 3) → { x : FL 3 } → perm→FL g ≡ x → g =p= FL→perm x
73 pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl )
74
72 open ≡-Reasoning 75 open ≡-Reasoning
73 76
74 st01 : ( x y : Permutation 3 3) → x =p= p3 → y =p= p3 → x ∘ₚ y =p= p4 77 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 78 st01 x y s t = record { peq = λ q → ( begin
76 (x ∘ₚ y) ⟨$⟩ʳ q 79 (x ∘ₚ y) ⟨$⟩ʳ q
80 p4 ⟨$⟩ʳ q 83 p4 ⟨$⟩ʳ q
81 ∎ ) } 84 ∎ ) }
82 85
83 st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4) 86 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 87 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 ( 88 ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
86 [ g , h ] ⟨$⟩ʳ q 89 ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
87 ≡⟨ ( peq (comm-cong-l {h} {g} {pid} (FL-inject ge )) ) q ⟩ 90 ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
88 [ pid , h ] ⟨$⟩ʳ q 91 case1 (ptrans (comm-resp (pFL g ge) (pFL h he) ) (comm-refl {FL→perm (zero :: (suc zero) :: (zero :: f0 ))} prefl ))
89 ≡⟨ peq (idcomtl h) q ⟩ 92 ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
90 q 93 case1 (ptrans (comm-resp (pFL g ge) (pFL h he) ) (comm-refl {FL→perm ((suc zero) :: (zero :: (zero :: f0 )))} prefl ))
91 ∎ ) } ) 94 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
92 ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = 95 case1 (ptrans (comm-resp (pFL g ge) (pFL h he) ) (comm-refl {FL→perm ((suc zero) :: (suc zero :: (zero :: f0 )))} prefl ))
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 = {!!} 96 ... | (zero :: (suc zero) :: (zero :: f0 )) | t | se | te = {!!}
95 ... | (suc zero) :: (zero :: (zero :: f0 )) | t | se | te = {!!} 97 ... | (suc zero) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
96 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | t | se | te = {!!} 98 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | t | se | te = {!!}
97 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | t | se | te = {!!} 99 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
98 ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | t | se | te = {!!} 100 ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | t | se | te = {!!}