Mercurial > hg > Members > kono > Proof > galois
diff sym3.agda @ 122:61310d395c1b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 04 Sep 2020 17:05:15 +0900 |
| parents | 54035eed6b9b |
| children | 465c42c9a99e |
line wrap: on
line diff
--- a/sym3.agda Fri Sep 04 12:37:54 2020 +0900 +++ b/sym3.agda Fri Sep 04 17:05:15 2020 +0900 @@ -69,6 +69,9 @@ p43=0 : ( p4 ∘ₚ p3 ) =p= pid p43=0 = pleq _ _ refl + pFL : ( g : Permutation 3 3) → { x : FL 3 } → perm→FL g ≡ x → g =p= FL→perm x + pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl ) + open ≡-Reasoning st01 : ( x y : Permutation 3 3) → x =p= p3 → y =p= p3 → x ∘ₚ y =p= p4 @@ -82,15 +85,14 @@ st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4) st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h - ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (record { peq = λ q → begin ( - [ g , h ] ⟨$⟩ʳ q - ≡⟨ ( peq (comm-cong-l {h} {g} {pid} (FL-inject ge )) ) q ⟩ - [ pid , h ] ⟨$⟩ʳ q - ≡⟨ peq (idcomtl h) q ⟩ - q - ∎ ) } ) - ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = - case1 (record { peq = λ q → trans (( peq (comm-cong-r {h} {g} {pid} (FL-inject he )) ) q) (peq (idcomtr g) q) } ) + ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) ) + ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) ) + ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he) ) (comm-refl {FL→perm (zero :: (suc zero) :: (zero :: f0 ))} prefl )) + ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he) ) (comm-refl {FL→perm ((suc zero) :: (zero :: (zero :: f0 )))} prefl )) + ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he) ) (comm-refl {FL→perm ((suc zero) :: (suc zero :: (zero :: f0 )))} prefl )) ... | (zero :: (suc zero) :: (zero :: f0 )) | t | se | te = {!!} ... | (suc zero) :: (zero :: (zero :: f0 )) | t | se | te = {!!} ... | (suc zero) :: (suc zero :: (zero :: f0 )) | t | se | te = {!!}