Mercurial > hg > Members > kono > Proof > galois
changeset 77:fba304a25c36
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 26 Aug 2020 04:56:29 +0900 |
| parents | cef943dcd18c |
| children | 9cffb308269a |
| files | sym5.agda |
| diffstat | 1 files changed, 28 insertions(+), 69 deletions(-) [+] |
line wrap: on
line diff
--- a/sym5.agda Wed Aug 26 01:41:52 2020 +0900 +++ b/sym5.agda Wed Aug 26 04:56:29 2020 +0900 @@ -21,9 +21,10 @@ open import Data.Fin.Permutation open import Data.List hiding ( [_] ) open import nat +open import fin ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) -¬sym5solvable sol = counter-example {!!} where -- (end5 (abc ? 0<4 ) (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) ) where +¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) ) where -- -- dba 1320 d → b → a → d @@ -53,78 +54,36 @@ save2 : Permutation 5 5 save2 = ( (( pid {5} ∘ₚ flip (pins (s≤s i<3) ) )) ∘ₚ flip (pins j<4)) - dba-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) - dba-0 = {!!} - dba-1 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 3 ) - dba-1 = {!!} - - dba : {i j : ℕ } → (i < 3 ) → ( j < 4 ) → Permutation 5 5 - dba i<3 j<4 = abc {!!} (dba-0 j<4 i<3 ) + record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where + field + dba0<3 : { i : ℕ } → i < 3 + dba1<4 : { i : ℕ } → i < 4 + aec0<3 : { i : ℕ } → i < 3 + aec1<4 : { i : ℕ } → i < 4 + abc= : abc i<3 j<4 =p= [ abc dba0<3 dba1<4 , abc aec0<3 aec1<4 ] - aec-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) - aec-0 = {!!} - aec-1 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 3 ) - aec-1 = {!!} - - aec : {i j : ℕ } → (i < 3 ) → ( j < 4 ) → Permutation 5 5 - aec i<3 j<4 = abc {!!} (aec-0 j<4 i<3 ) - - [dba,aec]=abc : {i j : ℕ } → (i<4 : i < 4 ) → (j<3 : j < 3 ) → [ dba j<3 i<4 , aec j<3 i<4 ] =p= abc {!!} i<4 - [dba,aec]=abc = {!!} + open Triple + + triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 + triple = {!!} - --- 2 ∷ 0 ∷ 1 ∷ [] abc - t10 : List (List ℕ ) - t10 = t101 (n≤ 3) (n≤ 4) [] where - t101 : { i j : ℕ } → i ≤ 3 → j ≤ 4 → List (List ℕ ) → List (List ℕ ) - t101 z≤n z≤n t = plist (abc z≤n z≤n) ∷ t - t101 z≤n (s≤s y) t = t101 (n≤ 3) (≤-trans y refl-≤s) ( plist (abc z≤n (s≤s y)) ∷ t ) - t101 (s≤s x) z≤n t = t101 (≤-trans x refl-≤s) z≤n ( plist (abc (s≤s x) z≤n) ∷ t ) - t101 (s≤s x) (s≤s y) t = t101 (≤-trans x refl-≤s) (s≤s y) ( plist (abc (s≤s x) (s≤s y)) ∷ t ) - -- t101 (s≤s x) z≤n t = t101 (≤-trans x ?) x ( abc (s≤s x) z≤n ∷ t ) - -- t101 (s≤s x) (s≤s y) t = {!!} - t12 = {!!} - --- 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] - --- 1 ∷ 0 ∷ 2 ∷ 3 ∷ 4 ∷ [] - --- 1 ∷ 2 ∷ 0 ∷ 3 ∷ 4 ∷ [] - --- 1 ∷ 2 ∷ 3 ∷ 0 ∷ 4 ∷ [] - --- 1 ∷ 2 ∷ 3 ∷ 4 ∷ 0 ∷ [] - - --- 2 ∷ 0 ∷ 1 ∷ 3 ∷ 4 ∷ [] abc (swap (pid {0}) ∘ₚ pins i<1 ) ∘ₚ pid - --- 3 ∷ 0 ∷ 2 ∷ 1 ∷ 4 ∷ [] abc pprep (swap (pid {0}) ∘ₚ pins i<1 ) ∘ₚ pid - --- 4 ∷ 0 ∷ 2 ∷ 3 ∷ 1 ∷ [] abc pprep (pprep (swap (pid {0}) ∘ₚ pins i<1 )) ∘ₚ pid - --- 3 ∷ 1 ∷ 0 ∷ 2 ∷ 4 ∷ [] abc - --- 4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] abc - --- 4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] abc - - --- 2 ∷ 0 ∷ 1 ∷ 3 ∷ 4 ∷ [] abc - --- 1 ∷ 3 ∷ 2 ∷ 0 ∷ 4 ∷ [] abd - -- 2 ∷ 1 ∷ 4 ∷ 3 ∷ 0 ∷ [] cea - - dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<3 : i < 3 ) → (j<4 : j < 4 ) → deriving n (abc {!!} j<4 ) + dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 ) dervie-any-3rot 0 i<3 j<4 = lift tt - dervie-any-3rot (suc i) i<3 j<4 = {!!} - -- ccong ( [dba,aec]=abc j<4 i<3 ) ( - -- comm {{!!}} {dba i<3 j<4} {aec i<3 j<4 } - -- ( dervie-any-3rot i (dba-1 j<4 i<3) (dba-0 j<4 i<3 ) ) - -- ( dervie-any-3rot i (aec-1 j<4 i<3) (aec-0 j<4 i<3 ) )) + dervie-any-3rot (suc i) i<3 j<4 = + ccong {deriving i} ( abc= (triple i<3 j<4 ) ) ( + comm {deriving i} {dba} {aec} + ( dervie-any-3rot i (dba0<3 tc) (dba1<4 tc) ) + ( dervie-any-3rot i (aec0<3 tc) (aec1<4 tc) )) where + tc : Triple i<3 j<4 + tc = triple i<3 j<4 + dba : Permutation 5 5 + dba = abc (dba0<3 tc) (dba1<4 tc) + aec : Permutation 5 5 + aec = abc (aec0<3 tc) (aec1<4 tc) open _=p=_ - counter-example : ¬ (abc {!!} 0<4 =p= pid ) - counter-example = {!!} + counter-example : ¬ (abc 0<3 0<4 =p= pid ) + counter-example p with peq p (# 1) + ... | () - --- 1 ∷ 0 ∷ 2 ∷ [] - --- 0 ∷ 2 ∷ 1 ∷ 3 ∷ [] - --- 1 ∷ 3 ∷ 2 ∷ 0 ∷ 4 ∷ [] - -- 2 ∷ 1 ∷ 3 ∷ 0 ∷ 4 ∷ [] (dba)⁻¹ = abd - dba99 : Permutation 5 5 - dba99 = pprep (pprep (pswap (pid {1}))) ∘ₚ pins (n≤ 3) - t1 = plist dba99 ∷ plist (pinv dba99) ∷ [] - -- 1 ∷ 0 ∷ [] - -- 0 ∷ 2 ∷ 1 ∷ [] - -- 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] - -- 2 ∷ 1 ∷ 4 ∷ 3 ∷ 0 ∷ [] - -- 4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] (aec)⁻¹ = cea - aec99 : Permutation 5 5 - aec99 = pprep (pprep (pprep (pswap (pid {0}))) ∘ₚ pins (n≤ 1)) ∘ₚ pins (n≤ 4) - tt2 = plist aec99 ∷ plist (pinv aec99) ∷ []