Mercurial > hg > Members > kono > Proof > galois
changeset 70:32004c9a70b1
sym2 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Aug 2020 22:37:21 +0900 |
| parents | fb1ccedf5853 |
| children | da1677fae9ac |
| files | Solvable.agda Symmetric.agda sym2.agda sym3.agda sym5.agda |
| diffstat | 5 files changed, 196 insertions(+), 80 deletions(-) [+] |
line wrap: on
line diff
--- a/Solvable.agda Mon Aug 24 20:01:18 2020 +0900 +++ b/Solvable.agda Mon Aug 24 22:37:21 2020 +0900 @@ -9,7 +9,7 @@ open import Relation.Nullary open import Data.Empty open import Data.Product -open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) open Group G @@ -61,3 +61,20 @@ deriving-inv {suc i} {_} (gen x x₁ ) = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix ) +idcomtr : (g : Carrier ) → [ g , ε ] ≈ ε +idcomtr g = begin + (g ⁻¹ ∙ ε ⁻¹ ∙ g ∙ ε ) ≈⟨ ∙-cong (∙-cong (∙-cong grefl (sym lemma3 )) grefl ) grefl ⟩ + (g ⁻¹ ∙ ε ∙ g ∙ ε ) ≈⟨ ∙-cong (∙-cong (proj₂ identity _) grefl) grefl ⟩ + (g ⁻¹ ∙ g ∙ ε ) ≈⟨ ∙-cong (proj₁ inverse _ ) grefl ⟩ + ( ε ∙ ε ) ≈⟨ proj₂ identity _ ⟩ + ε + ∎ where open EqReasoning (Algebra.Group.setoid G) + +idcomtl : (g : Carrier ) → [ ε , g ] ≈ ε +idcomtl g = begin + (ε ⁻¹ ∙ g ⁻¹ ∙ ε ∙ g ) ≈⟨ ∙-cong (proj₂ identity _) grefl ⟩ + (ε ⁻¹ ∙ g ⁻¹ ∙ g ) ≈⟨ ∙-cong (∙-cong (sym lemma3 ) grefl ) grefl ⟩ + (ε ∙ g ⁻¹ ∙ g ) ≈⟨ ∙-cong (proj₁ identity _) grefl ⟩ + (g ⁻¹ ∙ g ) ≈⟨ proj₁ inverse _ ⟩ + ε + ∎ where open EqReasoning (Algebra.Group.setoid G)
--- a/Symmetric.agda Mon Aug 24 20:01:18 2020 +0900 +++ b/Symmetric.agda Mon Aug 24 22:37:21 2020 +0900 @@ -43,6 +43,17 @@ ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y → y =p= z → x =p= z peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q) +peqˡ : {p : ℕ }{ x y : Permutation p p } → x =p= y → (q : Fin p) → x ⟨$⟩ˡ q ≡ y ⟨$⟩ˡ q +peqˡ {p} {x} {y} eq q = begin + x ⟨$⟩ˡ q + ≡⟨ sym ( inverseˡ y ) ⟩ + y ⟨$⟩ˡ (y ⟨$⟩ʳ ( x ⟨$⟩ˡ q )) + ≡⟨ cong (λ k → y ⟨$⟩ˡ k ) (sym (peq eq _ )) ⟩ + y ⟨$⟩ˡ (x ⟨$⟩ʳ ( x ⟨$⟩ˡ q )) + ≡⟨ cong (λ k → y ⟨$⟩ˡ k ) ( inverseʳ x ) ⟩ + y ⟨$⟩ˡ q + ∎ where open ≡-Reasoning + Symmetric : ℕ → Group Level.zero Level.zero Symmetric p = record { Carrier = Permutation p p
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/sym2.agda Mon Aug 24 22:37:21 2020 +0900 @@ -0,0 +1,125 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym2 where + +open import Symmetric +open import Data.Unit +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin +open import Data.Fin.Permutation + +sym2solvable : solvable (Symmetric 2) +solvable.dervied-length sym2solvable = 1 +solvable.end sym2solvable x d = solved x d where + + open import Data.List using ( List ; [] ; _∷_ ) + + open Solvable (Symmetric 2) + -- open Group (Symmetric 2) using (_⁻¹) + + p0 : FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid + p0 = record { peq = p00 } where + p00 : (q : Fin 2) → (FL→perm ((# 0) :: ((# 0) :: f0)) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) + p00 zero = refl + p00 (suc zero) = refl + + p1 : Permutation 2 2 + p1 = FL→perm ((# 1) :: ((# 0 ) :: f0)) + + p1rev : (p1 ∘ₚ p1 ) =p= pid + p1rev = record { peq = p01 } where + p01 : (q : Fin 2) → ((p1 ∘ₚ p1) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) + p01 zero = refl + p01 (suc zero) = refl + + open _=p=_ + + sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) + sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g + sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} = begin + [ g , h ] ⟨$⟩ʳ q + ≡⟨⟩ + h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ cong (λ k → h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ k))) ((peqˡ sym2lem1 _ )) ⟩ + h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) + ≡⟨ cong (λ k → h ⟨$⟩ʳ k ) (peq sym2lem1 _ ) ⟩ + h ⟨$⟩ʳ (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) + ≡⟨⟩ + [ pid , h ] ⟨$⟩ʳ q + ≡⟨ peq (idcomtl h) q ⟩ + q + ∎ where + open ≡-Reasoning + postulate sym2lem1 : g =p= pid + -- it works but very slow + -- sym2lem1 = ptrans (psym ( FL←iso g )) (subst (λ k → FL→perm k =p= pid) (sym g=00) p0 ) + sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} = begin + [ g , h ] ⟨$⟩ʳ q + ≡⟨⟩ + h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ peq sym2lem2 _ ⟩ + pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ cong (λ k → pid ⟨$⟩ʳ (g ⟨$⟩ʳ k)) ((peqˡ sym2lem2 _ )) ⟩ + pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨⟩ + [ g , pid ] ⟨$⟩ʳ q + ≡⟨ peq (idcomtr g) q ⟩ + q + ∎ where + open ≡-Reasoning + postulate sym2lem2 : h =p= pid + sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | _ = begin + [ g , h ] ⟨$⟩ʳ q + ≡⟨⟩ + h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ peq sym2lem3 _ ⟩ + pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )) + ≡⟨ cong (λ k → pid ⟨$⟩ʳ k) (peq sym2lem4 _ )⟩ + pid ⟨$⟩ʳ ( pid ⟨$⟩ˡ q ) + ≡⟨⟩ + q + ∎ where + open ≡-Reasoning + postulate + sym2lem3 : (g ∘ₚ h ) =p= pid + sym2lem4 : (pinv g ∘ₚ pinv h ) =p= pid + solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid + solved x uni = prefl + solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h } + solved x (gen {f} {g} d d₁) with solved f d | solved g d₁ + ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where + genlem : ( q : Fin 2 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q + genlem q = begin + g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) + ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩ + f ⟨$⟩ʳ q + ≡⟨ f=e q ⟩ + q + ∎ where open ≡-Reasoning + solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d + ... | record { peq = f=e } = record { peq = λ q → cc q } where + cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q + cc q = begin + x ⟨$⟩ʳ q + ≡⟨ sym (f=g q) ⟩ + f ⟨$⟩ʳ q + ≡⟨ f=e q ⟩ + q + ∎ where open ≡-Reasoning + +-- ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) +-- ¬sym5solvable sol = {!!} + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/sym3.agda Mon Aug 24 22:37:21 2020 +0900 @@ -0,0 +1,41 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym3 where + +open import Symmetric +open import Data.Unit +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin +open import Data.Fin.Permutation + +sym3solvable : solvable (Symmetric 3) +solvable.dervied-length sym3solvable = 2 +solvable.end sym3solvable x d = solved1 x d where + + open import Data.List using ( List ; [] ; _∷_ ) + + open Solvable (Symmetric 3) + -- open Group (Symmetric 2) using (_⁻¹) + + p0 : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid + p0 = record { peq = p00 } where + p00 : (q : Fin 3) → (FL→perm ((# 0) :: ((# 0) :: ((# 0) :: f0))) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) + p00 zero = refl + p00 (suc zero) = refl + p00 (suc (suc zero)) = refl + + open _=p=_ + + solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid + solved1 = {!!}
--- a/sym5.agda Mon Aug 24 20:01:18 2020 +0900 +++ b/sym5.agda Mon Aug 24 22:37:21 2020 +0900 @@ -1,6 +1,6 @@ open import Level hiding ( suc ; zero ) open import Algebra -module sym5 where +module sym3 where open import Symmetric open import Data.Unit @@ -19,83 +19,5 @@ open import Data.Fin open import Data.Fin.Permutation -sym4solvable : solvable (Symmetric 2) -solvable.dervied-length sym4solvable = 1 -solvable.end sym4solvable x d = solved x d where - - open Solvable (Symmetric 2) - -- open Group (Symmetric 2) using (_⁻¹) - - f2-⊥ : (x : Fin 2 ) → x ≡ zero → x ≡ suc zero → ⊥ - f2-⊥ x refl () - s2 : ( g : Permutation 2 2 ) → g =p= pinv g - s2 g = record { peq = λ q → s2lem q } where - s2lem : (q : Fin 2) → (g ⟨$⟩ʳ q) ≡ (pinv g ⟨$⟩ʳ q) - s2lem zero with g ⟨$⟩ʳ zero | inspect (_⟨$⟩ʳ_ g ) zero - s2lem zero | zero | record { eq = e1 } = begin - zero - ≡⟨ sym (inverseˡ g ) ⟩ - g ⟨$⟩ˡ ( g ⟨$⟩ʳ zero ) - ≡⟨ cong ( λ k → g ⟨$⟩ˡ k ) e1 ⟩ - g ⟨$⟩ˡ zero - ≡⟨⟩ - pinv g ⟨$⟩ʳ zero - ∎ where open ≡-Reasoning - s2lem zero | suc zero | record { eq = e2 } = sym shlem1 where - shlem1 : pinv g ⟨$⟩ʳ zero ≡ suc zero - shlem1 with g ⟨$⟩ˡ zero | inspect (_⟨$⟩ˡ_ g ) zero | inverseʳ g {zero} - shlem1 | zero | record { eq = e1 } | u = ⊥-elim (f2-⊥ _ u e2 ) - shlem1 | suc zero | s | u = refl - s2lem (suc zero) with g ⟨$⟩ʳ suc zero | inspect (_⟨$⟩ʳ_ g ) (suc zero) - s2lem (suc zero) | zero | record { eq = e1 } = sym shlem2 where - shlem2 : pinv g ⟨$⟩ʳ suc zero ≡ zero - shlem2 with g ⟨$⟩ˡ suc zero | inspect (_⟨$⟩ˡ_ g ) (suc zero ) | inverseʳ g {suc zero} - shlem2 | suc zero | record { eq = e2 } | u = ⊥-elim (f2-⊥ _ e1 u ) - shlem2 | zero | s | u = refl - s2lem (suc zero) | suc zero | record { eq = e2 } = begin - suc zero - ≡⟨ sym (inverseˡ g ) ⟩ - g ⟨$⟩ˡ ( g ⟨$⟩ʳ suc zero ) - ≡⟨ cong ( λ k → g ⟨$⟩ˡ k ) e2 ⟩ - pinv g ⟨$⟩ʳ suc zero - ∎ where open ≡-Reasoning - - sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) - sym2lem0 g h q = begin - [ g , h ] ⟨$⟩ʳ q - ≡⟨⟩ - h ⟨$⟩ʳ ( g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ {!!} ⟩ - q - ≡⟨⟩ - pid ⟨$⟩ʳ q - ∎ where open ≡-Reasoning - solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid - solved x uni = prefl - solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h } - solved x (gen {f} {g} d d₁) with solved f d | solved g d₁ - ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where - genlem : ( q : Fin 2 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q - genlem q = begin - g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) - ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩ - f ⟨$⟩ʳ q - ≡⟨ f=e q ⟩ - q - ∎ where open ≡-Reasoning - solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d - ... | record { peq = f=e } = record { peq = λ q → cc q } where - cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q - cc q = begin - x ⟨$⟩ʳ q - ≡⟨ sym (f=g q) ⟩ - f ⟨$⟩ʳ q - ≡⟨ f=e q ⟩ - q - ∎ where open ≡-Reasoning - ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) ¬sym5solvable sol = {!!} - - -