Mercurial > hg > Members > kono > Proof > galois

changeset 97:f4ff8e352aa7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
p=0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 31 Aug 2020 07:18:54 +0900
parents b43c4a7c57d9
children 3a37a8f8cb39
files Putil.agda sym2.agda
diffstat 2 files changed, 70 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sun Aug 30 08:40:31 2020 +0900
+++ b/Putil.agda	Mon Aug 31 07:18:54 2020 +0900
@@ -254,6 +254,52 @@
 t7 =  plist (pins {3} (n≤ 3)) ∷ plist (flip ( pins {3} (n≤ 3) )) ∷  plist ( pins {3} (n≤ 3)  ∘ₚ  flip ( pins {3} (n≤ 3))) ∷ []
 -- t8 =  {!!}
 
+open import logic 
+
+open _∧_
+
+perm1 :  {perm : Permutation 1 1 } {q : Fin 1}  → (perm ⟨$⟩ʳ q ≡ # 0)  ∧ ((perm ⟨$⟩ˡ q ≡ # 0))
+perm1 {p} {q} = ⟪ perm01 _ _ , perm00 _ _ ⟫ where
+   perm01 : (x y : Fin 1) → (p ⟨$⟩ʳ x) ≡  y
+   perm01 x y with p ⟨$⟩ʳ x
+   perm01 zero zero | zero = refl
+   perm00 : (x y : Fin 1) → (p ⟨$⟩ˡ x) ≡  y
+   perm00 x y with p ⟨$⟩ˡ x
+   perm00 zero zero | zero = refl
+
+
+p=0 : {n : ℕ }  → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0
+p=0 {zero} perm with ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) 
+... | zero = refl
+p=0 {suc n} perm with perm ⟨$⟩ʳ (# 0) | inspect (_⟨$⟩ʳ_ perm ) (# 0)| toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) | inspect toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))
+... | zero |  record { eq = e} |  m<n | _ = p001 where
+   p001 : perm ⟨$⟩ˡ ( pins m<n ⟨$⟩ʳ zero) ≡ zero
+   p001 = subst (λ k → perm ⟨$⟩ˡ k ≡ zero ) e (inverseˡ perm)
+... | suc t |  record { eq = e } | m<n | record { eq = e1 }  = p002 where   -- m<n  : suc (toℕ t) ≤ suc n
+   p002 : perm ⟨$⟩ˡ ( pins m<n ⟨$⟩ʳ zero) ≡ zero
+   p002 = p005 zero (toℕ t)  refl m<n refl where   -- suc (toℕ t) ≤ suc n
+      p003 : (s : Fin (suc (suc n))) → s ≡ (perm ⟨$⟩ʳ (# 0)) → perm ⟨$⟩ˡ s  ≡ # 0
+      p003 s eq = subst (λ k → perm ⟨$⟩ˡ k ≡ zero ) (sym eq) (inverseˡ perm)
+      p005 : (x :  Fin (suc (suc n))) → (m : ℕ ) → x ≡ zero → (m≤n : suc m ≤ suc n ) → m ≡ toℕ t → perm ⟨$⟩ˡ ( pins m≤n ⟨$⟩ʳ zero) ≡ zero
+      p005 zero m eq (s≤s m≤n) meq = p004 where
+          p006 : toℕ (suc t) < suc (suc n)
+          p006 = subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) 
+          p004 :  perm ⟨$⟩ˡ (fromℕ< (s≤s (s≤s m≤n))) ≡ zero
+          p004 = p003  (fromℕ< (s≤s (s≤s m≤n))) (
+             begin
+                fromℕ< (s≤s (s≤s m≤n))
+             ≡⟨  fromℕ<-irrelevant _ _ (cong suc meq) (s≤s (s≤s m≤n)) (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
+                fromℕ< (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) )
+             ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
+                suc t
+             ≡⟨ sym e ⟩
+                (perm ⟨$⟩ʳ (# 0))
+             ∎ )
+
+
+-- pp : {n : ℕ }  → (perm : Permutation (suc n) (suc n) ) →  Fin (suc n)
+-- pp  perm → (( perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0))
+
 
 plist2 : {n  : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ
 plist2  {n} perm zero _           = toℕ ( perm ⟨$⟩ʳ (fromℕ< {zero} (s≤s z≤n))) ∷ []
@@ -373,8 +419,6 @@
    f0 :  FL 0 
    _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
 
-open import logic 
-
 shlem→ : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n) ) →  perm ⟨$⟩ˡ x ≡ zero → x ≡ zero
 shlem→ perm p0=0 x px=0 = begin
           x                                  ≡⟨ sym ( inverseʳ perm ) ⟩
@@ -507,15 +551,14 @@
  
 t6 = perm→FL t4
 
-postulate
-   FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
+-- postulate
+--    FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
 -- FL→iso f0 = refl
 -- FL→iso (x :: fl) = {!!} -- with FL→iso fl
 -- ... | t = {!!}
 
 open _=p=_
-postulate
-   FL←iso : {n : ℕ }  → (perm : Permutation n n )  → FL→perm ( perm→FL perm  ) =p= perm
+--    FL←iso : {n : ℕ }  → (perm : Permutation n n )  → FL→perm ( perm→FL perm  ) =p= perm
 -- FL←iso {0} perm = record { peq = λ () }
 -- FL←iso {suc n} perm = {!!}
 
@@ -534,6 +577,9 @@
    fls6 zero = (zero :: f0) ∷ []
    fls6 (suc n) =  fls5 (suc n) (fls6 n) []   
 
+tf1 = ∀-FL 4
+tf2 = Data.List.map (λ k → ⟪ plist (FL→perm k ) , k ⟫ ) tf1
+
 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
 all-perm n = pls6 n where
    lem1 : {i n : ℕ } → i ≤ n → i < suc n
--- a/sym2.agda	Sun Aug 30 08:40:31 2020 +0900
+++ b/sym2.agda	Mon Aug 31 07:18:54 2020 +0900
@@ -28,16 +28,32 @@
    open Solvable (Symmetric 2)
    -- open Group (Symmetric 2) using (_⁻¹)
 
+
    p0 :  FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid
    p0 = pleq _ _ refl
 
-   p0r :  (p : Permutation 2 2 ) → perm→FL p ≡ ((# 0) :: ((# 0 ) :: f0)) → p =p= pid
-   p0r p eq = {!!}
+   p0r :  perm→FL pid ≡  ((# 0) :: ((# 0 ) :: f0)) 
+   p0r = refl
 
    p1 :  FL→perm ((# 1) :: ((# 0 ) :: f0)) =p= pswap pid
    p1 = pleq _ _ refl
 
+   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 : (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