Mercurial > hg > Members > kono > Proof > galois
changeset 39:7b890eb577a6
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 20 Aug 2020 09:44:08 +0900 |
| parents | bc289ffd0896 |
| children | e87ed47742b1 |
| files | Symmetric.agda |
| diffstat | 1 files changed, 10 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/Symmetric.agda Thu Aug 20 09:07:54 2020 +0900 +++ b/Symmetric.agda Thu Aug 20 09:44:08 2020 +0900 @@ -14,7 +14,7 @@ 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) +open import Data.List using (List; []; _∷_ ; length ; _++_ ) open import nat fid : {p : ℕ } → Fin p → Fin p @@ -173,7 +173,7 @@ NL (suc n) = List ( NL n ) pls : (n : ℕ ) → List (List ℕ ) -pls n = pls1 n n lem0 where +pls n = pls1 n n lem0 where lem0 : {n : ℕ } → n ≤ n lem0 {zero} = z≤n lem0 {suc n} = s≤s lem0 @@ -182,9 +182,12 @@ lem1 (s≤s lt) = s≤s (lem1 lt) lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n lem2 i≤n = ≤-trans i≤n ( refl-≤s ) - pls2 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation (suc n) (suc n) - pls2 0 n i≤<n = pid - pls2 (suc i) (suc n) (s≤s i≤n) = eperm {suc n} {i} (lem1 i≤n) ( pls2 i n i≤n) - pls1 : ( i n : ℕ ) → i ≤ n → List (List ℕ) + pls3 : ( i n : ℕ ) → (i<n : i < n ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) + pls3 i n i<n [] x = x + pls3 i n i<n (h ∷ t) x = pls3 i n i<n t ( eperm {n} {i} i<n h ∷ x ) + pls2 : ( i n : ℕ ) → (i<n : i ≤ n ) → List (Permutation (suc n) (suc n)) + pls2 0 n i≤<n = pid ∷ [] + pls2 (suc i) (suc n) (s≤s i≤n) = pls3 i (suc n) (lem1 i≤n) ( pls2 i n i≤n) [] + pls1 : ( i n : ℕ ) → i ≤ n → List (List ℕ) pls1 0 n _ = [] - pls1 (suc i) n (s≤s i≤n) = plist ( pls2 i n (lem2 i≤n)) ∷ pls1 i n (lem2 i≤n) + pls1 (suc i) n (s≤s i≤n) = (Data.List.map plist ( pls2 i n (lem2 i≤n)) ) ++ pls1 i n (lem2 i≤n)