Mercurial > hg > Members > kono > Proof > galois

changeset 75:4b17a4daf2df

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
3rot
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Aug 2020 00:53:33 +0900
parents 69ed81f8e212
children cef943dcd18c
files Putil.agda Solvable.agda sym5.agda
diffstat 3 files changed, 59 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Tue Aug 25 14:15:49 2020 +0900
+++ b/Putil.agda	Wed Aug 26 00:53:33 2020 +0900
@@ -313,4 +313,4 @@
    pls6 (suc n) =  pls5 (suc n) (rev (pls6 n) ) []   -- rev to put id first
 
 pls : (n : ℕ ) → List (List ℕ )
-pls n = Data.List.map plist (all-perm n) where
+pls n = Data.List.map plist (all-perm n) 
--- a/Solvable.agda	Tue Aug 25 14:15:49 2020 +0900
+++ b/Solvable.agda	Wed Aug 26 00:53:33 2020 +0900
@@ -57,8 +57,8 @@
 deriving-inv : { i : ℕ } → { x  : Carrier } → deriving i x → deriving i ( x ⁻¹ )
 deriving-inv {zero} {x} (lift tt) = lift tt
 deriving-inv {suc i} {ε} uni = ccong lemma3 uni
-deriving-inv {suc i} {_} (comm x x₁ )   = ccong (lemma4 _ _) (comm x₁ x) where
-deriving-inv {suc i} {_} (gen x x₁ )    = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where
+deriving-inv {suc i} {_} (comm x x₁ )   = ccong (lemma4 _ _) (comm x₁ x) 
+deriving-inv {suc i} {_} (gen x x₁ )    = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) 
 deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )
 
 idcomtr : (g  : Carrier ) → [ g , ε  ] ≈ ε 
--- a/sym5.agda	Tue Aug 25 14:15:49 2020 +0900
+++ b/sym5.agda	Wed Aug 26 00:53:33 2020 +0900
@@ -3,10 +3,11 @@
 module sym5 where
 
 open import Symmetric 
-open import Data.Unit
+open import Data.Unit using (⊤ ; tt )
 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
-open import Function
+open import Function hiding (flip)
 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
+open import Data.Nat.Properties
 open import Relation.Nullary
 open import Data.Empty
 open import Data.Product
@@ -16,12 +17,13 @@
 open import Solvable using (solvable)
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
-open import Data.Fin hiding (_<_ ; lift )
+open import Data.Fin hiding (_<_ ; _≤_  ; lift )
 open import Data.Fin.Permutation
 open import Data.List  hiding ( [_] )
+open import nat
 
 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
-¬sym5solvable sol = counter-example (end5 (abc 0<4 0<3 ) (dervie-any-3rot (dervied-length sol) 0<4 0<3 ) ) where
+¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) ) where
 
 --
 --    dba       1320      d → b → a → d
@@ -37,47 +39,78 @@
      end5 x der = end sol x der
 
      0<4 : 0 < 4
-     0<4 = {!!}
+     0<4 = s≤s z≤n
 
      0<3 : 0 < 3
-     0<3 = {!!}
+     0<3 = s≤s z≤n
 
-     --- 2 ∷ 0 ∷ 1 ∷ []
+     --- 2 ∷ 0 ∷ 1 ∷ []      abc
      3rot : Permutation 3 3
-     3rot = {!!} -- pswap (pid {0}) ∘ₚ pins (n≤ 1)
+     3rot = pprep (pswap (pid {0}) ) ∘ₚ pins (n≤ 1)
 
-     abc : {i j : ℕ }  → (i < 4 ) → ( j < 3 ) → Permutation  5 5
-     abc i<4 j<3 = {!!} -- (3rot ∘ₚ pins i<4 )  ∘ₚ pins j<3
+     abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     abc i<3 j<4 = (save2 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip save2  where
+          save2 : Permutation  5 5
+          save2 = ( (pprep ( pid {4} ∘ₚ flip (pins i<3 ) )) ∘ₚ flip (pins j<4)) 
 
      dba-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) 
      dba-0 = {!!}
      dba-1 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 3 )
      dba-1 = {!!}
 
-     dba : {i j : ℕ }  → (i < 4 ) → ( j < 3 ) → Permutation  5 5
-     dba i<4 j<3 = abc (dba-0 i<4 j<3 ) (dba-1 i<4 j<3 )
+     dba : {i j : ℕ }  → (i < 3 ) → ( j < 4 ) → Permutation  5 5
+     dba i<3 j<4 = abc (dba-1 j<4 i<3 ) (dba-0 j<4 i<3 )
 
      aec-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) 
      aec-0 = {!!}
      aec-1 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 3 )
      aec-1 = {!!}
 
