Mercurial > hg > Members > kono > Proof > galois
changeset 106:02f54eab9205
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 01 Sep 2020 18:26:21 +0900 |
| parents | e435dbe2e7a6 |
| children | 7e63fb16dc64 |
| files | Putil.agda |
| diffstat | 1 files changed, 8 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Tue Sep 01 17:45:33 2020 +0900 +++ b/Putil.agda Tue Sep 01 18:26:21 2020 +0900 @@ -636,20 +636,16 @@ 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 - f003 : perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm)) ≡ fl - f003 = {!!} - f004 : FL→perm ( x :: fl ) =p= perm - f004 = record { peq = λ q → ( begin - (pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x )) ⟨$⟩ʳ q - ≡⟨ cong (λ k → (pprep (FL→perm k) ∘ₚ pins ( toℕ≤pred[n] x )) ⟨$⟩ʳ q ) (sym f003 ) ⟩ - (pprep (FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ))) ∘ₚ pins ( toℕ≤pred[n] x )) ⟨$⟩ʳ 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] x )) ⟨$⟩ʳ q +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 ≡⟨ {!!} ⟩ 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 )