\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}