{-# 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
infix 3 _↭_
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
↭-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
↭-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)
↭-trans : Transitive _↭_
↭-trans refl ρ₂ = ρ₂
↭-trans ρ₁ refl = ρ₁
↭-trans ρ₁ ρ₂ = trans ρ₁ ρ₂
↭-isEquivalence : IsEquivalence _↭_
↭-isEquivalence = record
{ refl = ↭-refl
; sym = ↭-sym
; trans = ↭-trans
}
↭-setoid : Setoid _ _
↭-setoid = record
{ isEquivalence = ↭-isEquivalence
}
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)
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)
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
infixr 2 step-swap step-prep
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
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