module Symmetric where

open import Level hiding ( suc ; zero )
open import Algebra
open import Algebra.Structures
open import Data.Fin hiding ( _<_  )
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 Data.List.Relation.Binary.Permutation.Inductive renaming ( refl to irefl ; trans to itrans )
open import nat

f1 : Fin 3 → Fin 3
f1 zero = suc (suc zero)
f1 (suc zero) = zero
f1 (suc (suc zero)) = suc zero

lemma1  : Permutation 3 3
lemma1  = permutation f1 ( f1 ∘ f1 ) lemma2 where
   lemma3 : (x : Fin 3 ) → f1 (f1 (f1 x)) ≡ x
   lemma3 zero = refl
   lemma3 (suc zero) = refl
   lemma3 (suc (suc zero)) = refl
   lemma2 : :→-to-Π (λ x → f1 (f1 x)) InverseOf :→-to-Π f1
   lemma2 = record { left-inverse-of = λ x → lemma3 x ; right-inverse-of = λ x → lemma3 x }

finpid : (n i : ℕ ) → i Data.Nat.< n → List (Fin n)
finpid (suc n) zero _ = fromℕ≤ {zero} (s≤s z≤n) ∷ []
finpid (suc n) (suc i) (s≤s lt) = fromℕ≤ (s≤s lt) ∷ finpid (suc n) i (<-trans lt a<sa) 

fpid : (n : ℕ ) → List (Fin n)
fpid 0 = []
fpid (suc j) = finpid (suc j) j a<sa where

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

flist>0  : ( n : ℕ ) → n Data.Nat.> 0  → length (fpid n) ≡ n
flist>0 (suc n) _ = fn (suc n) n a<sa  where
   fn : (n i : ℕ ) → (i<n : i Data.Nat.< n ) → (length (finpid n i i<n)) ≡ suc i
   fn (suc n) zero _ = refl
   fn (suc n) (suc i) (s≤s i<n) = cong (λ k → suc k ) (fn (suc n) i (<-trans i<n a<sa ))

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 with <-cmp (toℕ x) (suc (suc n))
   p← x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn))  where
       x<sn : toℕ x < suc n
       x<sn = <-trans a ?
   p← x | tri≈ ¬a b ¬c = fromℕ≤ (s≤s (s≤s m<n))
   p← x | tri> ¬a ¬b c = ⊥-elim ( nat-<> c fin<n )
   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 = {!!} where
       lem4 : toℕ (fromℕ≤ (s≤s a<sa)) ≡ m → fromℕ≤ {!!} ≡ x 
       lem4 = {!!}
   piso← x | tri> ¬a ¬b c = {!!}
   piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
   piso→ = {!!}