Mercurial > hg > Members > kono > Proof > galois
changeset 89:dcb4450680ab
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 28 Aug 2020 13:33:35 +0900 |
| parents | 405c1f727ffe |
| children | bb8c5b366219 |
| files | Putil.agda |
| diffstat | 1 files changed, 52 insertions(+), 60 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Fri Aug 28 11:05:45 2020 +0900 +++ b/Putil.agda Fri Aug 28 13:33:35 2020 +0900 @@ -105,25 +105,6 @@ lem00 : {n m : ℕ } → n ≡ m → n ≤ m lem00 refl = lem0 --- pconcat : {n m : ℕ } → Permutation m m → Permutation n n → Permutation (m + n) (m + n) --- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ? - --- inductivley enmumerate permutations --- from n-1 length create n length inserting new element at position m - --- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] --- 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] plist ( pins {3} (n≤ 1) ) --- 1 ∷ 2 ∷ 0 ∷ 3 ∷ [] --- 1 ∷ 2 ∷ 3 ∷ 0 ∷ [] - -pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) -pins {_} {zero} _ = pid -pins {suc _} {suc zero} _ = pswap pid -pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc (suc n)) lem0 where - pins1 : (j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) - pins1 zero _ = pid - pins1 (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j} (s≤s (s≤s si≤n)) ∘ₚ pins1 j (≤-trans si≤n refl-≤s ) - plist1 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ plist1 {n} perm zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ< {zero} (s≤s z≤n))) ∷ [] plist1 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ< (s≤s lt))) ∷ plist1 perm i (<-trans lt a<sa) @@ -132,6 +113,56 @@ plist {0} perm = [] plist {suc n} perm = rev (plist1 perm n a<sa) +-- pconcat : {n m : ℕ } → Permutation m m → Permutation n n → Permutation (m + n) (m + n) +-- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ? + +-- inductivley enmumerate permutations +-- from n-1 length create n length inserting new element at position m + +-- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] +-- 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] plist ( pins {3} (n≤ 1) ) 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] +-- 1 ∷ 2 ∷ 0 ∷ 3 ∷ [] plist ( pins {3} (n≤ 2) ) 2 ∷ 0 ∷ 1 ∷ 3 ∷ [] +-- 1 ∷ 2 ∷ 3 ∷ 0 ∷ [] plist ( pins {3} (n≤ 3) ) 3 ∷ 0 ∷ 1 ∷ 2 ∷ [] +pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) +pins {_} {zero} _ = pid +pins {suc _} {suc zero} _ = pswap pid +pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc m) (suc (suc n)) lem0 where + pins1 : (i j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) + pins1 _ zero _ = pid + pins1 zero _ _ = pid + pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j} (s≤s (s≤s si≤n)) ∘ₚ pins1 i j (≤-trans si≤n refl-≤s ) + +pins' : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) +pins' {_} {zero} _ = pid +pins' {suc n} {suc m} (s≤s m≤n) = permutation p← p→ record { left-inverse-of = piso← ; right-inverse-of = piso→ } where + + next : Fin (suc (suc n)) → Fin (suc (suc n)) + next zero = suc zero + next (suc x) = fromℕ< (≤-trans (fin<n {_} {x} ) refl-≤s ) + + p→ : Fin (suc (suc n)) → Fin (suc (suc n)) + p→ x with <-cmp (toℕ x) (suc m) + ... | tri< a ¬b ¬c = fromℕ< (≤-trans (s≤s a) (≤-trans (s≤s (s≤s m≤n) ) lem0 )) + ... | tri≈ ¬a b ¬c = zero + ... | tri> ¬a ¬b c = x + + p← : Fin (suc (suc n)) → Fin (suc (suc n)) + p← zero = fromℕ< (s≤s (s≤s m≤n)) + p← (suc x) with <-cmp (toℕ x) (suc m) + ... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s ) + ... | tri≈ ¬a b ¬c = suc x + ... | tri> ¬a ¬b c = suc x + + piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x + piso← = {!!} + + piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x + piso→ = {!!} + +t7 = plist (pins' {3} (n≤ 3)) ∷ plist (flip ( pins' {3} (n≤ 3) )) ∷ plist ( pins' {3} (n≤ 3) ∘ₚ flip ( pins' {3} (n≤ 3))) ∷ [] +t8 = {!!} + + 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) @@ -345,45 +376,6 @@ shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm) refl =p= perm shrink-iso {n} {perm} = record { peq = λ q → refl } -p01 : (perm : Permutation 1 1) → perm =p= pid -p01 perm = record { peq = p01e } where - p01e : (q : Fin 1) → (perm ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) - p01e zero with perm ⟨$⟩ʳ zero - ... | zero = refl - -p=0 : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0 -p=0 {zero} perm with p01 perm | p01 ( flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))) -... | s | t = begin - ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) - ≡⟨ peqˡ (presp (p01 perm) (p01 (flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))))) (# 0) ⟩ - (pid ∘ₚ pid ) ⟨$⟩ʳ (# 0) - ≡⟨⟩ - # 0 - ∎ where open ≡-Reasoning -p=0 {suc (zero)} perm with perm ⟨$⟩ʳ (# 0) | inspect ( _⟨$⟩ʳ_ perm ) (# 0) -... | zero | record { eq = e } = begin - (perm ∘ₚ pid) ⟨$⟩ˡ (# 0) - ≡⟨⟩ - perm ⟨$⟩ˡ (# 0) - ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (sym e ) ⟩ - perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (# 0)) - ≡⟨ inverseˡ perm ⟩ - # 0 - ∎ where open ≡-Reasoning -... | suc zero | record { eq = e } = begin - (perm ∘ₚ pswap pid) ⟨$⟩ˡ (# 0) - ≡⟨⟩ - perm ⟨$⟩ˡ (# 1) - ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (sym e ) ⟩ - perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (# 0)) - ≡⟨ inverseˡ perm ⟩ - # 0 - ∎ where open ≡-Reasoning -p=0 {suc (suc n) } perm = p=01 (suc (suc n)) lem0 where - p=01 : (j : ℕ ) → j ≤ suc (suc n) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0 - p=01 zero _ = {!!} - p=01 (suc j) (s≤s si≤n) = {!!} - FL→perm : {n : ℕ } → FL n → Permutation n n FL→perm f0 = pid FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x ) @@ -411,8 +403,8 @@ perm→FL : {n : ℕ } → Permutation n n → FL n perm→FL {zero} perm = f0 --- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm) -perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) +perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm) +-- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) -- t5 = plist t4 ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 3 ) )) t5 = plist (t4) ∷ plist (flip t4)