Mercurial > hg > Members > kono > Proof > galois

changeset 111:d3da6e2c0d90

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 Tue, 01 Sep 2020 21:58:15 +0900
parents cb3281e83229
children 43731a549950
files Putil.agda sym2.agda sym3.agda sym4.agda sym5.agda
diffstat 5 files changed, 69 insertions(+), 71 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Tue Sep 01 20:41:38 2020 +0900
+++ b/Putil.agda	Tue Sep 01 21:58:15 2020 +0900
@@ -652,6 +652,18 @@
         perm ⟨$⟩ʳ q
      ∎  ) } 
 
+FL-inject : {n : ℕ }  → {g h : Permutation n n }  → perm→FL g ≡  perm→FL h → g =p= h
+FL-inject {n} {g} {h} g=h = record { peq = λ q → ( begin
+       g ⟨$⟩ʳ q
+     ≡⟨ peq (psym (FL←iso g )) q ⟩
+        (  FL→perm (perm→FL g) ) ⟨$⟩ʳ q
+     ≡⟨ cong ( λ k → FL→perm  k ⟨$⟩ʳ q  ) g=h  ⟩
+        (  FL→perm (perm→FL h) ) ⟨$⟩ʳ q
+     ≡⟨ peq (FL←iso h) q ⟩
+        h ⟨$⟩ʳ q
+     ∎  ) }
+
+
 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
 lem2 i≤n = ≤-trans i≤n ( a≤sa )
 
--- a/sym2.agda	Tue Sep 01 20:41:38 2020 +0900
+++ b/sym2.agda	Tue Sep 01 21:58:15 2020 +0900
@@ -41,23 +41,16 @@
    p1r :  perm→FL (pswap pid) ≡  ((# 1) :: ((# 0 ) :: f0)) 
    p1r = refl
 
-   open _=p=_
-   open import logic
-   p01 :  (p : Permutation 2 2  ) → ( p =p= pid ) ∨ ( p =p= pswap pid )   --- p =p= FL→perm ((# 0) :: ((# 0) :: f0))
-   p01 p with perm→FL p | inspect perm→FL p
-   p01 p |  (zero :: (zero :: f0))  | record { eq = e } = case1 (ptrans {!!} p0   )        -- e : perm→FL p = zero :: (zero :: f0)
-   p01 p  |((suc zero) :: (zero :: f0))  | record { eq = e } = case2 (ptrans {!!} p1 )
+   -- FL→iso : (fl : FL 2 )  → perm→FL ( FL→perm fl ) ≡ fl
+   -- FL→iso  (zero :: (zero :: f0)) = refl
+   -- FL→iso ((suc zero) :: (zero :: f0)) = refl
 
-   FL→iso : (fl : FL 2 )  → perm→FL ( FL→perm fl ) ≡ fl
-   FL→iso  (zero :: (zero :: f0)) = refl
-   FL→iso ((suc zero) :: (zero :: f0)) = refl
+   open _=p=_
+   open ≡-Reasoning
 
-   FL←iso : (perm : Permutation 2 2 )  → FL→perm ( perm→FL perm  ) =p= perm
-   FL←iso p = {!!}
-   
    sym2lem0 :  ( g h : Permutation 2 2 ) → (q : Fin 2)  → ([ g , h ]  ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
-   sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g
-   sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} = begin
+   sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
+   sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} | record { eq = h=00}  = begin
              [ g , h ]  ⟨$⟩ʳ q
            ≡⟨⟩
               h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
@@ -69,42 +62,39 @@
              [ pid , h ]  ⟨$⟩ʳ q
            ≡⟨ peq (idcomtl h) q ⟩
              q
-          ∎ where
-            open ≡-Reasoning
-            sym2lem1 :  g =p= pid
-            sym2lem1 = pleq _ _ {!!}
-            -- it works but very slow
-            -- sym2lem1 = ptrans  (psym ( FL←iso g )) (subst (λ k → FL→perm k =p= pid) (sym g=00) p0 ) 
-   sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} = begin
+           ∎ where
+             sym2lem1 :  g =p= pid
+             sym2lem1 = FL-inject  g=00
+   sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00} = begin
              [ g , h ]  ⟨$⟩ʳ q
            ≡⟨⟩
               h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
            ≡⟨ peq sym2lem2 _   ⟩
               pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
-           ≡⟨ cong (λ k → pid ⟨$⟩ʳ  (g ⟨$⟩ʳ k)) ((peqˡ sym2lem2 _ )) ⟩
+           ≡⟨ cong (λ k → pid ⟨$⟩ʳ  (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩
               pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
            ≡⟨⟩
              [ g , pid ]  ⟨$⟩ʳ q
            ≡⟨ peq (idcomtr g) q ⟩
              q
           ∎ where
-            open ≡-Reasoning
-            postulate sym2lem2 :  h =p= pid
-   sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | _ = begin
+             sym2lem2 :  h =p= pid
+             sym2lem2 = FL-inject h=00
+   sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00}= begin
              [ g , h ]  ⟨$⟩ʳ q
            ≡⟨⟩
               h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
-           ≡⟨ peq sym2lem3  _ ⟩
-              pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )) 
-           ≡⟨ cong (λ k → pid  ⟨$⟩ʳ k) (peq sym2lem4  _ )⟩
-              pid ⟨$⟩ʳ ( pid  ⟨$⟩ˡ q ) 
-           ≡⟨⟩
+           ≡⟨ peq (psym g=h ) _  ⟩
+              g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+           ≡⟨ cong (λ k →   g ⟨$⟩ʳ  (g ⟨$⟩ʳ  k) ) (peqˡ (psym g=h) _)  ⟩
+              g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+           ≡⟨ cong (λ k → g  ⟨$⟩ʳ k) ( inverseʳ g )  ⟩
+              g ⟨$⟩ʳ  ( g ⟨$⟩ˡ q ) 
+           ≡⟨ inverseʳ g   ⟩
              q
           ∎ where
