open import Level hiding ( suc ; zero )
open import Algebra
module sym5h 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 NormalSubgroup
open import Putil 
open import Solvable 
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

import Algebra.Morphism.Definitions as MorphismDefinitions
open import Algebra.Morphism.Structures

open import Tactic.MonoidSolver using (solve; solve-macro)
import Algebra.Morphism.Definitions as MorphismDefinitions
open import Algebra.Morphism.Structures

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 import FLutil
open import Putil

open _∧_

¬sym5solvable : ¬ ( solvable (Symmetric 5) )
¬sym5solvable sol = counter-example (dervied-length sol) (end5 _ (s02 (dervied-length sol))) 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
--      All stage of Commutator Group of Sym5 contains a sym 3 
--
--      if so, it contains arbitrary 3 different elements of Sym5 as a Sym 3
--           sym3' = p ∙ sym3 ∙ p⁻¹ 

     open _=p=_
     open ≡-Reasoning
     open solvable
     open import Data.Fin.Properties

     -- a group contains Symmetric 3 as a normal subgroup

     record HaveSym3 {c d : Level } (G : Group c d ) : Set (Level.suc c Level.⊔ Level.suc d) where
        field 
           isSub :  SubGroup {d} G 
           G→3 :  RawGroup.Carrier (GR (SGroup G isSub)) → Permutation 3 3
           is-sym3 : IsGroupIsomorphism (GR (SGroup G isSub)) (GR (Symmetric 3)) G→3

     open _=p=_
     -- Symmetric 3 is a normal subgroup of Symmetric 5
     s00 : HaveSym3 (Symmetric 5) 
     s00 = record {
           isSub = sub00
         ; G→3 = s15
         ; is-sym3 = ?
        } where
           open ≡-Reasoning
           s10 : Permutation 5 5 → Set
           s10 perm = (perm  ⟨$⟩ˡ (# 0) ≡ # 0) ×  (perm  ⟨$⟩ˡ (# 1) ≡ # 1)
           s11 : s10 pid
           s11 = refl , refl 
           s12 : (a : Permutation 5 5) → s10 a → s10 (pinv a)
           s12 p (eq3 , eq4) = s12a , s12b where
               s12a : pinv p ⟨$⟩ˡ # 0 ≡ # 0
               s12a = begin
                 pinv p ⟨$⟩ˡ # 0 ≡⟨ cong (λ k → pinv p ⟨$⟩ˡ k) (sym eq3) ⟩
                 pinv p ⟨$⟩ˡ (p ⟨$⟩ˡ # 0) ≡⟨ inverseʳ p ⟩
                 # 0 ∎ 
               s12b : pinv p ⟨$⟩ˡ # 1 ≡ # 1
               s12b = begin
                 pinv p ⟨$⟩ˡ # 1 ≡⟨ cong (λ k → pinv p ⟨$⟩ˡ k) (sym eq4) ⟩
                 pinv p ⟨$⟩ˡ (p ⟨$⟩ˡ # 1) ≡⟨ inverseʳ p ⟩
                 # 1 ∎ 
           s13 : {a b : Permutation 5 5} → a =p= b → s10 a → s10 b
           s13 {a} {b} eq (eq3 , eq4) = trans (peqˡ (psym eq) (# 0)) eq3  , trans (peqˡ (psym eq) (# 1)) eq4  
           s14 : {a b : Permutation 5 5} → s10 a → s10 b → s10 (a ∘ₚ b)
           s14 {a} {b} eqa eqb = s14a , s14b where
               s14a : a ∘ₚ b ⟨$⟩ˡ # 0 ≡ # 0
               s14a = begin
                  a ∘ₚ b ⟨$⟩ˡ # 0 ≡⟨ cong (λ k →  a ⟨$⟩ˡ k) (proj₁ eqb) ⟩
                  a ⟨$⟩ˡ # 0 ≡⟨ proj₁ eqa  ⟩
                  # 0 ∎
               s14b : a ∘ₚ b ⟨$⟩ˡ # 1 ≡ # 1
               s14b = begin
                  a ∘ₚ b ⟨$⟩ˡ # 1 ≡⟨ cong (λ k →  a ⟨$⟩ˡ k) (proj₂ eqb) ⟩
                  a ⟨$⟩ˡ # 1 ≡⟨ proj₂ eqa  ⟩
                  # 1 ∎
           sub00 = record { P = s10 ; Pε  = s11  ; P⁻¹ = s12 ; P≈ = s13 ; P∙ = λ {a} {b} → s14 {a} {b} }
           s15 : Nelm (Symmetric 5) sub00 → Permutation 3 3
           s15 record { elm = elm ; Pelm = Pelm } = shrink (shrink elm (proj₁ Pelm)) s16 where
               s16 :  shrink elm (proj₁ Pelm) ⟨$⟩ˡ # 0 ≡ # 0
               s16 = begin
                 shrink elm (proj₁ Pelm) ⟨$⟩ˡ # 0 ≡⟨ Data.Fin.Properties.suc-injective (
                    suc (shrink elm (proj₁ Pelm) ⟨$⟩ˡ # 0) ≡⟨ ? ⟩ 
                    elm  ⟨$⟩ˡ (suc (# 0))  ≡⟨ proj₂ Pelm ⟩ 
                    suc (# 0) ∎ ) ⟩
                 # 0 ∎
     s01 : (i : ℕ ) → HaveSym3 (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) i))) 
     s01 zero = ?
     s01 (suc i) = record {
           isSub = sub01
         ; G→3 = s15
         ; is-sym3 =  record {
              isGroupMonomorphism = record {    
                 isGroupHomomorphism = record {
                     isMonoidHomomorphism = record {
                          isMagmaHomomorphism = record {
                             isRelHomomorphism = record { cong = λ {x} {y} eq → ? }
                           ; homo = ? }
                        ; ε-homo = ? }
                       ; ⁻¹-homo = ?  }
                   ; injective = λ eq → ? }
           ;  surjective = λ nx → s16 nx , s17 nx  }
        } where
           sym3 : HaveSym3 (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) i))) 
           sym3 = s01 i
           s10 : Nelm (Symmetric 5) (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i))) → Set
           s10 record { elm = perm ; Pelm = Pelm } = (perm  ⟨$⟩ˡ (# 0) ≡ # 0) ×  (perm  ⟨$⟩ˡ (# 1) ≡ # 1)
           sub01 :  SubGroup (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i))))
           sub01 = record { P = s10 ; Pε  = refl , refl   ; P⁻¹ = ? ; P≈ = ? ; P∙ = λ {a} {b} → ? }
           s15 : Nelm (SGroup (Symmetric 5) (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i)))) sub01 → Permutation 3 3
           s15 record { elm = record { elm = elm ; Pelm = ic } ; Pelm = Pelm } = shrink (shrink elm (proj₁ Pelm)) ? 
           s16 : Permutation 3 3  → Nelm (SGroup (Symmetric 5) (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i)))) sub01
           s16 abc = record { elm = record { elm = ? ; Pelm = ? } ; Pelm = ? } where
              dba : Permutation 5 5
              dba = ?
              aec : Permutation 5 5
              aec = ?
              Cdba : deriving (Symmetric 5) i dba
              Cdba = ?
              Caec : deriving (Symmetric 5) i aec
              Caec = ?
              s18 :  iCommutator (Symmetric 5) (suc i) (pprep (pprep abc))
              s18 = iunit (ccong ? ( comm Cdba Caec ))
           s17 : (abc : Permutation 3 3 ) →  s15 (s16 abc) =p= abc
           s17 = ?


     -- if Symmetric 0 is a normal subgroup of Commutator Group of Symmetric 5
     -- the next stagee contains Symmetric 0 as a normal subgroup

     s03 : (i : ℕ) → Permutation 5 5
     s03 0 = FL→perm (plist→FL (0 ∷ 1 ∷ 0 ∷ 1 ∷ 2 ∷ []))
     s03 (suc zero) = FL→perm (plist→FL (0 ∷ 1 ∷ 1 ∷ 0 ∷ 2 ∷ []))
     s03 (suc (suc i)) = s03 i

     s02 : (i : ℕ) → deriving (Symmetric 5) i (s03 i)
     s02 i = ? where
        s04 : HaveSym3 (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) (dervied-length sol)))) 
        s04 = s01 (dervied-length sol)

     -- open Solvable ( Symmetric 5) 
     end5 : (x : Permutation 5 5) → deriving (Symmetric 5) (dervied-length sol) x →  x =p= pid  
     end5 x der = end sol x der

     counter-example :  (i : ℕ) → ¬ (s03 i  =p= pid )
     counter-example zero eq with ←pleq _ _ eq
     ... | ()
     counter-example (suc zero) eq with ←pleq _ _ eq
     ... | ()
     counter-example (suc (suc i)) eq = counter-example i eq