# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598580345 -32400
# Node ID 405c1f727ffe8e233304db6bb5a06ffc5c36829d
# Parent  c68956f6c3ad7dddb94c93136c28b5bd20b6b975
...

diff -r c68956f6c3ad -r 405c1f727ffe Putil.agda
--- 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)
diff -r c68956f6c3ad -r 405c1f727ffe sym2.agda
--- 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 = {!!}
 
 
 
diff -r c68956f6c3ad -r 405c1f727ffe sym3.agda
--- 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
diff -r c68956f6c3ad -r 405c1f727ffe sym4.agda
--- /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 = {!!}