\begin{code}
{-# OPTIONS --cubical --safe --postfix-projections #-}

module Data.List.Relation.Binary.Permutation where

open import Prelude
open import Data.List
open import Data.Fin
open import Data.Fin.Properties
open import Data.List.Membership
open import Cubical.Foundations.Equiv
import Function.Isomorphism as Isomorphism
open import Relation.Binary
open import Cubical.Foundations.Prelude using (J; _∧_)
open import Cubical.Foundations.Transport using (isSet-subst)
open import Cubical.Data.Sigma.Properties
open import Data.Nat.Properties using (znots; snotz)

infixr 0 _↝_
_↝_ : {A : Type a} (xs ys : List A)  Type a
xs  ys =  x  x  xs  x  ys

infix 4 _↭_
_↭_ : {A : Type a} (xs ys : List A)  Type a
\end{code}
%<*perm-def>
\begin{code}
xs  ys =  x  (x  xs)  (x  ys)
\end{code}
%</perm-def>
\begin{code}

reflₚ :  {xs : List A}  xs  xs
reflₚ _ = Isomorphism.refl-⇔

symₚ : {xs ys : List A}  xs  ys  ys  xs
symₚ xs↭ys x = Isomorphism.sym-⇔ (xs↭ys x)

transₚ : {xs ys zs : List A}  xs  ys  ys  zs  xs  zs
transₚ xs↭ys ys↭zs x = Isomorphism.trans-⇔ (xs↭ys x) (ys↭zs x)

consₚ :  x {xs ys : List A}  xs  ys  x  xs  x  ys
consₚ _ xs↭ys _ .fun       (f0   , x≡x )    = f0 , x≡x
consₚ _ xs↭ys _ .fun       (fs n  , x∈xs)    = push (xs↭ys _ .fun (n , x∈xs))
consₚ _ xs↭ys _ .inv       (f0   , x≡x )    = f0 , x≡x
consₚ _ xs↭ys _ .inv       (fs n  , x∈xs)    = push (xs↭ys _ .inv (n , x∈xs))
consₚ _ xs↭ys _ .leftInv   (f0   , x≡x)     = refl
consₚ _ xs↭ys _ .leftInv   (fs n  , x∈xs) i  = push (xs↭ys _ .leftInv (n , x∈xs) i)
consₚ _ xs↭ys _ .rightInv  (f0   , x≡x)     = refl
consₚ _ xs↭ys _ .rightInv  (fs n  , x∈xs) i  = push (xs↭ys _ .rightInv (n , x∈xs) i)

swapₚ-to :  (x₁ x₂ : A) xs  x₁  x₂  xs  x₂  x₁  xs
swapₚ-to _ _ _ _ (f0 , x≡x₁) = fs f0 , x≡x₁
swapₚ-to _ _ _ _ (fs f0 , x≡x₂) = f0 , x≡x₂
swapₚ-to _ _ _ _ (fs (fs n) , x∈xs) = fs (fs n) , x∈xs

swapₚ-inv :  (x₁ x₂ : A) xs x x∈xs  swapₚ-to x₂ x₁ xs x (swapₚ-to x₁ x₂ xs x x∈xs)  x∈xs
swapₚ-inv _ _ _ _ (f0 , x≡x₁) = refl
swapₚ-inv _ _ _ _ (fs f0 , x≡x₂) = refl
swapₚ-inv _ _ _ _ (fs (fs n) , x∈xs) = refl

swapₚ :  x₁ x₂ (xs : List A)  x₁  x₂  xs  x₂  x₁  xs
swapₚ x₁ x₂ xs x .fun = swapₚ-to x₁ x₂ xs x
swapₚ x₁ x₂ xs x .inv = swapₚ-to x₂ x₁ xs x
swapₚ x₁ x₂ xs x .leftInv  = swapₚ-inv x₁ x₂ xs x
swapₚ x₁ x₂ xs x .rightInv = swapₚ-inv x₂ x₁ xs x

Fin-length : (xs : List A)   (_∈ xs)  Fin (length xs)
Fin-length xs .inv n = xs ! n , n , refl
Fin-length xs .fun (x , n , p) = n
Fin-length xs .leftInv (x , n , p) i .fst = p i
Fin-length xs .leftInv (x , n , p) i .snd .fst = n
Fin-length xs .leftInv (x , n , p) i .snd .snd j = p (i  j)
Fin-length xs .rightInv n = refl

Fin-length-cong : (xs ys : List A) 
                xs  ys 
                Fin (length xs)  Fin (length ys)
Fin-length-cong xs ys xs↭ys =
  sym-⇔ (Fin-length xs)  trans-⇔  iso-Σ xs↭ys  trans-⇔  Fin-length ys

index-commutes :  (x : A) xs ys 
                 (xs↭ys : xs  ys) (x∈xs : x  xs) 
                 fst (xs↭ys x .fun x∈xs)  Fin-length-cong xs ys xs↭ys .fun (x∈xs .fst)
index-commutes x xs ys xs↭ys (n , p) =
  J  y y∈xs  xs↭ys y .fun (n , y∈xs) .fst  xs↭ys (xs ! n) .fun (n , refl) .fst) refl p

index-equality-preserved :  (x : A) xs ys (p q : x  xs) 
                           (xs↭ys : xs  ys) 
                           fst p  fst q 
                           xs↭ys x .fun p .fst  xs↭ys x .fun q .fst
index-equality-preserved x xs ys p q xs↭ys ip≡iq =
  xs↭ys x .fun p .fst ≡⟨ index-commutes x xs ys xs↭ys p 
  Fin-length-cong xs ys xs↭ys .fun (p .fst) ≡⟨ cong (Fin-length-cong xs ys xs↭ys .fun) ip≡iq 
  Fin-length-cong xs ys xs↭ys .fun (q .fst) ≡˘⟨ index-commutes x xs ys xs↭ys q 
  xs↭ys x .fun q .fst 
  where open import Path.Reasoning

perm-inj :  (x : A) xs ys n 
         (xs↭ys : x  xs  x  ys) 
          z
         (z∈ys : x  z)
         (x∈ys : x  z)
         (z∈xs : xs ! n  z)
         (p₁ : xs↭ys z .fun (fs n , z∈xs)  (f0 , z∈ys))
         (p₂ : xs↭ys z .fun (f0 , z∈ys)  (f0 , x∈ys)) 
         
perm-inj x xs ys n xs↭ys z z∈ys x∈ys z∈xs p₁ p₂ = znots (cong FinToℕ p₆)
  where
  open import Path.Reasoning

  p₃ = fs n , z∈xs ≡˘⟨ xs↭ys z .leftInv (fs n , z∈xs) 
       xs↭ys z .inv (xs↭ys z .fun (fs n , z∈xs)) ≡⟨ cong (xs↭ys z .inv) p₁ 
       xs↭ys z .inv (f0 , z∈ys) 

  p₄ = f0 , z∈ys ≡˘⟨ xs↭ys z .leftInv (f0 , z∈ys) 
       xs↭ys z .inv (xs↭ys z .fun (f0 , z∈ys)) ≡⟨ cong (xs↭ys z .inv) p₂ 
       xs↭ys z .inv (f0 , x∈ys) 

  p₅ = index-equality-preserved z (x  ys) (x  xs) (f0 , x∈ys) (f0 , z∈ys) (sym-⇔  xs↭ys) refl

  p₆ = f0 ≡⟨ cong fst p₄ 
       xs↭ys z .inv (f0 , x∈ys) .fst ≡⟨ p₅ 
       xs↭ys z .inv (f0 , z∈ys) .fst ≡˘⟨ cong fst p₃ 
       fs n 

tailₚ-to :  x (xs ys : List A)  x  xs  x  ys   z  z  xs  z  ys
tailₚ-to x xs ys xs↭ys z (n , z∈xs) with xs↭ys z .fun (fs n , z∈xs) | inspect (xs↭ys z .fun) (fs n , z∈xs)
... | fs m , z∈ys | _ = m , z∈ys
... | f0 , z∈ys |  p₁  with xs↭ys z .fun (f0 , z∈ys) | inspect (xs↭ys z .fun) (f0 , z∈ys)
... | fs o , x∈ys | _ = o , x∈ys
... | f0 , x∈ys |  p₂  = ⊥-elim (perm-inj x xs ys n xs↭ys z z∈ys x∈ys z∈xs p₁ p₂)

pred-∈-eq :  (x y : A) xs i j 
          (x∈xs₁ : xs ! i  x) 
          (x∈xs₂ : xs ! j  x) 
          Path (x  y  xs) (fs i , x∈xs₁) (fs j , x∈xs₂) 
          (i , x∈xs₁)  (j , x∈xs₂)
pred-∈-eq x y xs i j x∈xs₁ x∈xs₂ =
  J  { (fs n , x∈xs₃) _  (i , x∈xs₁)  (n , x∈xs₃)
       ; (f0     , x∈xs₃)  ⊥-elim  snotz  cong FinToℕ  cong fst })
  refl

open import Path.Reasoning

tailₚ-inv :  x (xs ys : List A) 
            (xs↭ys : x  xs  x  ys) 
             z (i : z  ys) 
            tailₚ-to x xs ys xs↭ys z (tailₚ-to x ys xs (sym-⇔  xs↭ys) z i)   i
tailₚ-inv x xs ys xs↭ys z (n , z∈ys) with xs↭ys z .inv (fs n , z∈ys) | inspect (xs↭ys z .inv) (fs n , z∈ys)
... | fs m , z∈xs  |  p₁  with xs↭ys z .fun (fs m , z∈xs) | inspect (xs↭ys z .fun) (fs m , z∈xs)
... | fs o , z∈ys₂ |  p₂  = pred-∈-eq z x ys o n z∈ys₂ z∈ys p₃

  where p₃ = fs o , z∈ys₂ ≡˘⟨ p₂ 
             xs↭ys z .fun (fs m , z∈xs) ≡˘⟨ cong (xs↭ys z .fun) p₁ 
             xs↭ys z .fun (xs↭ys z .inv (fs n , z∈ys)) ≡⟨ xs↭ys z .rightInv (fs n , z∈ys) 
             fs n , z∈ys 

... | f0     , z∈ys₂ |  p₂  with xs↭ys z .fun (f0 , z∈ys₂) | inspect (xs↭ys z .fun) (f0 , z∈ys₂)
... | f0     , x∈ys₃ |  p₃  = ⊥-elim (perm-inj x xs ys m xs↭ys z z∈ys₂ x∈ys₃ z∈xs p₂ p₃)
... | fs o , x∈ys₃ |  p₃  = ⊥-elim (snotz (cong (FinToℕ  fst) p₄))

  where p₄ = fs n , z∈ys ≡˘⟨ xs↭ys z .rightInv (fs n , z∈ys) 
             xs↭ys z .fun (xs↭ys z .inv (fs n , z∈ys)) ≡⟨ cong (xs↭ys z .fun) p₁ 
             xs↭ys z .fun (fs m , z∈xs) ≡⟨ p₂ 
             f0 , z∈ys₂ 

tailₚ-inv x xs ys xs↭ys z (n , z∈ys) | f0 , z∈xs |  p₁ 
  with xs↭ys z .inv (f0 , z∈xs) | inspect (xs↭ys z .inv) (f0 , z∈xs)
... | f0     , z∈ys₂ |  p₂  = ⊥-elim (perm-inj x ys xs n (sym-⇔  xs↭ys) z z∈xs z∈ys₂ z∈ys p₁ p₂)
... | fs o , z∈ys₂ |  p₂  with xs↭ys z .fun (fs o , z∈ys₂) | inspect (xs↭ys z .fun) (fs o , z∈ys₂)
... | fs m , z∈ys₃ |  p₃  = ⊥-elim (snotz (cong (FinToℕ  fst) p₄))

  where p₄ = fs m , z∈ys₃ ≡˘⟨ p₃ 
             xs↭ys z .fun (fs o , z∈ys₂) ≡˘⟨ cong (xs↭ys z .fun) p₂ 
             xs↭ys z .fun (xs↭ys z .inv (f0 , z∈xs)) ≡⟨ xs↭ys z .rightInv (f0 , z∈xs) 
             f0 , z∈xs 

... | f0     , z∈ys₃ |  p₃  with xs↭ys z .fun (f0 , z∈ys₃) | inspect (xs↭ys z .fun) (f0 , z∈ys₃)
... | f0     , z∈ys₄ |  p₄  = ⊥-elim (perm-inj x xs ys o xs↭ys z z∈ys₃ z∈ys₄ z∈ys₂ p₃ p₄)
... | fs l , z∈ys₄ |  p₄  = pred-∈-eq z x ys l n z∈ys₄ z∈ys p₇
  where

  p₅ : Path (z  x  ys) (f0 , z∈xs) (f0 , z∈ys₃)
  p₅ = (f0 , z∈xs) ≡˘⟨ xs↭ys z .rightInv (f0 , z∈xs) 
       xs↭ys z .fun (xs↭ys z .inv (f0 , z∈xs)) ≡⟨ cong (xs↭ys z .fun) p₂ 
       xs↭ys z .fun (fs o , z∈ys₂) ≡⟨ p₃ 
       (f0 , z∈ys₃) 

  p₆ = z∈xs ≡˘⟨ isSet-subst {B = λ n  (x  ys) ! n  z} (Discrete→isSet discreteFin) (cong fst p₅) z∈xs 
       subst  n  (x  ys) ! n  z) (cong fst p₅) z∈xs
         ≡⟨ pathSigma→sigmaPath (f0 , z∈xs) (f0 , z∈ys₃) p₅ .snd 
       z∈ys₃ 

  p₇ = fs l , z∈ys₄ ≡˘⟨ p₄ 
       xs↭ys z .fun (f0 , z∈ys₃) ≡˘⟨ cong (xs↭ys z .fun  _,_ f0) p₆ 
       xs↭ys z .fun (f0 , z∈xs) ≡˘⟨ cong (xs↭ys z .fun) p₁ 
       xs↭ys z .fun (xs↭ys z .inv (fs n , z∈ys)) ≡⟨ xs↭ys z .rightInv (fs n , z∈ys) 
       fs n , z∈ys 

tailₚ :  x (xs ys : List A) 
        x  xs  x  ys 
        xs  ys
tailₚ x xs ys x∷xs↭x∷ys k .fun = tailₚ-to x xs ys x∷xs↭x∷ys k
tailₚ x xs ys x∷xs↭x∷ys k .inv = tailₚ-to x ys xs (sym-⇔  x∷xs↭x∷ys) k
tailₚ x xs ys x∷xs↭x∷ys k .rightInv = tailₚ-inv x xs ys x∷xs↭x∷ys k
tailₚ x xs ys x∷xs↭x∷ys k .leftInv  = tailₚ-inv x ys xs (sym-⇔  x∷xs↭x∷ys) k
\end{code}