--- /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
+     ...  | ()
+