Mercurial > hg > Members > kono > Proof > galois
changeset 83:f2edc816740b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 26 Aug 2020 19:53:24 +0900 |
| parents | fcb9e29d1894 |
| children | 7e36bd8916a9 |
| files | fin.agda sym5.agda |
| diffstat | 2 files changed, 30 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/fin.agda Wed Aug 26 19:21:42 2020 +0900 +++ b/fin.agda Wed Aug 26 19:53:24 2020 +0900 @@ -2,7 +2,7 @@ module fin where -open import Data.Fin hiding (_<_) +open import Data.Fin hiding (_<_ ; _≤_ ) open import Data.Nat open import logic open import nat @@ -22,6 +22,10 @@ fin<n {_} {zero} = s≤s z≤n fin<n {suc n} {suc f} = s≤s (fin<n {n} {f}) +fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n +fin≤n {_} zero = z≤n +fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f) + pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0 → Data.Nat.pred (toℕ f) < n pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n pred<n {suc n} {suc f} (s≤s z≤n) = fin<n
--- a/sym5.agda Wed Aug 26 19:21:42 2020 +0900 +++ b/sym5.agda Wed Aug 26 19:53:24 2020 +0900 @@ -62,10 +62,6 @@ aec : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 aec i<3 j<4 = ins2 (pinv 3rot) i<3 j<4 - fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n - fin≤n {_} zero = z≤n - fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f) - record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where field dba0<3 : Fin 4 @@ -77,7 +73,7 @@ open Triple -- d e a b c t1 = plist ( abc (n≤ 0) (n≤ 0) ) -- ( ∷ ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ no 4 on top - ∷ plist ( abc (n≤ 0) (n≤ 1) ) -- ( ∷ ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ + ∷ plist ( abc (n≤ 0) (n≤ 1) ) -- ( ∷ ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ 342 043 312 ∷ plist ( abc (n≤ 0) (n≤ 2) ) -- (3 ∷ ∷ ∷ 4 ∷ 0 ∷ []) ∷ ∷ plist ( abc (n≤ 0) (n≤ 3) ) -- (2 ∷ ∷ 4 ∷ ∷ 0 ∷ []) ∷ ∷ plist ( abc (n≤ 0) (n≤ 4) ) -- (2 ∷ ∷ 3 ∷ 0 ∷ ∷ []) ∷ @@ -98,28 +94,37 @@ ∷ plist ( abc (n≤ 3) (n≤ 4) ) -- (1 ∷ 2 ∷ 0 ∷ ∷ ∷ []) ∷ [] ∷ [] + td = plist ( dba (n≤ 0) (n≤ 0) ) -- ( ∷ ∷ 4 ∷ 2 ∷ 3 ∷ []) ∷ + ∷ plist ( dba (n≤ 0) (n≤ 1) ) -- ( ∷ ∷ 4 ∷ 2 ∷ 3 ∷ []) ∷ + ∷ plist ( dba (n≤ 0) (n≤ 2) ) -- (4 ∷ ∷ ∷ 0 ∷ 3 ∷ []) ∷ + ∷ plist ( dba (n≤ 0) (n≤ 3) ) -- (4 ∷ ∷ 0 ∷ ∷ 2 ∷ []) ∷ + ∷ plist ( dba (n≤ 0) (n≤ 4) ) -- (3 ∷ ∷ 0 ∷ 2 ∷ ∷ []) ∷ + ∷ plist ( dba (n≤ 1) (n≤ 0) ) -- ( ∷ 4 ∷ ∷ 1 ∷ 3 ∷ []) ∷ + ∷ plist ( dba (n≤ 1) (n≤ 1) ) -- ( ∷ 4 ∷ ∷ 1 ∷ 3 ∷ []) ∷ + ∷ plist ( dba (n≤ 1) (n≤ 2) ) -- (4 ∷ ∷ ∷ 0 ∷ 3 ∷ []) ∷ + ∷ plist ( dba (n≤ 1) (n≤ 3) ) -- (4 ∷ 0 ∷ ∷ ∷ 1 ∷ []) ∷ + ∷ plist ( dba (n≤ 1) (n≤ 4) ) -- (3 ∷ 0 ∷ ∷ 1 ∷ ∷ []) ∷ + ∷ plist ( dba (n≤ 2) (n≤ 0) ) -- ( ∷ 4 ∷ 1 ∷ ∷ 2 ∷ []) ∷ + ∷ plist ( dba (n≤ 2) (n≤ 1) ) -- ( ∷ 4 ∷ 1 ∷ ∷ 2 ∷ []) ∷ + ∷ plist ( dba (n≤ 2) (n≤ 2) ) -- (4 ∷ ∷ 0 ∷ ∷ 2 ∷ []) ∷ + ∷ plist ( dba (n≤ 2) (n≤ 3) ) -- (4 ∷ 0 ∷ ∷ ∷ 1 ∷ []) ∷ + ∷ plist ( dba (n≤ 2) (n≤ 4) ) -- (2 ∷ 0 ∷ 1 ∷ ∷ ∷ []) ∷ + ∷ plist ( dba (n≤ 3) (n≤ 0) ) -- ( ∷ 3 ∷ 1 ∷ 2 ∷ ∷ []) ∷ + ∷ plist ( dba (n≤ 3) (n≤ 1) ) -- ( ∷ 3 ∷ 1 ∷ 2 ∷ ∷ []) ∷ + ∷ plist ( dba (n≤ 3) (n≤ 2) ) -- (3 ∷ ∷ 0 ∷ 2 ∷ ∷ []) ∷ + ∷ plist ( dba (n≤ 3) (n≤ 3) ) -- (3 ∷ 0 ∷ ∷ 1 ∷ ∷ []) ∷ + ∷ plist ( dba (n≤ 3) (n≤ 4) ) -- (2 ∷ 0 ∷ 1 ∷ ∷ ∷ []) ∷ [] + ∷ [] + --- 1 ∷ 2 ∷ 0 ∷ ∷ ∷ [] abc -- abc (n≤ 3) (n≤ 4) --- 3 ∷ 0 ∷ ∷ 1 ∷ ∷ [] dba - dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 4) + dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 2) --- 4 ∷ ∷ 0 ∷ ∷ 2 ∷ [] aec - aec99 = ins2 (pinv 3rot) (n≤ 0) (n≤ 3) + aec99 = ins2 (pinv 3rot) (n≤ 1) (n≤ 4) tt1 = plist dba99 ∷ plist (pinv dba99) ∷ [] tt2 = plist aec99 ∷ plist (pinv aec99) ∷ [] tt5 = plist [ dba99 , aec99 ] -- =p= abc - tt6 : [ dba99 , aec99 ] =p= abc (n≤ 3) (n≤ 4) - tt6 = record { peq = λ q → lll q } where - lll : (q : Fin 5) → ([ dba99 , aec99 ] ⟨$⟩ʳ q) ≡ (abc (n≤ 3) (n≤ 4) ⟨$⟩ʳ q) - lll zero = refl - lll (suc zero) = refl - lll (suc (suc zero)) = refl - lll (suc (suc (suc zero))) = refl - lll (suc (suc (suc (suc zero)))) = refl - tt8 = plist ( dba (fin<n {3} {# 0}) (fin<n {4} {# 3})) - tt9 : fin<n {4} {# 3} ≡ n≤ 4 - tt9 = refl - tta : fin≤n {3} (# 1) ≡ n≤ 1 - tta = refl triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 triple z≤n z≤n = record { dba0<3 = {!!} ; dba1<4 = {!!} ; aec0<3 = {!!} ; aec1<4 = {!!} ; abc= = {!!} }