Mercurial > hg > Members > kono > Proof > galois

changeset 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
files Putil.agda Solvable.agda sym3.agda
diffstat 3 files changed, 64 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Thu Sep 03 20:24:00 2020 +0900
+++ b/Putil.agda	Fri Sep 04 12:37:54 2020 +0900
@@ -418,6 +418,8 @@
    pswap-dist1 (suc zero) = refl
    pswap-dist1 (suc (suc q)) =  cong ( λ k → suc (suc k) ) refl
 
+infixr  100 _::_
+
 data  FL : (n : ℕ )→ Set where
    f0 :  FL 0 
    _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
--- a/Solvable.agda	Thu Sep 03 20:24:00 2020 +0900
+++ b/Solvable.agda	Fri Sep 04 12:37:54 2020 +0900
@@ -84,3 +84,9 @@
        (g ⁻¹   ∙    g     )                ≈⟨  proj₁ inverse _ ⟩
        ε
      ∎ where open EqReasoning (Algebra.Group.setoid G)
+
+comm-cong-l : {g h h1 : Carrier } → h ≈ h1   → [ h , g ] ≈ [ h1 , g ] 
+comm-cong-l {g} {h} {h1} h=h1 =  ∙-cong (∙-cong (∙-cong (⁻¹-cong h=h1 ) grefl ) h=h1 ) grefl
+
+comm-cong-r : {g h g1 : Carrier } → g ≈ g1 → [ h , g ] ≈ [ h , g1 ] 
+comm-cong-r {g} {h} {g1} g=g1 = ∙-cong (∙-cong (∙-cong grefl (⁻¹-cong g=g1) ) grefl ) g=g1
--- a/sym3.agda	Thu Sep 03 20:24:00 2020 +0900
+++ b/sym3.agda	Fri Sep 04 12:37:54 2020 +0900
@@ -17,7 +17,11 @@
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
 open import Data.Fin
-open import Data.Fin.Permutation
+open import Data.Fin.Permutation hiding (_∘ₚ_)
+
+infixr  200 _∘ₚ_
+_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
+
 
 sym3solvable : solvable (Symmetric 3)
 solvable.dervied-length sym3solvable = 2
@@ -52,19 +56,60 @@
    stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤)  x 
 
    open import logic
+
+   p33=4 : ( p3  ∘ₚ p3 ) =p= p4
+   p33=4 = pleq _ _ refl
+
+   p44=3 : ( p4  ∘ₚ p4 ) =p= p3
+   p44=3 = pleq _ _ refl
+
+   p34=0 : ( p3  ∘ₚ p4 ) =p= pid
+   p34=0 = pleq _ _ refl
+
+   p43=0 : ( p4  ∘ₚ p3 ) =p= pid
+   p43=0 = pleq _ _ refl
+
+   open ≡-Reasoning
+
+   st01 : ( x y : Permutation 3 3) →   x =p= p3 →  y =p= p3 → x ∘ₚ  y =p= p4 
+   st01 x y s t = record { peq = λ q → ( begin
+         (x ∘ₚ y) ⟨$⟩ʳ q
+       ≡⟨ peq ( presp s t ) q ⟩
+          ( p3  ∘ₚ p3 ) ⟨$⟩ʳ q
+       ≡⟨ peq  p33=4 q  ⟩
+         p4 ⟨$⟩ʳ q
+       ∎ ) }
+
+   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 :: (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 = {!!}
    
    stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
    stage12 x uni = case1 prefl
-   stage12 x (comm x1 y1 ) = {!!}
-   stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy --  x =p= pid : t , y =p= pid : s
-   ... | case1 t | case1 s = case1 ( {!!} )
-   ... | case1 t | case2 (case1 x₁) = {!!}
-   ... | case1 t | case2 (case2 x₁) = {!!}
-   ... | case2 t | case1 s = {!!}
-   ... | case2 (case1 s) | case2 (case1 t) = case2 (case2 (pleq _ _ {!!} ))
-   ... | case2 (case1 s) | case2 (case2 t) = {!!}
-   ... | case2 (case2 s) | case2 (case1 t) = {!!}
-   ... | case2 (case2 s) | case2 (case2 t) = {!!}
+   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₁ ))