open import Level hiding ( suc ; zero )
open import Algebra
module sym5 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
open import Data.List  hiding ( [_] )
open import nat

¬sym5solvable : ¬ ( solvable (Symmetric 5) )
¬sym5solvable sol = counter-example {!!} where -- (end5 (abc ? 0<4 ) (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) ) where

--
--    dba       1320      d → b → a → d
--    (dba)⁻¹   3021      a → b → d → a
--    aec       21430
--    (aec)⁻¹   41032
--    (abd)(cea)(dba)(aec)
-- 

     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

     --- 2 ∷ 0 ∷ 1 ∷ []      abc
     3rot : Permutation 3 3
     3rot = pprep (pswap (pid {0}) ) ∘ₚ pins (n≤ 1)

     abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
     abc i<3 j<4 = (save2 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip save2  where
          save2 : Permutation  5 5
          save2 = ( (( pid {5} ∘ₚ flip (pins (s≤s i<3) ) )) ∘ₚ flip (pins j<4)) 

     dba-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) 
     dba-0 = {!!}
     dba-1 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 3 )
     dba-1 = {!!}

     dba : {i j : ℕ }  → (i < 3 ) → ( j < 4 ) → Permutation  5 5
     dba i<3 j<4 = abc {!!} (dba-0 j<4 i<3 )

     aec-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) 
     aec-0 = {!!}
     aec-1 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 3 )
     aec-1 = {!!}

     aec : {i j : ℕ }  → (i < 3 ) → ( j < 4 ) → Permutation  5 5
     aec i<3 j<4 = abc {!!} (aec-0 j<4 i<3 )

     [dba,aec]=abc : {i j : ℕ }  → (i<4 : i < 4 ) → (j<3 : j < 3 ) → [ dba j<3 i<4 , aec j<3 i<4 ] =p= abc {!!} i<4
     [dba,aec]=abc = {!!}

     --- 2 ∷ 0 ∷ 1 ∷ []      abc
     t10 : List (List ℕ )
     t10 =   t101 (n≤ 3) (n≤ 4)  [] where
          t101 : { i j : ℕ } → i ≤ 3 → j ≤ 4  → List (List ℕ ) → List (List ℕ )
          t101 z≤n z≤n t =  plist (abc z≤n z≤n) ∷ t 
          t101 z≤n (s≤s y) t = t101 (n≤ 3) (≤-trans y refl-≤s) ( plist (abc z≤n (s≤s y)) ∷ t )
          t101 (s≤s x) z≤n t = t101 (≤-trans x refl-≤s) z≤n ( plist (abc (s≤s x) z≤n) ∷ t )
          t101 (s≤s x) (s≤s y) t = t101 (≤-trans x refl-≤s)  (s≤s y) ( plist (abc (s≤s x) (s≤s y)) ∷ t )
          -- t101 (s≤s x) z≤n t = t101 (≤-trans x ?) x ( abc (s≤s x) z≤n ∷ t )
          -- t101 (s≤s x) (s≤s y) t = {!!}
     t12 = {!!}
     --- 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] 
     --- 1 ∷ 0 ∷ 2 ∷ 3 ∷ 4 ∷ [] 
     --- 1 ∷ 2 ∷ 0 ∷ 3 ∷ 4 ∷ [] 
     --- 1 ∷ 2 ∷ 3 ∷ 0 ∷ 4 ∷ []     
     --- 1 ∷ 2 ∷ 3 ∷ 4 ∷ 0 ∷ []     

     --- 2 ∷ 0 ∷ 1 ∷ 3 ∷ 4 ∷ []     abc     (swap (pid {0}) ∘ₚ pins i<1 ) ∘ₚ pid 
     --- 3 ∷ 0 ∷ 2 ∷ 1 ∷ 4 ∷ []     abc     pprep (swap (pid {0}) ∘ₚ pins i<1 ) ∘ₚ pid 
     --- 4 ∷ 0 ∷ 2 ∷ 3 ∷ 1 ∷ []     abc     pprep (pprep (swap (pid {0}) ∘ₚ pins i<1 )) ∘ₚ pid 
     --- 3 ∷ 1 ∷ 0 ∷ 2 ∷ 4 ∷ []     abc
     --- 4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ []     abc
     --- 4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ []     abc

     --- 2 ∷ 0 ∷ 1 ∷ 3 ∷ 4 ∷ []     abc
     --- 1 ∷ 3 ∷ 2 ∷ 0 ∷ 4 ∷ []     abd 
     --  2 ∷ 1 ∷ 4 ∷ 3 ∷ 0 ∷ []     cea

     dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<3 : i < 3 ) → (j<4 : j < 4 ) → deriving n (abc {!!} j<4 )
     dervie-any-3rot 0 i<3 j<4 = lift tt
     dervie-any-3rot (suc i) i<3 j<4 =  {!!}
         -- ccong ( [dba,aec]=abc j<4 i<3 ) (
         -- comm {{!!}} {dba i<3 j<4} {aec i<3 j<4 } 
         --     ( dervie-any-3rot i (dba-1 j<4 i<3) (dba-0 j<4 i<3 ) ) 
         --     ( dervie-any-3rot i (aec-1 j<4 i<3) (aec-0 j<4 i<3 ) ))

     open _=p=_
     counter-example :  ¬ (abc {!!} 0<4  =p= pid )
     counter-example = {!!}


     --- 1 ∷ 0 ∷ 2 ∷ []
     --- 0 ∷ 2 ∷ 1 ∷ 3 ∷ []
     --- 1 ∷ 3 ∷ 2 ∷ 0 ∷ 4 ∷ []
     --  2 ∷ 1 ∷ 3 ∷ 0 ∷ 4 ∷ []  (dba)⁻¹ = abd
     dba99  : Permutation 5 5
     dba99 = pprep (pprep (pswap (pid {1}))) ∘ₚ pins (n≤ 3)
     t1 = plist dba99 ∷ plist (pinv dba99) ∷ []
     --  1 ∷ 0 ∷ []  
     --  0 ∷ 2 ∷ 1 ∷ []  
     --  1 ∷ 0 ∷ 3 ∷ 2 ∷ []  
     --  2 ∷ 1 ∷ 4 ∷ 3 ∷ 0 ∷ []  
     --  4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ []  (aec)⁻¹ = cea
     aec99 : Permutation 5 5
     aec99 = pprep (pprep (pprep (pswap (pid {0}))) ∘ₚ pins (n≤ 1)) ∘ₚ pins (n≤ 4)
     tt2 = plist aec99 ∷ plist (pinv aec99) ∷ []