-     aec : {i j : ℕ }  → (i < 4 ) → ( j < 3 ) → Permutation  5 5
-     aec i<4 j<3 = abc (aec-0 i<4 j<3 ) (aec-1 i<4 j<3 )
+     aec : {i j : ℕ }  → (i < 3 ) → ( j < 4 ) → Permutation  5 5
+     aec i<3 j<4 = abc (aec-1 j<4 i<3 ) (aec-0 j<4 i<3 )
 
-     [dba,aec]=abc : {i j : ℕ }  → (i<4 : i < 4 ) → (j<3 : j < 3 ) → [ dba i<4 j<3 , aec i<4 j<3 ] =p= abc i<4 j<3
+     [dba,aec]=abc : {i j : ℕ }  → (i<4 : i < 4 ) → (j<3 : j < 3 ) → [ dba j<3 i<4 , aec j<3 i<4 ] =p= abc j<3 i<4
      [dba,aec]=abc = {!!}
 
-     dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<4 : i < 4 ) → (j<3 : j < 3 ) → deriving n (abc i<4 j<3 )
-     dervie-any-3rot 0 i<4 j<3 = lift tt
-     dervie-any-3rot (suc i) i<4 j<3 = 
-         ccong ( [dba,aec]=abc i<4 j<3 ) (
-         comm {{!!}} {dba i<4 j<3} {aec i<4 j<3 } 
-             ( dervie-any-3rot i (dba-0 i<4 j<3) (dba-1 i<4 j<3) ) 
-             ( dervie-any-3rot i (aec-0 i<4 j<3) (aec-1 i<4 j<3) ))
+     --- 2 ∷ 0 ∷ 1 ∷ []      abc
+     t10 : List (List ℕ )
+     t10 =   t101 (n≤ 4) (n≤ 5)  [] where
+          t101 : { i j : ℕ } → i ≤ 4 → j ≤ 5  → List (List ℕ ) → List (List ℕ )
+          t101 z≤n z≤n t =  plist (abc z≤n z≤n) ∷ t 
+          t101 z≤n (s≤s y) t = t101 y (≤-trans y refl-≤s) ( plist (abc z≤n (y)) ∷ t )
+          t101 (s≤s x) z≤n t = t101 (≤-trans x refl-≤s)  z≤n  ( plist (abc (x) z≤n) ∷ t )
+          t101 (s≤s x) (s≤s y) t = t101 (≤-trans x refl-≤s)  (s≤s y) ( plist (abc (x) y) ∷ t )
+          -- t101 (s≤s x) z≤n t = t101 (≤-trans x ?) x ( abc (s≤s x) z≤n ∷ t )
+          -- t101 (s≤s x) (s≤s y) t = {!!}
+     t12 = {!!}
+     
+     --- 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] 
+     --- 1 ∷ 0 ∷ 2 ∷ 3 ∷ 4 ∷ [] 
+     --- 1 ∷ 2 ∷ 0 ∷ 3 ∷ 4 ∷ [] 
+     --- 1 ∷ 2 ∷ 3 ∷ 0 ∷ 4 ∷ []     
+     --- 1 ∷ 2 ∷ 3 ∷ 4 ∷ 0 ∷ []     
+
+     --- 2 ∷ 0 ∷ 1 ∷ 3 ∷ 4 ∷ []     abc     (swap (pid {0}) ∘ₚ pins i<1 ) ∘ₚ pid 
+     --- 3 ∷ 0 ∷ 2 ∷ 1 ∷ 4 ∷ []     abc     pprep (swap (pid {0}) ∘ₚ pins i<1 ) ∘ₚ pid 
+     --- 4 ∷ 0 ∷ 2 ∷ 3 ∷ 1 ∷ []     abc     pprep (pprep (swap (pid {0}) ∘ₚ pins i<1 )) ∘ₚ pid 
+     --- 3 ∷ 1 ∷ 0 ∷ 2 ∷ 4 ∷ []     abc
+     --- 4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ []     abc
+     --- 4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ []     abc
+
+     --- 2 ∷ 0 ∷ 1 ∷ 3 ∷ 4 ∷ []     abc
+     --- 1 ∷ 3 ∷ 2 ∷ 0 ∷ 4 ∷ []     abd 
+     --  2 ∷ 1 ∷ 4 ∷ 3 ∷ 0 ∷ []     cea
+
+     dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<3 : i < 3 ) → (j<4 : j < 4 ) → deriving n (abc i<3 j<4 )
+     dervie-any-3rot 0 i<3 j<4 = lift tt
+     dervie-any-3rot (suc i) i<3 j<4 = 
+         ccong ( [dba,aec]=abc j<4 i<3 ) (
+         comm {{!!}} {dba i<3 j<4} {aec i<3 j<4 } 
+             ( dervie-any-3rot i (dba-1 j<4 i<3) (dba-0 j<4 i<3 ) ) 
+             ( dervie-any-3rot i (aec-1 j<4 i<3) (aec-0 j<4 i<3 ) ))
 
      open _=p=_
-     counter-example :  ¬ (abc 0<4 0<3  =p= pid )
+     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
      counter-example = {!!}