# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607772509 -32400
# Node ID d782dd481a26afe0c10b1c846f648cd96019622d
# Parent  0b843361b6e23616265dee1d09ca21ada8c11f10
compile

diff -r 0b843361b6e2 -r d782dd481a26 FLComm.agda
--- a/FLComm.agda	Fri Dec 11 08:24:33 2020 +0900
+++ b/FLComm.agda	Sat Dec 12 20:28:29 2020 +0900
@@ -37,7 +37,6 @@
 open import Relation.Nullary.Decidable hiding (⌊_⌋)
 
 open import fin
-open AnyFL
 
 -- all cobmbination in P and Q (could be more general)
 record AnyComm {n m l : ℕ}  (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where
@@ -103,6 +102,8 @@
      allFL : FList n
      anyP : (x : FL n) → Any (x ≡_ ) allFL 
 
+open AnyFL
+
 --   all FL as all combination  
 --      anyComm ( #0 :: FL0 ... # n :: FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n)
 
@@ -145,11 +146,6 @@
 at3 = proj₁ (toList (allFL (anyFL 3)))
 at4 = proj₁ (toList (allFL (anyFL 4)))
 
--- open import Data.List.Fresh.Relation.Unary.All
--- at6 : All (_# allFL (anyFL 2)) (allFL (anyFL 2))
--- at6 = {!!}
--- at5 = append (allFL (anyFL 2)) (allFL (anyFL 2)) at6
-
 CommFListN  : ℕ →  FList n
 CommFListN  zero = allFL (anyFL n)
 CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))
diff -r 0b843361b6e2 -r d782dd481a26 FLutil.agda
--- a/FLutil.agda	Fri Dec 11 08:24:33 2020 +0900
+++ b/FLutil.agda	Sat Dec 12 20:28:29 2020 +0900
@@ -106,42 +106,8 @@
     fsuc1 =  Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
 
--- fsuc0 : { n : ℕ } → (x : FL n ) → FL n 
--- fsuc0 {n} (x :: y) (f<n lt) = fromℕ< fsuc2 :: y where
---     fsuc2 : suc (toℕ x) < n
---     fsuc2 =  Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
--- fsuc0 (x :: y) (f<t lt) = x :: fsuc y lt
-
-open import Data.Maybe
 open import fin
 
-fpredm : { n : ℕ } → (x : FL n ) → Maybe (FL n)
-fpredm f0 = nothing
-fpredm (x :: y) with fpredm y
-... | just y1 = just (x :: y1)
-fpredm (zero :: y) | nothing = nothing
-fpredm (suc x :: y) | nothing = just (fin+1 x :: fmax)
-
-¬<FL0 : {n : ℕ} {y : FL n} → ¬ y f< FL0
-¬<FL0 {suc n} {zero :: y} (f<t lt) = ¬<FL0 {n} {y} lt 
-
-fpred : { n : ℕ } → (x : FL n ) → FL0 f< x  → FL n
-fpred (zero :: y) (f<t lt) = zero :: fpred y lt
-fpred (x :: y) (f<n lt) with FLcmp FL0 y
-... | tri< a ¬b ¬c = x :: fpred y a
-... | tri> ¬a ¬b c = ⊥-elim (¬<FL0 c)
-fpred {suc _} (suc x :: y) (f<n lt) | tri≈ ¬a b ¬c = fin+1 x :: fmax
-
-fpred< : { n : ℕ } → (x : FL n ) → (lt : FL0 f< x ) → fpred x lt f< x
-fpred< (zero :: y) (f<t lt) = f<t (fpred< y lt)
-fpred< (suc x :: y) (f<n lt) with FLcmp FL0 y
-... | tri< a ¬b ¬c = f<t ( fpred< y a)
-... | tri> ¬a ¬b c = ⊥-elim (¬<FL0 c)
-... | tri≈ ¬a refl ¬c = f<n fpr1 where
-   fpr1 : {n : ℕ } {x : Fin n} → fin+1 x Data.Fin.< suc x
-   fpr1 {suc _} {zero} = s≤s z≤n
-   fpr1 {suc _} {suc x} = s≤s fpr1
-
 flist1 :  {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n)) 
 flist1 zero i<n [] _ = []
 flist1 zero i<n (a ∷ x ) z  = ( zero :: a ) ∷ flist1 zero i<n x z 
