Mercurial > hg > Members > kono > Proof > galois

changeset 63:d730fb6eea89

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 Mon, 24 Aug 2020 12:47:31 +0900
parents a66f773330b4
children 537903b159ef
files Putil.agda
diffstat 1 files changed, 10 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Mon Aug 24 12:41:57 2020 +0900
+++ b/Putil.agda	Mon Aug 24 12:47:31 2020 +0900
@@ -251,8 +251,8 @@
     -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 3) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) ))
     ∷ []
 
-p=0 : {n : ℕ }  → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0
-p=0 perm  = {!!}
+postulate
+   p=0 : {n : ℕ }  → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0
 
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0
@@ -269,15 +269,17 @@
  
 t6 = perm→FL t4
 
-FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
-FL→iso f0 = refl
-FL→iso (x :: fl) = {!!} -- with FL→iso 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=_
-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 = {!!}
+postulate
+   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 = {!!}
 
 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
 all-perm n = pls6 n where