Mercurial > hg > Members > kono > Proof > galois

comparison sym3.agda @ 124:803a45b280ef

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 19:07:39 +0900
parents 465c42c9a99e
children 11ccc9fe91c3
comparison
equal deleted inserted replaced
123:465c42c9a99e 124:803a45b280ef
95 -- ≡⟨ peq p33=4 q ⟩ 95 -- ≡⟨ peq p33=4 q ⟩
96 -- p4 ⟨$⟩ʳ q 96 -- p4 ⟨$⟩ʳ q
97 -- ∎ ) } 97 -- ∎ ) }
98 98
99 st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4) 99 st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
100 st02 = {!!} 100 st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
101 -- st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h 101 ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
102 -- ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) ) 102 ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
103 -- ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) ) 103 ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
104 -- ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = {!!} 104 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
105 -- ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = {!!} 105 ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
106 -- ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = {!!} 106 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
107 -- ... | (zero :: (suc zero) :: (zero :: f0 )) | t | se | te = {!!} 107 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
108 -- ... | (suc zero) :: (zero :: (zero :: f0 )) | t | se | te = {!!} 108 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
109 -- ... | (suc zero) :: (suc zero :: (zero :: f0 )) | t | se | te = {!!} 109 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } =
110 -- ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | t | se | te = {!!} 110 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
111 -- ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | t | se | te = {!!} 111 ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } | record { eq = he } =
112 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
113 ... | (zero :: (suc zero) :: (zero :: f0 )) | t | se | te = {!!}
114 ... | (suc zero) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
115 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | t | se | te = {!!}
116 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
117 ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | t | se | te = {!!}
112 118
113 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 ) 119 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
114 stage12 = {!!} 120 stage12 = {!!}
115 -- stage12 x uni = case1 prefl 121 -- stage12 x uni = case1 prefl
116 -- stage12 x (comm {g} {h} x1 y1 ) = st02 g h 122 -- stage12 x (comm {g} {h} x1 y1 ) = st02 g h
150 ≡⟨ sym (f=g q) ⟩ 156 ≡⟨ sym (f=g q) ⟩
151 f ⟨$⟩ʳ q 157 f ⟨$⟩ʳ q
152 ≡⟨ f=e q ⟩ 158 ≡⟨ f=e q ⟩
153 q 159 q
154 ∎ 160 ∎
155 solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y 161 solved1 _ (comm {g} {h} x y) = {!!}
156 ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl) 162 -- solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y
157 ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h) 163 -- ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
158 ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g) 164 -- ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
159 ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com33 q) } 165 -- ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g)
160 ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com44 q) } 166 -- ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com33 q) }
161 ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com34 q) } 167 -- ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com44 q) }
162 ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com43 q) } 168 -- ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com34 q) }
169 -- ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com43 q) }
163 170
164 -- = ptrans ( comm-resp {g} {h} t s ) ( comm-refl ? ) 171 -- = ptrans ( comm-resp {g} {h} t s ) ( comm-refl ? )