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 ; ≤-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

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

-- An inductive construction of permutation

pprep  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)
pprep {n} perm =  permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
   p→ : Fin (suc n) → Fin (suc n)
   p→ zero = zero
   p→ (suc x) = suc ( perm  ⟨$⟩ˡ x)

   p← : Fin (suc n) → Fin (suc n)
   p← zero = zero
   p← (suc x) = suc ( perm  ⟨$⟩ʳ x)

   piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x
   piso← zero = refl
   piso← (suc x) = cong (λ k → suc k ) (inverseˡ perm) 

   piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x
   piso→ zero = refl
   piso→ (suc x) = cong (λ k → suc k ) (inverseʳ perm) 

pswap  : {n : ℕ }  → Permutation n n → Permutation (suc (suc n)) (suc (suc  n ))
pswap {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→ zero = suc zero 
   p→ (suc zero) = zero 
   p→ (suc (suc x)) = suc ( suc ( perm  ⟨$⟩ˡ x) )

   p← : Fin (suc (suc n)) → Fin (suc (suc n)) 
   p← zero = suc zero 
   p← (suc zero) = zero 
   p← (suc (suc x)) = suc ( suc ( perm  ⟨$⟩ʳ x) )
   
   piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
   piso← zero = refl
   piso← (suc zero) = refl
   piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) 

   piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
   piso→ zero = refl
   piso→ (suc zero) = refl
   piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) 

-- enumeration

psawpn : {n m : ℕ} → suc m < n → Permutation n n
psawpn {suc zero} {m} (s≤s ())
psawpn {suc n} {m} (s≤s (s≤s x)) = pswap pid 

pfill : { n m : ℕ } → m ≤ n → Permutation  m m → Permutation n n
pfill {n} {m} m≤n perm = pfill1 (n - m) (n-m<n n m ) (subst (λ k → Permutation k k ) (n-n-m=m m≤n ) perm) where
   pfill1 : (i : ℕ ) → i ≤ n  → Permutation (n - i) (n - i)  →  Permutation n n
   pfill1 0 _ perm = perm
   pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) )

eperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
eperm {zero} ()
eperm {n} {0} (s≤s z≤n) perm = pprep perm
eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3 (pswap {0} pid ) (pprep perm) where
    lemm3 : 2 + m ≤ suc n
    lemm3 = ≤-trans (s≤s m<n) refl-≤s
    eperm1 : (m i : ℕ ) → i + m ≤ suc n  → Permutation i i → Permutation (suc n)(suc n)→ Permutation (suc n)(suc n)
    eperm1 zero i i<ssm sw perm = perm ∘ₚ ( pfill (subst (λ k → k ≤ suc n) (+-comm i _) i<ssm) sw )  -- i + zero ≤ suc (suc n) → i ≤ suc (suc n)
    eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) (lemm4 i<ssm ) (pprep sw) perm where
       lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n
       lemm4 lt = begin
          suc i + m  ≡⟨ cong (λ k → suc k ) ( +-comm i _ ) ⟩
          suc m + i  ≡⟨ +-comm (suc m)  _  ⟩
          i + suc m  ≤⟨ lt ⟩
          suc n
        ∎   where open  ≤-Reasoning


finpid : (n i : ℕ ) → i < 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

plist  : {n  : ℕ} → Permutation n n → List ℕ
plist {0} perm = []
plist {suc j} perm = plist1 j a<sa where
    n = suc j
    plist1 : (i : ℕ ) → i < n → List ℕ
    plist1  zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
    plist1  (suc i) (s≤s lt) = toℕ (  perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1  i (<-trans lt a<sa) 

test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )

NL : (n : ℕ ) → Set
NL 0 = ℕ
NL (suc n) = List ( NL n )

pls : (n : ℕ ) → List (List ℕ )
pls n = pls1 n n lem0  where
   lem0 : {n : ℕ } → n ≤ n
   lem0 {zero} = z≤n
   lem0 {suc n} = s≤s lem0
   lem1 : {i n : ℕ } → i ≤ n → i < suc n
   lem1 z≤n = s≤s z≤n
   lem1 (s≤s lt) = s≤s (lem1 lt)
   lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
   lem2 i≤n = ≤-trans i≤n ( refl-≤s )
   pls3 :  ( i n : ℕ ) → (i<n : i < n ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n))
   pls3 i n i<n [] x = x
   pls3 i n i<n (h ∷ t) x = pls3 i n i<n t (  eperm {n} {i} i<n h ∷ x )
   pls2 : ( i n : ℕ ) → (i<n : i ≤ n ) → List (Permutation (suc n) (suc n))
   pls2 0 n i≤<n = pid ∷ []
   pls2 (suc i) (suc n) (s≤s i≤n) = pls3 i (suc n) (lem1 i≤n) ( pls2 i n i≤n) []
   pls1 : ( i n : ℕ ) → i ≤ n  → List (List ℕ) 
   pls1 0 n _ = []
   pls1 (suc i) n (s≤s i≤n) = (Data.List.map plist ( pls2 i n (lem2 i≤n)) ) ++ pls1 i n (lem2 i≤n)