------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition for the permutation relation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Permutation.Propositional
  {a} {A : Set a} where

open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Binary.Equality.Propositional using (_≋_; ≋⇒≡)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.Definitions using (Reflexive; Transitive)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl)
import Relation.Binary.Reasoning.Setoid as EqReasoning
open import Relation.Binary.Reasoning.Syntax

import Data.List.Relation.Binary.Permutation.Setoid as Permutation

private
  variable
    x y z v w : A
    ws xs ys zs : List A

------------------------------------------------------------------------
-- An inductive definition of permutation

-- Note that one would expect that this would be defined in terms of
-- `Permutation.Setoid`. This is not currently the case as it involves
-- adding in a bunch of trivial `_≡_` proofs to the constructors which
-- a) adds noise and b) prevents easy access to the variables `x`, `y`.
-- This may be changed in future when a better solution is found.

infix  _↭_

data _↭_ : Rel (List A) a where
  refl  : xs ↭ xs
  prep  : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
  swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
  trans : xs ↭ ys → ys ↭ zs → xs ↭ zs

-- Constructor aliases

↭-refl : Reflexive _↭_
↭-refl = refl

↭-prep  : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
↭-prep = prep

↭-swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
↭-swap = swap

------------------------------------------------------------------------
-- _↭_ is an equivalence

↭-reflexive : _≡_ ⇒ _↭_
↭-reflexive refl = ↭-refl

↭-reflexive-≋ : _≋_ ⇒ _↭_
↭-reflexive-≋ xs≋ys = ↭-reflexive (≋⇒≡ xs≋ys)

↭-sym : xs ↭ ys → ys ↭ xs
↭-sym refl                = refl
↭-sym (prep x xs↭ys)      = prep x (↭-sym xs↭ys)
↭-sym (swap x y xs↭ys)    = swap y x (↭-sym xs↭ys)
↭-sym (trans xs↭ys ys↭zs) = trans (↭-sym ys↭zs) (↭-sym xs↭ys)

-- A smart version of trans that avoids unnecessary `refl`s (see #1113).
↭-trans : Transitive _↭_
↭-trans refl ρ₂ = ρ₂
↭-trans ρ₁ refl = ρ₁
↭-trans ρ₁ ρ₂   = trans ρ₁ ρ₂

↭-isEquivalence : IsEquivalence _↭_
↭-isEquivalence = record
  { refl  = ↭-refl
  ; sym   = ↭-sym
  ; trans = ↭-trans
  }

↭-setoid : Setoid _ _
↭-setoid = record
  { isEquivalence = ↭-isEquivalence
  }

------------------------------------------------------------------------
-- _↭_ is finer than `Setoid`-based permutation for any equivalence on A

module _ {ℓ} {_≈_ : Rel A ℓ} (isEquivalence : IsEquivalence _≈_) where

  private
    open module ↭ₛ′ = Permutation record { isEquivalence = isEquivalence }
      using ()
      renaming (_↭_ to _↭ₛ′_)

  ↭⇒↭ₛ′ : _↭_ ⇒ _↭ₛ′_
  ↭⇒↭ₛ′ refl         = ↭ₛ′.↭-refl
  ↭⇒↭ₛ′ (prep x p)   = ↭ₛ′.↭-prep x (↭⇒↭ₛ′ p)
  ↭⇒↭ₛ′ (swap x y p) = ↭ₛ′.↭-swap x y (↭⇒↭ₛ′ p)
  ↭⇒↭ₛ′ (trans p q)  = ↭ₛ′.↭-trans′ (↭⇒↭ₛ′ p) (↭⇒↭ₛ′ q)


------------------------------------------------------------------------
-- _↭_ is equivalent to `Setoid`-based permutation on `≡.setoid A`

private
  open module ↭ₛ = Permutation (≡.setoid A)
    using ()
    renaming (_↭_ to _↭ₛ_)

↭⇒↭ₛ : _↭_ ⇒ _↭ₛ_
↭⇒↭ₛ = ↭⇒↭ₛ′ ≡.isEquivalence

↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_
↭ₛ⇒↭ (↭ₛ.refl xs≋ys)       = ↭-reflexive-≋ xs≋ys
↭ₛ⇒↭ (↭ₛ.prep refl p)      = ↭-prep _ (↭ₛ⇒↭ p)
↭ₛ⇒↭ (↭ₛ.swap refl refl p) = ↭-swap _ _ (↭ₛ⇒↭ p)
↭ₛ⇒↭ (↭ₛ.trans p q)        = ↭-trans (↭ₛ⇒↭ p) (↭ₛ⇒↭ q)


------------------------------------------------------------------------
-- A reasoning API to chain permutation proofs and allow "zooming in"
-- to localised reasoning.

module PermutationReasoning where

  private module Base = EqReasoning ↭-setoid

  open Base public
    hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨)
    renaming (≈-go to ↭-go)

  open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public

  -- Some extra combinators that allow us to skip certain elements

  infixr  step-swap step-prep

  -- Skip reasoning on the first element
  step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
              xs ↭ ys → (x ∷ xs) IsRelatedTo zs
  step-prep x xs rel xs↭ys = ↭-go (↭-prep x xs↭ys) rel

  -- Skip reasoning about the first two elements
  step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
              xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
  step-swap x y xs rel xs↭ys = ↭-go (↭-swap x y xs↭ys) rel

  syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
  syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z