Mercurial > hg > Members > kono > Proof > galois

changeset 125:11ccc9fe91c3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sym3 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 04 Sep 2020 20:20:22 +0900
parents 803a45b280ef
children d5f093061b46
files sym3.agda
diffstat 1 files changed, 74 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/sym3.agda	Fri Sep 04 19:07:39 2020 +0900
+++ b/sym3.agda	Fri Sep 04 20:20:22 2020 +0900
@@ -42,13 +42,13 @@
    p5 =  FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) 
    t0  =  plist p0 ∷ plist p1 ∷  plist p2 ∷ plist p3 ∷ plist p4 ∷  plist p5 ∷ [] 
 
---   t1  =  plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷  plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷  plist [ p5 , p1 ] ∷ 
---          plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷  plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷  plist [ p5 , p1 ] ∷ 
---          plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷  plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷  plist [ p5 , p2 ] ∷ 
---          plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷  plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷  plist [ p5 , p3 ] ∷ 
---          plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷  plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p4 ] ∷ 
---          plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷  plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p5 ] ∷ 
---          []
+   t1  =  plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷  plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷  plist [ p5 , p1 ] ∷ 
+          plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷  plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷  plist [ p5 , p1 ] ∷ 
+          plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷  plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷  plist [ p5 , p2 ] ∷ 
+          plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷  plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷  plist [ p5 , p3 ] ∷ 
+          plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷  plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p4 ] ∷ 
+          plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷  plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p5 ] ∷ 
+          []
 
    open _=p=_
    
@@ -96,6 +96,8 @@
 --         p4 ⟨$⟩ʳ q
 --       ∎ ) }
 
+   st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm  ((suc (suc zero)) :: (suc zero) :: (zero :: f0))  ]
+
    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 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
@@ -110,30 +112,65 @@
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
    ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } |  record { eq = he } =
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
-   ... | (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 = {!!}
-   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | t | se | te = {!!}
-   ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | t | se | te = {!!}
+
+   ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
+           case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } = 
+           case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (suc (suc zero)) :: (zero :: (zero :: f0 ))| record { eq = ge } |  record { eq = he } =  
+           case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0))| record { eq = ge } |  record { eq = he } =   
+           case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } = 
+            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } = 
+            case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | ((suc (suc zero)) :: (zero :: (zero :: f0 )))| record { eq = ge } |  record { eq = he } =  
+            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | ((suc zero) :: (zero :: (zero :: f0 ))) |  (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } |  record { eq = he } =  
+            case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =  
+            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =  
+            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc (suc zero)) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =  
+         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } |  record { eq = he } =   
+            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } |  record { eq = he } =
+          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
+          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... | (suc (suc zero)) :: (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)) (FL-inject refl) )
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } |  record { eq = he } = 
+          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } |  record { eq = he } =
+          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
+          case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (suc zero :: (zero :: f0 )))  | record { eq = ge } |  record { eq = he } =
+          case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
+   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | (suc (suc zero)) :: (zero :: (zero :: f0 ))  | record { eq = ge } |  record { eq = he } =
+          case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
    
    stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
-   stage12 = {!!}
---   stage12 x uni = case1 prefl
---   stage12 x (comm {g} {h} x1 y1 ) = st02 g h
---   stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy 
---   ... | case1 t | case1 s = case1 ( record { peq = λ q → peq (presp t s) q} )
---   ... | case1 t | case2 (case1 s) = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } )) 
---   ... | case1 t | case2 (case2 s) = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } )) 
---   ... | case2 (case1 t) | case1 s = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } )) 
---   ... | case2 (case2 t) | case1 s = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } )) 
---   ... | case2 (case1 s) | case2 (case1 t) = case2 (case2 record { peq = λ q → trans (peq ( presp s t ) q) ( peq  p33=4 q) } ) 
---   ... | case2 (case1 s) | case2 (case2 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq  p34=0 q) }  
---   ... | case2 (case2 s) | case2 (case1 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq  p43=0 q) } 
---   ... | case2 (case2 s) | case2 (case2 t) = case2 (case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq  p44=3 q) } ) 
---   stage12 _ (ccong {y} x=y sx) with stage12 y sx
---   ... | case1 id = case1 ( ptrans (psym x=y ) id )
---   ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ ))
---   ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ ))
+   stage12 x uni = case1 prefl
+   stage12 x (comm {g} {h} x1 y1 ) = st02 g h
+   stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy 
+   ... | case1 t | case1 s = case1 ( record { peq = λ q → peq (presp t s) q} )
+   ... | case1 t | case2 (case1 s) = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } )) 
+   ... | case1 t | case2 (case2 s) = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } )) 
+   ... | case2 (case1 t) | case1 s = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } )) 
+   ... | case2 (case2 t) | case1 s = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } )) 
+   ... | case2 (case1 s) | case2 (case1 t) = case2 (case2 record { peq = λ q → trans (peq ( presp s t ) q) ( peq  p33=4 q) } ) 
+   ... | case2 (case1 s) | case2 (case2 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq  p34=0 q) }  
+   ... | case2 (case2 s) | case2 (case1 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq  p43=0 q) } 
+   ... | case2 (case2 s) | case2 (case2 t) = case2 (case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq  p44=3 q) } ) 
+   stage12 _ (ccong {y} x=y sx) with stage12 y sx
+   ... | case1 id = case1 ( ptrans (psym x=y ) id )
+   ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ ))
+   ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ ))
 
 
    solved1 :  (x : Permutation 3 3) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
@@ -158,14 +195,12 @@
           ≡⟨ f=e q ⟩
              q
           ∎ 
-   solved1 _ (comm {g} {h} x y) = {!!}
---   solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y
---   ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
---   ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
---   ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g)
---   ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com33 q) }
---   ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com44 q) }
---   ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com34 q) }
---   ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com43 q) }
+   solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y
+   ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
+   ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
+   ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g)
+   ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com33 q) }
+   ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com44 q) }
+   ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com34 q) }
+   ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h}  t s ) q ) (peq com43 q) }
 
-   -- = ptrans ( comm-resp {g} {h}  t s ) ( comm-refl ? )