Mercurial > hg > Members > kono > Proof > galois
changeset 48:ac2f21a2d467
cleanup
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 21 Aug 2020 23:44:28 +0900 |
| parents | 1f8e1e7b5770 |
| children | 8b3b95362ca9 |
| files | Putil.agda Symmetric.agda |
| diffstat | 2 files changed, 147 insertions(+), 148 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Putil.agda Fri Aug 21 23:44:28 2020 +0900 @@ -0,0 +1,147 @@ +module Putil where + +open import Level hiding ( suc ; zero ) +open import Algebra +open import Algebra.Structures +open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ) +open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ) renaming ( <-cmp to <-fcmp ) +open import Data.Fin.Permutation +open import Function hiding (id ; flip) +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function.LeftInverse using ( _LeftInverseOf_ ) +open import Function.Equality using (Π) +open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) +open import Data.Nat.Properties -- using (<-trans) +open import Relation.Binary.PropositionalEquality +open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ) renaming (reverse to rev ) +open import nat + +open import Symmetric + + +open import Relation.Nullary +open import Data.Empty +open import Relation.Binary.Core +open import fin + +-- An inductive construction of permutation + +-- we already have refl and trans in the Symmetric Group + +pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n) +pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where + p→ : Fin (suc n) → Fin (suc n) + p→ zero = zero + p→ (suc x) = suc ( perm ⟨$⟩ˡ x) + + p← : Fin (suc n) → Fin (suc n) + p← zero = zero + p← (suc x) = suc ( perm ⟨$⟩ʳ x) + + piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x + piso← zero = refl + piso← (suc x) = cong (λ k → suc k ) (inverseˡ perm) + + piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x + piso→ zero = refl + piso→ (suc x) = cong (λ k → suc k ) (inverseʳ perm) + +pswap : {n : ℕ } → Permutation n n → Permutation (suc (suc n)) (suc (suc n )) +pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where + p→ : Fin (suc (suc n)) → Fin (suc (suc n)) + p→ zero = suc zero + p→ (suc zero) = zero + p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) + + p← : Fin (suc (suc n)) → Fin (suc (suc n)) + p← zero = suc zero + p← (suc zero) = zero + p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) ) + + piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x + piso← zero = refl + piso← (suc zero) = refl + piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) + + piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x + piso→ zero = refl + piso→ (suc zero) = refl + piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) + +-- enumeration + +psawpn : {n : ℕ} → 1 < n → Permutation n n +psawpn {suc zero} (s≤s ()) +psawpn {suc n} (s≤s (s≤s x)) = pswap pid + +pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n +pfill {n} {m} m≤n perm = pfill1 (n - m) (n-m<n n m ) (subst (λ k → Permutation k k ) (n-n-m=m m≤n ) perm) where + pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n + pfill1 0 _ perm = perm + pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) ) + +-- +-- psawpim (inseert swap at position m ) +-- not easy to write directory beacause left-inverse-of may contains Fin relations +-- +psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n +psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) ) + +n≤ : (i : ℕ ) → {j : ℕ } → i ≤ i + j +n≤ (zero) {j} = z≤n +n≤ (suc i) {j} = s≤s ( n≤ i ) + +lem0 : {n : ℕ } → n ≤ n +lem0 {zero} = z≤n +lem0 {suc n} = s≤s lem0 + +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 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 ) + +plist : {n : ℕ} → Permutation n n → List ℕ +plist {0} perm = [] +plist {suc j} perm = rev (plist1 j a<sa) where + n = suc j + plist1 : (i : ℕ ) → i < n → List ℕ + plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ [] + plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa) + +all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) ) +all-perm n = pls6 n where + lem1 : {i n : ℕ } → i ≤ n → i < suc n + lem1 z≤n = s≤s z≤n + lem1 (s≤s lt) = s≤s (lem1 lt) + lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n + lem2 i≤n = ≤-trans i≤n ( refl-≤s ) + pls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) + pls4 zero n i≤n perm x = (pprep perm ∘ₚ pins i≤n ) ∷ x + pls4 (suc i) n i≤n perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (pprep perm ∘ₚ pins {n} {suc i} i≤n ∷ x) + pls5 : ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) + pls5 n [] x = x + pls5 n (h ∷ x) y = pls5 n x (pls4 n n lem0 h y) + pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n)) + pls6 zero = pid ∷ [] + pls6 (suc n) = pls5 (suc n) (rev (pls6 n) ) [] -- rev to put id first + +pls : (n : ℕ ) → List (List ℕ ) +pls n = Data.List.map plist (all-perm n) where
--- a/Symmetric.agda Fri Aug 21 19:24:56 2020 +0900 +++ b/Symmetric.agda Fri Aug 21 23:44:28 2020 +0900 @@ -73,151 +73,3 @@ j ⟨$⟩ˡ q ∎ where open ≡-Reasoning -open import Relation.Nullary -open import Data.Empty -open import Relation.Binary.Core -open import fin - --- An inductive construction of permutation - --- we already have refl and trans - -pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n) -pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where - p→ : Fin (suc n) → Fin (suc n) - p→ zero = zero - p→ (suc x) = suc ( perm ⟨$⟩ˡ x) - - p← : Fin (suc n) → Fin (suc n) - p← zero = zero - p← (suc x) = suc ( perm ⟨$⟩ʳ x) - - piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x - piso← zero = refl - piso← (suc x) = cong (λ k → suc k ) (inverseˡ perm) - - piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x - piso→ zero = refl - piso→ (suc x) = cong (λ k → suc k ) (inverseʳ perm) - -pswap : {n : ℕ } → Permutation n n → Permutation (suc (suc n)) (suc (suc n )) -pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where - p→ : Fin (suc (suc n)) → Fin (suc (suc n)) - p→ zero = suc zero - p→ (suc zero) = zero - p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) - - p← : Fin (suc (suc n)) → Fin (suc (suc n)) - p← zero = suc zero - p← (suc zero) = zero - p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) ) - - piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x - piso← zero = refl - piso← (suc zero) = refl - piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) - - piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x - piso→ zero = refl - piso→ (suc zero) = refl - piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) - --- enumeration - -psawpn : {n : ℕ} → 1 < n → Permutation n n -psawpn {suc zero} (s≤s ()) -psawpn {suc n} (s≤s (s≤s x)) = pswap pid - -pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n -pfill {n} {m} m≤n perm = pfill1 (n - m) (n-m<n n m ) (subst (λ k → Permutation k k ) (n-n-m=m m≤n ) perm) where - pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n - pfill1 0 _ perm = perm - pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) ) - -psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n -psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) ) - -n≤ : (i : ℕ ) → {j : ℕ } → i ≤ i + j -n≤ (zero) {j} = z≤n -n≤ (suc i) {j} = s≤s ( n≤ i ) - -lem0 : {n : ℕ } → n ≤ n -lem0 {zero} = z≤n -lem0 {suc n} = s≤s lem0 - -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 - -eperm : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) -eperm {_} {zero} _ = pid -eperm {suc _} {suc zero} _ = pswap pid -eperm {suc (suc n)} {suc m} (s≤s m<n) = eperm1 (suc m) (suc (suc n)) lem0 where - eperm1 : (i j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) - eperm1 _ zero _ = pid - eperm1 zero _ _ = pid - eperm1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j} (s≤s (s≤s si≤n)) ∘ₚ eperm1 i j (≤-trans si≤n refl-≤s ) - - -plist : {n : ℕ} → Permutation n n → List ℕ -plist {0} perm = [] -plist {suc j} perm = rev (plist1 j a<sa) where - n = suc j - plist1 : (i : ℕ ) → i < n → List ℕ - plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ [] - plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa) - -testi0 = plist (pprep (pid {3}) ) -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] -testi01 = plist (psawpim {4} {2} (n≤ 4 {0}) ) -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] -testi02 = plist (psawpim {4} {2} (n≤ 4 {0}) ∘ₚ psawpim {4} {1} (n≤ 3)) -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ [] -testi03 = plist ((psawpim (n≤ 4 {0}) ∘ₚ psawpim (n≤ 3) ) ∘ₚ psawpim {4} {0} (n≤ 2 )) -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ [] -ttt0 = testi0 ∷ testi01 ∷ testi02 ∷ testi03 ∷ [] - -tt0 = plist (eperm {3} {0} (n≤ 0)) ∷ plist ( eperm {3} {1} (n≤ 1 )) ∷ plist ( eperm {3} {2} (n≤ 2 )) ∷ plist ( eperm {3} {3} (n≤ 3 )) ∷ [] - -c0 = pid {2} -- pprep ( eperm {3} (n≤ 3) pid) --- e0 = pprep ( eperm {3} (n≤ 3) pid) -ct0 = c0 ∘ₚ eperm {1} (n≤ 0 ) -ct1 = c0 ∘ₚ eperm {1} (n≤ 1 ) -ttt1 = plist ct0 ∷ plist ct1 ∷ [] - -d0 = pid {3} -- pprep ( eperm {3} (n≤ 3) pid) --- e0 = pprep ( eperm {3} (n≤ 3) pid) -dt0 = d0 ∘ₚ eperm {2} (n≤ 0 ) -dt1 = d0 ∘ₚ eperm {2} (n≤ 1 ) -dt2 = d0 ∘ₚ eperm {2} (n≤ 2 ) -ttt3 = plist dt0 ∷ plist dt1 ∷ plist dt2 ∷ [] - --- e0 = pid {4} -- eperm (n≤ 2) (eperm (n≤ 2) (eperm (n≤ 1) (pid {1}))) -e0 = pid {5} -- pprep ( eperm {3} (n≤ 3) pid) --- e0 = pprep ( eperm {3} (n≤ 3) pid) -et0 = e0 ∘ₚ eperm {4} {4} (n≤ 4 ) -et1 = e0 ∘ₚ eperm {4} {3} (n≤ 3 ) -et2 = e0 ∘ₚ eperm {4} (n≤ 2 ) -et3 = e0 ∘ₚ eperm {4} (n≤ 1 ) -et4 = e0 ∘ₚ eperm {4} (n≤ 0 ) -ttt2 = plist et0 ∷ plist et1 ∷ plist et2 ∷ plist et3 ∷ plist et4 ∷ [] - -pls : (n : ℕ ) → List (List ℕ ) -pls n = Data.List.map plist (pls6 n) where - lem1 : {i n : ℕ } → i ≤ n → i < suc n - lem1 z≤n = s≤s z≤n - lem1 (s≤s lt) = s≤s (lem1 lt) - lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n - lem2 i≤n = ≤-trans i≤n ( refl-≤s ) - pls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) - pls4 zero n i≤n perm x = (pprep perm ∘ₚ eperm i≤n ) ∷ x - pls4 (suc i) n i≤n perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (pprep perm ∘ₚ eperm {n} {suc i} i≤n ∷ x) - pls5 : ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) - pls5 n [] x = x - pls5 n (h ∷ x) y = pls5 n x (pls4 n n lem0 h y) - pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n)) - pls6 zero = pid ∷ [] - pls6 (suc n) = pls5 (suc n) (pls6 n) [] - pls7 : List (List ℕ ) - pls7 = Data.List.map plist (pls4 2 2 lem0 (eperm (n≤ 0 ) ) (pls4 2 2 lem0 (eperm (n≤ 1 ) ) [] ))