Mercurial > hg > Members > kono > Proof > galois

changeset 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
files Solvable.agda sym3.agda
diffstat 2 files changed, 33 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/Solvable.agda	Fri Sep 04 12:37:54 2020 +0900
+++ b/Solvable.agda	Fri Sep 04 17:05:15 2020 +0900
@@ -43,6 +43,8 @@
 
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
+open EqReasoning (Algebra.Group.setoid G)
+
 lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
 lemma4 g h = begin
        [ h , g ]                               ≈⟨ grefl ⟩
@@ -54,7 +56,7 @@
        h ⁻¹ ∙ (g ⁻¹ ∙   h ⁻¹ ∙ g) ⁻¹           ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩
        (g ⁻¹ ∙ h ⁻¹ ∙   g ∙ h) ⁻¹              ≈⟨ grefl ⟩
        [ g , h ]  ⁻¹                  
-     ∎ where open EqReasoning (Algebra.Group.setoid G)
+     ∎ 
 
 deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y  → deriving i ( x ∙ y )
 deriving-mul {zero} {x} {y} _ _ = lift tt
@@ -74,7 +76,7 @@
        (g ⁻¹   ∙   g ∙ ε     )                ≈⟨ ∙-cong (proj₁ inverse _ )   grefl ⟩
        (  ε  ∙ ε     )                        ≈⟨  proj₂ identity _  ⟩
        ε
-     ∎ where open EqReasoning (Algebra.Group.setoid G)
+     ∎ 
 
 idcomtl : (g  : Carrier ) → [ ε ,  g ] ≈ ε 
 idcomtl g  = begin
@@ -83,10 +85,23 @@
        (ε  ∙ g  ⁻¹ ∙    g )                  ≈⟨ ∙-cong (proj₁ identity _) grefl ⟩
        (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-refl : {f g : Carrier } → f ≈ g  → [ f ,  g ] ≈ ε 
+comm-refl {f} {g} f=g = begin
+       f ⁻¹ ∙ g ⁻¹ ∙   f ∙ g
+     ≈⟨ ∙-cong (∙-cong (∙-cong (⁻¹-cong f=g ) grefl ) f=g ) grefl ⟩
+       g ⁻¹ ∙ g ⁻¹ ∙   g ∙ g
+     ≈⟨ ∙-cong (assoc _ _ _ ) grefl  ⟩
+       g ⁻¹ ∙ (g ⁻¹ ∙   g ) ∙ g
+     ≈⟨ ∙-cong (∙-cong grefl (proj₁ inverse _) ) grefl ⟩
+       g ⁻¹ ∙ ε  ∙ g 
+     ≈⟨ ∙-cong (proj₂ identity _) grefl  ⟩
+       g ⁻¹ ∙  g 
+     ≈⟨  proj₁ inverse _  ⟩
+       ε
+     ∎ 
 
-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
+comm-resp : {g h g1 h1  : Carrier } → g ≈ g1  → h ≈ h1 → [ g , h ] ≈ [ g1 , h1 ] 
+comm-resp {g} {h} {g1} {h1} g=g1 h=h1 =  ∙-cong (∙-cong (∙-cong (⁻¹-cong g=g1 ) (⁻¹-cong h=h1 )) g=g1 ) h=h1
+
--- 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 = {!!}