@@ -152,14 +118,6 @@
 flist {zero} f0 = f0 ∷ [] 
 flist {suc n} (x :: y)  = flist1 n a<sa (flist y) (flist y)   
 
-fr22 : fsuc (zero :: zero :: f0) (fmax¬ (λ ())) ≡ (suc zero :: zero :: f0)
-fr22 = refl
-
-fr4 : List (FL 4)
-fr4 = Data.List.reverse (flist (fmax {4}) ) 
--- fr5 : List (List ℕ)
--- fr5 = map plist (map FL→perm  (Data.List.reverse (flist (fmax {4}) )))
-
 FL1 : List ℕ → List ℕ
 FL1 [] = []
 FL1 (x ∷ y) = suc x ∷ FL1 y
@@ -177,7 +135,6 @@
 
 tt0 = (# 2) :: (# 1) :: (# 0) :: zero :: f0
 tt1 = FL→plist tt0
--- tt2 = plist ( FL→perm tt0 )
 
 open _∧_
 
@@ -188,7 +145,7 @@
 find-zero (suc x ∷ y) (s≤s (s≤s i<n)) with find-zero y (s≤s i<n) 
 ... | record { proj1 = i ; proj2 = y1 } = record { proj1 = suc i ; proj2 = suc x ∷ y1 }
 
-plist→FL : {n : ℕ} → List ℕ → FL n
+plist→FL : {n : ℕ} → List ℕ → FL n -- wrong implementation
 plist→FL {zero} [] = f0
 plist→FL {suc n} [] = zero :: plist→FL {n} []
 plist→FL {zero} x = f0
@@ -198,7 +155,14 @@
 tt2 = 2 ∷ 1 ∷ 0 ∷ 3 ∷ []
 tt3 : FL 4
 tt3 = plist→FL tt2
--- tt4 = proj1 (find-zero {5} {4} tt2 a<sa) , proj2 (find-zero {5} {4} tt2 a<sa)
+tt4 = FL→plist tt3
+tt5 = plist→FL {4} (FL→plist tt0)
+
+-- maybe FL→iso can be easier using this ...
+-- FL→plist-iso : {n : ℕ} → (f : FL n ) → plist→FL (FL→plist f ) ≡ f
+-- FL→plist-iso = {!!}
+-- FL→plist-inject : {n : ℕ} → (f g : FL n ) → FL→plist f ≡ FL→plist g → f ≡ g
+-- FL→plist-inject = {!!}
 
 open import Relation.Binary as B hiding (Decidable; _⇔_)
 open import Data.Sum.Base as Sum --  inj₁
@@ -265,9 +229,6 @@
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 
 
-¬x<FL0 : {n : ℕ} {x : FL n} → ¬ ( x f< FL0 )
-¬x<FL0 {suc n} {zero :: y} (f<t not) = ¬x<FL0 {n} {y} not
-
 open import Data.List.Fresh.Relation.Unary.Any 
 open import Data.List.Fresh.Relation.Unary.All 
 
diff -r 0b843361b6e2 -r d782dd481a26 Putil.agda
--- a/Putil.agda	Fri Dec 11 08:24:33 2020 +0900
+++ b/Putil.agda	Sat Dec 12 20:28:29 2020 +0900
@@ -197,7 +197,7 @@
             p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
             p11 = begin
                fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
-              ≡⟨ lemma10  p12  ⟩
+              ≡⟨ lemma10 {suc (suc n)} {_} {_} p12 {≤-trans (fin<n {_} {y}) a≤sa} {s≤s (fin<n {suc n} {x} )}  ⟩
                suc (fromℕ< (fin<n {suc n} {x} )) 
               ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
                suc x
@@ -232,7 +232,7 @@
              fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))
           ≡⟨⟩
              fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n))) 
