------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of permutation
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Vec.Functional.Relation.Binary.Permutation.Properties where

open import Level using (Level)
open import Data.Product.Base using (_,_; proj₁; proj₂)
open import Data.Nat.Base using (ℕ)
open import Data.Fin.Permutation using (id; flip; _⟨$⟩ʳ_; inverseʳ; _∘ₚ_)
open import Data.Vec.Functional using (Vector)
open import Data.Vec.Functional.Relation.Binary.Permutation using (_↭_)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; trans; cong)
open import Relation.Binary.PropositionalEquality.Properties
  using (module ≡-Reasoning)
open import Relation.Binary.Indexed.Heterogeneous
  using (Reflexive; Symmetric; Transitive; IsIndexedEquivalence; IndexedSetoid)

private
  variable
    a : Level
    A : Set a
    n : ℕ
    xs ys : Vector A n


------------------------------------------------------------------------
-- Basics

↭-refl : Reflexive (Vector A) _↭_
↭-refl = id , λ _ → refl

↭-reflexive : xs ≡ ys → xs ↭ ys
↭-reflexive refl = ↭-refl

↭-sym : Symmetric (Vector A) _↭_
proj₁ (↭-sym (xs↭ys , _)) = flip xs↭ys
proj₂ (↭-sym {x = xs} {ys} (xs↭ys , xs↭ys≡)) i = begin
  ys (flip xs↭ys ⟨$⟩ʳ i)              ≡⟨ xs↭ys≡ _ ⟨
  xs (xs↭ys ⟨$⟩ʳ (flip xs↭ys ⟨$⟩ʳ i)) ≡⟨ cong xs (inverseʳ xs↭ys) ⟩
  xs i                                ∎
  where open ≡-Reasoning

↭-trans : Transitive (Vector A) _↭_
proj₁ (↭-trans (xs↭ys , _) (ys↭zs , _))   = ys↭zs ∘ₚ xs↭ys
proj₂ (↭-trans (_ , xs↭ys) (_ , ys↭zs)) _ = trans (xs↭ys _) (ys↭zs _)

------------------------------------------------------------------------
-- Structure

isIndexedEquivalence : IsIndexedEquivalence (Vector A) _↭_
isIndexedEquivalence {A = A} = record
  { refl = ↭-refl
  ; sym = ↭-sym
  ; trans = λ {n₁ n₂ n₃} {xs : Vector A n₁} {ys : Vector A n₂} {zs : Vector A n₃}
              xs↭ys ys↭zs → ↭-trans {i = n₁} {i = xs} xs↭ys ys↭zs
  }

------------------------------------------------------------------------
-- Bundle

indexedSetoid : {A : Set a} → IndexedSetoid ℕ a _
indexedSetoid {A = A} = record
  { Carrier = Vector A
  ; _≈_ = _↭_
  ; isEquivalence = isIndexedEquivalence
  }