Mercurial > hg > Members > kono > Proof > galois

changeset 58:80d61b6776d3

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 Sun, 23 Aug 2020 20:07:23 +0900
parents 518d364a58a3
children afa989a4b7e9
files Putil.agda
diffstat 1 files changed, 22 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sun Aug 23 19:23:08 2020 +0900
+++ b/Putil.agda	Sun Aug 23 20:07:23 2020 +0900
@@ -264,7 +264,8 @@
 FL→perm (x :: fl) = pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )
 
 t1 = plist (shrink (pid {3}  ∘ₚ (pins (n≤ 1))) refl)
-t3 =  plist ( FL→perm ((# 1) :: ((# 0) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (0 ∷ 1 ∷ 2 ∷ []) ∷
+t3 = plist (pid {4} )
+    ∷ plist ( FL→perm ((# 0) :: ((# 0) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (0 ∷ 1 ∷ 2 ∷ []) ∷
     ∷ plist ( FL→perm ((# 1) :: ((# 0) :: ( (# 1) :: (( # 0 ) :: f0 )) )))  --  (0 ∷ 2 ∷ 1 ∷ []) ∷
     ∷ plist ( FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (1 ∷ 0 ∷ 2 ∷ []) ∷
     ∷ plist ( FL→perm ((# 1) :: ((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) )))  --  (2 ∷ 0 ∷ 1 ∷ []) ∷
@@ -274,25 +275,36 @@
     ∷ plist ( (flip (FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 1) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) ))
     ∷ []
 
+t4 =  FL→perm ((# 1) :: ((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) )) 
+-- t5 = plist t4 ∷ plist ( t4  ∘ₚ flip (pins ( n≤  3 ) ))
+t5 = plist (flip t4)
+    ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ≤ a<sa) ∷ [] )
+    ∷ ( toℕ (t4 ⟨$⟩ʳ fromℕ≤ ( fin<n {_} {(t4 ⟨$⟩ˡ fromℕ≤ a<sa)})) ∷ [] )
+    ∷  plist (shrink ( t4  ∘ₚ flip (pins ( n≤  3 ) ) ) refl )
+    ∷  plist ( FL→perm (((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) ))) 
+    ∷ []
+ 
+
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0
-perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL ( shrink fl1 {!!} ) where
+perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL ( shrink fl1 fl4 ) where
+    fl2 : Fin (suc n)
+    fl2 = perm ⟨$⟩ʳ fromℕ≤  (fin<n {suc n} {perm  ⟨$⟩ˡ fromℕ≤ a<sa} )
+    fl3 : toℕ fl2 < n
+    fl3 = {!!}
     fl1 : Permutation (suc n) (suc n)
-    fl1 = perm ∘ₚ pinv ( pins (fin<n {n} {{!!}}))
-    fl1=pprep : perm =p= pprep ( shrink fl1 {!!} )
-    fl1=pprep = {!!}
+    fl1 = perm ∘ₚ pinv ( pins fl3 )
+    fl4 : (fl1 ⟨$⟩ˡ fromℕ n) ≡ fromℕ n
+    fl4 = {!!}
 
 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 = {!!}
+FL→iso (x :: fl) = {!!} 
 
 open _=p=_
 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 = {!!} where
-   fl0 :  {n : ℕ }  → (fl : FL n )  → {!!} 
-   fl0 = {!!}
+FL←iso {suc n} perm = {!!} 
 
 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
 all-perm n = pls6 n where