-          ≡⟨ lemma10 (p3 x) {p6} {p2} ⟩
+          ≡⟨ lemma10 {suc (suc n)} (p3 x) {p6} {p2} ⟩
              fromℕ< ( s≤s (fin<n {suc n} {x}) )
           ≡⟨⟩
              suc (fromℕ< (fin<n {suc n} {x} )) 
@@ -278,7 +278,7 @@
           p004 = p003  (fromℕ< (s≤s (s≤s m≤n))) (
              begin
                 fromℕ< (s≤s (s≤s m≤n))
-             ≡⟨  lemma10  (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩
+             ≡⟨  lemma10 {suc (suc n)}  (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩
                 fromℕ< (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) )
              ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
                 suc t
@@ -578,10 +578,25 @@
     ∷ []
 
 
+-- FL→plist-iso : {n : ℕ} → (f : FL n ) → plist→FL (FL→plist f ) ≡ f
+-- FL→plist-inject : {n : ℕ} → (f g : FL n ) → FL→plist f ≡ FL→plist g → f ≡ g
+
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0
 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)  
+
+---FL→perm   : {n : ℕ }  → FL n → Permutation n n 
+---FL→perm   x = plist→perm ( FL→plis x)
+-- perm→FL   : {n : ℕ }  → Permutation n n → FL n
+-- perm→FL p  = plist→FL (plist p)
+
+-- pcong-pF : {n : ℕ }  → {x y : Permutation n n}  → x =p= y → perm→FL x ≡ perm→FL y
+-- pcong-pF {n} {x} {y} x=y = FL→plist-inject (subst ... (pleq← eq)) (perm→FL x) (perm→FL y)
+
+-- FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
+-- FL→iso = 
+-- pcong-Fp : {n : ℕ }  → {x y : FL n}  → x ≡ y → FL→perm x =p= FL→perm y
+-- FL←iso : {n : ℕ }  → (perm : Permutation n n )  → FL→perm ( perm→FL perm  ) =p= perm
 
 _p<_ : {n : ℕ } ( x y : Permutation n n ) → Set
 x p< y = perm→FL x f<  perm→FL y
@@ -676,8 +691,6 @@
         h ⟨$⟩ʳ q
      ∎  ) }
 
--- FLpid : (n : ℕ) → (x : Permutation n n) → perm→FL x ≡ FL0 → x =p= pid
-
 FLpid :  {n : ℕ} → (x : Permutation n n) → perm→FL x ≡ FL0 → FL→perm FL0 =p= pid   → x =p= pid
 FLpid x eq p0id = ptrans pf2 (ptrans pf0 p0id ) where
    pf2 : x =p= FL→perm (perm→FL x)
@@ -687,46 +700,4 @@
 
 pFL0 : {n : ℕ } → FL0 {n} ≡ perm→FL pid
 pFL0 {zero} = refl
