Mercurial > hg > Members > kono > Proof > galois
changeset 112:43731a549950
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 02 Sep 2020 11:29:04 +0900 |
| parents | d3da6e2c0d90 |
| children | d8a21c5db0e0 |
| files | Putil.agda nat.agda sym5.agda |
| diffstat | 3 files changed, 141 insertions(+), 41 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Tue Sep 01 21:58:15 2020 +0900 +++ b/Putil.agda Wed Sep 02 11:29:04 2020 +0900 @@ -4,8 +4,8 @@ open import Level hiding ( suc ; zero ) open import Algebra open import Algebra.Structures -open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ) -open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ) renaming ( <-cmp to <-fcmp ) +open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) +open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) open import Data.Fin.Permutation open import Function hiding (id ; flip) open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) @@ -370,6 +370,12 @@ pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) pleq2 = headeq eq +is-=p= : {n : ℕ} → (x y : Permutation n n ) → Dec (x =p= y ) +is-=p= {zero} x y = yes record { peq = λ () } +is-=p= {suc n} x y with ℕL-eq? (plist0 x ) ( plist0 y ) +... | yes t = yes (pleq x y t) +... | no t = no ( contra-position (←pleq x y) t ) + pprep-cong : {n : ℕ} → {x y : Permutation n n } → x =p= y → pprep x =p= pprep y pprep-cong {n} {x} {y} x=y = record { peq = pprep-cong1 } where pprep-cong1 : (q : Fin (suc n)) → (pprep x ⟨$⟩ʳ q) ≡ (pprep y ⟨$⟩ʳ q)
--- a/nat.agda Tue Sep 01 21:58:15 2020 +0900 +++ b/nat.agda Wed Sep 02 11:29:04 2020 +0900 @@ -311,3 +311,21 @@ suc (suc k * suc m) ∎ where open ≤-Reasoning open ≡-Reasoning + +open import Data.List + +ℕL-inject : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → h ≡ h1 +ℕL-inject refl = refl + +ℕL-inject-t : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → x ≡ y +ℕL-inject-t refl = refl + +ℕL-eq? : (x y : List ℕ ) → Dec (x ≡ y ) +ℕL-eq? [] [] = yes refl +ℕL-eq? [] (x ∷ y) = no (λ ()) +ℕL-eq? (x ∷ x₁) [] = no (λ ()) +ℕL-eq? (h ∷ x) (h1 ∷ y) with h ≟ h1 | ℕL-eq? x y +... | yes y1 | yes y2 = yes ( cong₂ (λ j k → j ∷ k ) y1 y2 ) +... | yes y1 | no n = no (λ e → n (ℕL-inject-t e)) +... | no n | t = no (λ e → n (ℕL-inject e)) +
--- a/sym5.agda Tue Sep 01 21:58:15 2020 +0900 +++ b/sym5.agda Wed Sep 02 11:29:04 2020 +0900 @@ -26,6 +26,7 @@ open _∧_ +{-# TERMINATING #-} ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (proj1 (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) )) where @@ -37,8 +38,10 @@ -- (abd)(cea)(dba)(aec) -- + open ≡-Reasoning + open solvable - open Solvable (Symmetric 5) + open Solvable ( Symmetric 5) end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid end5 x der = end sol x der @@ -58,6 +61,28 @@ ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) + ins2cong : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → ins2 x i<3 j<4 =p= ins2 y i<3 j<4 + ins2cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )} + (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl + + open _=p=_ + -- ins2distr : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → ins2 (x ∘ₚ y) i<3 j<4 =p= (ins2 x i<3 j<4 ∘ₚ ins2 y i<3 j<4) + -- ins2distr {i} {j} {x} {y} {i<3} {j<4} = record { peq = λ q → + -- ins2 (x ∘ₚ y) i<3 j<4 ⟨$⟩ʳ q + -- ≡⟨⟩ + -- ((save2 i<3 j<4 ∘ₚ (pprep (pprep (x ∘ₚ y)))) ∘ₚ flip (save2 i<3 j<4 )) ⟨$⟩ʳ q + -- ≡⟨ peq ( presp prefl ( presp (ptrans (pprep-cong pprep-dist) pprep-dist ) prefl )) q ⟩ + -- (((save2 i<3 j<4 ∘ₚ (pprep (pprep x))) ∘ₚ (pprep (pprep y))) ∘ₚ flip (save2 i<3 j<4 )) ⟨$⟩ʳ q + -- ≡⟨ peq (presp prefl (presp (psym ( record { peq = λ q → inverseˡ (save2 i<3 j<4) } )) prefl )) q ⟩ + -- (((save2 i<3 j<4 ∘ₚ (pprep (pprep x))) ∘ₚ ((flip (save2 i<3 j<4 ) ∘ₚ + -- save2 i<3 j<4 ) ∘ₚ (pprep (pprep y)))) ∘ₚ flip (save2 i<3 j<4 )) ⟨$⟩ʳ q + -- ≡⟨⟩ + -- (((save2 i<3 j<4 ∘ₚ (pprep (pprep x))) ∘ₚ flip (save2 i<3 j<4 )) ∘ₚ + -- ((save2 i<3 j<4 ∘ₚ (pprep (pprep y))) ∘ₚ flip (save2 i<3 j<4 ))) ⟨$⟩ʳ q + -- ≡⟨⟩ + -- (ins2 x i<3 j<4 ∘ₚ ins2 y i<3 j<4) ⟨$⟩ʳ q + -- ∎ } + abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 abc i<3 j<4 = ins2 3rot i<3 j<4 @@ -66,14 +91,12 @@ 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 = ? - - 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 = ? + -- 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 ⁻¹ + -- abc→dba i<3 j<4 = psym ins2distr + -- 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 ⁻¹ + -- dba→aec i<3 j<4 = psym ins2distr + -- 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 ⁻¹ + -- aec→abc i<3 j<4 = psym ins2distr record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where field @@ -106,45 +129,98 @@ triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } 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 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + + _⁻¹ : {n : ℕ } ( x : Permutation n n) → Permutation n n + _⁻¹ = pinv + -- abc0 = abc z≤n z≤n -- _ _ * * * + -- dba0 = dba z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) -- _ * * * _ + -- aec0 = aec (s≤s (s≤s z≤n)) z≤n -- _ * * _ * + + -- abc1 = abc (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) -- _ * * * _ + -- dba1 = dba z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) -- _ * * * _ + -- aec1 = aec z≤n (s≤s z≤n) + + -- t0 = plist abc0 ∷ plist dba0 ∷ plist aec0 ∷ plist [ dba0 , aec0 ] ∷ [] + -- t1 = plist aec0 ∷ plist abc0 ∷ plist dba0 ∷ plist [ aec1 , abc1 ⁻¹ ] ∷ [] + -- tt0 : (i : Fin 4) (j : Fin 5) → (x : Fin 5) (y : Fin 4) → (rot : Permutation 3 3 ) → List (List ℕ) + -- tt0 i j x y rot = + -- plist (ins2 rot (fin≤n i) (fin≤n j)) ∷ + -- plist [ ins2 (rot ∘ₚ rot) (fin≤n i) (fin≤n x) , ins2 (pinv rot) (fin≤n y) (fin≤n j) ] ∷ [] + + tt5 : (i : Fin 4) (j : Fin 5) → (x : Fin 5) (y : Fin 4) → (rot : Permutation 3 3 ) → List (List ℕ) → List (List ℕ) + tt5 i j x y rot t with is-=p= (ins2 rot (fin≤n i) (fin≤n j)) + [ ins2 (rot ∘ₚ rot) (fin≤n i) (fin≤n x) , ins2 (pinv rot) (fin≤n y) (fin≤n j) ] + ... | yes _ = ( toℕ x ∷ toℕ y ∷ [] ) ∷ t + ... | no _ = t + + open import Relation.Binary.Definitions + + tt2 : (i : Fin 4) (j : Fin 5) → (rot : Permutation 3 3 ) → List (List ℕ) + tt2 i j rot = tt3 (# 3) (# 4) [] where + tt3 : (x : Fin 4) (y : Fin 5) → List (List ℕ) → List (List ℕ) + tt3 zero zero t = t + tt3 zero (suc y) t = tt3 (# 3) (fin+1 y) (( tt5 i j (suc y) zero rot [] ) ++ t) + tt3 (suc x) y t = tt3 (fin+1 x) y (( tt5 i j y (suc x) rot [] ) ++ t) + + -- tt1 = tt0 (# 0) (# 0) (# 4) (# 2) 3rot ∷ + -- tt0 (# 0) (# 1) (# 4) (# 2) 3rot ∷ + -- tt0 (# 0) (# 2) (# 0) (# 3) 3rot ∷ + -- [] + + tt4 = tt2 (# 0) (# 0) (3rot ∘ₚ 3rot ) ∷ + tt2 (# 1) (# 0) (3rot ∘ₚ 3rot ) ∷ + tt2 (# 2) (# 0) (3rot ∘ₚ 3rot ) ∷ + tt2 (# 3) (# 0) (3rot ∘ₚ 3rot ) ∷ + tt2 (# 0) (# 1) (3rot ∘ₚ 3rot ) ∷ + [] + + + --- 1 = [ 2 , -1 ] = ((dba ⁻¹ ∘ₚ aec ⁻¹ ) ∘ₚ dba ) ∘ₚ aec ) = -1 1 2 -1 = 1 + --- dba = abc ∘ₚ 2 = [ 1 , -1 ] = ((aec ⁻¹ ∘ₚ abc ⁻¹ ) ∘ₚ aec ) ∘ₚ dab ) = 1 2 -1 1 2 + --- aec = dba ∘ₚ -1 = [ 1 , 2 ] = ((abc ⁻¹ ∘ₚ dba ⁻¹ ) ∘ₚ abc ) ∘ₚ dba ) = 2 1 1 2 + + open Triple dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot ) - dba-triple = ? + dba-triple = {!!} + -- dba-triple z≤n z≤n = {!!} -- record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ {!!} } aec-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (pinv 3rot ) - aec-triple = ? + aec-triple = {!!} + -- aec-triple z≤n z≤n = {!!} -- record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ {!!} } dervie-any-3rot : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 ) ∧ deriving n (dba i<3 j<4 ) ∧ deriving n (aec i<3 j<4 ) dervie-any-3rot 0 i<3 j<4 = ⟪ lift tt , ⟪ lift tt , lift tt ⟫ ⟫ - dervie-any-3rot (suc i) i<3 j<4 = ⟪ d0 , ⟪ d1 , d2 ⟫ ⟫ where - tc : Triple i<3 j<4 3rot - tc = triple i<3 j<4 - abc0 = abc i<3 j<4 - b<3 = fin≤n {3} (dba0<3 tc) - b<4 = fin≤n {4} (dba1<4 tc) - dba0 = dba b<3 b<4 - c<3 = fin≤n {3} (aec0<3 tc) - c<4 = fin≤n {4} (aec1<4 tc) - aec0 = aec c<3 c<4 - d0 : deriving (suc i) (abc i<3 j<4) - d0 = - ccong {deriving i} ( psym (abc= tc )) ( - comm {deriving i} {dba0} {aec0} - (proj1 (proj2 ( dervie-any-3rot i b<3 b<4))) - (proj2 (proj2 ( dervie-any-3rot i c<3 c<4 )))) - d1 : deriving (suc i) (dba i<3 j<4) - d1 = - ccong {deriving i} ( psym {!!}) ( -- dba i<3 j<4 =p= [ aec0 , abc0 ] -- dba= : dba b<3 b<4 =p= [ aec0 , abc0 ] is not enough... - comm {deriving i} {aec0} {abc0} - (proj2 (proj2 ( dervie-any-3rot i c<3 c<4 ))) - (proj1 ( dervie-any-3rot i i<3 j<4 ))) - d2 : deriving (suc i) (aec i<3 j<4) - d2 = - ccong {deriving i} ( psym {!!}) ( - comm {deriving i} {abc0} {dba0} - (proj1 ( dervie-any-3rot i i<3 j<4 )) - (proj1 (proj2 ( dervie-any-3rot i b<3 b<4 ) ))) + dervie-any-3rot (suc i) i<3 j<4 = {!!} -- ⟪ d0 , ⟪ d1 , d2 ⟫ ⟫ where + -- tc : Triple i<3 j<4 3rot + -- tc = triple i<3 j<4 + -- abc0 = abc i<3 j<4 + -- b<3 = fin≤n {3} (dba0<3 tc) + -- b<4 = fin≤n {4} (dba1<4 tc) + -- dba0 = dba b<3 b<4 + -- c<3 = fin≤n {3} (aec0<3 tc) + -- c<4 = fin≤n {4} (aec1<4 tc) + -- aec0 = aec c<3 c<4 + -- d0 : deriving (suc i) (abc i<3 j<4) + -- d0 = + -- ccong {deriving i} ( psym (abc= tc )) ( + -- comm {deriving i} {dba0} {aec0} + -- (proj1 (proj2 ( dervie-any-3rot i b<3 b<4))) + -- (proj2 (proj2 ( dervie-any-3rot i c<3 c<4 )))) + -- d1 : deriving (suc i) (dba i<3 j<4) + -- d1 = + -- ccong {deriving i} ( psym {!!}) ( -- dba i<3 j<4 =p= [ aec0 , abc0 ] -- dba= : dba b<3 b<4 =p= [ aec0 , abc0 ] is not enough... + -- comm {deriving i} {aec0} {abc0} + -- (proj2 (proj2 ( dervie-any-3rot i c<3 c<4 ))) + -- (proj1 ( dervie-any-3rot i i<3 j<4 ))) + -- d2 : deriving (suc i) (aec i<3 j<4) + -- d2 = + -- ccong {deriving i} ( psym {!!}) ( + -- comm {deriving i} {abc0} {dba0} + -- (proj1 ( dervie-any-3rot i i<3 j<4 )) + -- (proj1 (proj2 ( dervie-any-3rot i b<3 b<4 ) ))) open _=p=_ counter-example : ¬ (abc 0<3 0<4 =p= pid )