Mercurial > hg > Members > kono > Proof > galois

changeset 100:0fa8a49dc38b

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 15:25:45 +0900
parents cadfbf0c810b
children 92f3c9b926bd
files Putil.agda
diffstat 1 files changed, 15 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Mon Aug 31 11:45:09 2020 +0900
+++ b/Putil.agda	Mon Aug 31 15:25:45 2020 +0900
@@ -561,9 +561,11 @@
 
 pcong-pF : {n : ℕ }  → {x y : Permutation n n}  → x =p= y → perm→FL x ≡ perm→FL y
 pcong-pF {zero} eq = refl
-pcong-pF {suc n} {x} {y} eq = cong₂ (λ j k → j :: k ) ( peq eq (# 0)) (pcong-pF (shrink-cong (presp eq (record { peq = p-inv p001} )) (p=0 x) (p=0 y))) where
-    p001 : pins (toℕ≤pred[n] (x ⟨$⟩ʳ (# 0))) =p=  pins (toℕ≤pred[n] (y ⟨$⟩ʳ (# 0)))
-    p001 = {!!}
+pcong-pF {suc n} {x} {y} eq = cong₂ (λ j k → j :: k ) ( peq eq (# 0)) (pcong-pF (shrink-cong (presp eq p001 ) (p=0 x) (p=0 y))) where
+    p002 : x ⟨$⟩ʳ (# 0) ≡  y ⟨$⟩ʳ (# 0)
+    p002 = peq eq (# 0)
+    p001 : flip (pins (toℕ≤pred[n] (x ⟨$⟩ʳ (# 0)))) =p=  flip (pins (toℕ≤pred[n] (y ⟨$⟩ʳ (# 0))))
+    p001 = subst ( λ k →  flip (pins (toℕ≤pred[n] (x ⟨$⟩ʳ (# 0)))) =p=  flip (pins (toℕ≤pred[n] k ))) p002 prefl 
 
 -- t5 = plist t4 ∷ plist ( t4  ∘ₚ flip (pins ( n≤  3 ) ))
 t5 = plist (t4) ∷ plist (flip t4)
@@ -578,18 +580,22 @@
 
 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
+FL→iso {suc n} (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 = {!!}
+    f001 = begin
+       (pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )) ⟨$⟩ʳ (# 0) 
+     ≡⟨ {!!}  ⟩
+       x 
+     ∎
     x=0 :  (perm ∘ₚ flip (pins (toℕ≤pred[n] x))) ⟨$⟩ˡ (# 0) ≡ # 0
-    x=0 = {!!}
+    x=0 = subst ( λ k → (perm ∘ₚ flip (pins (toℕ≤pred[n] k))) ⟨$⟩ˡ (# 0) ≡ # 0 ) f001 (p=0 perm)
     x=0' : (pprep (FL→perm fl) ∘ₚ pid) ⟨$⟩ˡ (# 0) ≡ # 0
-    x=0' = {!!}
+    x=0' = refl
     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) ⟩
+     ≡⟨ pcong-pF (shrink-cong {n} (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 )
@@ -597,7 +603,7 @@
         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') ⟩
+     ≡⟨ pcong-pF (shrink-cong {n} prefl x=0' x=0') ⟩
         perm→FL (shrink (pprep (FL→perm fl)) x=0' )
      ≡⟨ pcong-pF shrink-iso ⟩
         perm→FL ( FL→perm fl )