-pFL0 {suc n} = sym ( begin
-        perm→FL pid
-     ≡⟨⟩
-        {!!}
-     ≡⟨ {!!} ⟩
-        FL0
-     ∎  )
-
-lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
-lem2 i≤n = ≤-trans i≤n ( a≤sa )
-
-∀-FL : (n : ℕ ) → List (FL (suc n))
-∀-FL  x  = fls6 x  where
-   fls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → FL  n → List (FL  (suc n))  → List (FL  (suc n)) 
-   fls4 zero n i≤n perm x = (zero :: perm ) ∷ x
-   fls4 (suc i) n i≤n  perm x = fls4 i n (≤-trans a≤sa i≤n ) perm ((fromℕ< (s≤s i≤n) :: perm ) ∷ x)
-   fls5 :  ( n : ℕ ) → List (FL n) → List (FL  (suc n))  → List (FL (suc n)) 
-   fls5 n [] x = x
-   fls5 n (h ∷ x) y = fls5  n x (fls4 n n lem0 h y)
-   fls6 :  ( n : ℕ ) → List (FL  (suc n)) 
-   fls6 zero = (zero :: f0) ∷ []
-   fls6 (suc n) =  fls5 (suc n) (fls6 n) []   
-
-tf1 = ∀-FL 4
-tf2 = Data.List.map (λ k → ⟪ plist (FL→perm k ) , k ⟫ ) tf1
-
-all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
-all-perm n = pls6 n where
-   lem1 : {i n : ℕ } → i ≤ n → i < suc n
-   lem1 z≤n = s≤s z≤n
-   lem1 (s≤s lt) = s≤s (lem1 lt)
-   pls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
-   pls4 zero n i≤n perm x = (pprep perm ∘ₚ pins i≤n ) ∷ x
-   pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans a≤sa i≤n ) perm (pprep perm ∘ₚ pins {n} {suc i} i≤n  ∷ x)
-   pls5 :  ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
-   pls5 n [] x = x
-   pls5 n (h ∷ x) y = pls5  n x (pls4 n n lem0 h y)
-   pls6 :  ( n : ℕ ) → List (Permutation (suc n) (suc n)) 
-   pls6 zero = pid ∷ []
-   pls6 (suc n) =  pls5 (suc n) (rev (pls6 n) ) []   -- rev to put id first
-
-pls : (n : ℕ ) → List (List ℕ )
-pls n = Data.List.map plist (all-perm n) 
+pFL0 {suc n} = cong (λ k → zero :: k ) pFL0
diff -r 0b843361b6e2 -r d782dd481a26 sym4.agda
--- a/sym4.agda	Fri Dec 11 08:24:33 2020 +0900
+++ b/sym4.agda	Sat Dec 12 20:28:29 2020 +0900
@@ -54,6 +54,9 @@
 
    stage3FList : CommFListN 4 3 ≡ cons (zero :: zero :: zero :: zero :: f0) [] (Level.lift tt)
    stage3FList = refl
+
+   st3 = proj₁ (toList ( CommFListN 4 2 ))
+   -- st4 = {!!}
  
    solved1 :  (x : Permutation 4 4) → deriving 3 x → x =p= pid 
    solved1 x dr = CommSolved 4 x ( CommFListN 4 3 ) stage3FList p0id solved2 where
