Mercurial > hg > Members > kono > Proof > galois
changeset 88:405c1f727ffe
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 28 Aug 2020 11:05:45 +0900 |
| parents | c68956f6c3ad |
| children | dcb4450680ab |
| files | Putil.agda sym2.agda sym3.agda sym4.agda |
| diffstat | 4 files changed, 157 insertions(+), 49 deletions(-) [+] |
line wrap: on
line diff
--- a/Putil.agda Thu Aug 27 11:44:58 2020 +0900 +++ b/Putil.agda Fri Aug 28 11:05:45 2020 +0900 @@ -29,13 +29,10 @@ -- Todo -- --- complete perm→FL --- describe property of pprep and pswap -- describe property of pins ( move 0 to any position) -- describe property of shrink ( remove one column ) -- prove FL→iso -- prove FL←iso --- prove FL enumerate all permutations -- we already have refl and trans in the Symmetric Group @@ -122,11 +119,10 @@ pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) pins {_} {zero} _ = pid pins {suc _} {suc zero} _ = pswap pid -pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc m) (suc (suc n)) lem0 where - pins1 : (i j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) - pins1 _ zero _ = pid - pins1 zero _ _ = pid - pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j} (s≤s (s≤s si≤n)) ∘ₚ pins1 i j (≤-trans si≤n refl-≤s ) +pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc (suc n)) lem0 where + pins1 : (j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) + pins1 zero _ = pid + pins1 (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j} (s≤s (s≤s si≤n)) ∘ₚ pins1 j (≤-trans si≤n refl-≤s ) plist1 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ plist1 {n} perm zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ< {zero} (s≤s z≤n))) ∷ [] @@ -258,11 +254,8 @@ open import logic --- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] -shrink : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n -shrink {n} perm p0=0 = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where - shlem→ : (x : Fin (suc n) ) → perm ⟨$⟩ˡ x ≡ zero → x ≡ zero - shlem→ x px=0 = begin +shlem→ : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n) ) → perm ⟨$⟩ˡ x ≡ zero → x ≡ zero +shlem→ perm p0=0 x px=0 = begin x ≡⟨ sym ( inverseʳ perm ) ⟩ perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ x) ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) px=0 ⟩ perm ⟨$⟩ʳ zero ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) (sym p0=0) ⟩ @@ -270,37 +263,42 @@ zero ∎ where open ≡-Reasoning - shlem← : (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero - shlem← x px=0 = begin +shlem← : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero +shlem← perm p0=0 x px=0 = begin x ≡⟨ sym (inverseˡ perm ) ⟩ perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x ) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) px=0 ⟩ perm ⟨$⟩ˡ zero ≡⟨ p0=0 ⟩ zero ∎ where open ≡-Reasoning - sh2 : {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero - sh2 {x} eq with shlem→ (suc x) eq - sh2 {x} eq | () +sh2 : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero +sh2 perm p0=0 {x} eq with shlem→ perm p0=0 (suc x) eq +sh2 perm p0=0 {x} eq | () + +sh1 : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ʳ (suc x) ≡ zero +sh1 perm p0=0 {x} eq with shlem← perm p0=0 (suc x) eq +sh1 perm p0=0 {x} eq | () + + +-- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] +shrink : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n +shrink {n} perm p0=0 = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where p→ : Fin n → Fin n - p→ x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) - p→ x | zero | record { eq = e } = ⊥-elim ( sh2 {x} e ) + p→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) + p→ x | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e ) p→ x | suc t | _ = t - sh1 : {x : Fin n} → ¬ perm ⟨$⟩ʳ (suc x) ≡ zero - sh1 {x} eq with shlem← (suc x) eq - sh1 {x} eq | () - p← : Fin n → Fin n - p← x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) - p← x | zero | record { eq = e } = ⊥-elim ( sh1 {x} e ) + p← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) + p← x | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e ) p← x | suc t | _ = t piso← : (x : Fin n ) → p→ ( p← x ) ≡ x - piso← x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) - piso← x | zero | record { eq = e } = ⊥-elim ( sh1 {x} e ) - piso← x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t) - piso← x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh2 e ) + piso← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) + piso← x | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e ) + piso← x | suc t | _ with perm ⟨$⟩ʳ (suc t) | inspect (_⟨$⟩ʳ_ perm ) (suc t) + piso← x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 e ) piso← x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin t1 ≡⟨ plem0 plem1 ⟩ @@ -313,18 +311,18 @@ plem1 = begin suc t1 ≡⟨ sym e1 ⟩ - Inverse.from perm Π.⟨$⟩ suc t - ≡⟨ cong (λ k → Inverse.from perm Π.⟨$⟩ k ) (sym e0 ) ⟩ - Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ suc x ) - ≡⟨ inverseˡ perm ⟩ + Inverse.to perm Π.⟨$⟩ suc t + ≡⟨ cong (λ k → Inverse.to perm Π.⟨$⟩ k ) (sym e0) ⟩ + Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ suc x ) + ≡⟨ inverseʳ perm ⟩ suc x ∎ piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x - piso→ x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) - piso→ x | zero | record { eq = e } = ⊥-elim ( sh2 {x} e ) - piso→ x | suc t | _ with perm ⟨$⟩ʳ (suc t) | inspect (_⟨$⟩ʳ_ perm ) (suc t) - piso→ x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh1 e ) + piso→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) + piso→ x | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e ) + piso→ x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t) + piso→ x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 e ) piso→ x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin t1 ≡⟨ plem2 plem3 ⟩ @@ -337,13 +335,55 @@ plem3 = begin suc t1 ≡⟨ sym e1 ⟩ - Inverse.to perm Π.⟨$⟩ suc t - ≡⟨ cong (λ k → Inverse.to perm Π.⟨$⟩ k ) (sym e0 ) ⟩ - Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ suc x ) - ≡⟨ inverseʳ perm ⟩ + Inverse.from perm Π.⟨$⟩ suc t + ≡⟨ cong (λ k → Inverse.from perm Π.⟨$⟩ k ) (sym e0 ) ⟩ + Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ suc x ) + ≡⟨ inverseˡ perm ⟩ suc x ∎ +shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm) refl =p= perm +shrink-iso {n} {perm} = record { peq = λ q → refl } + +p01 : (perm : Permutation 1 1) → perm =p= pid +p01 perm = record { peq = p01e } where + p01e : (q : Fin 1) → (perm ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) + p01e zero with perm ⟨$⟩ʳ zero + ... | zero = refl + +p=0 : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0 +p=0 {zero} perm with p01 perm | p01 ( flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))) +... | s | t = begin + ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) + ≡⟨ peqˡ (presp (p01 perm) (p01 (flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))))) (# 0) ⟩ + (pid ∘ₚ pid ) ⟨$⟩ʳ (# 0) + ≡⟨⟩ + # 0 + ∎ where open ≡-Reasoning +p=0 {suc (zero)} perm with perm ⟨$⟩ʳ (# 0) | inspect ( _⟨$⟩ʳ_ perm ) (# 0) +... | zero | record { eq = e } = begin + (perm ∘ₚ pid) ⟨$⟩ˡ (# 0) + ≡⟨⟩ + perm ⟨$⟩ˡ (# 0) + ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (sym e ) ⟩ + perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (# 0)) + ≡⟨ inverseˡ perm ⟩ + # 0 + ∎ where open ≡-Reasoning +... | suc zero | record { eq = e } = begin + (perm ∘ₚ pswap pid) ⟨$⟩ˡ (# 0) + ≡⟨⟩ + perm ⟨$⟩ˡ (# 1) + ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (sym e ) ⟩ + perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (# 0)) + ≡⟨ inverseˡ perm ⟩ + # 0 + ∎ where open ≡-Reasoning +p=0 {suc (suc n) } perm = p=01 (suc (suc n)) lem0 where + p=01 : (j : ℕ ) → j ≤ suc (suc n) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0 + p=01 zero _ = {!!} + p=01 (suc j) (s≤s si≤n) = {!!} + FL→perm : {n : ℕ } → FL n → Permutation n n FL→perm f0 = pid FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x ) @@ -368,13 +408,11 @@ -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 3) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) )) ∷ [] --- postulate --- p=0 : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0 perm→FL : {n : ℕ } → Permutation n n → FL n perm→FL {zero} perm = f0 -perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm) --- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) +-- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm) +perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) -- t5 = plist t4 ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 3 ) )) t5 = plist (t4) ∷ plist (flip t4)
--- a/sym2.agda Thu Aug 27 11:44:58 2020 +0900 +++ b/sym2.agda Fri Aug 28 11:05:45 2020 +0900 @@ -61,7 +61,7 @@ q ∎ where open ≡-Reasoning - postulate sym2lem1 : g =p= pid + 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 @@ -118,8 +118,6 @@ q ∎ where open ≡-Reasoning --- ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) --- ¬sym5solvable sol = {!!}
--- a/sym3.agda Thu Aug 27 11:44:58 2020 +0900 +++ b/sym3.agda Fri Aug 28 11:05:45 2020 +0900 @@ -35,6 +35,8 @@ p00 (suc zero) = refl p00 (suc (suc zero)) = refl + p1 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) + open _=p=_ solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/sym4.agda Fri Aug 28 11:05:45 2020 +0900 @@ -0,0 +1,70 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym4 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 hiding (_∘ₚ_) + +infixr 200 _∘ₚ_ +_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ + +sym4solvable : solvable (Symmetric 4) +solvable.dervied-length sym4solvable = 3 +solvable.end sym4solvable x d = solved1 x {!!} where + + open import Data.List using ( List ; [] ; _∷_ ) + + open Solvable (Symmetric 4) + -- open Group (Symmetric 2) using (_⁻¹) + + p0 : FL→perm ((# 0) :: ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))) =p= pid + p0 = {!!} -- record { peq = p00 } where + + open _=p=_ + + -- Klien + -- + -- 1 (1,2),(3,4) (1,3),(2,4) (1,4),(2,3) + -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] , 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] , 2 ∷ 3 ∷ 0 ∷ 1 ∷ [] , 3 ∷ 2 ∷ 1 ∷ 0 ∷ [] , + + + data Klein : (x : Permutation 4 4 ) → Set where + kid : Klein pid + ka : Klein (pswap (pswap pid)) + kb : Klein (pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) ) + kc : Klein (pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2})) + + a0 = pid {4} + a1 = pswap (pswap (pid {0})) + a2 = pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) + a3 = pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2}) + + -- 1 0 + -- 2 1 0 + -- 3 2 1 0 + + k1 : { x : Permutation 4 4 } → Klein x → List ℕ + k1 {x} kid = plist x + k1 {x} ka = plist x + k1 {x} kb = plist x + k1 {x} kc = plist x + + k2 = k1 kid ∷ k1 ka ∷ k1 kb ∷ k1 kc ∷ [] + k3 = plist (a1 ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3) ∷ plist (a2 ∘ₚ a1 ) ∷ [] + + solved1 : (x : Permutation 4 4) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid + solved1 = {!!}