open import Level hiding ( suc ; zero )
open import Algebra
module Solvable {n m : Level} (G : Group n m ) where

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  Relation.Binary.PropositionalEquality hiding ( [_] )


open Group G

[_,_] :  Carrier   → Carrier   → Carrier  
[ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h 

data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
  uni   : Commutator P ε
  comm  : {g h : Carrier} → P g → P h  → Commutator P [ g , h ] 
  gen   : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙  g  )
  ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g

deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
deriving (suc i) x = Commutator (deriving i) x 

record Solvable : Set (Level.suc n ⊔ m) where
  field 
     dervied-length : ℕ
     end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε  

-- deriving stage is closed on multiplication and inversion

import Relation.Binary.Reasoning.Setoid as EqReasoning

gsym = Algebra.Group.sym G
grefl = Algebra.Group.refl G
lemma3 : ε ≈ ε ⁻¹
lemma3 = begin
     ε          ≈⟨ gsym (proj₁ inverse _) ⟩
     ε ⁻¹ ∙ ε   ≈⟨ proj₂ identity _ ⟩
     ε ⁻¹
   ∎ where open EqReasoning (Algebra.Group.setoid G)

open import Data.List using ([] ; _∷_ ; List ; length )

data Node (A : Set n) : Set (Level.suc n) where
   leaf : A → Node A
   node : Node A → Node A → Node A

flatten : Node Carrier → List Carrier
flatten x = flatten1 x [] where
   flatten1 : Node Carrier → List Carrier → List Carrier
   flatten1 (leaf x)  y = x ∷ y
   flatten1 (node left right)  y = flatten1 left (flatten1 right y )

gnode : Node Carrier → Carrier
gnode (leaf x) = x
gnode (node left right) = gnode left ∙ gnode right 

glist : List Carrier → Carrier
glist [] = ε
glist (x ∷ []) = x
glist (x ∷ y) = x ∙ glist y

gpattern : (p q : Node Carrier) → flatten p ≡ flatten q  → gnode p ≈ gnode q
gpattern p q eq = gpattern1 p q (flatten p) _≡_.refl eq  where
   gnot0 : ( left right : Node Carrier ) →  length (flatten (node left right) ) > 1
   gnot0 (leaf x) (leaf x₁) = s≤s ( s≤s z≤n)
   gnot0 (leaf x) (node q q₁) = {!!}
   gnot0 (node p p₁) q = {!!}
   gnot1 : (x : Carrier ) → ( left right : Node Carrier ) →  ¬ ( x ∷ [] ≡ flatten (node left right) )
   gnot1 x p q eq0 = {!!}
   gpattern1 : (p q : Node Carrier) → (r : List Carrier ) → flatten p ≡ r → r ≡ flatten q → gnode p ≈ gnode q
   gpattern1 (leaf x) (leaf x) (x ∷ []) _≡_.refl _≡_.refl = grefl
   gpattern1 (leaf x) (node left right) (x ∷ []) _≡_.refl r=q = {!!}
   gpattern1 (node p p₁) (leaf x) r p=r r=q = {!!}
   gpattern1 (node (leaf x) p₁) (node (leaf x₁) q₁) r p=r r=q = {!!}
   gpattern1 (node (leaf x) p₁) (node (node q q₂) q₁) r p=r r=q = {!!}
   gpattern1 (node (node p p₂) p₁) (node (leaf x) q₁) r p=r r=q = {!!}
   gpattern1 (node (node p p₂) p₁) (node (node q q₂) q₁) r p=r r=q = {!!}

deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y  → deriving i ( x ∙ y )
deriving-mul {zero} {x} {y} _ _ = lift tt
deriving-mul {suc i} {x} {y} ix iy = gen ix iy

deriving-inv : { i : ℕ } → { x  : Carrier } → deriving i x → deriving i ( x ⁻¹ )
deriving-inv {zero} {x} (lift tt) = lift tt
deriving-inv {suc i} {ε} uni = ccong lemma3 uni
deriving-inv {suc i} {_} (comm x x₁ )   = ccong (lemma4 _ _) (comm x₁ x) where
   lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
   lemma4 g h = begin
       h ⁻¹ ∙ g ⁻¹ ∙ h ∙ g            ≈⟨ {!!} ⟩
      [ g , h ] ⁻¹
     ∎ where open EqReasoning (Algebra.Group.setoid G)
deriving-inv {suc i} {_} (gen x x₁ )    = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where
   lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
   lemma5 f g = begin
     g ⁻¹ ∙ f ⁻¹           ≈⟨ {!!} ⟩
     g ⁻¹ ∙ f ⁻¹  ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ {!!} ⟩
     (g ⁻¹ ∙ f ⁻¹  ∙ (f ∙ g)) ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
     (g ⁻¹ ∙ (f ⁻¹  ∙ f) ∙ g) ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
     (g ⁻¹ ∙ (ε  ∙ g)) ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
     (g ⁻¹ ∙ g) ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
     ε  ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
     (f ∙ g) ⁻¹
     ∎ where open EqReasoning (Algebra.Group.setoid G)
deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )