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 Data.Fin.Properties renaming ( <-cmp  to fcmp ; <-trans to ftrans )
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
open import logic

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  )))

   pincl :  (Fin (suc (suc n)) → Fin (suc (suc n)))
       ∧ (( p←i : Fin (suc (suc n)) → Fin (suc (suc n))) →  (x : Fin (suc (suc n)) ) → p←i (p→ x)   ≡ x )
       ∧ (( p←i : Fin (suc (suc n)) → Fin (suc (suc n))) →  (x : Fin (suc (suc n)) ) → p→ (p←i x)   ≡ x )
   pincl = {!!}

   open _∧_
   p← : Fin (suc (suc n)) → Fin (suc (suc n))
   p← = proj1 pincl
   piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
   piso← = proj1 (proj2 pincl) p←
   piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
   piso→ = proj2 (proj2 pincl) p←