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
gtrans = Algebra.Group.trans G

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

lemma6 : {f : Carrier } →  ( f ⁻¹ ) ⁻¹  ≈ f
lemma6 {f} = begin
     ( f ⁻¹ ) ⁻¹   ≈⟨ gsym ( proj₁ identity _) ⟩
      ε  ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩
     (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ assoc _ _ _ ⟩
     f ∙ ( f ⁻¹  ∙ ( f ⁻¹ ) ⁻¹ )  ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩
     f ∙ ε  ≈⟨ proj₂ identity _ ⟩
     f
   ∎ where open EqReasoning (Algebra.Group.setoid G)

≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g
≡→≈ refl = grefl

data MP  : Carrier → Set (Level.suc n) where
    am  : (x : Carrier )   →  MP  x
    _o_ : {x y : Carrier } →  MP  x →  MP  y → MP  ( x ∙ y )

mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
mpf {x} (am x) y = x ∙ y
mpf (m o m₁) y = mpf m ( mpf m₁ y )

mp-flatten : {x : Carrier } → (m : MP x ) → Carrier 
mp-flatten {x} m = mpf {x} m ε 
  
∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m
∙-flatten {x} (am x) = gsym (proj₂ identity _)
∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q )
∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ ( ∙-flatten {x ∙ y } (p o q )) ( ∙-flatten {z} r ) where
   mp-cong : {p q r : Carrier} → (P : MP p)  → q ≈ r → mpf P q ≈ mpf P r
   mp-cong (am x) q=r = ∙-cong grefl q=r
   mp-cong (P o P₁) q=r = mp-cong P ( mp-cong P₁ q=r )
   mp-assoc : {p q r : Carrier} → (P : MP p)  → mpf P q ∙ r ≈ mpf P (q ∙ r )
   mp-assoc (am x) = assoc _ _ _ 
   mp-assoc {p} {q} {r} (P o P₁) = begin
       mpf P (mpf  P₁ q) ∙ r      ≈⟨ mp-assoc P ⟩
       mpf P (mpf P₁ q ∙ r)       ≈⟨ mp-cong P (mp-assoc P₁)  ⟩
       mpf P ((mpf  P₁) (q ∙ r))
    ∎ where open EqReasoning (Algebra.Group.setoid G)
   lemma9 : (x y z : Carrier) →  x ∙ y ≈ mpf p (mpf q ε) → z ≈ mpf r ε →  x ∙ y ∙ z ≈ mp-flatten ((p o q) o r)
   lemma9 x y z t s = begin
       x ∙ y ∙ z                    ≈⟨ ∙-cong t grefl  ⟩
       mpf p (mpf q ε) ∙ z          ≈⟨ mp-assoc p ⟩
       mpf p (mpf q ε ∙ z)          ≈⟨ mp-cong p (mp-assoc q ) ⟩
       mpf p (mpf q (ε ∙ z))        ≈⟨ mp-cong p (mp-cong q (proj₁ identity _  )) ⟩
       mpf p (mpf q z)              ≈⟨ mp-cong p (mp-cong q s) ⟩
       mpf p (mpf q (mpf r ε))
    ∎ where open EqReasoning (Algebra.Group.setoid G)

mpg : {x : Carrier } → (m : MP x ) → Carrier → Carrier
mpg {x} (am x) y = y ∙ x
mpg (m o m₁) y = mpf m₁ ( mpf m y )

mp-flatten-g : {x : Carrier } → (m : MP x ) → Carrier 
mp-flatten-g {x} m = mpg {x} m ε 
  
∙-flatten-g : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten-g m
∙-flatten-g {x} (am x) = gsym (proj₁ identity _)
∙-flatten-g {_} (am x o q) = {!!} -- ∙-cong ( ∙-flatten-g q ) grefl
∙-flatten-g (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ {!!} ( ∙-flatten-g {z} r ) where
   mp-cong : {p q r : Carrier} → (P : MP p)  → q ≈ r → mpg P q ≈ mpg P r
   mp-cong (am x) q=r = {!!} -- ∙-cong grefl q=r
   mp-cong (P o P₁) q=r = {!!} -- mp-cong P ( mp-cong P₁ q=r )
   mp-assoc : {p q r : Carrier} → (P : MP p)  → mpg P q ∙ r ≈ mpg P (q ∙ r )
   mp-assoc (am x) = {!!} -- assoc _ _ _ 
   mp-assoc {p} {q} {r} (P o P₁) = begin
       {!!}      ≈⟨ {!!} ⟩
       {!!}
    ∎ where open EqReasoning (Algebra.Group.setoid G)
   lemma9 : (x y z : Carrier) →  x ∙ y ≈ mpg p (mpg q ε) → z ≈ mpg r ε →  x ∙ y ∙ z ≈ mp-flatten-g ((p o q) o r)
   lemma9 x y z t s = begin
       {!!}                ≈⟨ {!!}  ⟩
       {!!}
    ∎ where open EqReasoning (Algebra.Group.setoid G)

tet1 : (f g : Carrier ) → {!!}
tet1 f g = mp-flatten-g ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))

tet2 : (f g : Carrier ) → {!!}
tet2 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))

lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
lemma5 f g = begin
     g ⁻¹ ∙ f ⁻¹                                     ≈⟨ gsym (proj₂ identity _) ⟩
     g ⁻¹ ∙ f ⁻¹  ∙ ε                                ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
     g ⁻¹ ∙ f ⁻¹  ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ )         ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))  ⟩
     g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))))    ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩
     g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))    ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩
     g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))                   ≈⟨ gsym (assoc _ _ _) ⟩
     (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε)                  ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
     (f ∙ g) ⁻¹ ∙ ε                                  ≈⟨ proj₂ identity _ ⟩
     (f ∙ g) ⁻¹
     ∎ where open EqReasoning (Algebra.Group.setoid G)

lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
lemma4 g h = begin
       [ h , g ]                               ≈⟨ grefl ⟩
       (h ⁻¹ ∙ g ⁻¹ ∙   h ) ∙ g                ≈⟨ assoc _ _ _ ⟩
       h ⁻¹ ∙ g ⁻¹ ∙  (h ∙ g)                  ≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6))  ⟩
       h ⁻¹ ∙  g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹)  ≈⟨  ∙-cong grefl (lemma5 _ _ )  ⟩
       h ⁻¹ ∙  g ⁻¹ ∙  (g ⁻¹ ∙ h ⁻¹) ⁻¹        ≈⟨ assoc _ _ _ ⟩
       h ⁻¹ ∙ (g ⁻¹ ∙  (g ⁻¹ ∙ h ⁻¹) ⁻¹)       ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩
       h ⁻¹ ∙ (g ⁻¹ ∙   h ⁻¹ ∙ g) ⁻¹           ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩
       (g ⁻¹ ∙ h ⁻¹ ∙   g ∙ h) ⁻¹              ≈⟨ grefl ⟩
       [ g , h ]  ⁻¹                  
     ∎ where open EqReasoning (Algebra.Group.setoid G)

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
deriving-inv {suc i} {_} (gen x x₁ )    = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where
deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )