Mercurial > hg > Members > kono > Proof > galois

changeset 104:2d0738a38ac9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... bad approach
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 01 Sep 2020 17:21:31 +0900
parents 7595ee384b3d
children e435dbe2e7a6
files Putil.agda
diffstat 1 files changed, 16 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Tue Sep 01 16:54:56 2020 +0900
+++ b/Putil.agda	Tue Sep 01 17:21:31 2020 +0900
@@ -627,11 +627,23 @@
         fl 
      ∎ 
 
+pcong-Fp : {n : ℕ }  → {x y : FL n}  → x ≡ y → FL→perm x =p= FL→perm y
+pcong-Fp {n} {x} {x} refl = prefl
 
-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 = {!!}
+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 with  perm→FL perm | inspect  perm→FL perm
+... | x :: fl | record { eq = e } = ptrans (pcong-Fp e ) f004 where
+    f004 :    FL→perm ( x :: fl ) =p= perm 
+    f004 = record { peq = λ q → ( begin
+        (pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x ))  ⟨$⟩ʳ q
+     ≡⟨ {!!}  ⟩
+        (pprep (FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) )))  ∘ₚ pins ( toℕ≤pred[n] x ))  ⟨$⟩ʳ q
+     ≡⟨ {!!}  ⟩
+        (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))   ∘ₚ pins ( toℕ≤pred[n] x ))  ⟨$⟩ʳ q
+     ≡⟨ {!!}  ⟩
+        perm ⟨$⟩ʳ q
+     ∎  ) }
 
 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
 lem2 i≤n = ≤-trans i≤n ( a≤sa )