Mercurial > hg > Members > kono > Proof > galois

changeset 49:8b3b95362ca9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove (fromℕ≤ a<sa) perm is no good
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Aug 2020 19:55:41 +0900
parents ac2f21a2d467
children ddec1ef4f5e4
files Putil.agda
diffstat 1 files changed, 24 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Fri Aug 21 23:44:28 2020 +0900
+++ b/Putil.agda	Sat Aug 22 19:55:41 2020 +0900
@@ -126,6 +126,30 @@
     plist1  zero _           = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
     plist1  (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt)))         ∷ plist1  i (<-trans lt a<sa) 
 
+data  FL : (n : ℕ )→ Set where
+   f0 :  FL 0 
+   _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
+
+perm→FL   : {n : ℕ }  → Permutation n n → FL n
+perm→FL {zero} perm = f0
+perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL {n} ( remove (fromℕ≤ a<sa) perm )
+
+FL→perm   : {n : ℕ }  → FL n → Permutation n n 
+FL→perm f0 = pid
+FL→perm (x :: fl) = pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )
+
+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=_
+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 = {!!}
+
 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
 all-perm n = pls6 n where
    lem1 : {i n : ℕ } → i ≤ n → i < suc n