module Symmetric where

open import Level hiding ( suc ; zero )
open import Algebra
open import Algebra.Structures
open import Data.Fin hiding ( _<_  )
open import Data.Fin.Properties hiding ( <-cmp ; <-trans )
open import Data.Product
open import Data.Fin.Permutation
open import Function hiding (id ; flip)
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function.LeftInverse  using ( _LeftInverseOf_ )
open import Function.Equality using (Π)
open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
open import Data.Nat.Properties -- using (<-trans)
open import Relation.Binary.PropositionalEquality 
open import Data.List using (List; []; _∷_ ; length)
open import nat

fid : {p : ℕ } → Fin p → Fin p
fid x = x

-- Data.Fin.Permutation.id
pid : {p : ℕ } → Permutation p p
pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }

-- Data.Fin.Permutation.flip
pinv : {p : ℕ } → Permutation p p → Permutation p p
pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }

record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
    field
       peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q

open _=p=_

prefl : {p : ℕ } { x  : Permutation p p } → x =p= x
peq (prefl {p} {x}) q = refl

psym : {p : ℕ } { x y : Permutation p p } → x =p= y →  y =p= x
peq (psym {p} {x} {y}  eq ) q = sym (peq eq q)

ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y  → y =p= z →  x =p= z
peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q)

Symmetric : ℕ → Group  Level.zero Level.zero
Symmetric p = record {
      Carrier        = Permutation p p
    ; _≈_            = _=p=_
    ; _∙_            = _∘ₚ_
    ; ε              = pid
    ; _⁻¹            = pinv
    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
       isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym }
       ; ∙-cong = presp }
       ; assoc = passoc }
       ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } ))  }
       ; inverse   = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} ))  
       ; ⁻¹-cong   = λ i=j → record { peq = λ q → p-inv i=j q }
      }
   } where
       presp : {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
       presp {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
           lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
           lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
       passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p=  (x ∘ₚ (y ∘ₚ z))
       passoc x y z = record { peq = λ q → refl }
       p-inv : {i j : Permutation p p} →  i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
       p-inv {i} {j} i=j q = begin
           i ⟨$⟩ˡ q                      ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j)  )  ⟩
           i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k  →  i ⟨$⟩ˡ k) (sym (peq i=j _ ))  ⟩
           i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i  ⟩
           j ⟨$⟩ˡ q
           ∎ where open ≡-Reasoning

perm0 : Permutation zero zero
perm0 = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }

open import Relation.Nullary
open import Data.Empty
open import  Relation.Binary.Core
open import fin

fperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
fperm {zero} ()
fperm {suc n} {m} (s≤s m<n) perm = permutation p→ p← record { left-inverse-of = piso← ; right-inverse-of = piso→ } where
   p→ : Fin (suc (suc n)) → Fin (suc (suc n))
   p→ x with <-cmp (toℕ x) m
   p→ x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ʳ (fromℕ≤ x<sn))  where
       x<sn : toℕ x < suc n
       x<sn = <-trans a (s≤s m<n)
   p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
   p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))

   p← : Fin (suc (suc n)) → Fin (suc (suc n))
   p← x = lemma (suc n) refl x where
     lemma : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → Fin (suc (suc n))
     lemma i refl x with <-cmp (toℕ x) i
     lemma i refl x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn))  where
       x<sn : toℕ x < suc n
       x<sn = a
     lemma i refl x | tri≈ ¬a b ¬c = fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ) 
     lemma i refl x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c  fin<n )
   lem8 : {x : Fin (suc (suc n)) } → toℕ ( fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )) ≡ m
   lem8 {x} = toℕ-fromℕ≤ (<-trans (s≤s m<n ) a<sa )
   piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
   piso← x with <-cmp (toℕ x) m
   piso← x | tri< a ¬b ¬c = {!!}
   piso← x | tri> ¬a ¬b c = {!!}
   piso← x | tri≈ ¬a refl ¬c = begin
          p← ( fromℕ≤ a<sa )
       ≡⟨ lem4 refl ⟩
          fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )
       ≡⟨ {!!} ⟩
          x
       ∎  where
            open ≡-Reasoning
            lem4 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ {suc n} a<sa  → p← x ≡ fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )
            lem4 {x} refl with <-cmp (toℕ x) (suc n)
            lem4  refl | tri< a ¬b ¬c = ⊥-elim ( ¬b {!!} )
            lem4  refl | tri≈ ¬a b ¬c = refl
            lem4  refl | tri> ¬a ¬b c = ⊥-elim ( ¬b {!!} )
   piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
   piso→ x = lemma2 (suc n) refl x where
     lemma2 : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
     lemma2 i refl x with <-cmp (toℕ x)  i
     lemma2 i refl x | tri< a ¬b ¬c = {!!}
     lemma2 i refl x | tri> ¬a ¬b c = {!!}
     lemma2 i refl x | tri≈ ¬a b ¬c = begin
          p→ (fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ))
       ≡⟨ lem5 (fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ))  {!!} ⟩
          fromℕ≤ a<sa
       ≡⟨ {!!} ⟩
          x
       ∎  where
            open ≡-Reasoning
            lem7 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n)) → toℕ x ≡ m
            lem7 refl = trans (toℕ-fromℕ≤ _) {!!}
            lem6 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n)) → toℕ x ≡ (suc m)
            lem6 refl = toℕ-fromℕ≤ _
            -- lem5 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ) → p→ x ≡ fromℕ≤ a<sa
            lem5 : (x : Fin (suc (suc n)) ) → x ≡ fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ) → p→ x ≡ fromℕ≤ a<sa
            lem5 x eq with <-cmp (toℕ x) m
            lem5 x eq | tri< a ¬b ¬c = {!!}
            lem5 x eq | tri≈ ¬a refl ¬c = refl
            lem5 x eq | tri> ¬a ¬b c = {!!}