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 ( <-trans ; ≤-trans ) renaming ( <-cmp to <-fcmp )
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 ; _++_ ; head ) renaming (reverse to rev )
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

-- we already have refl and trans

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 : ℕ} → 1 < n → Permutation n n
psawpn {suc zero}  (s≤s ())
psawpn {suc n} (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 ) )

psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n
psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) )

n≤ : (i : ℕ ) → {j : ℕ } → i ≤ i + j
n≤ (zero) {j} = z≤n
n≤ (suc i) {j} = s≤s ( n≤ i )

lem0 : {n : ℕ } → n ≤ n
lem0 {zero} = z≤n
lem0 {suc n} = s≤s lem0

lem00 : {n m : ℕ } → n ≡ m → n ≤ m
lem00 refl = lem0

-- pconcat :  {n m : ℕ } → Permutation  m m → Permutation n n → Permutation (m + n)  (m + n) 
-- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ?

-- inductivley enmumerate permutations
--    from n-1 length create n length inserting new element at position m

eperm  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
eperm {_} {zero} _ = pid
eperm {suc _} {suc zero} _ = pswap pid
eperm {suc (suc n)} {suc m} (s≤s m<n) =  eperm1 (suc m) (suc (suc n)) lem0 where
    eperm1 : (i j : ℕ ) → j ≤ suc (suc n)  → Permutation (suc (suc (suc n ))) (suc (suc (suc n)))
    eperm1 _ zero _ = pid
    eperm1 zero _ _ = pid
    eperm1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j}  (s≤s (s≤s si≤n))  ∘ₚ  eperm1 i j (≤-trans si≤n refl-≤s ) 


plist  : {n  : ℕ} → Permutation n n → List ℕ
plist {0} perm = []
plist {suc j} perm = rev (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) 

testi0 = plist   (pprep (pid {3}) )                                                          -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ []
testi01 = plist  (psawpim {4} {2} (n≤ 4 {0}) )                                               -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ []
testi02 = plist  (psawpim {4} {2} (n≤ 4 {0}) ∘ₚ psawpim {4} {1}  (n≤ 3))                     -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ []
testi03 = plist ((psawpim (n≤  4 {0}) ∘ₚ psawpim  (n≤ 3) ) ∘ₚ psawpim {4} {0}  (n≤ 2 ))      -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ []
ttt0 =  testi0 ∷ testi01 ∷ testi02 ∷ testi03 ∷ []

tt0 = plist (eperm {3} {0} (n≤ 0)) ∷ plist ( eperm {3} {1} (n≤ 1 )) ∷ plist ( eperm {3} {2} (n≤ 2 )) ∷ plist ( eperm {3} {3} (n≤ 3 )) ∷ [] 

c0 = pid {2} -- pprep ( eperm {3} (n≤ 3) pid)
-- e0 =  pprep ( eperm {3} (n≤ 3) pid)
ct0 = c0 ∘ₚ eperm {1} (n≤ 0 ) 
ct1 = c0 ∘ₚ eperm {1} (n≤ 1 ) 
ttt1 = plist ct0 ∷ plist ct1 ∷ [] 

d0 = pid {3} -- pprep ( eperm {3} (n≤ 3) pid)
-- e0 =  pprep ( eperm {3} (n≤ 3) pid)
dt0 = d0 ∘ₚ eperm {2} (n≤ 0 ) 
dt1 = d0 ∘ₚ eperm {2} (n≤ 1 ) 
dt2 = d0 ∘ₚ eperm {2} (n≤ 2 ) 
ttt3 = plist dt0 ∷ plist dt1 ∷ plist dt2 ∷ [] 

-- e0 = pid {4} -- eperm (n≤ 2) (eperm (n≤ 2) (eperm (n≤ 1) (pid {1})))
e0 = pid {5} -- pprep ( eperm {3} (n≤ 3) pid)
-- e0 =  pprep ( eperm {3} (n≤ 3) pid)
et0 = e0 ∘ₚ eperm {4} {4} (n≤ 4 ) 
et1 = e0 ∘ₚ eperm {4} {3} (n≤ 3 ) 
et2 = e0 ∘ₚ eperm {4} (n≤ 2 ) 
et3 = e0 ∘ₚ eperm {4} (n≤ 1 ) 
et4 = e0 ∘ₚ eperm {4} (n≤ 0 ) 
ttt2 = plist et0 ∷ plist et1 ∷ plist et2 ∷  plist et3 ∷ plist et4 ∷ [] 

pls : (n : ℕ ) → List (List ℕ )
pls n = Data.List.map plist (pls6 n) where
   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 )
   pls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
   pls4 zero n i≤n perm x = (pprep perm ∘ₚ eperm i≤n ) ∷ x
   pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (pprep perm ∘ₚ eperm {n} {suc i} i≤n  ∷ x)
   pls5 :  ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
   pls5 n [] x = x
   pls5 n (h ∷ x) y = pls5  n x (pls4 n n lem0 h y)
   pls6 :  ( n : ℕ ) → List (Permutation (suc n) (suc n)) 
   pls6 zero = pid ∷ []
   pls6 (suc n) =  pls5 (suc n) (pls6 n) []
   pls7 : List (List ℕ )
   pls7 = Data.List.map plist (pls4 2 2 lem0 (eperm (n≤ 0 ) ) (pls4 2 2 lem0 (eperm (n≤ 1 ) ) [] ))