# HG changeset patch # User Shinji KONO # Date 1598370813 -32400 # Node ID 4b17a4daf2df7f38a83fb3bf6f0f1cf75f8ba717 # Parent 69ed81f8e2126614e6ac193f7ee946d89b812752 3rot diff -r 69ed81f8e212 -r 4b17a4daf2df Putil.agda --- a/Putil.agda Tue Aug 25 14:15:49 2020 +0900 +++ b/Putil.agda Wed Aug 26 00:53:33 2020 +0900 @@ -313,4 +313,4 @@ pls6 (suc n) = pls5 (suc n) (rev (pls6 n) ) [] -- rev to put id first pls : (n : ℕ ) → List (List ℕ ) -pls n = Data.List.map plist (all-perm n) where +pls n = Data.List.map plist (all-perm n) diff -r 69ed81f8e212 -r 4b17a4daf2df Solvable.agda --- a/Solvable.agda Tue Aug 25 14:15:49 2020 +0900 +++ b/Solvable.agda Wed Aug 26 00:53:33 2020 +0900 @@ -57,8 +57,8 @@ deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ ) deriving-inv {zero} {x} (lift tt) = lift tt deriving-inv {suc i} {ε} uni = ccong lemma3 uni -deriving-inv {suc i} {_} (comm x x₁ ) = ccong (lemma4 _ _) (comm x₁ x) where -deriving-inv {suc i} {_} (gen x x₁ ) = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where +deriving-inv {suc i} {_} (comm x x₁ ) = ccong (lemma4 _ _) (comm x₁ x) +deriving-inv {suc i} {_} (gen x x₁ ) = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix ) idcomtr : (g : Carrier ) → [ g , ε ] ≈ ε diff -r 69ed81f8e212 -r 4b17a4daf2df sym5.agda --- a/sym5.agda Tue Aug 25 14:15:49 2020 +0900 +++ b/sym5.agda Wed Aug 26 00:53:33 2020 +0900 @@ -3,10 +3,11 @@ module sym5 where open import Symmetric -open import Data.Unit +open import Data.Unit using (⊤ ; tt ) open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function +open import Function hiding (flip) open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Data.Nat.Properties open import Relation.Nullary open import Data.Empty open import Data.Product @@ -16,12 +17,13 @@ open import Solvable using (solvable) open import Relation.Binary.PropositionalEquality hiding ( [_] ) -open import Data.Fin hiding (_<_ ; lift ) +open import Data.Fin hiding (_<_ ; _≤_ ; lift ) open import Data.Fin.Permutation open import Data.List hiding ( [_] ) +open import nat ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) -¬sym5solvable sol = counter-example (end5 (abc 0<4 0<3 ) (dervie-any-3rot (dervied-length sol) 0<4 0<3 ) ) 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 @@ -37,47 +39,78 @@ end5 x der = end sol x der 0<4 : 0 < 4 - 0<4 = {!!} + 0<4 = s≤s z≤n 0<3 : 0 < 3 - 0<3 = {!!} + 0<3 = s≤s z≤n - --- 2 ∷ 0 ∷ 1 ∷ [] + --- 2 ∷ 0 ∷ 1 ∷ [] abc 3rot : Permutation 3 3 - 3rot = {!!} -- pswap (pid {0}) ∘ₚ pins (n≤ 1) + 3rot = pprep (pswap (pid {0}) ) ∘ₚ pins (n≤ 1) - abc : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → Permutation 5 5 - abc i<4 j<3 = {!!} -- (3rot ∘ₚ pins i<4 ) ∘ₚ pins j<3 + abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 + abc i<3 j<4 = (save2 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip save2 where + save2 : Permutation 5 5 + save2 = ( (pprep ( pid {4} ∘ₚ flip (pins 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 < 4 ) → ( j < 3 ) → Permutation 5 5 - dba i<4 j<3 = abc (dba-0 i<4 j<3 ) (dba-1 i<4 j<3 ) + dba : {i j : ℕ } → (i < 3 ) → ( j < 4 ) → Permutation 5 5 + dba i<3 j<4 = abc (dba-1 j<4 i<3 ) (dba-0 j<4 i<3 ) 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 < 4 ) → ( j < 3 ) → Permutation 5 5 - aec i<4 j<3 = abc (aec-0 i<4 j<3 ) (aec-1 i<4 j<3 ) + aec : {i j : ℕ } → (i < 3 ) → ( j < 4 ) → Permutation 5 5 + aec i<3 j<4 = abc (aec-1 j<4 i<3 ) (aec-0 j<4 i<3 ) - [dba,aec]=abc : {i j : ℕ } → (i<4 : i < 4 ) → (j<3 : j < 3 ) → [ dba i<4 j<3 , aec i<4 j<3 ] =p= abc i<4 j<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 j<3 i<4 [dba,aec]=abc = {!!} - dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<4 : i < 4 ) → (j<3 : j < 3 ) → deriving n (abc i<4 j<3 ) - dervie-any-3rot 0 i<4 j<3 = lift tt - dervie-any-3rot (suc i) i<4 j<3 = - ccong ( [dba,aec]=abc i<4 j<3 ) ( - comm {{!!}} {dba i<4 j<3} {aec i<4 j<3 } - ( dervie-any-3rot i (dba-0 i<4 j<3) (dba-1 i<4 j<3) ) - ( dervie-any-3rot i (aec-0 i<4 j<3) (aec-1 i<4 j<3) )) + --- 2 ∷ 0 ∷ 1 ∷ [] abc + t10 : List (List ℕ ) + t10 = t101 (n≤ 4) (n≤ 5) [] where + t101 : { i j : ℕ } → i ≤ 4 → j ≤ 5 → 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 y (≤-trans y refl-≤s) ( plist (abc z≤n (y)) ∷ t ) + t101 (s≤s x) z≤n t = t101 (≤-trans x refl-≤s) z≤n ( plist (abc (x) z≤n) ∷ t ) + t101 (s≤s x) (s≤s y) t = t101 (≤-trans x refl-≤s) (s≤s y) ( plist (abc (x) 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 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 ) )) open _=p=_ - counter-example : ¬ (abc 0<4 0<3 =p= pid ) + counter-example : ¬ (abc 0<3 0<4 =p= pid ) counter-example = {!!}