Mercurial > hg > Members > kono > Proof > galois

changeset 107:7e63fb16dc64

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 Tue, 01 Sep 2020 18:56:10 +0900
parents 02f54eab9205
children d9cd155310e5
files Putil.agda
diffstat 1 files changed, 14 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Tue Sep 01 18:26:21 2020 +0900
+++ b/Putil.agda	Tue Sep 01 18:56:10 2020 +0900
@@ -516,6 +516,10 @@
 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm)  refl =p=  perm
 shrink-iso {n} {perm} = record { peq = λ q → refl  } 
 
+shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} 
+   → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0)  → pprep (shrink perm p=0) =p= pid
+shrink-iso2 = {!!}
+
 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 
@@ -639,13 +643,18 @@
 FL←iso {suc n} perm = record { peq = λ q → ( begin
         FL→perm ( perm→FL perm  ) ⟨$⟩ʳ q
      ≡⟨⟩
-        (pprep (FL→perm (perm→FL f001))  ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ) ) ⟨$⟩ʳ q
-     ≡⟨  peq (presp {suc n} {pprep (FL→perm (perm→FL f001))} {_} {pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ) } (pprep-cong (FL←iso _)) record { peq = λ q → refl } ) q  ⟩
-         (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm)) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q 
+        (pprep (FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) )))  ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ) ) ⟨$⟩ʳ q
+     ≡⟨  peq (presp (pprep-cong (FL←iso _ ) ) prefl ) q  ⟩
+         (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))   ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q 
+     ≡⟨ {!!}  ⟩
+         ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q 
+     ≡⟨ peq (passoc _ _ _ ) q ⟩
+         (perm ∘ₚ (flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )))  ⟨$⟩ʳ q 
+     ≡⟨ {!!}  ⟩
+        ( perm ∘ₚ pid ) ⟨$⟩ʳ q
      ≡⟨ {!!}  ⟩
         perm ⟨$⟩ʳ q
-     ∎  ) }  where
-        f001 = shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm)
+     ∎  ) } 
 
 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
 lem2 i≤n = ≤-trans i≤n ( a≤sa )