Mercurial > hg > Members > kono > Proof > galois

changeset 184:59d12d02dfa8

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 Thu, 26 Nov 2020 14:09:54 +0900
parents 0dce8a009f4a
children b99927719b8e
files FLComm.agda Putil.agda README.md sym2.agda sym2n.agda sym3n.agda sym4.agda sym5.agda sym5n.agda
diffstat 9 files changed, 68 insertions(+), 44 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Thu Nov 26 13:19:42 2020 +0900
+++ b/FLComm.agda	Thu Nov 26 14:09:54 2020 +0900
@@ -53,5 +53,5 @@
 CommStage→ (suc i) x (gen {f} {g} p q) = {!!}
 CommStage→ (suc i) x (ccong {f} {g} eq p) = {!!}
 
-CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (perm→FL x ≡ FL0 → x =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
-CommSolved x .(cons FL0 [] (Level.lift tt)) refl fl0→pid (here eq) = fl0→pid eq
+CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
+CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0
--- a/Putil.agda	Thu Nov 26 13:19:42 2020 +0900
+++ b/Putil.agda	Thu Nov 26 14:09:54 2020 +0900
@@ -678,6 +678,14 @@
 
 -- FLpid : (n : ℕ) → (x : Permutation n n) → perm→FL x ≡ FL0 → x =p= pid
 
+FLpid :  {n : ℕ} → (x : Permutation n n) → perm→FL x ≡ FL0 → FL→perm FL0 =p= pid   → x =p= pid
+FLpid x eq p0id = ptrans pf2 (ptrans pf0 p0id ) where
+   pf2 : x =p= FL→perm (perm→FL x)
+   pf2 = psym (FL←iso x)
+   pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
+   pf0 = pcong-Fp eq
+
+
 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
 lem2 i≤n = ≤-trans i≤n ( a≤sa )
 
--- a/README.md	Thu Nov 26 13:19:42 2020 +0900
+++ b/README.md	Thu Nov 26 14:09:54 2020 +0900
@@ -20,8 +20,14 @@
 sym4.agda            Symmetric 4 is solvable
 sym5.agda            Symmetric 5 is not solvable
 
+FLutil.agda          unique concrete representation of Permutation
+                     with Fresh List
+FLComm.agda          Solvable in FL / FList
+
+sym2n.agda           proved by Any
+sym3n.agda           
+sym4n.agda           
 
 ```
 
-Todo :  Use Data.List.Fresh to obtain all list of FL, and Commutator of FL.
-        It should make sym2, sym3 and sym4 simpler.
+Todo :  some proofs in FLutil / FLComm are not finished
--- a/sym2.agda	Thu Nov 26 13:19:42 2020 +0900
+++ b/sym2.agda	Thu Nov 26 14:09:54 2020 +0900
@@ -13,6 +13,7 @@
 
 open import Gutil 
 open import Putil 
+open import FLutil 
 open import Solvable using (solvable)
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
--- a/sym2n.agda	Thu Nov 26 13:19:42 2020 +0900
+++ b/sym2n.agda	Thu Nov 26 14:09:54 2020 +0900
@@ -44,14 +44,7 @@
    stage2FList = refl
 
    solved1 :  (x : Permutation 2 2) → deriving 1 x → x =p= pid
-   solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList pf solved0 where
-      --    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
-      pf : perm→FL x ≡ FL0 → x =p= pid
-      pf eq = ptrans pf1 (ptrans pf0 p0id ) where
-         pf1 : x =p= FL→perm (perm→FL x)
-         pf1 = psym (FL←iso x)
-         pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
-         pf0 = pcong-Fp eq
+   solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList p0id solved0 where
       solved0 : Any (perm→FL x ≡_) ( CommFListN 2 1 )
       solved0 = CommStage→ 2 1 x dr
 
--- a/sym3n.agda	Thu Nov 26 13:19:42 2020 +0900
+++ b/sym3n.agda	Thu Nov 26 14:09:54 2020 +0900
@@ -44,14 +44,7 @@
    stage3FList = refl
 
    solved1 :  (x : Permutation 3 3) → deriving 2 x → x =p= pid
-   solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList pf solved2 where
-      --    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
-      pf : perm→FL x ≡ FL0 → x =p= pid
-      pf eq = ptrans pf2 (ptrans pf0 p0id ) where
-         pf2 : x =p= FL→perm (perm→FL x)
-         pf2 = psym (FL←iso x)
-         pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
-         pf0 = pcong-Fp eq
+   solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where
       solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 )
       solved2 = CommStage→ 3 2 x dr
 
--- a/sym4.agda	Thu Nov 26 13:19:42 2020 +0900
+++ b/sym4.agda	Thu Nov 26 14:09:54 2020 +0900
@@ -27,18 +27,13 @@
 solvable.end sym4solvable x d = solved1 x d where
 
    open import Data.List using ( List ; [] ; _∷_ )
-
    open Solvable (Symmetric 4)
-   -- open Group (Symmetric 2) using (_⁻¹)
-
-   open _=p=_
 
    -- Klien
    --
    --  1                     (1,2),(3,4)           (1,3),(2,4)           (1,4),(2,3)
    --  0 ∷ 1 ∷ 2 ∷ 3 ∷ [] ,  1 ∷ 0 ∷ 3 ∷ 2 ∷ [] ,  2 ∷ 3 ∷ 0 ∷ 1 ∷ [] ,  3 ∷ 2 ∷ 1 ∷ 0 ∷ [] ,  
 
-
    a0 =  pid {4}
    a1 =  pswap (pswap (pid {0}))
    a2 =  pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) 
@@ -61,13 +56,7 @@
    stage3FList = refl
  
    solved1 :  (x : Permutation 4 4) → deriving 3 x → x =p= pid 
-   solved1 x dr = CommSolved 4 x ( CommFListN 4 3 ) stage3FList pf solved2 where
+   solved1 x dr = CommSolved 4 x ( CommFListN 4 3 ) stage3FList p0id solved2 where
       --    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
-      pf : perm→FL x ≡ FL0 → x =p= pid
-      pf eq = ptrans pf2 (ptrans pf0 p0id ) where
-         pf2 : x =p= FL→perm (perm→FL x)
-         pf2 = psym (FL←iso x)
-         pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
-         pf0 = pcong-Fp eq
       solved2 : Any (perm→FL x ≡_) ( CommFListN 4 3 )
       solved2 = CommStage→ 4 3 x dr 
--- a/sym5.agda	Thu Nov 26 13:19:42 2020 +0900
+++ b/sym5.agda	Thu Nov 26 14:09:54 2020 +0900
@@ -32,7 +32,6 @@
 
 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
 ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where
-
 --
 --    dba       1320      d → b → a → d
 --    (dba)⁻¹   3021      a → b → d → a
@@ -75,6 +74,10 @@
      dba : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
      dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4
 
+     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
+     counter-example eq with ←pleq _ _ eq
+     ...  | ()
+
      record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
        field 
          dba0<3 : Fin 4
@@ -196,11 +199,6 @@
         tc = triple i<3 j<4
         dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
         aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
-        --
-        -- abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot)  (fin≤n {3} dba0<3) (fin≤n {4} dba1<4)  , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]
-        --
-        ceq'  : ins2 3rot i<3 j<4 =p= [ ins2 (3rot ∘ₚ 3rot)  (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))  , ins2 (3rot ∘ₚ 3rot) (fin≤n {3} (aec0<3 tc )) (fin≤n {4} (aec1<4 tc)) ]
-        ceq'  = abc= tc
         ceq : abc i<3 j<4  =p=  [ dba0 , aec0 ]  
         ceq = record { peq = peq (abc= tc) }
         df =  dervie-any-3rot1 i  (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
@@ -220,9 +218,3 @@
         dg = deriving-subst (psym (ins2cong {toℕ (aec0<3 (dba-triple i<3 j<4))} {toℕ (aec1<4 (dba-triple i<3 j<4))} 4=1 )) 
              (dervie-any-3rot0 n  (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)))
 
-     open _=p=_
-     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
-     counter-example eq with ←pleq _ _ eq
-     ...  | ()
-
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sym5n.agda	Thu Nov 26 14:09:54 2020 +0900
@@ -0,0 +1,42 @@
+open import Level hiding ( suc ; zero )
+open import Algebra
+module sym5n where
+
+open import Symmetric 
+open import Data.Unit
+open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function
+open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Product
+
+open import Gutil 
+open import Putil 
+open import Solvable using (solvable)
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+open import Data.Fin
+open import Data.Fin.Permutation hiding (_∘ₚ_)
+
+infixr  200 _∘ₚ_
+_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
+
+sym5solvable : ¬ solvable (Symmetric 5)
+sym5solvable = {!!} where
+
+   open import Data.List using ( List ; [] ; _∷_ )
+   open Solvable (Symmetric 5)
+
+   open import FLutil
+   open import Data.List.Fresh hiding ([_])
+   open import Relation.Nary using (⌊_⌋)
+
+   p0id :  FL→perm (zero :: zero :: zero :: (zero :: (zero :: f0))) =p= pid
+   p0id = pleq _ _ refl
+
+   open import Data.List.Fresh.Relation.Unary.Any
+   open import FLComm
+
+   stage4FList = CommFListN 5 2 
+