Mercurial > hg > Members > kono > Proof > galois
changeset 87:c68956f6c3ad
tc fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Aug 2020 11:44:58 +0900 |
| parents | c5329963c583 |
| children | 405c1f727ffe |
| files | Gutil.agda Putil.agda Symmetric.agda sym5.agda |
| diffstat | 4 files changed, 122 insertions(+), 94 deletions(-) [+] |
line wrap: on
line diff
--- a/Gutil.agda Thu Aug 27 08:29:56 2020 +0900 +++ b/Gutil.agda Thu Aug 27 11:44:58 2020 +0900 @@ -102,6 +102,12 @@ mpf p (mpf q (mpf r ε)) ∎ where open EqReasoning (Algebra.Group.setoid G) +grepl : { x y0 y1 z : Carrier } → x ∙ y0 ≈ y1 → x ∙ ( y0 ∙ z ) ≈ y1 ∙ z +grepl eq = gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl ) + +grm : { x y0 y1 z : Carrier } → x ∙ y0 ≈ ε → x ∙ ( y0 ∙ z ) ≈ z +grm eq = gtrans ( gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )) ( proj₁ identity _ ) + -- ∙-flattenl : {x : Carrier } → (m : MP x ) → x ≈ mp-flattenl m -- ∙-flattenl (am x) = gsym (proj₂ identity _) -- ∙-flattenl (q o am x) with ∙-flattenl q -- x₁ ∙ x ≈ mpl q (am x o am ε) , t : x₁ ≈ mpl q (am ε)
--- a/Putil.agda Thu Aug 27 08:29:56 2020 +0900 +++ b/Putil.agda Thu Aug 27 11:44:58 2020 +0900 @@ -210,28 +210,47 @@ pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) pleq2 = headeq eq -pprep-cong : {n : ℕ} → (x y : Permutation n n ) → x =p= y → pprep x =p= pprep y -pprep-cong {n} x y x=y = {!!} where - pprep-cong02 : (x : Permutation 1 1 ) → (q : Fin 1) → (x ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) - pprep-cong02 x zero with x ⟨$⟩ʳ zero | inspect (_⟨$⟩ʳ_ x) zero - ... | zero | record { eq = e } = refl - pprep-cong01 : (x : Permutation 1 1 ) → x =p= pid - pprep-cong01 x = record { peq = pprep-cong02 x } - pprep-cong0 : (n : ℕ) → (x : Permutation (suc n) (suc n) ) → toℕ (x ⟨$⟩ʳ fromℕ< a<sa ) ≡ n - pprep-cong0 zero x = begin - toℕ (x ⟨$⟩ʳ fromℕ< a<sa) - ≡⟨⟩ - toℕ (x ⟨$⟩ʳ zero) - ≡⟨ cong (λ k → toℕ k) (pprep-cong02 x zero) ⟩ - toℕ {suc zero} zero - ≡⟨⟩ - zero - ∎ where open ≡-Reasoning - pprep-cong0 (suc n) x = {!!} - t1 = plist0 (pprep (pid {3})) - pprep-cong1 : (n : ℕ) → (x : Permutation n n ) → plist0 (pprep x) ≡ n ∷ plist0 x - pprep-cong1 zero x = refl - pprep-cong1 (suc n) x = {!!} +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) + pprep-cong1 zero = refl + pprep-cong1 (suc q) = begin + pprep x ⟨$⟩ʳ suc q + ≡⟨⟩ + suc ( x ⟨$⟩ʳ q ) + ≡⟨ cong ( λ k → suc k ) ( peq x=y q ) ⟩ + suc ( y ⟨$⟩ʳ q ) + ≡⟨⟩ + pprep y ⟨$⟩ʳ suc q + ∎ where open ≡-Reasoning + +pprep-dist : {n : ℕ} → {x y : Permutation n n } → pprep (x ∘ₚ y) =p= (pprep x ∘ₚ pprep y) +pprep-dist {n} {x} {y} = record { peq = pprep-dist1 } where + pprep-dist1 : (q : Fin (suc n)) → (pprep (x ∘ₚ y) ⟨$⟩ʳ q) ≡ ((pprep x ∘ₚ pprep y) ⟨$⟩ʳ q) + pprep-dist1 zero = refl + pprep-dist1 (suc q) = cong ( λ k → suc k ) refl + +pswap-cong : {n : ℕ} → {x y : Permutation n n } → x =p= y → pswap x =p= pswap y +pswap-cong {n} {x} {y} x=y = record { peq = pswap-cong1 } where + pswap-cong1 : (q : Fin (suc (suc n))) → (pswap x ⟨$⟩ʳ q) ≡ (pswap y ⟨$⟩ʳ q) + pswap-cong1 zero = refl + pswap-cong1 (suc zero) = refl + pswap-cong1 (suc (suc q)) = begin + pswap x ⟨$⟩ʳ suc (suc q) + ≡⟨⟩ + suc (suc (x ⟨$⟩ʳ q)) + ≡⟨ cong ( λ k → suc (suc k) ) ( peq x=y q ) ⟩ + suc (suc (y ⟨$⟩ʳ q)) + ≡⟨⟩ + pswap y ⟨$⟩ʳ suc (suc q) + ∎ where open ≡-Reasoning + +pswap-dist : {n : ℕ} → {x y : Permutation n n } → pprep (pprep (x ∘ₚ y)) =p= (pswap x ∘ₚ pswap y) +pswap-dist {n} {x} {y} = record { peq = pswap-dist1 } where + pswap-dist1 : (q : Fin (suc (suc n))) → ((pprep (pprep (x ∘ₚ y))) ⟨$⟩ʳ q) ≡ ((pswap x ∘ₚ pswap y) ⟨$⟩ʳ q) + pswap-dist1 zero = refl + pswap-dist1 (suc zero) = refl + pswap-dist1 (suc (suc q)) = cong ( λ k → suc (suc k) ) refl data FL : (n : ℕ )→ Set where f0 : FL 0
--- a/Symmetric.agda Thu Aug 27 08:29:56 2020 +0900 +++ b/Symmetric.agda Thu Aug 27 11:44:58 2020 +0900 @@ -54,6 +54,20 @@ y ⟨$⟩ˡ q ∎ where open ≡-Reasoning +presp : { p : ℕ } {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v) +presp {p} {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where + lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q) + lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ ) +passoc : { p : ℕ } (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p= (x ∘ₚ (y ∘ₚ z)) +passoc x y z = record { peq = λ q → refl } +p-inv : { p : ℕ } {i j : Permutation p p} → i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q +p-inv {p} {i} {j} i=j q = begin + i ⟨$⟩ˡ q ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j) ) ⟩ + i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (peq i=j _ )) ⟩ + i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i ⟩ + j ⟨$⟩ˡ q + ∎ where open ≡-Reasoning + Symmetric : ℕ → Group Level.zero Level.zero Symmetric p = record { Carrier = Permutation p p @@ -69,18 +83,5 @@ ; inverse = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} )) ; ⁻¹-cong = λ i=j → record { peq = λ q → p-inv i=j q } } - } where - presp : {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v) - presp {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where - lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q) - lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ ) - passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p= (x ∘ₚ (y ∘ₚ z)) - passoc x y z = record { peq = λ q → refl } - p-inv : {i j : Permutation p p} → i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q - p-inv {i} {j} i=j q = begin - i ⟨$⟩ˡ q ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j) ) ⟩ - i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (peq i=j _ )) ⟩ - i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i ⟩ - j ⟨$⟩ˡ q - ∎ where open ≡-Reasoning + }
--- a/sym5.agda Thu Aug 27 08:29:56 2020 +0900 +++ b/sym5.agda Thu Aug 27 11:44:58 2020 +0900 @@ -70,62 +70,41 @@ 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 - ∎ + S = Symmetric 5 + open Group (Symmetric 5) + postulate lemma : (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p= dba i<3 j<4 + -- some kind of functional extentionaly required? + -- 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 )) + -- ≈⟨ ∙-flatten (Symmetric 5) (((am (save2 i<3 j<4) o am (pprep (pprep 3rot))) o am (flip (save2 i<3 j<4 ))) o + -- ((am (save2 i<3 j<4) o am (pprep (pprep 3rot))) o am ( 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 ) ∘ₚ pid ))))) + -- ≈⟨ ∙-cong prefl ( ∙-cong prefl (grm S (proj₁ inverse _))) ⟩ + -- save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ pid ))) + -- ≈⟨ ∙-cong prefl (grepl S (pprep-cong prefl ) ) ⟩ + -- (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 = {!!} + postulate -- someday + 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 + 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 : {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 + record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where field 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) ] - - 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 ] - ∎ - - 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= = {!!} + abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (pinv rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] open Triple - triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 + triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot 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 } triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } @@ -148,21 +127,44 @@ 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 } + dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot ) + dba-triple = ? + + aec-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (pinv 3rot ) + aec-triple = ? + 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 = {!!} - -- ccong {deriving i} ( abc= (triple i<3 j<4 ) ) ( - -- comm {deriving i} {dba} {aec} - -- ( dervie-any-3rot i (fin<n {3} {dba0<3 tc}) (fin<n {4} {dba1<4 tc}) ) - -- ( dervie-any-3rot i (fin<n {3} {aec0<3 tc}) (fin<n {4} {aec1<4 tc}) )) where - -- tc : Triple i<3 j<4 - -- tc = triple i<3 j<4 - -- dba : Permutation 5 5 - -- dba = abc (fin<n {3} {dba0<3 tc}) (fin<n {4} {dba1<4 tc}) - -- aec : Permutation 5 5 - -- aec = abc (fin<n {3} {aec0<3 tc}) (fin<n {4} {aec1<4 tc}) + 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 )