Mercurial > hg > Members > kono > Proof > galois
changeset 103:7595ee384b3d
FL→iso done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 01 Sep 2020 16:54:56 +0900 |
| parents | 00a711f99096 |
| children | 2d0738a38ac9 |
| files | Putil.agda |
| diffstat | 1 files changed, 17 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Tue Sep 01 12:11:11 2020 +0900 +++ b/Putil.agda Tue Sep 01 16:54:56 2020 +0900 @@ -296,26 +296,17 @@ px=x : {n : ℕ } → (x : Fin (suc n)) → pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡ x px=x {n} zero = refl -px=x {suc n} (suc x) = trans p001 (cong suc pprev ) where - pprev : pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡ x - pprev = px=x x - m<n : toℕ x ≤ n - m<n = toℕ≤pred[n] x - p001 : (pins (toℕ≤pred[n] (suc x)) ⟨$⟩ʳ (# 0)) ≡ suc (pins (toℕ≤pred[n] x) ⟨$⟩ʳ (# 0)) - p001 with <-cmp 0 (toℕ (Data.Fin.pred x)) - ... | tri< a ¬b ¬c = cong suc ? - ... | tri≈ ¬a b ¬c = cong suc ? --- p001 = cong suc ( begin --- fromℕ< (≤-pred (s≤s (s≤s (toℕ≤pred[n] x)))) --- ≡⟨ {!!} ⟩ --- pins (toℕ≤pred[n] x) ⟨$⟩ʳ (# 0) --- ∎ ) - +px=x {suc n} (suc x) = p001 where + p002 : fromℕ< (s≤s (toℕ≤pred[n] x)) ≡ x + p002 = fromℕ<-toℕ x (s≤s (toℕ≤pred[n] x)) + p001 : (pins (toℕ≤pred[n] (suc x)) ⟨$⟩ʳ (# 0)) ≡ suc x + p001 with <-cmp 0 ((toℕ x)) + ... | tri< a ¬b ¬c = cong suc p002 + ... | tri≈ ¬a b ¬c = cong suc p002 -- pp : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → Fin (suc n) -- pp perm → (( perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) - plist2 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ plist2 {n} perm zero _ = toℕ ( perm ⟨$⟩ʳ (fromℕ< {zero} (s≤s z≤n))) ∷ [] plist2 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ʳ (fromℕ< (s≤s lt))) ∷ plist2 perm i (<-trans lt a<sa) @@ -611,18 +602,24 @@ 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' = refl + f003 : (q : Fin (suc n)) → + ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ʳ q) ≡ + ((perm ∘ₚ flip (pins (toℕ≤pred[n] x))) ⟨$⟩ʳ q) + f003 q = cong (λ k → (perm ∘ₚ flip (pins (toℕ≤pred[n] k))) ⟨$⟩ʳ q ) f001 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 {n} (presp prefl {!!}) (p=0 perm) x=0) ⟩ + ≡⟨ pcong-pF (shrink-cong {n} {perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))} {perm ∘ₚ flip (pins (toℕ≤pred[n] x))} record {peq = f003 } (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) ⟩ + ≡⟨ pcong-pF (shrink-cong (passoc (pprep (FL→perm fl)) (pins ( toℕ≤pred[n] x )) (flip (pins (toℕ≤pred[n] x))) ) 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') ⟩ + ≡⟨ pcong-pF (shrink-cong {n} {pprep (FL→perm fl) ∘ₚ (pins ( toℕ≤pred[n] x ) ∘ₚ flip (pins (toℕ≤pred[n] x)))} {pprep (FL→perm fl) ∘ₚ pid} + ( presp {suc n} {pprep (FL→perm fl) } {_} {(pins ( toℕ≤pred[n] x ) ∘ₚ flip (pins (toℕ≤pred[n] x)))} {pid} prefl + record { peq = λ q → inverseˡ (pins ( toℕ≤pred[n] x )) } ) x=0 x=0') ⟩ perm→FL (shrink (pprep (FL→perm fl) ∘ₚ pid) x=0' ) - ≡⟨ pcong-pF (shrink-cong {n} prefl x=0' x=0') ⟩ + ≡⟨ pcong-pF (shrink-cong {n} {pprep (FL→perm fl) ∘ₚ pid} {pprep (FL→perm fl)} record {peq = λ q → refl } x=0' x=0') ⟩ -- prefl won't work perm→FL (shrink (pprep (FL→perm fl)) x=0' ) ≡⟨ pcong-pF shrink-iso ⟩ perm→FL ( FL→perm fl )