Mercurial > hg > Members > kono > Proof > galois

changeset 98:3a37a8f8cb39

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, 31 Aug 2020 09:51:13 +0900
parents f4ff8e352aa7
children cadfbf0c810b
files Putil.agda
diffstat 1 files changed, 39 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Mon Aug 31 07:18:54 2020 +0900
+++ b/Putil.agda	Mon Aug 31 09:51:13 2020 +0900
@@ -282,8 +282,6 @@
       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
@@ -510,6 +508,11 @@
 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm)  refl =p=  perm
 shrink-iso {n} {perm} = record { peq = λ q → refl  } 
 
+shrink-cong : { n : ℕ } → {x y : Permutation (suc n) (suc n)}
+    → x =p= y
+    → (x=0 :  x ⟨$⟩ˡ (# 0) ≡ # 0 ) → (y=0 : y ⟨$⟩ˡ (# 0) ≡ # 0 )  → shrink x x=0 =p=  shrink y y=0 
+shrink-cong {n} {x} {y} x=0 y=0  = {!!}
+
 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 )
@@ -537,8 +540,11 @@
 
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0
-perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm)  
--- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) 
+perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) 
+-- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm)  
+
+pcong-pF : {n : ℕ }  → {x y : Permutation n n}  → x =p= y → perm→FL x ≡ perm→FL y
+pcong-pF = {!!}
 
 -- t5 = plist t4 ∷ plist ( t4  ∘ₚ flip (pins ( n≤  3 ) ))
 t5 = plist (t4) ∷ plist (flip t4)
@@ -551,11 +557,35 @@
  
 t6 = perm→FL t4
 
--- 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 = {!!}
+FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
+FL→iso f0 = refl
+FL→iso (x :: fl) = cong₂ ( λ j k → j :: k ) f001 f002 where
+    perm = pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )
+    f001 : perm ⟨$⟩ʳ (# 0) ≡ x
+    f001 = {!!}
+    x=0 :  (perm ∘ₚ flip (pins (toℕ≤pred[n] x))) ⟨$⟩ˡ (# 0) ≡ # 0
+    x=0 = {!!}
+    x=0' : (pprep (FL→perm fl) ∘ₚ pid) ⟨$⟩ˡ (# 0) ≡ # 0
+    x=0' = {!!}
+    f002 : perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) )  ≡ fl
+    f002 = begin
+        perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) )  
+     ≡⟨ pcong-pF (shrink-cong (presp prefl {!!})  (p=0 perm)  x=0) ⟩
+        perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] x))) x=0 ) 
+     ≡⟨⟩
+        perm→FL (shrink ((pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )) ∘ₚ flip (pins (toℕ≤pred[n] x))) x=0 )
+     ≡⟨ pcong-pF (shrink-cong (passoc _ _ _ )  x=0 x=0) ⟩
+        perm→FL (shrink (pprep (FL→perm fl)  ∘ₚ (pins ( toℕ≤pred[n] x ) ∘ₚ flip (pins (toℕ≤pred[n] x)))) x=0 )
+     ≡⟨ pcong-pF (shrink-cong record { peq = λ q → inverseʳ _ }  x=0 x=0') ⟩
+        perm→FL (shrink (pprep (FL→perm fl)  ∘ₚ pid) x=0' )
+     ≡⟨ pcong-pF (shrink-cong prefl x=0' x=0') ⟩
+        perm→FL (shrink (pprep (FL→perm fl)) x=0' )
+     ≡⟨ pcong-pF shrink-iso ⟩
+        perm→FL ( FL→perm fl ) 
+     ≡⟨ FL→iso fl  ⟩
+        fl 
+     ∎ 
+
 
 open _=p=_
 --    FL←iso : {n : ℕ }  → (perm : Permutation n n )  → FL→perm ( perm→FL perm  ) =p= perm