Mercurial > hg > Members > kono > Proof > galois
changeset 82:fcb9e29d1894
... pleq worked
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 26 Aug 2020 19:21:42 +0900 |
| parents | 59aaf2000591 |
| children | f2edc816740b |
| files | sym5.agda |
| diffstat | 1 files changed, 6 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/sym5.agda Wed Aug 26 19:09:32 2020 +0900 +++ b/sym5.agda Wed Aug 26 19:21:42 2020 +0900 @@ -62,16 +62,16 @@ 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 n) → toℕ f ≤ n + 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 3 - dba1<4 : Fin 4 - aec0<3 : Fin 3 - aec1<4 : Fin 4 + dba0<3 : Fin 4 + dba1<4 : Fin 5 + aec0<3 : Fin 4 + aec1<4 : Fin 5 abc= : abc i<3 j<4 =p= [ dba (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , aec (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] open Triple @@ -142,17 +142,7 @@ triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = {!!} triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = {!!} triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = - record { dba0<3 = # 1 ; dba1<4 = fromℕ< a<sa ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = tt7 } where - tt7 : abc (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =p= - [ dba (fin≤n {3} (# 1))(fin≤n {4} (fromℕ< a<sa)) , aec (fin≤n {3} (# 0)) (fin≤n {4} (# 3)) ] - tt7 = record { peq = λ q → lll q } where - lll : (q : Fin 5) → _ - 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 - tt19 = {!!} + record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 )