Mercurial > hg > Members > kono > Proof > galois
changeset 85:2d79a2c06c6c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Aug 2020 01:19:32 +0900 |
| parents | 7e36bd8916a9 |
| children | c5329963c583 |
| files | Putil.agda sym5.agda |
| diffstat | 2 files changed, 63 insertions(+), 63 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Wed Aug 26 23:53:40 2020 +0900 +++ b/Putil.agda Thu Aug 27 01:19:32 2020 +0900 @@ -144,6 +144,14 @@ plist0 {0} perm = [] plist0 {suc n} perm = plist2 perm n a<sa +open _=p=_ + +←pleq : {n : ℕ} → (x y : Permutation n n ) → x =p= y → plist0 x ≡ plist0 y +←pleq {zero} x y eq = refl +←pleq {suc n} x y eq = ←pleq1 n a<sa where + ←pleq1 : (i : ℕ ) → (i<sn : i < suc n ) → plist2 x i i<sn ≡ plist2 y i i<sn + ←pleq1 zero _ = cong ( λ k → toℕ k ∷ [] ) ( peq eq (fromℕ< {zero} (s≤s z≤n))) + ←pleq1 (suc i) (s≤s lt) = cong₂ ( λ j k → toℕ j ∷ k ) ( peq eq (fromℕ< (s≤s lt))) ( ←pleq1 i (<-trans lt a<sa) ) headeq : {A : Set } → {x y : A } → {xt yt : List A } → (x ∷ xt) ≡ (y ∷ yt) → x ≡ y headeq refl = refl
--- a/sym5.agda Wed Aug 26 23:53:40 2020 +0900 +++ b/sym5.agda Thu Aug 27 01:19:32 2020 +0900 @@ -52,10 +52,11 @@ 3rot : Permutation 3 3 3rot = pid {3} ∘ₚ pins (n≤ 2) + save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 + save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) + ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 - ins2 abc i<3 j<4 = (save2 ∘ₚ (pprep (pprep abc))) ∘ₚ flip save2 where - save2 : Permutation 5 5 - save2 = ( (( pid {5} ∘ₚ flip (pins (s≤s i<3) ) )) ∘ₚ flip (pins j<4)) + ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 abc i<3 j<4 = ins2 3rot i<3 j<4 @@ -65,6 +66,33 @@ aec : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 aec i<3 j<4 = ins2 (pinv 3rot) i<3 j<4 + import Relation.Binary.Reasoning.Setoid as EqReasoning + abc→dba : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p= dba i<3 j<4 + abc→dba i<3 j<4 = lemma where + open EqReasoning (Algebra.Group.setoid (Symmetric 5)) + lemma : (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p= dba i<3 j<4 + lemma = begin + abc i<3 j<4 ∘ₚ abc i<3 j<4 + ≈⟨ prefl ⟩ + ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 )) ∘ₚ + ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 )) + ≈⟨ {!!} ⟩ + (((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ (flip (save2 i<3 j<4 ))) ∘ₚ + (save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot)))) ∘ₚ flip (save2 i<3 j<4 ) + ≈⟨ {!!} ⟩ + (save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 ) + ≈⟨ {!!} ⟩ + (save2 i<3 j<4 ∘ₚ (pprep (pprep (3rot ∘ₚ 3rot)))) ∘ₚ flip (save2 i<3 j<4 ) + ≈⟨ prefl ⟩ + dba i<3 j<4 + ∎ + + dba→aec : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → (dba i<3 j<4 ∘ₚ dba i<3 j<4 ) =p= aec i<3 j<4 + dba→aec = {!!} + + aec→abc : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → (aec i<3 j<4 ∘ₚ aec i<3 j<4 ) =p= abc i<3 j<4 + aec→abc = {!!} + record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where field dba0<3 : Fin 4 @@ -73,66 +101,30 @@ 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 - -- a b c d e - t1 = (plist ( abc (n≤ 0) (n≤ 0) ) ++ ( 0 ∷ 0 ∷ [])) -- ( ∷ ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ cde no 4 on top - -- ∷ (plist ( abc (n≤ 0) (n≤ 1) ) ++ ( 0 ∷ 1 ∷ [])) -- ( ∷ ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 0) (n≤ 2) ) ++ ( 0 ∷ 2 ∷ [])) -- (3 ∷ ∷ ∷ 4 ∷ 0 ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 0) (n≤ 3) ) ++ ( 0 ∷ 3 ∷ [])) -- (2 ∷ ∷ 4 ∷ ∷ 0 ∷ []) ∷ 120 : aec - -- ∷ (plist ( abc (n≤ 0) (n≤ 4) ) ++ ( 0 ∷ 4 ∷ [])) -- (2 ∷ ∷ 3 ∷ 0 ∷ ∷ []) ∷ 342 : dba, (open c, put 1st) - ∷ (plist ( abc (n≤ 1) (n≤ 0) ) ++ ( 1 ∷ 0 ∷ [])) -- ( ∷ 3 ∷ ∷ 4 ∷ 1 ∷ []) ∷ - ∷ (plist ( abc (n≤ 1) (n≤ 1) ) ++ ( 1 ∷ 1 ∷ [])) -- ( ∷ 3 ∷ ∷ 4 ∷ 1 ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 1) (n≤ 2) ) ++ ( 1 ∷ 2 ∷ [])) -- (3 ∷ ∷ ∷ 4 ∷ 0 ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 1) (n≤ 3) ) ++ ( 1 ∷ 3 ∷ [])) -- (1 ∷ 4 ∷ ∷ ∷ 0 ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 1) (n≤ 4) ) ++ ( 1 ∷ 4 ∷ [])) -- (1 ∷ 3 ∷ ∷ 0 ∷ ∷ []) ∷ 120 dba , 340 : dba - -- ∷ (plist ( abc (n≤ 2) (n≤ 0) ) ++ ( 2 ∷ 0 ∷ [])) -- ( ∷ 2 ∷ 4 ∷ ∷ 1 ∷ []) ∷ 342 : aec (open b, put 2nd) - -- ∷ (plist ( abc (n≤ 2) (n≤ 1) ) ++ ( 2 ∷ 1 ∷ [])) -- ( ∷ 2 ∷ 4 ∷ ∷ 1 ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 2) (n≤ 2) ) ++ ( 2 ∷ 2 ∷ [])) -- (2 ∷ ∷ 4 ∷ ∷ 0 ∷ []) ∷ 340 : aec -- 1 3 3 4 - -- ∷ (plist ( abc (n≤ 2) (n≤ 3) ) ++ ( 2 ∷ 3 ∷ [])) -- (1 ∷ 4 ∷ ∷ ∷ 0 ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 2) (n≤ 4) ) ++ ( 2 ∷ 4 ∷ [])) -- (1 ∷ 2 ∷ 0 ∷ ∷ ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 3) (n≤ 0) ) ++ ( 3 ∷ 0 ∷ [])) -- ( ∷ 2 ∷ 3 ∷ 1 ∷ ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 3) (n≤ 1) ) ++ ( 3 ∷ 1 ∷ [])) -- ( ∷ 2 ∷ 3 ∷ 1 ∷ ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 3) (n≤ 2) ) ++ ( 3 ∷ 2 ∷ [])) -- (2 ∷ ∷ 3 ∷ 0 ∷ ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 3) (n≤ 3) ) ++ ( 3 ∷ 3 ∷ [])) -- (1 ∷ 3 ∷ ∷ 0 ∷ ∷ []) ∷ - -- ∷ (plist ( abc (n≤ 3) (n≤ 4) ) ++ ( 3 ∷ 4 ∷ [])) -- (1 ∷ 2 ∷ 0 ∷ ∷ ∷ []) ∷ - ∷ [] + dba= : + {a a' : ℕ } → (a<3 : a ≤ 3 ) → ( a<4 : a' ≤ 4 ) → + {b b' : ℕ } → (b<3 : b ≤ 3 ) → ( b<4 : b' ≤ 4 ) → + {c c' : ℕ } → (c<3 : c ≤ 3 ) → ( c<4 : c' ≤ 4 ) → + abc a<3 a<4 =p= [ dba b<3 b<4 , aec c<3 c<4 ] → + dba a<3 a<4 =p= [ aec b<3 b<4 , abc c<3 c<4 ] + dba= a<3 a<4 b<3 b<4 c<3 c<4 dq = {!!} where + open EqReasoning (Algebra.Group.setoid (Symmetric 5)) + lemma1 : dba a<3 a<4 =p= [ aec b<3 b<4 , abc c<3 c<4 ] + lemma1 = begin + dba a<3 a<4 + ≈⟨ ? ⟩ + [ aec b<3 b<4 , abc c<3 c<4 ] + ∎ - t8 : ( i : Fin 4 ) → (j : Fin 5) → List ( List ℕ ) - t8 i j = ((plist [ dba (n≤ 0) (n≤ 0) , aec (fin≤n {3} i) (fin≤n {4} j) ] ) ++ (8 ∷ 0 ∷ 0 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 0) (n≤ 1) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 0 ∷ 1 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 0) (n≤ 2) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 0 ∷ 2 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 0) (n≤ 3) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 0 ∷ 3 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 0) (n≤ 4) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 0 ∷ 4 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 1) (n≤ 0) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 0 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 1) (n≤ 1) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 1 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 1) (n≤ 2) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 2 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 1) (n≤ 3) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 3 ∷ [] )) -- - ∷ ((plist ( [ dba (n≤ 1) (n≤ 4) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 1 ∷ 4 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 2) (n≤ 0) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 0 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 2) (n≤ 1) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 1 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 2) (n≤ 2) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 2 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 2) (n≤ 3) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 3 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 2) (n≤ 4) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 2 ∷ 4 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 3) (n≤ 0) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 0 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 3) (n≤ 1) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 1 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 3) (n≤ 2) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 2 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 3) (n≤ 3) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 4 ∷ [] )) - ∷ ((plist ( [ dba (n≤ 3) (n≤ 4) , aec (fin≤n {3} i) (fin≤n {4} j) ] )) ++ (8 ∷ 3 ∷ 4 ∷ [] )) - ∷ [] + aec= : + {a a' : ℕ } → (a<3 : a ≤ 3 ) → ( a<4 : a' ≤ 4 ) → + {b b' : ℕ } → (b<3 : b ≤ 3 ) → ( b<4 : b' ≤ 4 ) → + {c c' : ℕ } → (c<3 : c ≤ 3 ) → ( c<4 : c' ≤ 4 ) → + dba a<3 a<4 =p= [ aec b<3 b<4 , abc c<3 c<4 ] → + aec a<3 a<4 =p= [ abc b<3 b<4 , dba c<3 c<4 ] + aec= = {!!} - t88 = t1 ++ t8 (# 3) (# 1) - ++ t8 (# 3) (# 2) - ++ t8 (# 3) (# 3) - ++ t8 (# 3) (# 4) - - --- 1 ∷ 2 ∷ 0 ∷ ∷ ∷ [] abc -- abc (n≤ 3) (n≤ 4) - --- 3 ∷ 0 ∷ ∷ 1 ∷ ∷ [] dba - dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 4) - --- 4 ∷ ∷ 0 ∷ ∷ 2 ∷ [] aec - aec99 = ins2 (pinv 3rot) (n≤ 0) (n≤ 3) - tt1 = plist dba99 ∷ plist (pinv dba99) ∷ [] - tt2 = plist aec99 ∷ plist (pinv aec99) ∷ [] - tt5 = plist [ dba99 , aec99 ] -- =p= abc + open Triple triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } @@ -174,7 +166,7 @@ open _=p=_ counter-example : ¬ (abc 0<3 0<4 =p= pid ) - counter-example = {!!} -- p with peq p (# 1) - -- ... | () + counter-example eq with ←pleq _ _ eq + ... | ()