-            open ≡-Reasoning
-            postulate
-              sym2lem3 :  (g  ∘ₚ  h ) =p= pid
-              sym2lem4 :  (pinv g   ∘ₚ pinv h ) =p= pid
+              g=h :  g =p= h
+              g=h =  FL-inject (trans g=00 (sym h=00))
    solved :  (x : Permutation 2 2) → Commutator  (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
    solved x uni = prefl
    solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h  } 
--- a/sym3.agda	Tue Sep 01 20:41:38 2020 +0900
+++ b/sym3.agda	Tue Sep 01 21:58:15 2020 +0900
@@ -26,16 +26,17 @@
    open import Data.List using ( List ; [] ; _∷_ )
 
    open Solvable (Symmetric 3)
-   -- open Group (Symmetric 2) using (_⁻¹)
+
+   p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
+   p0id = pleq _ _ refl 
 
-   p0 :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
-   p0 = record { peq = p00 } where
-      p00 : (q : Fin 3) → (FL→perm ((# 0) :: ((# 0) :: ((# 0) :: f0))) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
-      p00 zero = refl
-      p00 (suc zero) = refl
-      p00 (suc (suc zero)) = refl
-
-   p1 =  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) 
+   p0 =  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) 
+   p1 =  FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) 
+   p2 =  FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) 
+   p3 =  FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) 
+   p4 =  FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) 
+   p5 =  FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) 
+   t0  =  plist p0 ∷ plist p1 ∷  plist p2 ∷ plist p3 ∷ plist p4 ∷  plist p5 ∷ [] 
 
    open _=p=_
    
--- a/sym4.agda	Tue Sep 01 20:41:38 2020 +0900
+++ b/sym4.agda	Tue Sep 01 21:58:15 2020 +0900
@@ -31,9 +31,6 @@
    open Solvable (Symmetric 4)
    -- open Group (Symmetric 2) using (_⁻¹)
 