diff -r 0b843361b6e2 -r d782dd481a26 sym5a.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sym5a.agda	Sat Dec 12 20:28:29 2020 +0900
@@ -0,0 +1,94 @@
+open import Level hiding ( suc ; zero )
+open import Algebra
+module sym5a where
+
+open import Symmetric 
+open import Data.Unit using (⊤ ; tt )
+open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function hiding (flip)
+open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
+open import Data.Nat.Properties
+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 hiding (_<_ ; _≤_  ; lift )
+open import Data.Fin.Permutation  hiding (_∘ₚ_)
+
+infixr  200 _∘ₚ_
+_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
+
+open import Data.List  hiding ( [_] )
+open import nat
+open import fin
+open import logic
+
+open _∧_
+
+¬sym5solvable : ¬ ( solvable (Symmetric 5) )
+¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (any3de (dervied-length sol) 3rot 0<3 0<4 ) ) where
+--
+--    dba       1320      d → b → a → d
+--    (dba)⁻¹   3021      a → b → d → a
+--    aec       21430
+--    (aec)⁻¹   41032
+--    [ dba , aec ] = (abd)(cea)(dba)(aec) = abc
+--      so commutator always contains abc, dba and aec
+
+     open ≡-Reasoning
+
+     open solvable
+     open Solvable ( Symmetric 5) 
+     end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →  x =p= pid  
+     end5 x der = end sol x der
+
+     0<4 : 0 < 4
+     0<4 = s≤s z≤n
+
+     0<3 : 0 < 3
+     0<3 = s≤s z≤n
+
+     --- 1 ∷ 2 ∷ 0 ∷ []      abc
+     3rot : Permutation 3 3
+     3rot = pid {3} ∘ₚ pins (n≤ 2)
+
+     save2 : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) →  Permutation  5 5 
+     save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) 
+
+     -- Permutation 5 5 include any Permutation 3 3
+     any3 : {i j : ℕ }  → Permutation 3 3  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     any3 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) 
+
+     any3cong : {i j : ℕ }  → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → any3 x i<3 j<4  =p= any3 y i<3 j<4
+     any3cong {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=_
+
+     -- derving n includes any Permutation 3 3, 
+     any3de : {i j : ℕ } → (n : ℕ) → (abc : Permutation 3 3) →  (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) → deriving n (any3 abc i<3 j<4)
+     any3de {i} {j} zero abc i<3 j<4 = Level.lift tt
+     any3de {i} {j} (suc n) abc i<3 j<4 = ccong abc-from-comm (comm (any3de n (abc  ∘ₚ abc) i<3 j0<4 ) (any3de n (abc  ∘ₚ abc) i0<3 j<4 ))  where
+         i0 : ℕ
+         i0 = ?
+         j0 : ℕ
+         j0 = ?
+         i0<3 : i0 ≤ 3
+         i0<3 = {!!}
+         j0<4 : j0 ≤ 4
+         j0<4 = {!!}
+         abc-from-comm : [ any3 (abc  ∘ₚ abc) i<3 j0<4  , any3 (abc  ∘ₚ abc) i0<3 j<4 ] =p= any3 abc i<3 j<4
+         abc-from-comm = {!!}
+
+     abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     abc i<3 j<4 = any3 3rot i<3 j<4
+
+     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
+     counter-example eq with ←pleq _ _ eq
+     ...  | ()
+
diff -r 0b843361b6e2 -r d782dd481a26 sym5n.agda
--- a/sym5n.agda	Fri Dec 11 08:24:33 2020 +0900
+++ b/sym5n.agda	Sat Dec 12 20:28:29 2020 +0900
@@ -22,8 +22,13 @@
 infixr  200 _∘ₚ_
 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
 
-sym5solvable : ¬ solvable (Symmetric 5)
-sym5solvable = {!!} where
+-- open import IO
+open import Data.String hiding (toList)
+open import Data.Unit
+open import Agda.Builtin.String 
+
+sym5solvable : (n : ℕ) → String -- ¬ solvable (Symmetric 5)
+sym5solvable n = FListtoStr (CommFListN 5 n) where
 
    open import Data.List using ( List ; [] ; _∷_ )
    open Solvable (Symmetric 5)
@@ -38,5 +43,23 @@
    open import Data.List.Fresh.Relation.Unary.Any
    open import FLComm
 
-   stage4FList = CommFListN 5 2 
- 
+
+   stage4FList = CommFListN 5 0 
+   stage6FList = CommFListN 5 3 
+
+   -- stage5FList = {!!}
+   -- s2=s3 :  CommFListN 5 2 ≡ CommFListN 5 3 
+   -- s2=s3 = refl
+
+   FLtoStr : {n : ℕ} → (x : FL n) → String
+   FLtoStr f0 = "f0"
+   FLtoStr (x :: y) = primStringAppend ( primStringAppend (primShowNat (toℕ x)) " :: " ) (FLtoStr y)
+
+   FListtoStr : {n : ℕ} → (x : FList n) → String
+   FListtoStr [] = ""
+   FListtoStr (cons a x x₁) = primStringAppend (FLtoStr a) (primStringAppend "\n" (FListtoStr x))
+
+open import IO -- using (IO)
+
+main = run ( putStrLn $ sym5solvable 4)
+