-   p0 :  FL→perm ((# 0) :: ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))) =p= pid
-   p0 = {!!} -- record { peq = p00 } where
-
    open _=p=_
 
    -- Klien
@@ -65,6 +62,24 @@
 
    k2 = k1 kid ∷ k1 ka ∷ k1 kb ∷ k1 kc ∷ []
    k3 = plist  (a1  ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3)  ∷ plist (a2 ∘ₚ a1 ) ∷  []
+
+   p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
+   p0id = pleq _ _ refl
+
+   p0 =  FL→perm ((# 0) :: ((# 0) :: ((# 0) :: ((# 0 ) :: f0))))
+   p1 =  FL→perm ((# 0) :: ((# 0) :: ((# 1) :: ((# 0 ) :: f0))))
+   p2 =  FL→perm ((# 0) :: ((# 1) :: ((# 0) :: ((# 0 ) :: f0))))
+   p3 =  FL→perm ((# 0) :: ((# 1) :: ((# 1) :: ((# 0 ) :: f0))))
+   p4 =  FL→perm ((# 0) :: ((# 2) :: ((# 0) :: ((# 0 ) :: f0))))
+   p5 =  FL→perm ((# 0) :: ((# 2) :: ((# 1) :: ((# 0 ) :: f0))))
+   p6 =  FL→perm ((# 1) :: ((# 0) :: ((# 0) :: ((# 0 ) :: f0))))
+   p7 =  FL→perm ((# 1) :: ((# 0) :: ((# 1) :: ((# 0 ) :: f0))))
+   p8 =  FL→perm ((# 1) :: ((# 1) :: ((# 0) :: ((# 0 ) :: f0))))
+   p9 =  FL→perm ((# 1) :: ((# 1) :: ((# 1) :: ((# 0 ) :: f0))))
+   pa =  FL→perm ((# 1) :: ((# 2) :: ((# 0) :: ((# 0 ) :: f0))))
+   pb =  FL→perm ((# 1) :: ((# 2) :: ((# 1) :: ((# 0 ) :: f0))))
+   t0  =  plist p0 ∷ plist p1 ∷  plist p2 ∷ plist p3 ∷ plist p4 ∷  plist p5 ∷ []
+
    
    solved1 :  (x : Permutation 4 4) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
    solved1 = {!!}
--- a/sym5.agda	Tue Sep 01 20:41:38 2020 +0900
+++ b/sym5.agda	Tue Sep 01 21:58:15 2020 +0900
@@ -68,32 +68,12 @@
 
      import Relation.Binary.Reasoning.Setoid as EqReasoning
      abc→dba : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p=  dba i<3 j<4 
-     abc→dba i<3 j<4 = lemma where
-       open EqReasoning (Algebra.Group.setoid (Symmetric 5))
-       S = Symmetric 5
-       open Group (Symmetric 5)
-       postulate lemma : (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p=  dba i<3 j<4 
-       -- some kind of functional extentionaly required?
-       -- lemma = begin
-       --    abc i<3 j<4 ∘ₚ abc i<3 j<4 
-       --   ≈⟨ prefl ⟩
-       --    ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 )) ∘ₚ
-       --       ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 ))
-       --   ≈⟨  ∙-flatten (Symmetric 5) (((am (save2 i<3 j<4) o am (pprep (pprep 3rot))) o am (flip (save2 i<3 j<4 ))) o 
-       --       ((am (save2 i<3 j<4) o am (pprep (pprep 3rot))) o am ( flip (save2 i<3 j<4 )))) ⟩
-       --       save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ (
-       --         save2 i<3 j<4  ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ pid  )))))
-       --   ≈⟨ ∙-cong prefl ( ∙-cong prefl (grm S (proj₁ inverse _))) ⟩
-       --       save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ pid  )))
-       --   ≈⟨ ∙-cong prefl (grepl S (pprep-cong prefl ) ) ⟩
-       --    (save2 i<3 j<4 ∘ₚ (pprep (pprep (3rot ∘ₚ 3rot)))) ∘ₚ flip (save2 i<3 j<4 )
-       --   ≈⟨ prefl ⟩
-       --    dba i<3 j<4
-       --   ∎
+     abc→dba i<3 j<4 = ?
 
-     postulate  -- someday
-        dba→aec : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (dba i<3 j<4 ∘ₚ dba i<3 j<4 ) =p=  aec i<3 j<4 
-        aec→abc : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (aec i<3 j<4 ∘ₚ aec i<3 j<4 ) =p=  abc i<3 j<4 
+     dba→aec : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (dba i<3 j<4 ∘ₚ dba i<3 j<4 ) =p=  aec i<3 j<4 
+     dba→aec = ?
+     aec→abc : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (aec i<3 j<4 ∘ₚ aec i<3 j<4 ) =p=  abc i<3 j<4 
+     aec→abc = ?
 
      record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
        field